Merge remote-tracking branch 'upstream/master' into sets

9 files changed, 48 insertions, 32 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index d815e0ee8..098a7819a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
   Node curr;
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
-    Node v = getRepresentative( d_models[op]->d_value[i] );
+    Node v = d_models[op]->d_value[i];
+    if( !hasTerm( v ) ){
+      //can happen when the model basis term does not exist in ground assignment
+      TypeNode tn = v.getType();
+      if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
+        //see full_model_check.cpp line 366
+        v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
+      }else{
+        Assert( false );
+      }
+    }
+    v = getRepresentative( v );
     if( curr.isNull() ){
       curr = v;
     }else{
@@ -656,6 +667,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       Node cond = d_models[op]->d_cond[i];
       std::vector< Node > children;
       for( unsigned j=0; j<cond.getNumChildren(); j++) {
+        TypeNode tn = vars[j].getType();
         if (isInterval(cond[j])){
           if( !isStar(cond[j][0]) ){
             children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) );
@@ -663,7 +675,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
           if( !isStar(cond[j][1]) ){
             children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
           }
-        }else if (!isStar(cond[j])){
+        }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground eqc of this type
+                   d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
           Node c = getUsedRepresentative( cond[j] );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }
@@ -673,6 +686,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
     }
   }
+  Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
   curr = Rewriter::rewrite( curr );
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 3b6c8e492..0f3e53827 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
 void FullModelChecker::doNegate( Def & dc ) {
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
     if (!dc.d_value[i].isNull()) {
-      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;
+      dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] );
     }
   }
 }
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index 10185914e..8bd97a8a7 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -79,8 +79,8 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m
 
 std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
   switch(mode) {
-  case theory::quantifiers::MBQI_DEFAULT:
-    out << "MBQI_DEFAULT";
+  case theory::quantifiers::MBQI_GEN_EVAL:
+    out << "MBQI_GEN_EVAL";
     break;
   case theory::quantifiers::MBQI_NONE:
     out << "MBQI_NONE";
@@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode)
   case theory::quantifiers::MBQI_INTERVAL:
     out << "MBQI_INTERVAL";
     break;
+  case theory::quantifiers::MBQI_TRUST:
+    out << "MBQI_TRUST";
+    break;
   default:
     out << "MbqiMode!UNKNOWN";
   }
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 89e10b175..80534c8b0 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -58,13 +58,13 @@ typedef enum {
 } AxiomInstMode;
 
 typedef enum {
-  /** default, mbqi from CADE 24 paper */
-  MBQI_DEFAULT,
+  /** mbqi from CADE 24 paper */
+  MBQI_GEN_EVAL,
   /** no mbqi */
   MBQI_NONE,
   /** implementation that mimics inst-gen */
   MBQI_INST_GEN,
-  /** mbqi from Section 5.4.2 of AJR thesis */
+  /** default, mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
   /** mbqi with integer intervals */
   MBQI_FMC_INTERVAL,
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 0865f2c0b..e733764f0 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -67,11 +67,13 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false
 
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
+option instMaxLevel --inst-max-level=N int :default -1
+ maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
  
-option fullSaturateQuant --full-saturate-quant bool :default true
+option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
@@ -95,7 +97,7 @@ option internalReps /--disable-quant-internal-reps bool :default true
 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
  use finite model finding heuristic for quantifier instantiation
 
-option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
+option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
 option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for mbqi
@@ -112,7 +114,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
-option fmfBoundInt --fmf-bound-int bool :default false :read-write
+option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
  finite model finding on bounded integer quantification
 
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e9c754d4a..b7e624a66 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -82,8 +82,8 @@ static const std::string mbqiModeHelp = "\
 Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
 \n\
 default \n\
-+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper.\n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
+  Modulo Theories.\n\
 \n\
 none \n\
 + Disable model-based quantifier instantiation.\n\
@@ -91,12 +91,12 @@ none \n\
 instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
-fmc \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
-  Modulo Theories.\n\
+gen-ev \n\
++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper based on generalizing evaluations.\n\
 \n\
 fmc-interval \n\
-+ Same as fmc, but with intervals for models of integer functions.\n\
++ Same as default, but with intervals for models of integer functions.\n\
 \n\
 interval \n\
 + Use algorithm that abstracts domain elements as intervals. \n\
@@ -131,9 +131,6 @@ conflict \n\
 partial \n\
 + Apply QCF algorithm to instantiate heuristically as well. \n\
 \n\
-partial \n\
-+ Apply QCF to instantiate heuristically as well. \n\
-\n\
 mc \n\
 + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
 \n\
@@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar
 }
 
 inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default") {
-    return MBQI_DEFAULT;
-  } else if(optarg ==  "none") {
+  if(optarg == "gen-ev") {
+    return MBQI_GEN_EVAL;
+  } else if(optarg == "none") {
     return MBQI_NONE;
-  } else if(optarg ==  "instgen") {
+  } else if(optarg == "instgen") {
     return MBQI_INST_GEN;
-  } else if(optarg ==  "fmc") {
+  } else if(optarg == "default" || optarg ==  "fmc") {
     return MBQI_FMC;
-  } else if(optarg ==  "fmc-interval") {
+  } else if(optarg == "fmc-interval") {
     return MBQI_FMC_INTERVAL;
-  } else if(optarg ==  "interval") {
+  } else if(optarg == "interval") {
     return MBQI_INTERVAL;
-  } else if(optarg ==  "trust") {
+  } else if(optarg == "trust") {
     return MBQI_TRUST;
-  } else if(optarg ==  "help") {
+  } else if(optarg == "help") {
     puts(mbqiModeHelp.c_str());
     exit(1);
   } else {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c0b318f23..e27d438be 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 

 bool MatchGen::isHandledUfTerm( TNode n ) {

   return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||

-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;

+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;

 }

 

 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cf183dd18..3168d21a0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) {
     }
     d_par_op_map[op][tn1][tn2] = n;
     return n;
-  }else if( n.getKind()==APPLY_UF ){
+  }else if( inst::Trigger::isAtomicTrigger( n ) ){
     return n.getOperator();
   }else{
     return Node::null();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 6912c9e89..3de12b9c9 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 
 bool Trigger::isAtomicTrigger( Node n ){
   return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE ||
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;
+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
 }
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){