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, 8 insertions, 7 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 33c853328..a0665cb7f 100644..100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -405,7 +405,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       bool needsDefault = true;
       for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
         Node n = fm->d_uf_terms[op][i];
-        if( !n.getAttribute(NoMatchAttribute()) ){
+        if( d_qe->getTermDatabase()->isTermActive( n ) ){
           add_conds.push_back( n );
           add_values.push_back( n );
           Node r = fm->getUsedRepresentative(n);
@@ -764,7 +764,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
     Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
     //set the domains based on the entry
     for (unsigned i=0; i<c.getNumChildren(); i++) {
-      if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
+      if( riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS || riter.d_enum_type[i]==RepSetIterator::ENUM_SET_MEMBERS ){
         TypeNode tn = c[i].getType();
         if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
           if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
@@ -773,6 +773,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
             if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
               riter.d_domain[i].clear();
               riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+              riter.d_enum_type[i] = RepSetIterator::ENUM_DOMAIN_ELEMENTS;
             }else{
               Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl;
               return false;
@@ -792,7 +793,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       std::vector< Node > ev_inst;
       std::vector< Node > inst;
       for( int i=0; i<riter.getNumTerms(); i++ ){
-        Node rr = riter.getTerm( i );
+        Node rr = riter.getCurrentTerm( i );
         Node r = rr;
         //if( r.getType().isSort() ){
         r = fm->getUsedRepresentative( r );
@@ -826,18 +827,18 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       int index = riter.increment();
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
       if( !riter.isFinished() ){
-        if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
+        if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_INT_RANGE) {
           Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
           riter.increment2( index-1 );
         }
       }
     }
     d_addedLemmas += addedLemmas;
-    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
-    return addedLemmas>0 || !riter.d_incomplete;
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.isIncomplete() << std::endl;
+    return addedLemmas>0 || !riter.isIncomplete();
   }else{
     Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
-    return false;
+    return !riter.isIncomplete();
   }
 }