summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_instantiation.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.h12
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback