diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-10-03 22:38:37 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-10-03 22:38:37 +0000 |
| commit | c7d04993e8d73105d091e0b732ddb63131b431a3 (patch) | |
| tree | 42c80ecf9990839349310d2baefbd1ab7c543c6d /src/theory/bv/theory_bv.cpp | |
| parent | b60ea598f9e45b6b82ea6085e786be394ac9f012 (diff) | |
implemented collectModelInfo for TheoryBV
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index aa5281d2f..51e09ee5a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -23,7 +23,7 @@ #include "theory/bv/bitblaster.h" #include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" - +#include "theory/model.h" using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; @@ -126,7 +126,11 @@ void TheoryBV::check(Effort e) } void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ - + Assert(!inConflict()); + Assert (fullModel); // can only query full model + d_equalitySolver.collectModelInfo(m); + d_bitblastSolver.collectModelInfo(m); + } void TheoryBV::propagate(Effort e) { |