diff options
Diffstat (limited to 'src/theory/bv/bv_eager_solver.cpp')
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index af35c0499..166d43e35 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -24,11 +24,12 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -EagerBitblastSolver::EagerBitblastSolver() +EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv) : d_assertionSet() , d_bitblaster(NULL) , d_aigBitblaster(NULL) , d_useAig(options::bitvectorAig()) + , d_bv(bv) {} EagerBitblastSolver::~EagerBitblastSolver() { @@ -53,7 +54,7 @@ void EagerBitblastSolver::initialize() { if (d_useAig) { d_aigBitblaster = new AigBitblaster(); } else { - d_bitblaster = new EagerBitblaster(); + d_bitblaster = new EagerBitblaster(d_bv); } } @@ -106,3 +107,8 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode> &formulas) { } return true; } + +void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { + AlwaysAssert(!d_useAig && d_bitblaster); + d_bitblaster->collectModelInfo(m, fullModel); +} |