diff options
Diffstat (limited to 'src/theory/bv/bitblaster.cpp')
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 505 |
1 files changed, 0 insertions, 505 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp deleted file mode 100644 index 552f3b448..000000000 --- a/src/theory/bv/bitblaster.cpp +++ /dev/null @@ -1,505 +0,0 @@ -/********************* */ -/*! \file bitblaster.cpp - ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Dejan Jovanovic, Andrew Reynolds - ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Morgan Deters - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** - **/ - -#include "bitblaster.h" -#include "theory_bv_utils.h" -#include "theory/rewriter.h" -#include "prop/cnf_stream.h" -#include "prop/sat_solver.h" -#include "prop/sat_solver_factory.h" -#include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/bv/theory_bv.h" -#include "theory/bv/options.h" -#include "theory/theory_model.h" - -using namespace std; - -using namespace CVC4::theory::bv::utils; -using namespace CVC4::context; -using namespace CVC4::prop; - -namespace CVC4 { -namespace theory { -namespace bv{ - -std::string toString(Bits& bits) { - ostringstream os; - for (int i = bits.size() - 1; i >= 0; --i) { - TNode bit = bits[i]; - if (bit.getKind() == kind::CONST_BOOLEAN) { - os << (bit.getConst<bool>() ? "1" : "0"); - } else { - os << bit<< " "; - } - } - os <<"\n"; - - return os.str(); -} -/////// Bitblaster - -Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : - d_bv(bv), - d_bvOutput(bv->d_out), - d_termCache(), - d_bitblastedAtoms(), - d_assertedAtoms(c), - d_statistics() - { - d_satSolver = prop::SatSolverFactory::createMinisat(c); - d_nullRegistrar = new NullRegistrar(); - d_nullContext = new Context(); - d_cnfStream = new TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext); - - d_notify = new MinisatNotify(d_cnfStream, bv); - d_satSolver->setNotify(d_notify); - // initializing the bit-blasting strategies - initAtomBBStrategies(); - initTermBBStrategies(); - } - -Bitblaster::~Bitblaster() { - delete d_cnfStream; - delete d_nullContext; - delete d_nullRegistrar; - delete d_satSolver; - delete d_notify; -} - - -/** - * 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 Bitblaster::bbAtom(TNode node) { - node = node.getKind() == kind::NOT? node[0] : node; - - if (hasBBAtom(node)) { - return; - } - - // make sure it is marked as an atom - addAtom(node); - - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; - ++d_statistics.d_numAtoms; - // 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 = mkNode(kind::IFF, node, atom_bb); - - if (!options::bitvectorEagerBitblast()) { - d_cnfStream->convertAndAssert(atom_definition, false, false); - d_bitblastedAtoms.insert(node); - } else { - d_bvOutput->lemma(atom_definition, false); - d_bitblastedAtoms.insert(node); - } -} - -uint64_t Bitblaster::computeAtomWeight(TNode node) { - node = node.getKind() == kind::NOT? node[0] : node; - - Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); - uint64_t size = utils::numNodes(atom_bb); - return size; -} - -void Bitblaster::bbTerm(TNode node, Bits& bits) { - - if (hasBBTerm(node)) { - getBBTerm(node, bits); - return; - } - - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; - ++d_statistics.d_numTerms; - - d_termBBStrategies[node.getKind()] (node, bits,this); - - Assert (bits.size() == utils::getSize(node)); - - cacheTermDef(node, bits); -} - -Node Bitblaster::bbOptimize(TNode node) { - std::vector<Node> children; - - if (node.getKind() == kind::BITVECTOR_PLUS) { - if (RewriteRule<BBPlusNeg>::applies(node)) { - Node res = RewriteRule<BBPlusNeg>::run<false>(node); - return res; - } - // if (RewriteRule<BBFactorOut>::applies(node)) { - // Node res = RewriteRule<BBFactorOut>::run<false>(node); - // return res; - // } - - } else if (node.getKind() == kind::BITVECTOR_MULT) { - if (RewriteRule<MultPow2>::applies(node)) { - Node res = RewriteRule<MultPow2>::run<false>(node); - return res; - } - } - - return node; -} - -/// Public methods - -void Bitblaster::addAtom(TNode atom) { - if (!options::bitvectorEagerBitblast()) { - d_cnfStream->ensureLiteral(atom); - SatLiteral lit = d_cnfStream->getLiteral(atom); - d_satSolver->addMarkerLiteral(lit); - } -} - -void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { - std::vector<SatLiteral> literal_explanation; - d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation); - for (unsigned i = 0; i < literal_explanation.size(); ++i) { - explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); - } -} - - -/* - * Asserts the clauses corresponding to the atom to the Sat Solver - * by turning on the marker literal (i.e. setting it to false) - * @param node the atom to be asserted - * - */ - -bool Bitblaster::propagate() { - return d_satSolver->propagate() == prop::SAT_VALUE_TRUE; -} - -bool Bitblaster::assertToSat(TNode lit, bool propagate) { - // strip the not - TNode atom; - if (lit.getKind() == kind::NOT) { - atom = lit[0]; - } else { - atom = lit; - } - - Assert (hasBBAtom(atom)); - - SatLiteral markerLit = d_cnfStream->getLiteral(atom); - - if(lit.getKind() == kind::NOT) { - markerLit = ~markerLit; - } - - Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; - Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; - - SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); - - d_assertedAtoms.push_back(markerLit); - - Assert(ret != prop::SAT_VALUE_UNKNOWN); - return ret == prop::SAT_VALUE_TRUE; -} - -/** - * Calls the solve method for the Sat Solver. - * passing it the marker literals to be asserted - * - * @return true for sat, and false for unsat - */ - -bool Bitblaster::solve(bool quick_solve) { - if (Trace.isOn("bitvector")) { - Trace("bitvector") << "Bitblaster::solve() asserted atoms "; - context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin(); - for (; it != d_assertedAtoms.end(); ++it) { - Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; - } - } - Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; - return SAT_VALUE_TRUE == d_satSolver->solve(); -} - -void Bitblaster::getConflict(std::vector<TNode>& conflict) { - SatClause conflictClause; - d_satSolver->getUnsatCore(conflictClause); - - for (unsigned i = 0; i < conflictClause.size(); i++) { - SatLiteral lit = conflictClause[i]; - TNode atom = d_cnfStream->getNode(lit); - Node not_atom; - if (atom.getKind() == kind::NOT) { - not_atom = atom[0]; - } else { - not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); - } - conflict.push_back(not_atom); - } -} - - -/// Helper methods - - -void Bitblaster::initAtomBBStrategies() { - for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_atomBBStrategies[i] = UndefinedAtomBBStrategy; - } - - /// setting default bb strategies for atoms - d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB; - d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB; - d_atomBBStrategies [ kind::BITVECTOR_ULE ] = DefaultUleBB; - d_atomBBStrategies [ kind::BITVECTOR_UGT ] = DefaultUgtBB; - d_atomBBStrategies [ kind::BITVECTOR_UGE ] = DefaultUgeBB; - d_atomBBStrategies [ kind::BITVECTOR_SLT ] = DefaultSltBB; - d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB; - d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB; - d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB; - -} - -void Bitblaster::initTermBBStrategies() { - // Changed this to DefaultVarBB because any foreign kind should be treated as a variable - // TODO: check this is OK - for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_termBBStrategies[i] = DefaultVarBB; - } - - /// setting default bb strategies for terms: - // d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; - d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; - d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB; - d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB; - d_termBBStrategies [ kind::BITVECTOR_AND ] = DefaultAndBB; - d_termBBStrategies [ kind::BITVECTOR_OR ] = DefaultOrBB; - d_termBBStrategies [ kind::BITVECTOR_XOR ] = DefaultXorBB; - d_termBBStrategies [ kind::BITVECTOR_XNOR ] = DefaultXnorBB; - d_termBBStrategies [ kind::BITVECTOR_NAND ] = DefaultNandBB ; - d_termBBStrategies [ kind::BITVECTOR_NOR ] = DefaultNorBB; - d_termBBStrategies [ kind::BITVECTOR_COMP ] = DefaultCompBB ; - d_termBBStrategies [ kind::BITVECTOR_MULT ] = DefaultMultBB; - d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; - d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; - d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; - d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB; - d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; - d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; - d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; - d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB; - d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB; - d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB; - d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ] = DefaultSignExtendBB; - d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB; - d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB; - -} - -bool Bitblaster::hasBBAtom(TNode atom) const { - return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end(); -} - -void Bitblaster::cacheTermDef(TNode term, Bits def) { - Assert (d_termCache.find(term) == d_termCache.end()); - d_termCache[term] = def; -} - -bool Bitblaster::hasBBTerm(TNode node) const { - return d_termCache.find(node) != d_termCache.end(); -} - -void Bitblaster::getBBTerm(TNode node, Bits& bits) const { - Assert (hasBBTerm(node)); - // copy? - bits = d_termCache.find(node)->second; -} - -Bitblaster::Statistics::Statistics() : - d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0), - d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), - d_numTerms("theory::bv::NumberOfBitblastedTerms", 0), - d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), - d_bitblastTimer("theory::bv::BitblastTimer") -{ - StatisticsRegistry::registerStat(&d_numTermClauses); - StatisticsRegistry::registerStat(&d_numAtomClauses); - StatisticsRegistry::registerStat(&d_numTerms); - StatisticsRegistry::registerStat(&d_numAtoms); - StatisticsRegistry::registerStat(&d_bitblastTimer); -} - - -Bitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numTermClauses); - StatisticsRegistry::unregisterStat(&d_numAtomClauses); - StatisticsRegistry::unregisterStat(&d_numTerms); - StatisticsRegistry::unregisterStat(&d_numAtoms); - StatisticsRegistry::unregisterStat(&d_bitblastTimer); -} - -bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) { - return d_bv->storePropagation(d_cnf->getNode(lit), SUB_BITBLAST); -}; - -void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { - if (clause.size() > 1) { - NodeBuilder<> lemmab(kind::OR); - for (unsigned i = 0; i < clause.size(); ++ i) { - lemmab << d_cnf->getNode(clause[i]); - } - Node lemma = lemmab; - d_bv->d_out->lemma(lemma); - } else { - d_bv->d_out->lemma(d_cnf->getNode(clause[0])); - } -}; - -void Bitblaster::MinisatNotify::safePoint() { - d_bv->d_out->safePoint(); -} - -EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { - - // We don't want to bit-blast every possibly expensive term for the sake of equality checking - if (hasBBTerm(a) && hasBBTerm(b)) { - - Bits a_bits, b_bits; - getBBTerm(a, a_bits); - getBBTerm(b, b_bits); - EqualityStatus status = EQUALITY_TRUE_IN_MODEL; - for (unsigned i = 0; i < a_bits.size(); ++ i) { - if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) { - SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]); - SatValue a_lit_value = d_satSolver->value(a_lit); - if (a_lit_value != SAT_VALUE_UNKNOWN) { - SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]); - SatValue b_lit_value = d_satSolver->value(b_lit); - if (b_lit_value != SAT_VALUE_UNKNOWN) { - if (a_lit_value != b_lit_value) { - return EQUALITY_FALSE_IN_MODEL; - } - } else { - status = EQUALITY_UNKNOWN; - } - } { - status = EQUALITY_UNKNOWN; - } - } else { - status = EQUALITY_UNKNOWN; - } - } - - return status; - - } else { - return EQUALITY_UNKNOWN; - } -} - - -bool Bitblaster::isSharedTerm(TNode node) { - return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); -} - -bool Bitblaster::hasValue(TNode a) { - Assert (d_termCache.find(a) != d_termCache.end()); - Bits bits = d_termCache[a]; - for (int i = bits.size() -1; i >= 0; --i) { - SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { - SatLiteral bit = d_cnfStream->getLiteral(bits[i]); - bit_value = d_satSolver->value(bit); - if (bit_value == SAT_VALUE_UNKNOWN) - return false; - } else { - return false; - } - } - return true; -} -/** - * 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 Bitblaster::getVarValue(TNode a, bool fullModel) { - if (d_termCache.find(a) == d_termCache.end()) { - Assert(isSharedTerm(a)); - return Node(); - } - Bits bits = d_termCache[a]; - Integer value(0); - for (int i = bits.size() -1; i >= 0; --i) { - SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { - SatLiteral bit = d_cnfStream->getLiteral(bits[i]); - bit_value = d_satSolver->value(bit); - Assert (bit_value != SAT_VALUE_UNKNOWN); - } else { - //TODO: return Node() if fullModel=false? - // the bit is unconstrainted so we can give it an arbitrary value - bit_value = SAT_VALUE_FALSE; - } - Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); - value = value * 2 + bit_int; - } - return utils::mkConst(BitVector(bits.size(), value)); -} - -void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); - for (; it!= d_variables.end(); ++it) { - TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var, fullModel); - if(const_value == Node()) { - if( fullModel ){ - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); - } - } - if(const_value != Node()) { - Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; - m->assertEquality(var, const_value, true); - } - } - } -} - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ |