From 90eeba935ba0334699ba646ca099568562cd141d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Jul 2024 13:52:10 +0200 Subject: [PATCH] Simplify ProofRule::SKOLEMIZE (#10898) Changes: - ProofRule::SKOLEMIZE only expects negated universals as premises. - Skolems of id `QUANTIFIERS_SKOLEMIZE` take a universal instead of an existential. After doing this change, several BV invertibility condition benchmarks became "unknown", since the witness term elimination introduced in https://github.com/cvc5/cvc5/pull/10848 was not quite optimal: in particular, the skolems introduced when eliminating witness for BV invertibility condition instantiations would in rare cases not align with the quantified formulas since we did not run theory preprocessing on them. This fixes the issue by making the witness elimination take this into account via a new callback in this utility. --------- Co-authored-by: Abdalrhman Mohamed --- include/cvc5/cvc5_proof_rule.h | 12 ++------ include/cvc5/cvc5_skolem_id.h | 2 +- proofs/alf/cvc5/rules/Quantifiers.smt3 | 14 +++------ src/expr/elim_witness_converter.cpp | 13 +++++--- src/expr/elim_witness_converter.h | 6 ++++ .../quantifiers/cegqi/ceg_instantiator.cpp | 30 ++++++++++++++++++- src/theory/quantifiers/proof_checker.cpp | 27 +++++------------ src/theory/quantifiers/skolemize.cpp | 22 ++++---------- 8 files changed, 66 insertions(+), 60 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 6131d316556..c4f88b17e21 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -1308,18 +1308,12 @@ enum ENUM(ProofRule) * * .. math:: * - * \inferrule{\exists x_1\dots x_n.\> F\mid -}{F\sigma} - * - * or - * - * .. math:: - * * \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma} * * where :math:`\sigma` maps :math:`x_1,\dots,x_n` to their representative - * skolems obtained by ``SkolemManager::mkSkolemize``, returned in the skolems - * argument of that method. The witness terms for the returned skolems can be - * obtained by ``SkolemManager::getWitnessForm``. + * skolems, which are skolems :math:`k_1,\dots,k_n`. For each :math:`k_i`, + * its skolem identifier is :cpp:enumerator:`QUANTIFIERS_SKOLEMIZE `, + * and its indices are :math:`(\forall x_1\dots x_n.\> F)` and :math:`x_i`. * \endverbatim */ EVALUE(SKOLEMIZE), diff --git a/include/cvc5/cvc5_skolem_id.h b/include/cvc5/cvc5_skolem_id.h index fb49a6f35c3..93e571e5368 100644 --- a/include/cvc5/cvc5_skolem_id.h +++ b/include/cvc5/cvc5_skolem_id.h @@ -175,7 +175,7 @@ enum ENUM(SkolemId) */ EVALUE(SHARED_SELECTOR), /** - * The n^th skolem for quantified formula Q. + * The n^th skolem for the negation of universally quantified formula Q. * * - Number of skolem indices: ``2`` * - ``1:`` The quantified formula Q. diff --git a/proofs/alf/cvc5/rules/Quantifiers.smt3 b/proofs/alf/cvc5/rules/Quantifiers.smt3 index 28479dd05d8..84510bd5583 100644 --- a/proofs/alf/cvc5/rules/Quantifiers.smt3 +++ b/proofs/alf/cvc5/rules/Quantifiers.smt3 @@ -35,16 +35,10 @@ ; - Q Bool: The quantified formula to skolemize. This is either an existential or a negated universal. ; conclusion: > ; The skolemized body of Q, where its variables are replaced by skolems -; introduced via $mk_skolems, -(declare-rule skolemize ((F Bool)) - :premises (F) - :conclusion - (alf.match ((T Type) (x @List) (G Bool)) - F - ( - ((exists x G) ($substitute_list x ($mk_skolems x F) G)) - ((not (forall x G)) ($substitute_list x ($mk_skolems x (exists x (not G))) (not G))) - )) +; introduced via $mk_skolems. +(declare-rule skolemize ((x @List) (G Bool)) + :premises ((not (forall x G))) + :conclusion ($substitute_list x ($mk_skolems x (forall x G)) (not G)) ) ; rule: skolem_intro diff --git a/src/expr/elim_witness_converter.cpp b/src/expr/elim_witness_converter.cpp index bc7a9617761..48b4a2436ea 100644 --- a/src/expr/elim_witness_converter.cpp +++ b/src/expr/elim_witness_converter.cpp @@ -32,14 +32,19 @@ Node ElimWitnessNodeConverter::postConvert(Node n) NodeManager* nm = nodeManager(); SkolemManager* skm = nm->getSkolemManager(); std::vector nchildren(n.begin(), n.end()); - Node exists = nm->mkNode(Kind::EXISTS, nchildren); - Node k = skm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE, - {exists, n[0][0]}); - d_exists.push_back(exists); + nchildren[1] = nchildren[1].notNode(); + Node q = nm->mkNode(Kind::FORALL, nchildren); + Node qn = getNormalFormFor(q); + Node k = + skm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE, {qn, n[0][0]}); + d_exists.push_back(qn.notNode()); return k; } return n; } + +Node ElimWitnessNodeConverter::getNormalFormFor(const Node& q) { return q; } + const std::vector& ElimWitnessNodeConverter::getExistentials() const { return d_exists; diff --git a/src/expr/elim_witness_converter.h b/src/expr/elim_witness_converter.h index fce8f373b67..3eef199896b 100644 --- a/src/expr/elim_witness_converter.h +++ b/src/expr/elim_witness_converter.h @@ -45,6 +45,12 @@ class ElimWitnessNodeConverter : protected EnvObj, public NodeConverter */ const std::vector& getExistentials() const; + /** + * Get the normal form of a quantified formula for which we are introducing + * a skolem variable based on eliminating a witness term. + */ + virtual Node getNormalFormFor(const Node& q); + private: /** The list of existentials introduced by eliminating witness */ std::vector d_exists; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 3ff814e7d5b..e5deb6a5e3f 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -941,6 +941,34 @@ bool CegInstantiator::constructInstantiationInc(Node pv, } } +/** + * A class for eliminating witness terms. We require overriding the method of + * the base class to ensure that quantified formulas have been run through + * theory preprocessing. This ensures that the skolem variables introduced + * align exactly with the quantified formula we will assert in the corresponding + * QUANTIFIERS_CEGQI_WITNESS lemma. + */ +class PreprocessElimWitnessNodeConverter : public ElimWitnessNodeConverter +{ + public: + PreprocessElimWitnessNodeConverter(Env& env, Valuation& val) + : ElimWitnessNodeConverter(env), d_val(val) + { + } + /** + * Get the normal form for quantified formula q, which must perform theory + * preprocessing. + */ + Node getNormalFormFor(const Node& q) override + { + return d_val.getPreprocessedTerm(q); + } + + private: + /** Reference to a valuation */ + Valuation& d_val; +}; + bool CegInstantiator::doAddInstantiation(std::vector& vars, std::vector& subs) { @@ -983,7 +1011,7 @@ bool CegInstantiator::doAddInstantiation(std::vector& vars, { if (expr::hasSubtermKind(Kind::WITNESS, s)) { - ElimWitnessNodeConverter ewc(d_env); + PreprocessElimWitnessNodeConverter ewc(d_env, d_qstate.getValuation()); Node sc = ewc.convert(s); const std::vector& wexists = ewc.getExistentials(); exists.insert(exists.end(), wexists.begin(), wexists.end()); diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 3a1548d2260..7e7d5d19282 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -45,7 +45,6 @@ Node QuantifiersProofRuleChecker::checkInternal( const std::vector& children, const std::vector& args) { - NodeManager* nm = nodeManager(); if (id == ProofRule::SKOLEM_INTRO) { Assert(children.empty()); @@ -57,28 +56,18 @@ Node QuantifiersProofRuleChecker::checkInternal( { Assert(children.size() == 1); Assert(args.empty()); - // can use either negated FORALL or EXISTS - if (children[0].getKind() != Kind::EXISTS - && (children[0].getKind() != Kind::NOT - || children[0][0].getKind() != Kind::FORALL)) + // must use negated FORALL + if (children[0].getKind() != Kind::NOT + || children[0][0].getKind() != Kind::FORALL) { return Node::null(); } - Node exists; - if (children[0].getKind() == Kind::EXISTS) - { - exists = children[0]; - } - else - { - std::vector echildren(children[0][0].begin(), children[0][0].end()); - echildren[1] = echildren[1].notNode(); - exists = nm->mkNode(Kind::EXISTS, echildren); - } - std::vector vars(exists[0].begin(), exists[0].end()); - std::vector skolems = Skolemize::getSkolemConstants(exists); - Node res = exists[1].substitute( + Node q = children[0][0]; + std::vector vars(q[0].begin(), q[0].end()); + std::vector skolems = Skolemize::getSkolemConstants(q); + Node res = q[1].substitute( vars.begin(), vars.end(), skolems.begin(), skolems.end()); + res = res.notNode(); return res; } else if (id == ProofRule::INSTANTIATE) diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 18dbac2cc2d..e49cf647be1 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -64,17 +64,15 @@ TrustNode Skolemize::process(Node q) // if using proofs and not using induction, we use the justified // skolemization NodeManager* nm = NodeManager::currentNM(); - std::vector echildren(q.begin(), q.end()); - echildren[1] = echildren[1].notNode(); - Node existsq = nm->mkNode(Kind::EXISTS, echildren); - std::vector vars(existsq[0].begin(), existsq[0].end()); // cache the skolems in d_skolem_constants[q] std::vector& skolems = d_skolem_constants[q]; - skolems = getSkolemConstants(existsq); - Node res = existsq[1].substitute( + skolems = getSkolemConstants(q); + std::vector vars(q[0].begin(), q[0].end()); + Node res = q[1].substitute( vars.begin(), vars.end(), skolems.begin(), skolems.end()); Node qnot = q.notNode(); CDProof cdp(d_env); + res = res.notNode(); cdp.addStep(res, ProofRule::SKOLEMIZE, {qnot}, {}); std::shared_ptr pf = cdp.getProofFor(res); std::vector assumps; @@ -106,15 +104,7 @@ TrustNode Skolemize::process(Node q) std::vector Skolemize::getSkolemConstants(const Node& q) { - if (q.getKind()==Kind::FORALL) - { - std::vector echildren(q.begin(), q.end()); - echildren[1] = echildren[1].notNode(); - NodeManager* nm = NodeManager::currentNM(); - Node existsq = nm->mkNode(Kind::EXISTS, echildren); - return getSkolemConstants(existsq); - } - Assert(q.getKind() == Kind::EXISTS); + Assert(q.getKind() == Kind::FORALL); std::vector skolems; for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) { @@ -125,7 +115,7 @@ std::vector Skolemize::getSkolemConstants(const Node& q) Node Skolemize::getSkolemConstant(const Node& q, size_t i) { - Assert(q.getKind() == Kind::EXISTS); + Assert(q.getKind() == Kind::FORALL); Assert(i < q[0].getNumChildren()); NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager();