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, 27 insertions, 22 deletions

diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index c3064116f..5190025ee 100644..100755
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -53,10 +53,10 @@ void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) {
 }
 
 void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) {
-  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
+  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
   if( re_i!=d_rep_exp.end() ){
-    for( unsigned i=0; i<(*re_i).second->size(); i++ ){
-      addToExplanation( exp, (*(*re_i).second)[i] );
+    for( int i=0; i<(*re_i).second; i++ ){
+      addToExplanation( exp, d_rep_exp_data[eqc][i] );
     }
   }
   //for( unsigned i=0; i<d_eqci[n]->d_rep_exp.size(); i++ ){
@@ -65,16 +65,19 @@ void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc
 }
 
 void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) {
-  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
-  NodeList* re;
+  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
+  int n_re = 0;
   if( re_i != d_rep_exp.end() ){
-    re = (*re_i).second;
-  }else{
-    re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
-    d_rep_exp.insertDataFromContextMemory( eqc, re );
+    n_re = (*re_i).second;
   }
+  d_rep_exp[eqc] = n_re + exp_to_add.size();
   for( unsigned i=0; i<exp_to_add.size(); i++ ){
-    re->push_back( exp_to_add[i] );
+    if( n_re<(int)d_rep_exp_data[eqc].size() ){
+      d_rep_exp_data[eqc][n_re] = exp_to_add[i];
+    }else{
+      d_rep_exp_data[eqc].push_back( exp_to_add[i] );
+    }
+    n_re++;
   }
   //for( unsigned i=0; i<exp_to_add.size(); i++ ){
   //  eqci->d_rep_exp.push_back( exp_to_add[i] );
@@ -204,16 +207,18 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
 
 void EqualityInference::addToUseList( Node used, Node eqc ) {
 #if 1
-  NodeListMap::iterator ul_i = d_uselist.find( used );
-  NodeList* ul;
+  NodeIntMap::iterator ul_i = d_uselist.find( used );
+  int n_ul = 0;
   if( ul_i != d_uselist.end() ){
-    ul = (*ul_i).second;
-  }else{
-    ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
-    d_uselist.insertDataFromContextMemory( used, ul );
+    n_ul = (*ul_i).second;
   }
+  d_uselist[ used ] = n_ul + 1;
   Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
-  (*ul).push_back( eqc );  
+  if( n_ul<(int)d_uselist_data[used].size() ){
+    d_uselist_data[used][n_ul] = eqc;
+  }else{
+    d_uselist_data[used].push_back( eqc );  
+  }
 #else
   std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used );
   EqcInfo * eqci_used;
@@ -356,12 +361,12 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
               //go through all equivalence classes that may refer to v_solve
               std::map< Node, bool > processed;
               processed[v_solve] = true;
-              NodeListMap::iterator ul_i = d_uselist.find( v_solve );
+              NodeIntMap::iterator ul_i = d_uselist.find( v_solve );
               if( ul_i != d_uselist.end() ){
-                NodeList* ul = (*ul_i).second;
-                Trace("eq-infer-debug") << "      use list size = " << ul->size() << std::endl;
-                for( unsigned j=0; j<ul->size(); j++ ){
-                  Node r = (*ul)[j];
+                int n_ul = (*ul_i).second;
+                Trace("eq-infer-debug") << "      use list size = " << n_ul << std::endl;
+                for( int j=0; j<n_ul; j++ ){
+                  Node r = d_uselist_data[v_solve][j];
                 //Trace("eq-infer-debug") << "      use list size = " << eqci_solved->d_uselist.size() << std::endl;
                 //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){
                 //  Node r = eqci_solved->d_uselist[j];