Decouple counter-example guided quantifier instantiation from Sygus.

1 files changed, 32 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 72ab5d247..e139d0b6f 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -22,6 +22,7 @@
 #include "theory/arith/arithvar.h"
 
 #include "util/statistics_registry.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
 
 namespace CVC4 {
 namespace theory {
@@ -80,6 +81,37 @@ public:
 };
 
 
+//generalized counterexample guided quantifier instantiation
+
+class InstStrategyCegqi;
+
+class CegqiOutputInstStrategy : public CegqiOutput
+{
+public:
+  CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
+  InstStrategyCegqi * d_out;
+  bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
+  bool isEligibleForInstantiation( Node n );
+};
+
+class InstStrategyCegqi : public InstStrategy {
+private:
+  CegqiOutputInstStrategy * d_out;
+  std::map< Node, CegInstantiator * > d_cinst;
+  Node d_curr_quant;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategyCegqi( QuantifiersEngine * qe );
+  ~InstStrategyCegqi(){}
+  
+  bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
+  bool isEligibleForInstantiation( Node n );  
+  /** identify */
+  std::string identify() const { return std::string("Cegqi"); }
+};
+
 }
 }
 }