Prenex quantified formulas with user annotations by default (#7048)

Our policy is now accurate to the help message on prenexUserQuant: we only prenex quantified formulas if they do not have user-provided patterns. Previously we also did not prenex any quantified formulas with any annotations.

This should avoid some more "unknown" responses on facebook benchmarks.

Also fixes a minor issue with when we print warnings about quantified formulas with no triggers.

FYI @barrettcw .

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8901ec314923848b16c2cb2fbded7c1a836547f4..e01a8fee2ad3cee391ef289978235395f434a5b6 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -147,7 +147,7 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
   {
     generateTriggers(f);
     if (d_counter[f] == 0 && d_auto_gen_trigger[0][f].empty()
-        && d_auto_gen_trigger[1][f].empty() && f.getNumChildren() == 2)
+        && d_auto_gen_trigger[1][f].empty() && !QuantAttributes::hasPattern(f))
     {
       Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
       Output(options::OutputTag::TRIGGER)

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 99949e223f8985b70ebe8afdd95342fd3d6d221d..ead42a3cd51f47ff62ce8bf12a3915e04a9de958 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -204,16 +204,8 @@ void InstantiationEngine::checkOwnership(Node q)
       && q.getNumChildren() == 3)
   {
     //if strict triggers, take ownership of this quantified formula
-    bool hasPat = false;
-    for (const Node& qc : q[2])
+    if (QuantAttributes::hasPattern(q))
     {
-      if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
-      {
-        hasPat = true;
-        break;
-      }
-    }
-    if( hasPat ){
       d_qreg.setOwner(q, this, 1);
     }
   }

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 7204a60e185feba72bb4ce9bd8a43a07b3082fec..deed1c7611f3ea5bba08b20ac9c7aa865fce3ac8 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -168,6 +168,23 @@ bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) {
   return false;
 }
 
+bool QuantAttributes::hasPattern(Node q)
+{
+  Assert(q.getKind() == FORALL);
+  if (q.getNumChildren() != 3)
+  {
+    return false;
+  }
+  for (const Node& qc : q[2])
+  {
+    if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
 void QuantAttributes::computeAttributes( Node q ) {
   computeQuantAttributes( q, d_qattr[q] );
   QAttributes& qa = d_qattr[q];

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 48fb4f15908101be8e4c9001b881fb55eb5d2651..cb25546dd979ece721670e92cc7d4589c39542c5 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -208,6 +208,8 @@ class QuantAttributes
   static Node getFunDefBody( Node q );
   /** is quant elim annotation */
   static bool checkQuantElimAnnotation( Node ipl );
+  /** does q have a user-provided pattern? */
+  static bool hasPattern(Node q);
 
   /** is function definition */
   bool isFunDef( Node q );

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 02af92887c35daf601e27885ba4e363b253c45f6..0412513b2b319870a80c7f998a8273727c5416a5 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1270,7 +1270,9 @@ Node QuantifiersRewriter::computePrenex(Node q,
   Kind k = body.getKind();
   if (k == FORALL)
   {
-    if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){
+    if ((pol || prenexAgg)
+        && (options::prenexQuantUser() || !QuantAttributes::hasPattern(body)))
+    {
       std::vector< Node > terms;
       std::vector< Node > subs;
       BoundVarManager* bvm = nm->getBoundVarManager();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1f2e17a7c18cab801e86eb2487cae0daabac20f7..483e3a01e4c5919537581cb33cd83b33e5cce8c2 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1832,6 +1832,7 @@ set(regress_1_tests
   regress1/quantifiers/cdt-0208-to.smt2
   regress1/quantifiers/const.cvc
   regress1/quantifiers/constfunc.cvc
+  regress1/quantifiers/ddatv-delta2.smt2
   regress1/quantifiers/dt-tc-opt-small.smt2
   regress1/quantifiers/dump-inst-i.smt2
   regress1/quantifiers/dump-inst-proof.smt2

diff --git a/test/regress/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/regress1/quantifiers/ddatv-delta2.smt2
new file mode 100644 (file)
index 0000000..b41b8c9
--- /dev/null
+++ b/test/regress/regress1/quantifiers/ddatv-delta2.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-datatypes ((T 0) (D 0)) (((E) (o (b Bool)) (I (t Int)) (i (v D)) (R (l T) (u T))) ((i (v U)))))
+(declare-datatypes ((H 0)) (((M (h T)))))
+(declare-fun S (U Int) T)
+(declare-fun n () H)
+(assert (and 
+(not (b (o (or (b (o (or (b (o (or (b (o (= (t (S (v (v (S (v (v E)) 0))) (t E))) (t (S (v (v (S (v (v (h n))) 0))) (t E))))))))))))))))
+(b (o (forall ((i Int)) (or (< i (t (u (R E E)))) (b (o (forall ((z Int)) (! (or (b (o (or (b (o (< (t (S (v (v (S (v (v (h n))) z))) (t E))) (t (S (v (v (S (v (v (h n))) 0))) (t (I i))))))))))) :qid id))))))))))
+(check-sat)