projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 883298e) | patch
Standardization of Theory (#5181)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 3 Oct 2020 11:11:02 +0000 (06:11 -0500)
committerGitHub <noreply@github.com>
Sat, 3 Oct 2020 11:11:02 +0000 (06:11 -0500)
commitd972bd973320ed3b4c7a41ff6a16e76f754d7f58
treeed64dfeafcb698219cfeaaec302c06a728c651dftree
parent883298e4d5bf54b83125fc256601cdbb6c21ad03commit | diff
Standardization of Theory (#5181)

This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.
17 files changed:
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/fp/theory_fp.cpp diff | blob | history
src/theory/fp/theory_fp.h diff | blob | history
src/theory/model_manager_distributed.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/theory.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
test/unit/theory/theory_engine_white.h diff | blob | history