cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation

1 files changed, 2 insertions, 0 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 6d995097a..b3bbbce4a 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -34,6 +34,7 @@ private:
   bool d_setIncomplete;
   /** inst round counter */
   int d_ierCounter;
+  bool d_performCheck;
   /** whether each quantifier is active */
   std::map< Node, bool > d_quant_active;
   /** whether we have added cbqi lemma */
@@ -62,6 +63,7 @@ public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
   ~InstantiationEngine(){}
 
+  bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
   void assertNode( Node f );