(new theory) Update TheoryBV to new standard for collectModelValues (#5025)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 4 Sep 2020 21:00:24 +0000 (16:00 -0500)
committerGitHub <noreply@github.com>
Fri, 4 Sep 2020 21:00:24 +0000 (16:00 -0500)
commit7f72cbde36a54cd661f2c8f784ecc6785f36211d
tree30e9b2f07325d263fa6acdf60e286a7ed6a44319
parent9b61eff37935cd0fa29b4c8c59a9648e7621f753
(new theory) Update TheoryBV to new standard for collectModelValues (#5025)

This makes collectModelValues the main model interface in BV instead of collectModelInfo. BV is no longer responsible for asserting its equality engine or computing relevant/asserted terms.

This involved updating the interface on many subsolvers of BvSolverLazy. This includes moving the responsibility of addSharedTerm (regarding trigger terms) from the subsolvers to TheoryBV, this eventually will be automatically handled in Theory once all theories are migrated to the new standard.

This ensures that TheoryBV is updated to the new standard (check was already migrated on c9e23f6).
18 files changed:
src/theory/bv/bitblast/lazy_bitblaster.cpp
src/theory/bv/bitblast/lazy_bitblaster.h
src/theory/bv/bv_quick_check.cpp
src/theory/bv/bv_quick_check.h
src/theory/bv/bv_solver.h
src/theory/bv/bv_solver_lazy.cpp
src/theory/bv/bv_solver_lazy.h
src/theory/bv/bv_subtheory.h
src/theory/bv/bv_subtheory_algebraic.cpp
src/theory/bv/bv_subtheory_algebraic.h
src/theory/bv/bv_subtheory_bitblast.cpp
src/theory/bv/bv_subtheory_bitblast.h
src/theory/bv/bv_subtheory_core.cpp
src/theory/bv/bv_subtheory_core.h
src/theory/bv/bv_subtheory_inequality.cpp
src/theory/bv/bv_subtheory_inequality.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h