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.

1 files changed, 9 insertions, 9 deletions

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;