Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

1 files changed, 43 insertions, 47 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 8ed59778b..c9f62243f 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -34,25 +34,64 @@ 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;
+  std::map< Node, bool > d_active_quant;
   /** whether we have instantiated quantified formulas */
   //NodeSet d_added_inst;
-  /** whether to do cbqi for this quantified formula */
-  std::map< Node, bool > d_do_cbqi;
+  /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */
+  std::map< Node, int > 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 */
-  bool hasNonCbqiVariable( Node q );
+  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< Node, Node > d_id_to_ce_quant;
+  std::map< Node, Node > 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() : d_doVts(false){}
+    ~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();
@@ -64,56 +103,13 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
+  bool checkCompleteFor( Node q );
   void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   /** get next decision request */
   Node getNextDecisionRequest();
 };
 
-
-class InstStrategySimplex : public InstStrategyCbqi {
-protected:
-  /** reference to theory arithmetic */
-  arith::TheoryArith* d_th;
-  /** quantifiers we should process */
-  std::map< Node, bool > d_quantActive;
-  /** delta */
-  std::map< TypeNode, Node > d_deltas;
-  /** for each quantifier, simplex rows */
-  std::map< Node, std::vector< arith::ArithVar > > d_instRows;
-  /** tableaux */
-  std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term;
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term;
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux;
-  /** ce tableaux */
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux;
-  /** get value */
-  //Node getTableauxValue( Node n, bool minus_delta = false );
-  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
-  /** do instantiation */
-  bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var );
-  bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
-  /** add term to row */
-  void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t );
-  /** print debug */
-  void debugPrint( const char* c );
-private:
-  /** */
-  int d_counter;
-  /** constants */
-  Node d_zero;
-  Node d_negOne;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  void process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
-  ~InstStrategySimplex() throw() {}
-  /** identify */
-  std::string identify() const { return std::string("Simplex"); }
-};
-
-
 //generalized counterexample guided quantifier instantiation
 
 class InstStrategyCegqi;