diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-23 19:33:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-24 00:33:18 +0000 |
| commit | 3b76dcf208986709fefbd0978982de3fe8ecc626 (patch) | |
| tree | d7dd101c4664ed59e9a268275eff14dfdebca094 /src/theory/arith/constraint.cpp | |
| parent | fe655f21e7cea33e9057c46fc8b2573314cbf302 (diff) | |
Uniform treatment of trusted theory inferences in proofs (#7044)
Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.
Diffstat (limited to 'src/theory/arith/constraint.cpp')
| -rw-r--r-- | src/theory/arith/constraint.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index d8fc1c578..03db36bb5 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -29,6 +29,7 @@ #include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" using namespace std; @@ -1820,9 +1821,11 @@ std::shared_ptr<ProofNode> Constraint::externalExplain( } case ArithProofType::IntHoleAP: { - pf = pnm->mkNode(PfRule::INT_TRUST, + Node t = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); + pf = pnm->mkNode(PfRule::THEORY_INFERENCE, children, - {getProofLiteral()}, + {getProofLiteral(), t}, getProofLiteral()); break; } |