Fix policy for eliminating quantified formulas (#7017)

This also consolidates the option strictTriggers into userPatMode.

Fixes #6996.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 58632aafc88b23b6635421635a81e7e9eb9d4e0e..ad74e4ab9510fc02aa2dc5100c095545bde192f6 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -226,14 +226,6 @@ name   = "Quantifiers"
   default    = "false"
   help       = "consider ground terms within bodies of quantified formulas for matching"
 
-[[option]]
-  name       = "strictTriggers"
-  category   = "regular"
-  long       = "strict-triggers"
-  type       = "bool"
-  default    = "false"
-  help       = "only instantiate quantifiers with user patterns based on triggers"
-
 [[option]]
   name       = "relevantTriggers"
   category   = "regular"
@@ -388,6 +380,9 @@ name   = "Quantifiers"
 [[option.mode.TRUST]]
   name = "trust"
   help = "When provided, use only user-provided patterns for a quantified formula."
+[[option.mode.STRICT]]
+  name = "trust"
+  help = "When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques."
 [[option.mode.RESORT]]
   name = "resort"
   help = "Use user-provided patterns only after auto-generated patterns saturate."

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6fd2a3f6835fd1257ba93ef188cc4b6841d21460..12433d8ace832c132b39e1b6ae74d10d2f1865a9 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1104,13 +1104,6 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
     }
   }
   // implied options...
-  if (opts.quantifiers.strictTriggers)
-  {
-    if (!opts.quantifiers.userPatternsQuantWasSetByUser)
-    {
-      opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST;
-    }
-  }
   if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint)
   {
     opts.quantifiers.quantConflictFind = true;

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index ab237fc6cd0e5fdcfd2d2836eaef8754c2821a36..8901ec314923848b16c2cb2fbded7c1a836547f4 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -111,7 +111,10 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
                                                         int e)
 {
   options::UserPatMode upMode = getInstUserPatMode();
-  if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
+  // we don't auto-generate triggers if the mode is trust or strict
+  if (hasUserPatterns(f)
+      && (upMode == options::UserPatMode::TRUST
+          || upMode == options::UserPatMode::STRICT))
   {
     return InstStrategyStatus::STATUS_UNKNOWN;
   }

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index d490dce839fefada6578a25c79306452b39bee77..d9bec820ce6285c81b1e86d977b4026b5221069d 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -200,11 +200,15 @@ bool InstantiationEngine::checkCompleteFor( Node q ) {
 
 void InstantiationEngine::checkOwnership(Node q)
 {
-  if( options::strictTriggers() && q.getNumChildren()==3 ){
+  if (options::userPatternsQuant() == options::UserPatMode::STRICT
+      && q.getNumChildren() == 3)
+  {
     //if strict triggers, take ownership of this quantified formula
     bool hasPat = false;
-    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
-      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN  ){
+    for (const Node& qc : q)
+    {
+      if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
+      {
         hasPat = true;
         break;
       }

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 1abbd198926e17fb65ab56adcdfafae114aed579..33ed6f53662467d6276ee0c593f6da34db1ff4ee 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -30,8 +30,7 @@ namespace quantifiers {
 
 bool QAttributes::isStandard() const
 {
-  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull()
-         && !d_isInternal;
+  return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal;
 }
 
 QuantAttributes::QuantAttributes() {}

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index b3fdd09da2819fa5a50bd987d1b0cbe250fa4f83..910dbab5bca2429be7df2a4b12a4d6355854c50a 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -162,8 +162,7 @@ struct QAttributes
    * perform destructive updates (variable elimination, miniscoping, etc).
    *
    * A quantified formula is not standard if it is sygus, one for which
-   * we are performing quantifier elimination, is a function definition, or
-   * has a name.
+   * we are performing quantifier elimination, or is a function definition.
    */
   bool isStandard() const;
 };

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 48106b858420fdfea1a0caebaca1cd64b0915cfa..aba2d79bf5387c26af9cffb3498672ec14084ef6 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1797,7 +1797,7 @@ bool QuantifiersRewriter::doOperation(Node q,
 {
   bool is_strict_trigger =
       qa.d_hasPattern
-      && options::userPatternsQuant() == options::UserPatMode::TRUST;
+      && options::userPatternsQuant() == options::UserPatMode::STRICT;
   bool is_std = qa.isStandard() && !is_strict_trigger;
   if (computeOption == COMPUTE_ELIM_SYMBOLS)
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2706dee8af176df543322a3f9c108942d35cf9bd..6f71e09936f242d3845766cd6577c3bf6f6f7c6b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -910,6 +910,7 @@ set(regress_0_tests
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
   regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
+  regress0/quantifiers/issue6996-trivial-elim.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2

diff --git a/test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2 b/test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2
new file mode 100644 (file)
index 0000000..939044b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((@ 0)) (((V))))
+(declare-fun I (@ Int) Bool)
+(assert (forall ((v @) (i Int)) (! false :qid |outputbpl.122:24| :pattern ((I v i)))))
+(check-sat)