diff options
Diffstat (limited to 'src/theory/bv/eager_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 3f076bd4c..ec2bfd9c0 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -9,27 +9,31 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief + ** \brief ** - ** Bitblaster for the eager bv solver. + ** Bitblaster for the eager bv solver. **/ #include "cvc4_private.h" -#include "theory/bv/bitblaster_template.h" -#include "theory/bv/options.h" -#include "theory/theory_model.h" -#include "theory/bv/theory_bv.h" +#include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/theory_bv.h" +#include "theory/theory_model.h" using namespace CVC4; using namespace CVC4::theory; -using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv; + +namespace CVC4 { +namespace theory { +namespace bv { void BitblastingRegistrar::preRegister(Node n) { - d_bitblaster->bbAtom(n); + d_bitblaster->bbAtom(n); }; EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) @@ -38,12 +42,12 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) , d_bbAtoms() , d_variables() { - d_bitblastingRegistrar = new BitblastingRegistrar(this); + d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); - + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); } @@ -68,7 +72,7 @@ void EagerBitblaster::bbFormula(TNode node) { void EagerBitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT? node[0] : node; if (node.getKind() == kind::BITVECTOR_BITOF) - return; + return; if (hasBBAtom(node)) { return; } @@ -83,18 +87,18 @@ void EagerBitblaster::bbAtom(TNode node) { // asserting that the atom is true iff the definition holds Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); - AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); storeBBAtom(node, atom_definition); d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); } void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { // no need to store the definition for the lazy bit-blaster - d_bbAtoms.insert(atom); + d_bbAtoms.insert(atom); } bool EagerBitblaster::hasBBAtom(TNode atom) const { - return d_bbAtoms.find(atom) != d_bbAtoms.end(); + return d_bbAtoms.find(atom) != d_bbAtoms.end(); } void EagerBitblaster::bbTerm(TNode node, Bits& bits) { @@ -161,7 +165,7 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { if (!hasBBTerm(a)) { return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); } - + Bits bits; getBBTerm(a, bits); Integer value(0); @@ -191,9 +195,9 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { (var.isVar() && var.getType().isBoolean())) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - + Node const_value = getModelFromSatSolver(var, fullModel); - + if(const_value != Node()) { Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " << var << " " @@ -207,3 +211,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { bool EagerBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } + +} /* namespace CVC4::theory::bv; */ +} /* namespace CVC4::theory; */ +} /* namespace CVC4; */ |