Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.

6 files changed, 24 insertions, 18 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index f3203da4b..54be11b44 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -656,6 +656,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 +664,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 representatives 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 +675,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/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..b7f015f47 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -71,7 +71,7 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de
 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 +95,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
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e9c754d4a..164e9e643 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\
++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper.\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\
@@ -217,13 +217,13 @@ 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;
+  if(optarg ==  "gen-ev") {
+    return MBQI_GEN_EVAL;
   } else if(optarg ==  "none") {
     return MBQI_NONE;
   } 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") {
     return MBQI_FMC_INTERVAL;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ea1231e7a..e6ee8f53b 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();