diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-09-29 09:39:11 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-29 11:39:11 -0500 |
| commit | 4b023ebf819e9d909d1542b79adc38fe1529a7fc (patch) | |
| tree | 5f7f1a733ab53271db4188f50fb64632c8d03c95 /src/theory/arith/theory_arith.cpp | |
| parent | 69e1472971f4aae9771630f911565a6f4548894b (diff) | |
(proof-new) Add proof managers and eager gens to arith (#5159)
This commit threads ProofNodeManager, EagerProofGenerator, etc
throughout the arith theory into the appropriate locations. These
objects are currently unused, but will be used in future commits.
Crediting Andy, since he set up some of this.
Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9324c94af..f16e0a297 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -205,6 +205,10 @@ std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit) std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase); return res; } +eq::ProofEqEngine* TheoryArith::getProofEqEngine() +{ + return d_inferenceManager.getProofEqEngine(); +} }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ |