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, 19 insertions, 4 deletions

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index b9da524de..2deb09654 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -33,6 +33,11 @@
 
 namespace CVC4 {
 namespace theory {
+
+namespace quantifiers{
+  class TermArgTrie;
+}
+
 namespace strings {
 
 /**
@@ -45,7 +50,6 @@ typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttri
 
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
@@ -160,7 +164,8 @@ private:
   std::map< Node, std::vector< Node > > d_normal_forms_exp;
   std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend;
   //map of pairs of terms that have the same normal form
-  NodeListMap d_nf_pairs;
+  NodeIntMap d_nf_pairs;
+  std::map< Node, std::vector< Node > > d_nf_pairs_data;
   void addNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair2( Node n1, Node n2 );
@@ -176,6 +181,8 @@ private:
   // extended functions inferences cache
   NodeSet d_extf_infer_cache;
   std::vector< Node > d_empty_vec;
+  //
+  NodeList d_ee_disequalities;
 private:
   NodeSet d_congruent;
   std::map< Node, Node > d_eqc_to_const;
@@ -236,6 +243,8 @@ private:
   //maintain which concat terms have the length lemma instantiated
   NodeNodeMap d_proxy_var;
   NodeNodeMap d_proxy_var_to_length;
+  /** All the function terms that the theory has seen */
+  context::CDList<TNode> d_functionsTerms;
 private:
   //initial check
   void checkInit();
@@ -304,6 +313,8 @@ private:
   //cardinality check
   void checkCardinality();
 
+private:
+  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 public:
   /** preregister term */
   void preRegisterTerm(TNode n);
@@ -410,8 +421,12 @@ private:
   NodeSet d_regexp_ucached;
   NodeSet d_regexp_ccached;
   // stored assertions
-  NodeListMap d_pos_memberships;
-  NodeListMap d_neg_memberships;
+  NodeIntMap d_pos_memberships;
+  std::map< Node, std::vector< Node > > d_pos_memberships_data;
+  NodeIntMap d_neg_memberships;
+  std::map< Node, std::vector< Node > > d_neg_memberships_data;
+  unsigned getNumMemberships( Node n, bool isPos );
+  Node getMembership( Node n, bool isPos, unsigned i );
   // semi normal forms for symbolic expression
   std::map< Node, Node > d_nf_regexps;
   std::map< Node, std::vector< Node > > d_nf_regexps_exp;