This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.
Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.
#include "expr/node_manager.h"
#include "options/smt_options.h"
#include "proof/proof_manager.h"
+#include "theory/builtin/proof_checker.h"
#include "theory/rewriter.h"
namespace CVC4 {
Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
d_numAssumptions++;
}
- if (!isInput && isProofEnabled())
+ if (isProofEnabled())
{
- // notice this is always called, regardless of whether pgen is nullptr
- d_pppg->notifyNewAssert(n, pgen);
+ if (!isInput)
+ {
+ // notice this is always called, regardless of whether pgen is nullptr
+ d_pppg->notifyNewAssert(n, pgen);
+ }
+ else
+ {
+ Trace("smt-pppg") << "...input assertion " << n << std::endl;
+ }
}
}
void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
{
+ if (n == d_nodes[i])
+ {
+ // no change, skip
+ return;
+ }
+ Trace("smt-pppg-repl") << "Replace " << d_nodes[i] << " with " << n
+ << std::endl;
if (options::unsatCores())
{
ProofManager::currentPM()->addDependence(n, d_nodes[i]);
replace(i, trn.getNode(), trn.getGenerator());
}
-void AssertionPipeline::replace(size_t i,
- Node n,
- const std::vector<Node>& addnDeps,
- ProofGenerator* pgen)
-{
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, d_nodes[i]);
- for (const auto& addnDep : addnDeps)
- {
- ProofManager::currentPM()->addDependence(n, addnDep);
- }
- }
- if (isProofEnabled())
- {
- d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
- }
- d_nodes[i] = n;
-}
-
void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
{
d_pppg = pppg;
d_storeSubstsInAsserts = false;
}
-void AssertionPipeline::addSubstitutionNode(Node n)
+void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
{
Assert(d_storeSubstsInAsserts);
Assert(n.getKind() == kind::EQUAL);
- d_nodes[d_substsIndex] = theory::Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex]));
- Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex])
- == d_nodes[d_substsIndex]);
+ conjoin(d_substsIndex, n, pg);
+}
+
+void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
+ Node newConjr = theory::Rewriter::rewrite(newConj);
+ if (newConjr == d_nodes[i])
+ {
+ // trivial, skip
+ return;
+ }
+ if (isProofEnabled())
+ {
+ // ---------- from pppg --------- from pg
+ // d_nodes[i] n
+ // -------------------------------- AND_INTRO
+ // d_nodes[i] ^ n
+ // -------------------------------- MACRO_SR_PRED_TRANSFORM
+ // rewrite( d_nodes[i] ^ n )
+ // allocate a fresh proof which will act as the proof generator
+ LazyCDProof* lcp = d_pppg->allocateHelperProof();
+ lcp->addLazyStep(d_nodes[i], d_pppg, false);
+ lcp->addLazyStep(
+ n, pg, false, "AssertionPipeline::conjoin", false, PfRule::PREPROCESS);
+ lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
+ if (newConjr != newConj)
+ {
+ lcp->addStep(
+ newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
+ }
+ // Notice we have constructed a proof of a new assertion, where d_pppg
+ // is referenced in the lazy proof above. If alternatively we had
+ // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
+ // have used notifyPreprocessed. However, it is simpler to make the
+ // above proof.
+ d_pppg->notifyNewAssert(newConjr, lcp);
+ }
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
+ }
+ d_nodes[i] = newConjr;
+ Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
}
} // namespace preprocessing
*/
void clear();
+ /** TODO (projects #75): remove this */
Node& operator[](size_t i) { return d_nodes[i]; }
+ /** Get the assertion at index i */
const Node& operator[](size_t i) const { return d_nodes[i]; }
/**
/** Same as above, with TrustNode */
void pushBackTrusted(theory::TrustNode trn);
+ /** TODO (projects #75): remove this */
std::vector<Node>& ref() { return d_nodes; }
+
+ /**
+ * Get the constant reference to the underlying assertions. It is only
+ * possible to modify these via the replace methods below.
+ */
const std::vector<Node>& ref() const { return d_nodes; }
std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
/** Same as above, with TrustNode */
void replaceTrusted(size_t i, theory::TrustNode trn);
- /*
- * Replaces assertion i with node n and records that this replacement depends
- * on assertion i and the nodes listed in addnDeps. The dependency
- * information is used for unsat cores and proofs.
- *
- * @param i The position of the assertion to replace.
- * @param n The replacement assertion.
- * @param addnDeps The dependencies.
- * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
- * where d_nodes[i] is the assertion at position i prior to this call.
- */
- void replace(size_t i,
- Node n,
- const std::vector<Node>& addnDeps,
- ProofGenerator* pg = nullptr);
-
IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
/**
* Adds a substitution node of the form (= lhs rhs) to the assertions.
+ * This conjoins n to assertions at a distinguished index given by
+ * d_substsIndex.
+ *
+ * @param n The substitution node
+ * @param pg The proof generator that can provide a proof of n.
+ */
+ void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr);
+
+ /**
+ * Conjoin n to the assertion vector at position i. This replaces
+ * d_nodes[i] with the rewritten form of (AND d_nodes[i] n).
+ *
+ * @param i The assertion to replace
+ * @param n The formula to conjoin at position i
+ * @param pg The proof generator that can provide a proof of n
*/
- void addSubstitutionNode(Node n);
+ void conjoin(size_t i, Node n, ProofGenerator* pg = nullptr);
/**
* Checks whether the assertion at a given index represents substitutions.
namespace CVC4 {
namespace smt {
-PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm)
- : d_pnm(pnm)
+PreprocessProofGenerator::PreprocessProofGenerator(context::UserContext* u,
+ ProofNodeManager* pnm)
+ : d_pnm(pnm), d_src(u), d_helperProofs(u)
{
}
void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
{
- Trace("smt-proof-pp-debug") << "- notifyNewAssert: " << n << std::endl;
- d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+ Trace("smt-proof-pp-debug")
+ << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
+ if (d_src.find(n) == d_src.end())
+ {
+ d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+ }
+ else
+ {
+ Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
+ }
}
void PreprocessProofGenerator::notifyPreprocessed(Node n,
if (n != np)
{
Trace("smt-proof-pp-debug")
- << "- notifyPreprocessed: " << n << "..." << np << std::endl;
- d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg);
+ << "PreprocessProofGenerator::notifyPreprocessed: " << n << "..." << np
+ << std::endl;
+ if (d_src.find(np) == d_src.end())
+ {
+ d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg);
+ }
+ else
+ {
+ Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
+ }
}
}
std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
{
- std::map<Node, theory::TrustNode>::iterator it = d_src.find(f);
+ NodeTrustNodeMap::iterator it = d_src.find(f);
if (it == d_src.end())
{
// could be an assumption, return nullptr
// make CDProof to construct the proof below
CDProof cdp(d_pnm);
+ Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: input " << f
+ << std::endl;
Node curr = f;
std::vector<Node> transChildren;
+ std::unordered_set<Node, NodeHashFunction> processed;
bool success;
+ // we connect the proof of f to its source via the map d_src until we
+ // discover that its source is a preprocessing lemma (a lemma stored in d_src)
+ // or otherwise it is assumed to be an input assumption.
do
{
success = false;
if (it != d_src.end())
{
- Assert(it->second.getNode() == curr);
+ Assert((*it).second.getNode() == curr);
+ // get the proven node
+ Node proven = (*it).second.getProven();
+ Assert(!proven.isNull());
+ Trace("smt-pppg") << "...process proven " << proven << std::endl;
+ if (processed.find(proven) != processed.end())
+ {
+ Unhandled() << "Cyclic steps in preprocess proof generator";
+ continue;
+ }
+ processed.insert(proven);
bool proofStepProcessed = false;
- std::shared_ptr<ProofNode> pfr = it->second.toProofNode();
+
+ // if a generator for the step was provided, it is stored in the proof
+ Trace("smt-pppg") << "...get provided proof" << std::endl;
+ std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
if (pfr != nullptr)
{
- Assert(pfr->getResult() == it->second.getProven());
+ Trace("smt-pppg") << "...add provided" << std::endl;
+ Assert(pfr->getResult() == proven);
cdp.addProof(pfr);
proofStepProcessed = true;
}
- if (it->second.getKind() == theory::TrustNodeKind::REWRITE)
+ Trace("smt-pppg") << "...update" << std::endl;
+ theory::TrustNodeKind tnk = (*it).second.getKind();
+ if (tnk == theory::TrustNodeKind::REWRITE)
{
- Node eq = it->second.getProven();
- Assert(eq.getKind() == kind::EQUAL);
+ Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
+ Assert(proven.getKind() == kind::EQUAL);
if (!proofStepProcessed)
{
// maybe its just a simple rewrite?
- if (eq[1] == theory::Rewriter::rewrite(eq[0]))
+ if (proven[1] == theory::Rewriter::rewrite(proven[0]))
{
- cdp.addStep(eq, PfRule::REWRITE, {}, {eq[0]});
+ cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
proofStepProcessed = true;
}
}
- transChildren.push_back(eq);
+ transChildren.push_back(proven);
// continue with source
- curr = eq[0];
+ curr = proven[0];
success = true;
// find the next node
it = d_src.find(curr);
}
else
{
- Assert(it->second.getKind() == theory::TrustNodeKind::LEMMA);
+ Trace("smt-pppg") << "...lemma" << std::endl;
+ Assert(tnk == theory::TrustNodeKind::LEMMA);
}
if (!proofStepProcessed)
{
- // add trusted step
- Node proven = it->second.getProven();
- cdp.addStep(proven, PfRule::PREPROCESS, {}, {proven});
+ Trace("smt-pppg") << "...add missing step" << std::endl;
+ // add trusted step, the rule depends on the kind of trust node
+ cdp.addStep(proven,
+ tnk == theory::TrustNodeKind::LEMMA
+ ? PfRule::PREPROCESS_LEMMA
+ : PfRule::PREPROCESS,
+ {},
+ {proven});
}
}
} while (success);
- Assert(curr != f);
- // prove ( curr == f )
- Node fullRewrite = curr.eqNode(f);
- if (transChildren.size() >= 2)
+ // prove ( curr == f ), which is not necessary if they are the same
+ // modulo symmetry.
+ if (!CDProof::isSame(f, curr))
{
- cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
+ Node fullRewrite = curr.eqNode(f);
+ if (transChildren.size() >= 2)
+ {
+ Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
+ std::reverse(transChildren.begin(), transChildren.end());
+ cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
+ }
+ Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
+ // prove f
+ cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
+ Trace("smt-pppg") << "...finished" << std::endl;
}
- // prove f
- cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
// overall, proof is:
// --------- from proof generator ---------- from proof generator
return cdp.getProofFor(f);
}
+ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
+
+LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
+{
+ std::shared_ptr<LazyCDProof> helperPf = std::make_shared<LazyCDProof>(d_pnm);
+ d_helperProofs.push_back(helperPf);
+ return helperPf.get();
+}
+
std::string PreprocessProofGenerator::identify() const
{
return "PreprocessProofGenerator";
#include <map>
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/lazy_proof.h"
#include "expr/proof_generator.h"
#include "expr/proof_node_manager.h"
+#include "theory/eager_proof_generator.h"
#include "theory/trust_node.h"
namespace CVC4 {
*/
class PreprocessProofGenerator : public ProofGenerator
{
+ typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction>
+ NodeTrustNodeMap;
+
public:
- PreprocessProofGenerator(ProofNodeManager* pnm);
+ PreprocessProofGenerator(context::UserContext* u, ProofNodeManager* pnm);
~PreprocessProofGenerator() {}
/**
* Notify that n is a new assertion, where pg can provide a proof of n.
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/** Identify */
std::string identify() const override;
+ /** Get the proof manager */
+ ProofNodeManager* getManager();
+ /**
+ * Allocate a helper proof. This returns a fresh lazy proof object that
+ * remains alive in this user context. This feature is used to construct
+ * helper proofs for preprocessing, e.g. to support the skeleton of proofs
+ * that connect AssertionPipeline::conjoin steps.
+ *
+ * Internally, this adds a LazyCDProof to the list d_helperProofs below.
+ */
+ LazyCDProof* allocateHelperProof();
private:
/** The proof node manager */
* (1) A trust node REWRITE proving (n_src = n) for some n_src, or
* (2) A trust node LEMMA proving n.
*/
- std::map<Node, theory::TrustNode> d_src;
+ NodeTrustNodeMap d_src;
+ /** A context-dependent list of LazyCDProof, allocated for conjoin steps */
+ context::CDList<std::shared_ptr<LazyCDProof> > d_helperProofs;
};
} // namespace smt
namespace CVC4 {
namespace smt {
-PfManager::PfManager(SmtEngine* smte)
+PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
: d_pchecker(new ProofChecker(options::proofNewPedantic())),
d_pnm(new ProofNodeManager(d_pchecker.get())),
- d_pppg(new PreprocessProofGenerator(d_pnm.get())),
+ d_pppg(new PreprocessProofGenerator(u, d_pnm.get())),
d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
d_finalProof(nullptr)
{
class PfManager
{
public:
- PfManager(SmtEngine* smte);
+ PfManager(context::UserContext* u, SmtEngine* smte);
~PfManager();
/**
* Print the proof on the output channel of the current options in scope.
ProofNodeManager* pnm = nullptr;
if (options::proofNew())
{
- d_pfManager.reset(new PfManager(this));
+ d_pfManager.reset(new PfManager(getUserContext(), this));
// use this proof node manager
pnm = d_pfManager->getProofNodeManager();
// enable proof support in the rewriter
bool TrustNode::isNull() const { return d_proven.isNull(); }
-std::shared_ptr<ProofNode> TrustNode::toProofNode()
+std::shared_ptr<ProofNode> TrustNode::toProofNode() const
{
if (d_gen == nullptr)
{
* Gets the proof node for this trust node, which is obtained by
* calling the generator's getProofFor method on the proven node.
*/
- std::shared_ptr<ProofNode> toProofNode();
+ std::shared_ptr<ProofNode> toProofNode() const;
/** Get the proven formula corresponding to a conflict call */
static Node getConflictProven(Node conf);
projects / cvc5.git / commitdiff