No longer takes a backwards reference to SmtEngine.
Also takes minor changes to proof post-processor from proof-new.
name = "none"
help = "do not check rule applications"
+[[option]]
+ name = "proofPpMerge"
+ category = "regular"
+ long = "proof-pp-merge"
+ type = "bool"
+ default = "true"
+ help = "merge subproofs in final proof post-processor"
+
[[option]]
name = "proofGranularityMode"
category = "regular"
namespace smt {
class DumpManager;
+class PfManager;
}
namespace theory {
class Env
{
friend class SmtEngine;
+ friend class smt::PfManager;
public:
/**
namespace cvc5 {
namespace smt {
-PfManager::PfManager(Env& env, SmtEngine* smte)
- : d_env(env),
+PfManager::PfManager(Env& env)
+ : EnvObj(env),
d_pchecker(new ProofChecker(
- d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER,
- d_env.getOptions().proof.proofPedantic)),
+ options().proof.proofCheck == options::ProofCheckMode::EAGER,
+ options().proof.proofPedantic)),
d_pnm(new ProofNodeManager(d_pchecker.get())),
d_pppg(new PreprocessProofGenerator(
d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
- d_pfpp(new ProofPostproccess(
- d_pnm.get(),
- smte,
- d_pppg.get(),
- // by default the post-processor will update all assumptions, which
- // can lead to SCOPE subproofs of the form
- // A
- // ...
- // B1 B2
- // ... ...
- // ------------
- // C
- // ------------- SCOPE [B1, B2]
- // B1 ^ B2 => C
- //
- // where A is an available assumption from outside the scope (note
- // that B1 was an assumption of this SCOPE subproof but since it could
- // be inferred from A, it was updated). This shape is problematic for
- // the veriT reconstruction, so we disable the update of scoped
- // assumptions (which would disable the update of B1 in this case).
- options::proofFormatMode() != options::ProofFormatMode::VERIT)),
+ d_pfpp(nullptr),
d_finalProof(nullptr)
{
+ // enable proof support in the environment/rewriter
+ d_env.setProofNodeManager(d_pnm.get());
+ // Now, initialize the proof postprocessor with the environment.
+ // By default the post-processor will update all assumptions, which
+ // can lead to SCOPE subproofs of the form
+ // A
+ // ...
+ // B1 B2
+ // ... ...
+ // ------------
+ // C
+ // ------------- SCOPE [B1, B2]
+ // B1 ^ B2 => C
+ //
+ // where A is an available assumption from outside the scope (note
+ // that B1 was an assumption of this SCOPE subproof but since it could
+ // be inferred from A, it was updated). This shape is problematic for
+ // the veriT reconstruction, so we disable the update of scoped
+ // assumptions (which would disable the update of B1 in this case).
+ d_pfpp.reset(new ProofPostproccess(
+ env,
+ d_pppg.get(),
+ nullptr,
+ options::proofFormatMode() != options::ProofFormatMode::VERIT));
+
// add rules to eliminate here
if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
{
// TODO (proj #37) according to the proof format, post process the proof node
// TODO (proj #37) according to the proof format, print the proof node
+ // according to the proof format, post process and print the proof node
if (options::proofFormatMode() == options::ProofFormatMode::DOT)
{
proof::DotPrinter dotPrinter;
}
else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
{
- out << "% SZS output start Proof for " << d_env.getOptions().driver.filename << std::endl;
+ out << "% SZS output start Proof for " << options().driver.filename
+ << std::endl;
// TODO (proj #37) print in TPTP compliant format
out << *fp << std::endl;
- out << "% SZS output end Proof for " << d_env.getOptions().driver.filename << std::endl;
+ out << "% SZS output end Proof for " << options().driver.filename
+ << std::endl;
}
else
{
+ // otherwise, print using default printer
out << "(proof\n";
out << *fp;
out << "\n)\n";
ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
+rewriter::RewriteDb* PfManager::getRewriteDatabase() const { return nullptr; }
+
smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
{
return d_pppg.get();
#include "context/cdhashmap.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
-class Env;
class ProofChecker;
class ProofNode;
class ProofNodeManager;
class SmtEngine;
+namespace rewriter {
+class RewriteDb;
+}
+
namespace smt {
class Assertions;
* - If SmtEngine has been configured in a way that is incompatible with proofs
* then unsat core production will be disabled.
*/
-class PfManager
+class PfManager : protected EnvObj
{
public:
- PfManager(Env& env, SmtEngine* smte);
+ PfManager(Env& env);
~PfManager();
/**
* Print the proof on the given output stream.
ProofChecker* getProofChecker() const;
/** Get a pointer to the ProofNodeManager owned by this. */
ProofNodeManager* getProofNodeManager() const;
+ /** Get the rewrite database, containing definitions of rewrites from DSL. */
+ rewriter::RewriteDb* getRewriteDatabase() const;
/** Get the proof generator for proofs of preprocessing. */
smt::PreprocessProofGenerator* getPreprocessProofGenerator() const;
//--------------------------- end access to utilities
*/
void getAssertions(Assertions& as,
std::vector<Node>& assertions);
- /** Reference to the env of SmtEngine */
- Env& d_env;
/** The false node */
Node d_false;
/** For the new proofs module */
std::unique_ptr<smt::PreprocessProofGenerator> d_pppg;
/** The proof post-processor */
std::unique_ptr<smt::ProofPostproccess> d_pfpp;
+
/**
* The final proof produced by the SMT engine.
* Combines the proofs of preprocessing, prop engine and theory engine, to be
#include "expr/skolem_manager.h"
#include "options/proof_options.h"
-#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "proof/proof_node_manager.h"
#include "smt/smt_engine.h"
+#include "theory/arith/arith_utilities.h"
#include "theory/builtin/proof_checker.h"
#include "theory/bv/bitblast/proof_bitblaster.h"
#include "theory/rewriter.h"
namespace cvc5 {
namespace smt {
-ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm,
- SmtEngine* smte,
+ProofPostprocessCallback::ProofPostprocessCallback(Env& env,
ProofGenerator* pppg,
+ rewriter::RewriteDb* rdb,
bool updateScopedAssumptions)
- : d_pnm(pnm),
- d_smte(smte),
+ : d_env(env),
+ d_pnm(env.getProofNodeManager()),
d_pppg(pppg),
- d_wfpm(pnm),
+ d_wfpm(env.getProofNodeManager()),
d_updateScopedAssumptions(updateScopedAssumptions)
{
d_true = NodeManager::currentNM()->mkConst(true);
{
// get the kind of rewrite
MethodId idr = MethodId::RW_REWRITE;
+ TheoryId theoryId = Theory::theoryOf(args[0]);
if (args.size() >= 2)
{
getMethodId(args[1], idr);
// rewrites from theory::Rewriter
bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
// use rewrite with proof interface
- Rewriter* rr = d_smte->getRewriter();
+ Rewriter* rr = d_env.getRewriter();
TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
std::shared_ptr<ProofNode> pfn = trn.toProofNode();
if (pfn == nullptr)
{
// update to THEORY_REWRITE with idr
Assert(args.size() >= 1);
- TheoryId theoryId = Theory::theoryOf(args[0].getType());
Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]});
}
}
else
{
- // don't know how to eliminate
- return Node::null();
+ // try to reconstruct as a standalone rewrite
+ std::vector<Node> targs;
+ targs.push_back(eq);
+ targs.push_back(
+ builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId));
+ // in this case, must be a non-standard rewrite kind
+ Assert(args.size() >= 2);
+ targs.push_back(args[1]);
+ Node eqp = expandMacros(PfRule::THEORY_REWRITE, {}, targs, cdp);
+ if (eqp.isNull())
+ {
+ // don't know how to eliminate
+ return Node::null();
+ }
}
if (args[0] == ret)
{
return true;
}
-ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
- SmtEngine* smte,
+ProofPostproccess::ProofPostproccess(Env& env,
ProofGenerator* pppg,
+ rewriter::RewriteDb* rdb,
bool updateScopedAssumptions)
- : d_pnm(pnm),
- d_cb(pnm, smte, pppg, updateScopedAssumptions),
+ : d_cb(env, pppg, rdb, updateScopedAssumptions),
// the update merges subproofs
- d_updater(d_pnm, d_cb, true),
- d_finalCb(pnm),
- d_finalizer(d_pnm, d_finalCb)
+ d_updater(env.getProofNodeManager(), d_cb, options::proofPpMerge()),
+ d_finalCb(env.getProofNodeManager()),
+ d_finalizer(env.getProofNodeManager(), d_finalCb)
{
}
namespace cvc5 {
-class SmtEngine;
+class Env;
+
+namespace rewriter {
+class RewriteDb;
+}
namespace smt {
class ProofPostprocessCallback : public ProofNodeUpdaterCallback
{
public:
- ProofPostprocessCallback(ProofNodeManager* pnm,
- SmtEngine* smte,
+ ProofPostprocessCallback(Env& env,
ProofGenerator* pppg,
+ rewriter::RewriteDb* rdb,
bool updateScopedAssumptions);
~ProofPostprocessCallback() {}
/**
private:
/** Common constants */
Node d_true;
- /** The proof node manager */
+ /** Reference to the env */
+ Env& d_env;
+ /** Pointer to the proof node manager */
ProofNodeManager* d_pnm;
- /** Pointer to the SmtEngine, which should have proofs enabled */
- SmtEngine* d_smte;
/** The preprocessing proof generator */
ProofGenerator* d_pppg;
/** The witness form proof generator */
{
public:
/**
- * @param pnm The proof node manager we are using
- * @param smte The SMT engine whose proofs are being post-processed
+ * @param env The environment we are using
* @param pppg The proof generator for pre-processing proofs
* @param updateScopedAssumptions Whether we post-process assumptions in
* scope. Since doing so is sound and only problematic depending on who is
* consuming the proof, it's true by default.
*/
- ProofPostproccess(ProofNodeManager* pnm,
- SmtEngine* smte,
+ ProofPostproccess(Env& env,
ProofGenerator* pppg,
+ rewriter::RewriteDb* rdb,
bool updateScopedAssumptions = true);
~ProofPostproccess();
/** post-process */
void setEliminateRule(PfRule rule);
private:
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** The post process callback */
ProofPostprocessCallback d_cb;
/**
SetDefaults sdefaults(d_isInternalSubsolver);
sdefaults.setDefaults(d_env->d_logic, getOptions());
- ProofNodeManager* pnm = nullptr;
if (d_env->getOptions().smt.produceProofs)
{
// ensure bound variable uses canonical bound variables
getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
// make the proof manager
- d_pfManager.reset(new PfManager(*d_env.get(), this));
+ d_pfManager.reset(new PfManager(*d_env.get()));
PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
// start the unsat core manager
d_ucManager.reset(new UnsatCoreManager());
- // use this proof node manager
- pnm = d_pfManager->getProofNodeManager();
- // enable proof support in the environment/rewriter
- d_env->setProofNodeManager(pnm);
// enable it in the assertions pipeline
d_asserts->setProofGenerator(pppg);
// enabled proofs in the preprocessor
projects / cvc5.git / commitdiff