diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-04 16:00:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-04 16:00:24 -0500 |
| commit | 7f72cbde36a54cd661f2c8f784ecc6785f36211d (patch) | |
| tree | 30e9b2f07325d263fa6acdf60e286a7ed6a44319 /src/theory/bv/bv_quick_check.cpp | |
| parent | 9b61eff37935cd0fa29b4c8c59a9648e7621f753 (diff) | |
(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).
Diffstat (limited to 'src/theory/bv/bv_quick_check.cpp')
| -rw-r--r-- | src/theory/bv/bv_quick_check.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index f8e30247f..10fc8c4b7 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -140,9 +140,10 @@ void BVQuickCheck::popToZero() { } } -bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) +bool BVQuickCheck::collectModelValues(theory::TheoryModel* model, + const std::set<Node>& termSet) { - return d_bitblaster->collectModelInfo(model, fullModel); + return d_bitblaster->collectModelValues(model, termSet); } BVQuickCheck::~BVQuickCheck() { |