Add term db mode. Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup.

1 files changed, 24 insertions, 0 deletions

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e00879303..08fcf319d 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -188,6 +188,16 @@ none \n\
 + Do not enforce fairness. \n\
 \n\
 ";
+static const std::string termDbModeHelp = "\
+Modes for term database, supported by --term-db-mode:\n\
+\n\
+all  \n\
++ Consider all terms in the system.\n\
+\n\
+relevant \n\
++ Consider only terms connected to current assertions. \n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -380,6 +390,20 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar
   }
 }
 
+inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "all" ) {
+    return TERM_DB_ALL;
+  } else if(optarg == "relevant") {
+    return TERM_DB_RELEVANT;
+  } else if(optarg ==  "help") {
+    puts(termDbModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --term-db-mode: `") +
+                          optarg + "'.  Try --term-db-mode help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */