diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-04-02 12:48:44 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-04-02 12:48:44 -0700 |
commit | a917cc2ab4956b542b1f565abf0e62b197692f8d (patch) | |
tree | 7579ae2a631696fcfe750f8d29a56871af519185 /src/theory/bv/bitblast/eager_bitblaster.cpp | |
parent | 2d40d7ade3c66ba10a1f20ae5ab014aed8e2df01 (diff) |
Reorganize bitblaster code. (#1695)
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
Diffstat (limited to 'src/theory/bv/bitblast/eager_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 263 |
1 files changed, 263 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp new file mode 100644 index 000000000..d49c1f432 --- /dev/null +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -0,0 +1,263 @@ +/********************* */ +/*! \file eager_bitblaster.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief + ** + ** Bitblaster for the eager bv solver. + **/ + +#include "cvc4_private.h" + +#include "theory/bv/bitblast/eager_bitblaster.h" + +#include "options/bv_options.h" +#include "proof/bitvector_proof.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_factory.h" +#include "smt/smt_statistics_registry.h" +#include "theory/bv/theory_bv.h" +#include "theory/theory_model.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) + : TBitblaster<Node>(), + d_satSolver(), + d_bitblastingRegistrar(new BitblastingRegistrar(this)), + d_nullContext(new context::Context()), + d_cnfStream(), + d_bv(theory_bv), + d_bbAtoms(), + d_variables(), + d_notify() +{ + prop::SatSolver *solver = nullptr; + switch (options::bvSatSolver()) + { + case SAT_SOLVER_MINISAT: + { + prop::BVSatSolverInterface* minisat = + prop::SatSolverFactory::createMinisat( + d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster"); + d_notify.reset(new MinisatEmptyNotify()); + minisat->setNotify(d_notify.get()); + solver = minisat; + break; + } + case SAT_SOLVER_CADICAL: + solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), + "EagerBitblaster"); + break; + case SAT_SOLVER_CRYPTOMINISAT: + solver = prop::SatSolverFactory::createCryptoMinisat( + smtStatisticsRegistry(), "EagerBitblaster"); + break; + default: Unreachable("Unknown SAT solver type"); + } + d_satSolver.reset(solver); + d_cnfStream.reset( + new prop::TseitinCnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + options::proof(), + "EagerBitblaster")); +} + +EagerBitblaster::~EagerBitblaster() {} + +void EagerBitblaster::bbFormula(TNode node) { + d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, + TNode::null()); +} + +/** + * 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 + ? d_atomBBStrategies[normalized.getKind()](normalized, this) + : normalized; + + if (!options::proof()) + { + atom_bb = Rewriter::rewrite(atom_bb); + } + + // asserting that the atom is true iff the definition holds + Node atom_definition = + NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb); + + AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + storeBBAtom(node, atom_bb); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); +} + +void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { + if (d_bvp) { + d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); + } + d_bbAtoms.insert(atom); +} + +void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) { + if (d_bvp) { + d_bvp->registerTermBB(node.toExpr()); + } + d_termCache.insert(std::make_pair(node, bits)); +} + +bool EagerBitblaster::hasBBAtom(TNode atom) const { + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + +void EagerBitblaster::bbTerm(TNode node, Bits& bits) { + Assert(node.getType().isBitVector()); + + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + + d_bv->spendResource(options::bitblastStep()); + 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)); + } + d_variables.insert(var); +} + +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(); +} + +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return + */ +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); + for (int i = bits.size() - 1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert(bit_value != prop::SAT_VALUE_UNKNOWN); + } else { + if (!fullModel) return Node(); + // unconstrained bits default to false + bit_value = prop::SAT_VALUE_FALSE; + } + Integer bit_int = + bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(bits.size(), value); +} + +bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) +{ + TNodeSet::iterator it = d_variables.begin(); + for (; it != d_variables.end(); ++it) { + TNode var = *it; + if (d_bv->isLeaf(var) || isSharedTerm(var) || + (var.isVar() && var.getType().isBoolean())) { + // only shared terms could not have been bit-blasted + Assert(hasBBTerm(var) || isSharedTerm(var)); + + Node const_value = getModelFromSatSolver(var, true); + + if (const_value != Node()) { + Debug("bitvector-model") + << "EagerBitblaster::collectModelInfo (assert (= " << var << " " + << const_value << "))\n"; + if (!m->assertEquality(var, const_value, true)) + { + return false; + } + } + } + } + return true; +} + +void EagerBitblaster::setProofLog(BitVectorProof* bvp) { + d_bvp = bvp; + d_satSolver->setProofLog(bvp); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); +} + +bool EagerBitblaster::isSharedTerm(TNode node) { + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); +} + + +} // namespace bv +} // namespace theory +} // namespace CVC4 |