diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 17:43:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 17:43:27 -0500 |
commit | 5ab00f919611cc5ca98e4fdee257d02098442412 (patch) | |
tree | 2d5478eb7decd18fea3f8db4e706052ce90120b3 /src/expr | |
parent | a529b43f0b081fd03c91cc8a02820786bacf03b4 (diff) | |
parent | 1cb249c9dd06a049953f001cd6d82c0e6f1246f2 (diff) |
Merge branch 'master' into nodeArrayStoreAll
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/proof_node_updater.cpp | 14 | ||||
-rw-r--r-- | src/expr/proof_rule.cpp | 2 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 17 |
3 files changed, 26 insertions, 7 deletions
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 227be2122..1e8fe4e7d 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -16,7 +16,6 @@ #include "expr/lazy_proof.h" - namespace CVC4 { ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} @@ -39,6 +38,7 @@ void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) do { cur = visit.back(); + visit.pop_back(); it = visited.find(cur); if (it == visited.end()) { @@ -67,12 +67,12 @@ void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) // then, update the original proof node based on this one d_pnm->updateNode(cur, npn.get()); } - const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); - // now, process children - for (const std::shared_ptr<ProofNode>& cp : ccp) - { - visit.push_back(cp.get()); - } + } + const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); + // now, process children + for (const std::shared_ptr<ProofNode>& cp : ccp) + { + visit.push_back(cp.get()); } } } while (!visit.empty()); diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index d00f1658b..08998e66e 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -31,8 +31,10 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; + case PfRule::PREPROCESS: return "PREPROCESS"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; + case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; case PfRule::AND_ELIM: return "AND_ELIM"; case PfRule::AND_INTRO: return "AND_INTRO"; case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index a15d8a2d2..87e8565ca 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -164,6 +164,16 @@ enum class PfRule : uint32_t // MACRO_SR_PRED_INTRO. MACRO_SR_PRED_TRANSFORM, + //================================================= Processing rules + // ======== Preprocess + // Children: none + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // where F is an equality of the form t = t' where t was replaced by t' + // based on some preprocessing pass, or otherwise F was added as a new + // assertion by some preprocessing pass. + PREPROCESS, //================================================= Boolean rules // ======== Split // Children: none @@ -171,6 +181,13 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (or F (not F)) SPLIT, + // ======== Equality resolution + // Children: (P1:F1, P2:(= F1 F2)) + // Arguments: none + // --------------------- + // Conclusion: (F2) + // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION. + EQ_RESOLVE, // ======== And elimination // Children: (P:(and F1 ... Fn)) // Arguments: (i) |