From 78e84e867417642b04da5c136ef548dfde8ca7f0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 22 Aug 2021 14:37:50 -0500 Subject: [PATCH] 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 . --- .../ematching/inst_strategy_e_matching.cpp | 2 +- .../ematching/instantiation_engine.cpp | 10 +--------- .../quantifiers/quantifiers_attributes.cpp | 17 +++++++++++++++++ src/theory/quantifiers/quantifiers_attributes.h | 2 ++ src/theory/quantifiers/quantifiers_rewriter.cpp | 4 +++- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/ddatv-delta2.smt2 | 11 +++++++++++ 7 files changed, 36 insertions(+), 11 deletions(-) create mode 100644 test/regress/regress1/quantifiers/ddatv-delta2.smt2 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 8901ec314..e01a8fee2 100644 --- 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 99949e223..ead42a3cd 100644 --- 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 7204a60e1..deed1c761 100644 --- 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 48fb4f159..cb25546dd 100644 --- 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 02af92887..0412513b2 100644 --- 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 1f2e17a7c..483e3a01e 100644 --- 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 index 000000000..b41b8c9b0 --- /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) -- 2.30.2