Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.

3 files changed, 12 insertions, 15 deletions

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 164e9e643..b7e624a66 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -92,8 +92,8 @@ instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
 gen-ev \n\
-+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper.\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 default, but with intervals for models of integer functions.\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 ==  "gen-ev") {
+  if(optarg == "gen-ev") {
     return MBQI_GEN_EVAL;
-  } else if(optarg ==  "none") {
+  } else if(optarg == "none") {
     return MBQI_NONE;
-  } else if(optarg ==  "instgen") {
+  } else if(optarg == "instgen") {
     return MBQI_INST_GEN;
-  } else if(optarg ==  "default" || 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/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 ) ){