From dfb4a4a988ffcc39f41c5cb9c74c7ffc9ed74513 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Jan 2022 17:42:14 -0600 Subject: [PATCH] Make alpha equivalence user context dependent (#7889) Fixes #5373 Issues were occurring due to using quantified formulas in alpha equivalence that were stale. This also removes spurious warnings from quantifier elimination (dropping the "strict" requirement, which unnecessarily warns if we are in a non-arithmetic logic). --- src/api/cpp/cvc5.cpp | 4 +- src/smt/solver_engine.cpp | 8 +-- src/smt/solver_engine.h | 7 +-- src/theory/quantifiers/alpha_equivalence.cpp | 38 ++++++++++++-- src/theory/quantifiers/alpha_equivalence.h | 49 +++++++++++-------- src/theory/quantifiers/cegqi/nested_qe.cpp | 2 +- .../quantifiers/sygus/sygus_qe_preproc.cpp | 2 +- test/regress/CMakeLists.txt | 2 + .../quantifiers/issue5373-1-qe-inc.smt2 | 6 +++ .../regress1/quantifiers/issue5373-2.smt2 | 13 +++++ 10 files changed, 88 insertions(+), 43 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5373-2.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a6036485f..868fdd028 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7466,7 +7466,7 @@ Term Solver::getQuantifierElimination(const Term& q) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term(this, d_slv->getQuantifierElimination(q.getNode(), true, true)); + return Term(this, d_slv->getQuantifierElimination(q.getNode(), true)); //////// CVC5_API_TRY_CATCH_END; } @@ -7476,7 +7476,7 @@ Term Solver::getQuantifierEliminationDisjunct(const Term& q) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term(this, d_slv->getQuantifierElimination(q.getNode(), false, true)); + return Term(this, d_slv->getQuantifierElimination(q.getNode(), false)); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 4bb3bfabf..97774a739 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1622,16 +1622,10 @@ bool SolverEngine::getSubsolverSynthSolutions(std::map& solMap) return d_sygusSolver->getSubsolverSynthSolutions(solMap); } -Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict) +Node SolverEngine::getQuantifierElimination(Node q, bool doFull) { SolverEngineScope smts(this); finishInit(); - const LogicInfo& logic = getLogicInfo(); - if (!logic.isPure(THEORY_ARITH) && strict) - { - d_env->warning() << "Unexpected logic for quantifier elimination " << logic - << endl; - } return d_quantElimSolver->getQuantifierElimination( *d_asserts, q, doFull, d_isInternalSubsolver); } diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 99d2502b9..dd98c674e 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -617,13 +617,8 @@ class CVC5_EXPORT SolverEngine * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. - * - * The argument strict is whether to output - * warnings, such as when an unexpected logic is used. - * - * throw@ Exception */ - Node getQuantifierElimination(Node q, bool doFull, bool strict = true); + Node getQuantifierElimination(Node q, bool doFull); /** * This method asks this SMT engine to find an interpolant with respect to diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 0c9a5ba46..d36343c6b 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -32,7 +32,13 @@ struct sortTypeOrder { } }; +AlphaEquivalenceTypeNode::AlphaEquivalenceTypeNode(context::Context* c) + : d_quant(c) +{ +} + Node AlphaEquivalenceTypeNode::registerNode( + context::Context* c, Node q, Node t, std::vector& typs, @@ -40,25 +46,47 @@ Node AlphaEquivalenceTypeNode::registerNode( { AlphaEquivalenceTypeNode* aetn = this; size_t index = 0; + std::map, + std::unique_ptr>::iterator itc; while (index < typs.size()) { TypeNode curr = typs[index]; Assert(typCount.find(curr) != typCount.end()); Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] "; std::pair key(curr, typCount[curr]); - aetn = &(aetn->d_children[key]); + itc = aetn->d_children.find(key); + if (itc == aetn->d_children.end()) + { + aetn->d_children[key] = std::make_unique(c); + aetn = aetn->d_children[key].get(); + } + else + { + aetn = itc->second.get(); + } index = index + 1; } Trace("aeq-debug") << " : "; - std::map::iterator it = aetn->d_quant.find(t); - if (it != aetn->d_quant.end()) + NodeMap::iterator it = aetn->d_quant.find(t); + if (it != aetn->d_quant.end() && !it->second.isNull()) { + Trace("aeq-debug") << it->second << std::endl; return it->second; } + Trace("aeq-debug") << "(new)" << std::endl; aetn->d_quant[t] = q; return q; } +AlphaEquivalenceDb::AlphaEquivalenceDb(context::Context* c, + expr::TermCanonize* tc, + bool sortCommChildren) + : d_context(c), + d_ae_typ_trie(c), + d_tc(tc), + d_sortCommutativeOpChildren(sortCommChildren) +{ +} Node AlphaEquivalenceDb::addTerm(Node q) { Assert(q.getKind() == FORALL); @@ -129,7 +157,7 @@ Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q) sto.d_tu = d_tc; std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; - Node ret = d_ae_typ_trie.registerNode(q, t, typs, typCount); + Node ret = d_ae_typ_trie.registerNode(d_context, q, t, typs, typCount); Trace("aeq") << " ...result : " << ret << std::endl; return ret; } @@ -137,7 +165,7 @@ Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q) AlphaEquivalence::AlphaEquivalence(Env& env) : EnvObj(env), d_termCanon(), - d_aedb(&d_termCanon, true), + d_aedb(userContext(), &d_termCanon, true), d_pnm(env.getProofNodeManager()), d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr) { diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index d1a05e486..ce39eb434 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -35,23 +35,29 @@ namespace quantifiers { * d_children[T1][2].d_children[T2][3]. */ class AlphaEquivalenceTypeNode { -public: - /** children of this node */ - std::map, AlphaEquivalenceTypeNode> d_children; - /** - * map from canonized quantifier bodies to a quantified formula whose - * canonized body is that term. - */ - std::map d_quant; - /** register node - * - * This registers term q to this trie. The term t is the canonical form of - * q, typs/typCount represent a multi-set of types of free variables in t. - */ - Node registerNode(Node q, - Node t, - std::vector& typs, - std::map& typCount); + using NodeMap = context::CDHashMap; + + public: + AlphaEquivalenceTypeNode(context::Context* c); + /** children of this node */ + std::map, + std::unique_ptr> + d_children; + /** + * map from canonized quantifier bodies to a quantified formula whose + * canonized body is that term. + */ + NodeMap d_quant; + /** register node + * + * This registers term q to this trie. The term t is the canonical form of + * q, typs/typCount represent a multi-set of types of free variables in t. + */ + Node registerNode(context::Context* c, + Node q, + Node t, + std::vector& typs, + std::map& typCount); }; /** @@ -60,10 +66,9 @@ public: class AlphaEquivalenceDb { public: - AlphaEquivalenceDb(expr::TermCanonize* tc, bool sortCommChildren) - : d_tc(tc), d_sortCommutativeOpChildren(sortCommChildren) - { - } + AlphaEquivalenceDb(context::Context* c, + expr::TermCanonize* tc, + bool sortCommChildren); /** adds quantified formula q to this database * * This function returns a quantified formula q' that is alpha-equivalent to @@ -87,6 +92,8 @@ class AlphaEquivalenceDb * had been added to this class, or q otherwise. */ Node addTermToTypeTrie(Node t, Node q); + /** The context we depend on */ + context::Context* d_context; /** a trie per # of variables per type */ AlphaEquivalenceTypeNode d_ae_typ_trie; /** pointer to the term canonize utility */ diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 0d01efba7..fddcb0712 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -139,7 +139,7 @@ Node NestedQe::doQe(Env& env, Node q) q = nm->mkNode(kind::EXISTS, q[0], q[1].negate()); std::unique_ptr smt_qe; initializeSubsolver(smt_qe, env); - Node qqe = smt_qe->getQuantifierElimination(q, true, false); + Node qqe = smt_qe->getQuantifierElimination(q, true); if (expr::hasBoundVar(qqe)) { Trace("cegqi-nested-qe") << " ...failed QE" << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index b57c65f0f..590703879 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -117,7 +117,7 @@ Node SygusQePreproc::preprocess(Node q) Trace("cegqi-qep") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; - Node qeRes = smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true, false); + Node qeRes = smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true); Trace("cegqi-qep") << "Result : " << qeRes << std::endl; // create single invocation conjecture, if QE was successful diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bc084714d..66098220e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2019,6 +2019,8 @@ set(regress_1_tests regress1/quantifiers/issue5279-nqe.smt2 regress1/quantifiers/issue5288-vts-real-int.smt2 regress1/quantifiers/issue5365-nqe.smt2 + regress1/quantifiers/issue5373-1-qe-inc.smt2 + regress1/quantifiers/issue5373-2.smt2 regress1/quantifiers/issue5378-witness.smt2 regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 diff --git a/test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2 b/test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2 new file mode 100644 index 000000000..48bbe2df1 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -i +; EXPECT: true +; EXPECT: true +(set-logic ALL) +(get-qe (exists ((q Real) (q Bool) (q Bool) (q Bool) (q Real) (q Real) (q Real)) true)) +(get-qe (exists ((q Real) (q Bool) (f Bool) (q Bool) (q Real) (q Real) (q Real)) true)) diff --git a/test/regress/regress1/quantifiers/issue5373-2.smt2 b/test/regress/regress1/quantifiers/issue5373-2.smt2 new file mode 100644 index 000000000..1987b71a6 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5373-2.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: -i +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-sort U 0) +(declare-fun c (U U) U) +(declare-fun k () U) +(declare-fun a (U Int) Int) +(assert (or (not (forall ((g U)) (! (or (forall ((x Int)) (! (distinct (a g x) (a k x)) :qid k!10))) :qid k!10))) (exists ((f U) (g U) (x Int)) (distinct (a (c f g) x) (a f (a g x)))))) +(check-sat) +(check-sat-assuming ((exists ((f U) (g U) (x Int)) (distinct (a (c f g) x) (a f (a g x)))))) +(check-sat-assuming ((exists ((f U) (g U) (x Int)) (distinct (a (c f g) x) (a f (a g x)))))) -- 2.30.2