summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/assertion_pipeline.cpp92
-rw-r--r--src/preprocessing/assertion_pipeline.h41
-rw-r--r--src/smt/preprocess_proof_generator.cpp117
-rw-r--r--src/smt/preprocess_proof_generator.h24
-rw-r--r--src/smt/proof_manager.cpp4
-rw-r--r--src/smt/proof_manager.h2
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/trust_node.cpp2
-rw-r--r--src/theory/trust_node.h2
9 files changed, 205 insertions, 81 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 99e22b28f..cd92e5f3d 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -18,6 +18,7 @@
#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 {
@@ -61,10 +62,17 @@ void AssertionPipeline::push_back(Node n,
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;
+ }
}
}
@@ -77,6 +85,13 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
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]);
@@ -94,26 +109,6 @@ void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
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;
@@ -133,14 +128,55 @@ void AssertionPipeline::disableStoreSubstsInAsserts()
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
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 63e2bdd2a..6ca430ac4 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -49,7 +49,9 @@ class AssertionPipeline
*/
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]; }
/**
@@ -70,7 +72,13 @@ class AssertionPipeline
/** 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(); }
@@ -89,22 +97,6 @@ class AssertionPipeline
/** 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; }
@@ -136,8 +128,23 @@ class AssertionPipeline
/**
* 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.
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 5c7ed0356..1739a4e7d 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -21,15 +21,24 @@
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,
@@ -40,14 +49,22 @@ 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
@@ -56,67 +73,102 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
// 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
@@ -130,6 +182,15 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
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";
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 5319071f0..b71187188 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -19,8 +19,12 @@
#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 {
@@ -41,8 +45,11 @@ namespace smt {
*/
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.
@@ -61,6 +68,17 @@ class PreprocessProofGenerator : public ProofGenerator
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 */
@@ -72,7 +90,9 @@ class PreprocessProofGenerator : public ProofGenerator
* (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
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index f51a116b7..df7b6bf4d 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -22,10 +22,10 @@
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)
{
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index bda741a05..118b82bec 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -41,7 +41,7 @@ class Assertions;
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.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3caf03946..755822d2a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -270,7 +270,7 @@ void SmtEngine::finishInit()
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
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index fe66fc3cb..b0c8f3b79 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -101,7 +101,7 @@ ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
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)
{
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index 0e0bfddf5..a0586bd0c 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -132,7 +132,7 @@ class TrustNode
* 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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback