Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.

1 files changed, 35 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 18931f8f6..eb80de3ce 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -34,11 +34,14 @@ namespace quantifiers {
 
 class InstStrategyCbqi : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 protected:
   bool d_cbqi_set_quant_inactive;
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
+  /** whether we have added cbqi lemma */
+  NodeSet d_elim_quants;
   /** parent guards */
   std::map< Node, std::vector< Node > > d_parent_quant;
   std::map< Node, std::vector< Node > > d_children_quant;
@@ -48,15 +51,47 @@ protected:
   /** whether to do cbqi for this quantified formula */
   std::map< Node, bool > d_do_cbqi;
   /** register ce lemma */
+  bool registerCbqiLemma( Node q );
   virtual void registerCounterexampleLemma( Node q, Node lem );
   /** has added cbqi lemma */
   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
   /** helper functions */
   int hasNonCbqiVariable( Node q );
   bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+  /** get next decision request with dependency checking */
+  Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );  
   /** process functions */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   virtual void process( Node q, Theory::Effort effort, int e ) = 0;
+protected:
+  //for identification
+  uint64_t d_qid_count;
+  //nested qe map
+  std::map< Node, Node > d_nested_qe;
+  //mark ids on quantifiers 
+  Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
+  // id to ce quant
+  std::map< int, Node > d_id_to_ce_quant;
+  std::map< Node, int > d_ce_quant_to_id;
+  //do nested quantifier elimination recursive
+  Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
+  Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
+  //elimination information (for delayed elimination)
+  class NestedQEInfo {
+  public:
+    NestedQEInfo(){}
+    ~NestedQEInfo(){}
+    Node d_q;
+    std::vector< Node > d_inst_terms;
+    bool d_doVts;
+  };
+  std::map< Node, NestedQEInfo > d_nested_qe_info;
+  NodeIntMap d_nested_qe_waitlist_size;
+  NodeIntMap d_nested_qe_waitlist_proc;
+  std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
+public:
+  //do nested quantifier elimination
+  Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
 public:
   InstStrategyCbqi( QuantifiersEngine * qe );
   ~InstStrategyCbqi() throw();