(proof-new) Add proof managers and eager gens to arith (#5159)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 29 Sep 2020 16:39:11 +0000 (09:39 -0700)
committerGitHub <noreply@github.com>
Tue, 29 Sep 2020 16:39:11 +0000 (11:39 -0500)
commit4b023ebf819e9d909d1542b79adc38fe1529a7fc
tree5f7f1a733ab53271db4188f50fb64632c8d03c95
parent69e1472971f4aae9771630f911565a6f4548894b
(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
src/theory/arith/congruence_manager.cpp
src/theory/arith/congruence_manager.h
src/theory/arith/constraint.cpp
src/theory/arith/constraint.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h