diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-01-19 14:25:02 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-19 16:25:02 -0600 |
| commit | 3c754308f66d92cd4b03d5f159464585c315b528 (patch) | |
| tree | 5dccdb0cad66968888b30b652c89ee45a1ac9979 /src/theory/arith/theory_arith.h | |
| parent | de79f1ad325036ca90be9144a74606310b5dab9b (diff) | |
Implement proofs for arith BRAB lemmas (#5784)
All changes:
Add a Pf type alias for std::shared_ptr to
expr/proof_rule.h
Add an eager proof generator to TheoryArith for preprocessing
rewrites. Right now those are proven with INT_TRUST. Will eventually
fix.
Generate proved lemmas in TheoryArithPrivate::branchIntegerVariable.
Same for TheoryArithPrivate::roundRobinBranch
Add EagerProofGenerator::mkTrustedRewrite.
Add some proofsEnabled methods.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
| -rw-r--r-- | src/theory/arith/theory_arith.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e26ff51ef..eba84e339 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -45,6 +45,9 @@ class TheoryArith : public Theory { TimerStat d_ppRewriteTimer; + /** Used to prove pp-rewrites */ + EagerProofGenerator d_ppPfGen; + public: TheoryArith(context::Context* c, context::UserContext* u, @@ -152,6 +155,7 @@ class TheoryArith : public Theory { ArithPreprocess d_arithPreproc; /** The theory rewriter for this theory. */ ArithRewriter d_rewriter; + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ |