diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-13 19:50:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-13 19:50:19 -0500 |
| commit | 53b3cf646549200e4986a47872abf6121fcbfe5b (patch) | |
| tree | e33a7b9a1140c9196733b0917e18a8e8524d4683 /src/theory/builtin | |
| parent | 0fdf29ba194b8f6763ae41bea05b3208345d89b9 (diff) | |
(proof-new) Simplifications for proof rule checker interface (#5244)
Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.
This also updates STRING_TRUST to have pedantic level 2.
Diffstat (limited to 'src/theory/builtin')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 1a30f4449..8824859d4 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -201,6 +201,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, const std::vector<Node>& children, const std::vector<Node>& args) { + NodeManager * nm = NodeManager::currentNM(); // compute what was proven if (id == PfRule::ASSUME) { @@ -217,7 +218,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, // no antecedant return children[0]; } - Node ant = mkAnd(args); + Node ant = nm->mkAnd(args); // if the conclusion is false, its the negated antencedant only if (children[0].isConst() && !children[0].getConst<bool>()) { |