diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index cb1825377..2502416bd 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -68,18 +68,6 @@ private: /** allocate literal */ Node getLiteral( QuantifiersEngine * qe, int i ); }; - class CegFairness { - public: - CegFairness( context::Context* c ); - /** which conjecture we are looking at */ - CegConjecture * d_conj; - /** the cardinality literals */ - std::map< int, Node > d_lits; - /** current cardinality */ - context::CDO< int > d_curr_lit; - /** allocate literal */ - Node getLiteral( int i ); - }; /** the quantified formula stating the synthesis conjecture */ CegConjecture * d_conj; private: //for enforcing fairness |