From 61258d16bb812c5b5c8fb8dade1d2b497c69570b Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 19 Jun 2014 18:19:25 -0400 Subject: added model generation to eager bit-blasting and turned abc off by default --- src/theory/bv/bv_eager_solver.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src/theory/bv/bv_eager_solver.cpp') 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 &formulas) { } return true; } + +void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { + AlwaysAssert(!d_useAig && d_bitblaster); + d_bitblaster->collectModelInfo(m, fullModel); +} -- cgit v1.2.3