diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/proof_node_updater.cpp | 8 | ||||
| -rw-r--r-- | src/expr/proof_node_updater.h | 10 |
2 files changed, 14 insertions, 4 deletions
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index af32c223d..16e339645 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -35,11 +35,13 @@ bool ProofNodeUpdaterCallback::update(Node res, ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb, - bool mergeSubproofs) + bool mergeSubproofs, + bool autoSym) : d_pnm(pnm), d_cb(cb), d_debugFreeAssumps(false), - d_mergeSubproofs(mergeSubproofs) + d_mergeSubproofs(mergeSubproofs), + d_autoSym(autoSym) { } @@ -183,7 +185,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, } PfRule id = cur->getRule(); // use CDProof to open a scope for which the callback updates - CDProof cpf(d_pnm); + CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); std::vector<Node> ccn; for (const std::shared_ptr<ProofNode>& cp : cc) diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 82c2ee068..9814c8166 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -80,10 +80,13 @@ class ProofNodeUpdater * @param cb The callback to apply to each node * @param mergeSubproofs Whether to automatically merge subproofs within * the same SCOPE that prove the same fact. + * @param autoSym Whether intermediate CDProof objects passed to updater + * callbacks automatically introduce SYMM steps. */ ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb, - bool mergeSubproofs = false); + bool mergeSubproofs = false, + bool autoSym = true); /** * Post-process, which performs the main post-processing technique described * above. @@ -142,6 +145,11 @@ class ProofNodeUpdater std::vector<Node> d_freeAssumps; /** Whether we are merging subproofs */ bool d_mergeSubproofs; + /** + * Whether intermediate CDProof objects passed to updater callbacks + * automatically introduce SYMM steps. + */ + bool d_autoSym; }; } // namespace CVC4 |