Add dt.size to datatypes theory. Add option for fairness strategy used by CEGQI. Improve care graph/equality status for datatypes. Only do FULL effort check in datatypes if no other theories used output channel.

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