This class is responsible for the connection between terms and their witness form in the final proof.
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
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);
* @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.
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";
THEORY_REWRITE,
//================================================= Processing rules
- // ======== Preprocess
+ // ======== Preprocess (trusted)
// Children: none
// Arguments: (F)
// ---------------------------------------------------------------
// 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)
--- /dev/null
+/********************* */
+/*! \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<ProofNode> 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<ProofNode> 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<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> 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<bool>();
+}
+
+const std::unordered_set<Node, NodeHashFunction>&
+WitnessFormGenerator::getWitnessFormEqs() const
+{
+ return d_eqs;
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 <unordered_set>
+
+#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<ProofNode> 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<Node, NodeHashFunction>& 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<TNode, TNodeHashFunction> d_visited;
+ /** The set of equalities added as proof steps */
+ std::unordered_set<Node, NodeHashFunction> d_eqs;
+ /** Lazy proof storing witness intro steps */
+ LazyCDProof d_wintroPf;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
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);
}
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);
projects / cvc5.git / commitdiff