diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-30 08:20:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-30 08:20:03 -0500 |
| commit | 0cf0dc3b3661e668f8c03113faad5078d91cea98 (patch) | |
| tree | 78bd8ec763638e662d1f945d82f26607d2472793 /src/expr/proof_node_manager.cpp | |
| parent | f51491e43e86abb862ea081568b8aa106293d64a (diff) | |
(proof-new) Add the term conversion sequence generator (#5097)
This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.
Diffstat (limited to 'src/expr/proof_node_manager.cpp')
| -rw-r--r-- | src/expr/proof_node_manager.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index eb298cc83..9f60a49e4 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -56,6 +56,18 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact) return mkNode(PfRule::ASSUME, {}, {fact}, fact); } +std::shared_ptr<ProofNode> ProofNodeManager::mkTrans( + const std::vector<std::shared_ptr<ProofNode>>& children, Node expected) +{ + Assert(!children.empty()); + if (children.size() == 1) + { + Assert(expected.isNull() || children[0]->getResult() == expected); + return children[0]; + } + return mkNode(PfRule::TRANS, children, {}, expected); +} + std::shared_ptr<ProofNode> ProofNodeManager::mkScope( std::shared_ptr<ProofNode> pf, std::vector<Node>& assumps, |