From 9d1ce085de6df543d9d9a2fa9b8fa9001feb4b6b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Aug 2020 11:41:26 -0500 Subject: [PATCH] (proof-new) Witness form proof generator (#4782) This class is responsible for the connection between terms and their witness form in the final proof. --- src/CMakeLists.txt | 2 + src/expr/lazy_proof.cpp | 19 +++- src/expr/lazy_proof.h | 7 +- src/expr/proof_rule.cpp | 1 + src/expr/proof_rule.h | 10 ++- src/smt/witness_form.cpp | 128 +++++++++++++++++++++++++++ src/smt/witness_form.h | 97 ++++++++++++++++++++ src/theory/builtin/proof_checker.cpp | 3 +- 8 files changed, 262 insertions(+), 5 deletions(-) create mode 100644 src/smt/witness_form.cpp create mode 100644 src/smt/witness_form.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d19719b6d..2a5639e9e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -272,6 +272,8 @@ libcvc4_add_sources( smt/term_formula_removal.cpp smt/term_formula_removal.h smt/update_ostream.h + smt/witness_form.cpp + smt/witness_form.h smt_util/boolean_simplification.cpp smt_util/boolean_simplification.h smt_util/nary_builder.cpp diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 3980a3cb3..df0258af7 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -109,9 +109,24 @@ std::shared_ptr LazyCDProof::getProofFor(Node fact) void LazyCDProof::addLazyStep(Node expected, ProofGenerator* pg, - bool forceOverwrite) + bool forceOverwrite, + PfRule idNull) { - Assert(pg != nullptr); + if (pg == nullptr) + { + // null generator, should have given a proof rule + if (idNull == PfRule::ASSUME) + { + Assert(false); + return; + } + Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected + << " set (trusted) step " << idNull << "\n"; + addStep(expected, idNull, {}, {expected}); + return; + } + Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected + << " set to generator " << pg->identify() << "\n"; if (!forceOverwrite) { NodeProofGeneratorMap::const_iterator it = d_gens.find(expected); diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index c802de39e..1f68a3ccb 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -69,10 +69,15 @@ class LazyCDProof : public CDProof * @param forceOverwrite If this flag is true, then this call overwrites * an existing proof generator provided for expected, if one was provided * via a previous call to addLazyStep in the current context. + * @param trustId If a null proof generator is provided, we add a step to + * the proof that has trustId as the rule and expected as the sole argument. + * We do this only if trustId is not PfRule::ASSUME. This is primarily used + * for identifying the kind of hole when a proof generator is not given. */ void addLazyStep(Node expected, ProofGenerator* pg, - bool forceOverwrite = false); + bool forceOverwrite = false, + PfRule trustId = PfRule::ASSUME); /** * Does this have any proof generators? This method always returns true * if the default is non-null. diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 7844dfccb..9713adbec 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -33,6 +33,7 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; case PfRule::PREPROCESS: return "PREPROCESS"; + case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 62bc77cfb..3d468d08e 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -174,7 +174,7 @@ enum class PfRule : uint32_t THEORY_REWRITE, //================================================= Processing rules - // ======== Preprocess + // ======== Preprocess (trusted) // Children: none // Arguments: (F) // --------------------------------------------------------------- @@ -183,6 +183,14 @@ enum class PfRule : uint32_t // based on some preprocessing pass, or otherwise F was added as a new // assertion by some preprocessing pass. PREPROCESS, + // ======== Witness axiom (trusted) + // Children: none + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // where F is an existential (exists ((x T)) (P x)) used for introducing + // a witness term (witness ((x T)) (P x)). + WITNESS_AXIOM, // ======== Remove Term Formulas Axiom // Children: none // Arguments: (t) diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp new file mode 100644 index 000000000..891c0f731 --- /dev/null +++ b/src/smt/witness_form.cpp @@ -0,0 +1,128 @@ +/********************* */ +/*! \file witness_form.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The module for managing witness form conversion in proofs + **/ + +#include "smt/witness_form.h" + +#include "expr/skolem_manager.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace smt { + +WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) + : d_tcpg(pnm), d_wintroPf(pnm) +{ +} + +std::shared_ptr WitnessFormGenerator::getProofFor(Node eq) +{ + if (eq.getKind() != kind::EQUAL) + { + // expecting an equality + return nullptr; + } + Node lhs = eq[0]; + Node rhs = convertToWitnessForm(eq[0]); + if (rhs != eq[1]) + { + // expecting witness form + return nullptr; + } + std::shared_ptr pn = d_tcpg.getProofFor(eq); + Assert(pn != nullptr); + return pn; +} + +std::string WitnessFormGenerator::identify() const +{ + return "WitnessFormGenerator"; +} + +Node WitnessFormGenerator::convertToWitnessForm(Node t) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* skm = nm->getSkolemManager(); + Node tw = SkolemManager::getWitnessForm(t); + if (t == tw) + { + // trivial case + return tw; + } + std::unordered_set::iterator it; + std::vector visit; + TNode cur; + TNode curw; + visit.push_back(t); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_visited.find(cur); + if (it == d_visited.end()) + { + d_visited.insert(cur); + curw = SkolemManager::getWitnessForm(cur); + // if its witness form is different + if (cur != curw) + { + if (cur.isVar()) + { + Node eq = cur.eqNode(curw); + // equality between a variable and its witness form + d_eqs.insert(eq); + Assert(curw.getKind() == kind::WITNESS); + Node skBody = SkolemManager::getSkolemForm(curw[1]); + Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody); + ProofGenerator* pg = skm->getProofGenerator(exists); + // --------------------------- from pg + // (exists ((x T)) (P x)) + // --------------------------- WITNESS_INTRO + // k = (witness ((x T)) (P x)) + d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM); + d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); + d_tcpg.addRewriteStep(cur, curw, &d_wintroPf); + } + else + { + // A term whose witness form is different from itself, recurse. + // It should be the case that cur has children, since the witness + // form of constants are themselves. + Assert(cur.getNumChildren() > 0); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + } + } while (!visit.empty()); + return tw; +} + +bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const +{ + return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s); +} + +bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const +{ + Node tr = theory::Rewriter::rewrite(t); + return !tr.isConst() || !tr.getConst(); +} + +const std::unordered_set& +WitnessFormGenerator::getWitnessFormEqs() const +{ + return d_eqs; +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h new file mode 100644 index 000000000..10e4bd07b --- /dev/null +++ b/src/smt/witness_form.h @@ -0,0 +1,97 @@ +/********************* */ +/*! \file witness_form.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The module for managing witness form conversion in proofs + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__WITNESS_FORM_H +#define CVC4__SMT__WITNESS_FORM_H + +#include + +#include "expr/node_manager.h" +#include "expr/proof.h" +#include "expr/proof_generator.h" +#include "expr/term_conversion_proof_generator.h" + +namespace CVC4 { +namespace smt { + +/** + * The witness form proof generator, which acts as a wrapper around a + * TConvProofGenerator for adding rewrite steps for witness introduction. + * + * The proof steps managed by this class are stored in a context-independent + * manager, which matches how witness forms are managed in SkolemManager. + */ +class WitnessFormGenerator : public ProofGenerator +{ + public: + WitnessFormGenerator(ProofNodeManager* pnm); + ~WitnessFormGenerator() {} + /** + * Get proof for, which expects an equality of the form t = toWitness(t). + * This returns a proof based on the term conversion proof generator utility. + * This proof may contain open assumptions of the form: + * k = toWitness(k) + * Each of these assumptions are included in the set getWitnessFormEqs() + * below after returning this call. + */ + std::shared_ptr getProofFor(Node eq) override; + /** Identify */ + std::string identify() const override; + /** + * Does the rewrite require witness form conversion? + * When calling this method, it should be the case that: + * Rewriter::rewrite(toWitness(t)) == Rewriter::rewrite(toWitness(s)) + * The rule MACRO_SR_PRED_TRANSFORM concludes t == s if the above holds. + * This method returns false if: + * Rewriter::rewrite(t) == Rewriter::rewrite(s) + * which means that the proof of the above fact does not need to do + * witness form conversion to prove conclusions of MACRO_SR_PRED_TRANSFORM. + */ + bool requiresWitnessFormTransform(Node t, Node s) const; + /** + * Same as above, with s = true. This is intended for use with + * MACRO_SR_PRED_INTRO. + */ + bool requiresWitnessFormIntro(Node t) const; + /** + * Get witness form equalities. This returns a set of equalities of the form: + * k = toWitness(k) + * where k is a skolem, containing all rewrite steps used in calls to + * getProofFor during the entire lifetime of this generator. + */ + const std::unordered_set& getWitnessFormEqs() const; + + private: + /** + * Convert to witness form. This internally constructs rewrite steps that + * suffice to show t = toWitness(t) using the term conversion proof generator + * of this class (d_tcpg). + */ + Node convertToWitnessForm(Node t); + /** The term conversion proof generator */ + TConvProofGenerator d_tcpg; + /** The nodes we have already added rewrite steps for in d_tcpg */ + std::unordered_set d_visited; + /** The set of equalities added as proof steps */ + std::unordered_set d_eqs; + /** Lazy proof storing witness intro steps */ + LazyCDProof d_wintroPf; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 817d21fdf..05c17dedf 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -62,6 +62,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); pc->registerChecker(PfRule::THEORY_REWRITE, this); pc->registerChecker(PfRule::PREPROCESS, this); + pc->registerChecker(PfRule::WITNESS_AXIOM, this); pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); } @@ -329,7 +330,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args.size() == 1); return RemoveTermFormulas::getAxiomFor(args[0]); } - else if (id == PfRule::PREPROCESS) + else if (id == PfRule::PREPROCESS || id == PfRule::WITNESS_AXIOM) { Assert(children.empty()); Assert(args.size() == 1); -- 2.30.2