Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.

4 files changed, 34 insertions, 23 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a2809bd67..7d41ae862 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -254,15 +254,21 @@ last-call\n\
 const std::string OptionsHandler::s_literalMatchHelp = "\
 Literal match modes currently supported by the --literal-match option:\n\
 \n\
-none (default)\n\
+none \n\
 + Do not use literal matching.\n\
 \n\
-predicate\n\
-+ Consider the phase requirements of predicate literals when applying heuristic\n\
-  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
-  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
-  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
-  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+use (default)\n\
++ Consider phase requirements of triggers conservatively. For example, the\n\
+  trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\
+  terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\
+  terms in the equivalence class of false. Extends to equality.\n\
+\n\
+agg-predicate \n\
++ Consider phase requirements aggressively for predicates. In the above example,\n\
+  only match P( x ) with terms that are in the equivalence class of false.\n\
+\n\
+agg \n\
++ Consider the phase requirements aggressively for all triggers.\n\
 \n\
 ";
 
@@ -506,10 +512,12 @@ void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::
 theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg ==  "none") {
     return theory::quantifiers::LITERAL_MATCH_NONE;
-  } else if(optarg ==  "predicate") {
-    return theory::quantifiers::LITERAL_MATCH_PREDICATE;
-  } else if(optarg ==  "equality") {
-    return theory::quantifiers::LITERAL_MATCH_EQUALITY;
+  } else if(optarg ==  "use") {
+    return theory::quantifiers::LITERAL_MATCH_USE;
+  } else if(optarg ==  "agg-predicate") {
+    return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
+  } else if(optarg ==  "agg") {
+    return theory::quantifiers::LITERAL_MATCH_AGG;
   } else if(optarg ==  "help") {
     puts(s_literalMatchHelp.c_str());
     exit(1);
@@ -520,9 +528,7 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s
 }
 
 void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) {
-  if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) {
-    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
-  }
+
 }
 
 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) {
diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index a58120974..e2cd78de5 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -46,11 +46,14 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
   case theory::quantifiers::LITERAL_MATCH_NONE:
     out << "LITERAL_MATCH_NONE";
     break;
-  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
-    out << "LITERAL_MATCH_PREDICATE";
+  case theory::quantifiers::LITERAL_MATCH_USE:
+    out << "LITERAL_MATCH_USE";
     break;
-  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
-    out << "LITERAL_MATCH_EQUALITY";
+  case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE:
+    out << "LITERAL_MATCH_AGG_PREDICATE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_AGG:
+    out << "LITERAL_MATCH_AGG";
     break;
   default:
     out << "LiteralMatchMode!UNKNOWN";
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 5749da972..b4b9abdaf 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -44,10 +44,12 @@ enum InstWhenMode {
 enum LiteralMatchMode {
   /** Do not consider polarity of patterns */
   LITERAL_MATCH_NONE,
-  /** Consider polarity of boolean predicates only */
-  LITERAL_MATCH_PREDICATE,
-  /** Consider polarity of boolean predicates, as well as equalities */
-  LITERAL_MATCH_EQUALITY,
+  /** Conservatively consider polarity of patterns */
+  LITERAL_MATCH_USE,
+  /** Aggressively consider polarity of Boolean predicates */
+  LITERAL_MATCH_AGG_PREDICATE,
+  /** Aggressively consider polarity of all terms */
+  LITERAL_MATCH_AGG,
 };
 
 enum MbqiMode {
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f69a8df8b..9fef0295e 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -120,7 +120,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
 option fullSaturateInst --fs-inst bool :default false
  interleave full saturate instantiation with other techniques
 
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
  choose literal matching mode
 
 ### finite model finding options