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

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

1 files changed, 20 insertions, 8 deletions

diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 0c02c7f95..6201cf152 100644..100755
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -64,9 +64,11 @@ public:
   bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
   /** returns true is a and b are disequal in the current context */
   bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+  /** get congruent term */
+  TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
 private:
   /** term index */
-  std::map< Node, TermArgTrie > d_func_map_trie;
+  std::map< Node, TermArgTrie > d_uf_func_map_trie;
   /** union find for terms beyond what is stored in equality engine */
   std::map< Node, Node > d_uf;
   std::map< Node, std::vector< Node > > d_uf_exp;
@@ -74,7 +76,9 @@ private:
   /** disequality list, stores explanations */
   std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
   /** add arg */
-  void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol );
+  void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
+  /** register term */
+  void registerUfTerm( TNode n );
 public:
   enum {
     STATUS_CONFLICT,
@@ -89,10 +93,13 @@ public:
 public:
   //for explanations
   static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
+  //for watch list
+  static void setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out );
+  static void collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list );
 
-  Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
-                        std::map< Node, bool >& watch_list_out, std::vector< Node >& props );
-  static bool isLiteral( Node n );
+  Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited,
+                        bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props );
+  bool isPropagateLiteral( Node n );
 };
 
 class InstPropagator : public QuantifiersUtil {
@@ -104,13 +111,18 @@ private:
     InstPropagator& d_ip;
   public:
     InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
-    virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { 
-      return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); 
+    virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+      return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
     }
+    virtual void filterInstantiations() { d_ip.filterInstantiations(); }
   };
   InstantiationNotifyInstPropagator d_notify;
   /** notify instantiation method */
   bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+  /** remove instance ids */
+  void filterInstantiations();  
+  /** allocate instantiation */
+  unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
   /** equality query */
   EqualityQueryInstProp d_qy;
   class InstInfo {
@@ -137,13 +149,13 @@ private:
   std::vector< unsigned > d_update_list;
   /** relevant instances */
   std::map< unsigned, bool > d_relevant_inst;
+  bool d_has_relevant_inst;
 private:
   bool update( unsigned id, InstInfo& i, bool firstTime = false );
   void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
   void conflict( std::vector< Node >& exp );
   bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
   void addRelevantInstances( std::vector< Node >& exp, const char * c );
-
   void debugPrintExplanation( std::vector< Node >& exp, const char * c );
 public:
   InstPropagator( QuantifiersEngine* qe );