diff options
Diffstat (limited to 'src/theory/bv/eager_bitblaster.h')
-rw-r--r-- | src/theory/bv/eager_bitblaster.h | 163 |
1 files changed, 163 insertions, 0 deletions
diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.h new file mode 100644 index 000000000..da73c7f09 --- /dev/null +++ b/src/theory/bv/eager_bitblaster.h @@ -0,0 +1,163 @@ +/********************* */ +/*! \file eager_bitblaster.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): lianah + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief + ** + ** Bitblaster for the lazy bv solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EAGER__BITBLASTER_H +#define __CVC4__EAGER__BITBLASTER_H + + +#include "bitblaster_template.h" +#include "theory/theory_registrar.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_factory.h" +#include "theory/bv/options.h" + +namespace CVC4 { +namespace theory { +namespace bv { + + +class BitblastingRegistrar: public prop::Registrar { + EagerBitblaster* d_bitblaster; +public: + BitblastingRegistrar(EagerBitblaster* bb) + : d_bitblaster(bb) + {} + void preRegister(Node n) { + d_bitblaster->bbAtom(n); + }; + +};/* class Registrar */ + +EagerBitblaster::EagerBitblaster() + : TBitblaster<Node>() + , d_bbAtoms() +{ + 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); +} + +EagerBitblaster::~EagerBitblaster() { + delete d_cnfStream; + delete d_satSolver; + delete d_nullContext; + delete d_bitblastingRegistrar; +} + +void EagerBitblaster::bbFormula(TNode node) { + d_cnfStream->convertAndAssert(node, false, false); +} + +/** + * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver + * NOTE: duplicate clauses are not detected because of marker literal + * @param node the atom to be bitblasted + * + */ +void EagerBitblaster::bbAtom(TNode node) { + node = node.getKind() == kind::NOT? node[0] : node; + if (node.getKind() == kind::BITVECTOR_BITOF) + return; + if (hasBBAtom(node)) { + return; + } + + Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + + // the bitblasted definition of the atom + Node normalized = Rewriter::rewrite(node); + Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? + Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : + normalized; + // 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); + storeBBAtom(node, atom_definition); + d_cnfStream->convertAndAssert(atom_definition, false, false); +} + +void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { + // no need to store the definition for the lazy bit-blaster + d_bbAtoms.insert(atom); +} + +bool EagerBitblaster::hasBBAtom(TNode atom) const { + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + +void EagerBitblaster::bbTerm(TNode node, Bits& bits) { + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + + Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + + d_termBBStrategies[node.getKind()] (node, bits, this); + + Assert (bits.size() == utils::getSize(node)); + + storeBBTerm(node, bits); +} + +void EagerBitblaster::makeVariable(TNode var, Bits& bits) { + Assert(bits.size() == 0); + for (unsigned i = 0; i < utils::getSize(var); ++i) { + bits.push_back(utils::mkBitOf(var, i)); + } +} + +Node EagerBitblaster::getBBAtom(TNode node) const { + return node; +} + + +/** + * Calls the solve method for the Sat Solver. + * + * @return true for sat, and false for unsat + */ + +bool EagerBitblaster::solve() { + if (Trace.isOn("bitvector")) { + Trace("bitvector") << "EagerBitblaster::solve(). \n"; + } + Debug("bitvector") << "EagerBitblaster::solve(). \n"; + // TODO: clear some memory + // if (something) { + // NodeManager* nm= NodeManager::currentNM(); + // Rewriter::garbageCollect(); + // nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + // } + return prop::SAT_VALUE_TRUE == d_satSolver->solve(); +} + + +} /*bv namespace */ +} /* theory namespace */ +} /* CVC4 namespace*/ + + + +#endif |