projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f5e2348) | patch
(proof-new) Split operator elimination from arithmetic (#4581)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 19 Jun 2020 20:18:24 +0000 (15:18 -0500)
committerGitHub <noreply@github.com>
Fri, 19 Jun 2020 20:18:24 +0000 (15:18 -0500)
commite0633c091c37b79f9e3a2517cf95113c788db083
tree8e7155ceb28d5b8cfeb6aa5c53ecd8b33cd12cc2tree
parentf5e2348c7350ce21716f595eb8703635782c6285commit | diff
(proof-new) Split operator elimination from arithmetic (#4581)

This class will be undergoing further refactoring for the sake of proofs.

This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.
src/CMakeLists.txt diff | blob | history
src/theory/arith/operator_elim.cpp [new file with mode: 0644] blob
src/theory/arith/operator_elim.h [new file with mode: 0644] blob
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.h diff | blob | history