New module for generating candidate equality conjectures used in inductive proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).

1 files changed, 28 insertions, 0 deletions

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 38567d166..86d0c27e4 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -152,6 +152,19 @@ ignore \n\
 + Ignore user-provided patterns. \n\
 \n\
 ";
+static const std::string triggerSelModeHelp = "\
+User pattern modes currently supported by the --trigger-sel option:\n\
+\n\
+default \n\
++ Default, consider all subterms of quantified formulas for trigger selection.\n\
+\n\
+min \n\
++ Consider only minimal subterms that meet criteria for triggers.\n\
+\n\
+max \n\
++ Consider only maximal subterms that meet criteria for triggers. \n\
+\n\
+";
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
     return INST_WHEN_PRE_FULL;
@@ -296,6 +309,21 @@ inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, S
                           optarg + "'.  Try --user-pat help.");
   }
 }
+inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default" || optarg == "all" ) {
+    return TRIGGER_SEL_DEFAULT;
+  } else if(optarg == "min") {
+    return TRIGGER_SEL_MIN;
+  } else if(optarg == "max") {
+    return TRIGGER_SEL_MAX;
+  } else if(optarg ==  "help") {
+    puts(triggerSelModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --trigger-sel: `") +
+                          optarg + "'.  Try --trigger-sel help.");
+  }
+}
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */