From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 17 Aug 2021 17:07:00 +0000 (-0500)
Subject: Fix policy for eliminating quantified formulas (#7017)
X-Git-Tag: cvc5-1.0.0~1377
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf5376c18d8e4d6b3ed2d7b341279cf65fc16418;p=cvc5.git

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 58632aafc..ad74e4ab9 100644
--- 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 6fd2a3f68..12433d8ac 100644
--- 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 ab237fc6c..8901ec314 100644
--- 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 d490dce83..d9bec820c 100644
--- 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 1abbd1989..33ed6f536 100644
--- 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 b3fdd09da..910dbab5b 100644
--- 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 48106b858..aba2d79bf 100644
--- 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 2706dee8a..6f71e0993 100644
--- 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
index 000000000..939044b4e
--- /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)