From: Liana Hadarean Date: Tue, 15 May 2012 18:53:54 +0000 (+0000) Subject: renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively X-Git-Tag: cvc5-1.0.0~8175 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fe2088f892af594765fc50d8cc9f2b4f87286b7c;p=cvc5.git renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively --- diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index af760e520..3bb7e3056 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -9,8 +9,8 @@ noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ theory_bv_utils.h \ - bv_sat.h \ - bv_sat.cpp \ + bitblaster.h \ + bitblaster.cpp \ bitblast_strategies.h \ bitblast_strategies.cpp \ theory_bv.h \ diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index b579122e5..6871a5421 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -17,7 +17,7 @@ **/ #include "bitblast_strategies.h" -#include "bv_sat.h" +#include "bitblaster.h" #include "prop/sat_solver.h" #include "theory/booleans/theory_bool_rewriter.h" diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp new file mode 100644 index 000000000..60fc8f9c1 --- /dev/null +++ b/src/theory/bv/bitblaster.cpp @@ -0,0 +1,372 @@ +/********************* */ +/*! \file bitblaster.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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" + +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() ? "1" : "0"); + } else { + os << bit<< " "; + } + } + os <<"\n"; + + return os.str(); +} +/////// Bitblaster + +Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : + d_bvOutput(bv->d_out), + d_termCache(), + d_bitblastedAtoms(), + d_assertedAtoms(c), + d_statistics() + { + d_satSolver = prop::SatSolverFactory::createMinisat(c); + d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); + + MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); + d_satSolver->setNotify(notify); + // initializing the bit-blasting strategies + initAtomBBStrategies(); + initTermBBStrategies(); + } + +Bitblaster::~Bitblaster() { + delete d_cnfStream; + delete d_satSolver; +} + + +/** + * 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); + + BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + ++d_statistics.d_numAtoms; + // the bitblasted definition of the atom + Node atom_bb = d_atomBBStrategies[node.getKind()](node, this); + // asserting that the atom is true iff the definition holds + Node atom_definition = mkNode(kind::IFF, node, atom_bb); + // do boolean simplifications if possible + Node rewritten = Rewriter::rewrite(atom_definition); + + if (!Options::current()->bitvectorEagerBitblast) { + d_cnfStream->convertAndAssert(rewritten, true, false); + d_bitblastedAtoms.insert(node); + } else { + d_bvOutput->lemma(rewritten, false); + } +} + + +void Bitblaster::bbTerm(TNode node, Bits& bits) { + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + ++d_statistics.d_numTerms; + + Node optimized = bbOptimize(node); + + // if we already bitblasted the optimized version + if(hasBBTerm(optimized)) { + getBBTerm(optimized, bits); + // cache it as the same for this node + cacheTermDef(node, bits); + return; + } + + d_termBBStrategies[optimized.getKind()] (optimized, bits,this); + + Assert (bits.size() == utils::getSize(node) && + bits.size() == utils::getSize(optimized)); + + if(optimized != node) { + cacheTermDef(optimized, bits); + } + cacheTermDef(node, bits); +} + +Node Bitblaster::bbOptimize(TNode node) { + std::vector children; + + if (node.getKind() == kind::BITVECTOR_PLUS) { + if (RewriteRule::applies(node)) { + Node res = RewriteRule::run(node); + return res; + } + // if (RewriteRule::applies(node)) { + // Node res = RewriteRule::run(node); + // return res; + // } + + } else if (node.getKind() == kind::BITVECTOR_MULT) { + if (RewriteRule::applies(node)) { + Node res = RewriteRule::run(node); + return res; + } + } + + return node; +} + +/// Public methods + +void Bitblaster::addAtom(TNode atom) { + if (!Options::current()->bitvectorEagerBitblast) { + d_cnfStream->ensureLiteral(atom); + SatLiteral lit = d_cnfStream->getLiteral(atom); + d_satSolver->addMarkerLiteral(lit); + } +} + +void Bitblaster::explain(TNode atom, std::vector& explanation) { + std::vector 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 aserted + * + */ + +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; + } + + BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; + BVDebug("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) { + BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; + return SAT_VALUE_TRUE == d_satSolver->solve(); +} + +void Bitblaster::getConflict(std::vector& 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 ] = DefaultUdivBB; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = DefaultUremBB; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = DefaultSdivBB; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = DefaultSremBB; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = DefaultSmodBB; + 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) { + 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) { + return d_termCache.find(node) != d_termCache.end(); +} + +void Bitblaster::getBBTerm(TNode node, Bits& bits) { + + Assert (hasBBTerm(node)); + // copy? + bits = d_termCache[node]; +} + +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), TheoryBV::SUB_BITBLASTER); +}; + +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])); + } +}; + + +} /*bv namespace */ +} /* theory namespace */ +} /* CVC4 namespace*/ diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h new file mode 100644 index 000000000..6de84fc01 --- /dev/null +++ b/src/theory/bv/bitblaster.h @@ -0,0 +1,158 @@ +/********************* */ +/*! \file bitblaster.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Wrapper around the SAT solver used for bitblasting + ** + ** Wrapper around the SAT solver used for bitblasting. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BITBLASTER_H +#define __CVC4__BITBLASTER_H + + +#include "expr/node.h" +#include +#include +#include +#include +#include + +#include "context/cdo.h" +#include "context/cdhashset.h" +#include "context/cdlist.h" + +#include "theory_bv_utils.h" +#include "util/stats.h" +#include "bitblast_strategies.h" + +#include "prop/sat_solver.h" + +namespace CVC4 { + +// forward declarations +namespace prop { +class CnfStream; +class BVSatSolverInterface; +} + +namespace theory { + +class OutputChannel; + +namespace bv { + +typedef std::vector Bits; + +std::string toString (Bits& bits); + +class TheoryBV; + +/** + * The Bitblaster that manages the mapping between Nodes + * and their bitwise definition + * + */ +class Bitblaster { + + /** This class gets callbacks from minisat on propagations */ + class MinisatNotify : public prop::BVSatSolverInterface::Notify { + prop::CnfStream* d_cnf; + TheoryBV *d_bv; + public: + MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv) + : d_cnf(cnf) + , d_bv(bv) + {} + bool notify(prop::SatLiteral lit); + void notify(prop::SatClause& clause); + }; + + typedef __gnu_cxx::hash_map TermDefMap; + typedef __gnu_cxx::hash_set AtomSet; + + typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); + typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); + + // sat solver used for bitblasting and associated CnfStream + theory::OutputChannel* d_bvOutput; + prop::BVSatSolverInterface* d_satSolver; + prop::CnfStream* d_cnfStream; + + // caches and mappings + TermDefMap d_termCache; + AtomSet d_bitblastedAtoms; + + context::CDList d_assertedAtoms; /**< context dependent list storing the atoms + currently asserted by the DPLL SAT solver. */ + + /// helper methods + public: + bool hasBBAtom(TNode node); + private: + bool hasBBTerm(TNode node); + void getBBTerm(TNode node, Bits& bits); + + /// function tables for the various bitblasting strategies indexed by node kind + TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + + // helper methods to initialize function tables + void initAtomBBStrategies(); + void initTermBBStrategies(); + + // returns a node that might be easier to bitblast + Node bbOptimize(TNode node); + + void addAtom(TNode atom); + // division is bitblasted in terms of constraints + // so it needs to use private bitblaster interface + void bbUdiv(TNode node, Bits& bits); + void bbUrem(TNode node, Bits& bits); +public: + void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division + void bbTerm(TNode node, Bits& bits); + void bbAtom(TNode node); + + Bitblaster(context::Context* c, bv::TheoryBV* bv); + ~Bitblaster(); + bool assertToSat(TNode node, bool propagate = true); + bool solve(bool quick_solve = false); + void getConflict(std::vector& conflict); + void explain(TNode atom, std::vector& explanation); + +private: + + + class Statistics { + public: + IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTerms, d_numAtoms; + TimerStat d_bitblastTimer; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + + + +} /* bv namespace */ + +} /* theory namespace */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__BITBLASTER_H */ diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp deleted file mode 100644 index ed3101459..000000000 --- a/src/theory/bv/bv_sat.cpp +++ /dev/null @@ -1,372 +0,0 @@ -/********************* */ -/*! \file bv_sat.cpp - ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** 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 "bv_sat.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" - -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() ? "1" : "0"); - } else { - os << bit<< " "; - } - } - os <<"\n"; - - return os.str(); -} -/////// Bitblaster - -Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : - d_bvOutput(bv->d_out), - d_termCache(), - d_bitblastedAtoms(), - d_assertedAtoms(c), - d_statistics() - { - d_satSolver = prop::SatSolverFactory::createMinisat(c); - d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); - - MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); - d_satSolver->setNotify(notify); - // initializing the bit-blasting strategies - initAtomBBStrategies(); - initTermBBStrategies(); - } - -Bitblaster::~Bitblaster() { - delete d_cnfStream; - delete d_satSolver; -} - - -/** - * 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); - - BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; - ++d_statistics.d_numAtoms; - // the bitblasted definition of the atom - Node atom_bb = d_atomBBStrategies[node.getKind()](node, this); - // asserting that the atom is true iff the definition holds - Node atom_definition = mkNode(kind::IFF, node, atom_bb); - // do boolean simplifications if possible - Node rewritten = Rewriter::rewrite(atom_definition); - - if (!Options::current()->bitvectorEagerBitblast) { - d_cnfStream->convertAndAssert(rewritten, true, false); - d_bitblastedAtoms.insert(node); - } else { - d_bvOutput->lemma(rewritten, false); - } -} - - -void Bitblaster::bbTerm(TNode node, Bits& bits) { - if (hasBBTerm(node)) { - getBBTerm(node, bits); - return; - } - BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; - ++d_statistics.d_numTerms; - - Node optimized = bbOptimize(node); - - // if we already bitblasted the optimized version - if(hasBBTerm(optimized)) { - getBBTerm(optimized, bits); - // cache it as the same for this node - cacheTermDef(node, bits); - return; - } - - d_termBBStrategies[optimized.getKind()] (optimized, bits,this); - - Assert (bits.size() == utils::getSize(node) && - bits.size() == utils::getSize(optimized)); - - if(optimized != node) { - cacheTermDef(optimized, bits); - } - cacheTermDef(node, bits); -} - -Node Bitblaster::bbOptimize(TNode node) { - std::vector children; - - if (node.getKind() == kind::BITVECTOR_PLUS) { - if (RewriteRule::applies(node)) { - Node res = RewriteRule::run(node); - return res; - } - // if (RewriteRule::applies(node)) { - // Node res = RewriteRule::run(node); - // return res; - // } - - } else if (node.getKind() == kind::BITVECTOR_MULT) { - if (RewriteRule::applies(node)) { - Node res = RewriteRule::run(node); - return res; - } - } - - return node; -} - -/// Public methods - -void Bitblaster::addAtom(TNode atom) { - if (!Options::current()->bitvectorEagerBitblast) { - d_cnfStream->ensureLiteral(atom); - SatLiteral lit = d_cnfStream->getLiteral(atom); - d_satSolver->addMarkerLiteral(lit); - } -} - -void Bitblaster::explain(TNode atom, std::vector& explanation) { - std::vector 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 aserted - * - */ - -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; - } - - BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; - BVDebug("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) { - BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; - return SAT_VALUE_TRUE == d_satSolver->solve(); -} - -void Bitblaster::getConflict(std::vector& 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 ] = DefaultUdivBB; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = DefaultSdivBB; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = DefaultSremBB; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = DefaultSmodBB; - 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) { - 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) { - return d_termCache.find(node) != d_termCache.end(); -} - -void Bitblaster::getBBTerm(TNode node, Bits& bits) { - - Assert (hasBBTerm(node)); - // copy? - bits = d_termCache[node]; -} - -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), TheoryBV::SUB_BITBLASTER); -}; - -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])); - } -}; - - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h deleted file mode 100644 index 7016879a0..000000000 --- a/src/theory/bv/bv_sat.h +++ /dev/null @@ -1,158 +0,0 @@ -/********************* */ -/*! \file bv_sat.h - ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Wrapper around the SAT solver used for bitblasting - ** - ** Wrapper around the SAT solver used for bitblasting. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__BV__SAT_H -#define __CVC4__BV__SAT_H - - -#include "expr/node.h" -#include -#include -#include -#include -#include - -#include "context/cdo.h" -#include "context/cdhashset.h" -#include "context/cdlist.h" - -#include "theory_bv_utils.h" -#include "util/stats.h" -#include "bitblast_strategies.h" - -#include "prop/sat_solver.h" - -namespace CVC4 { - -// forward declarations -namespace prop { -class CnfStream; -class BVSatSolverInterface; -} - -namespace theory { - -class OutputChannel; - -namespace bv { - -typedef std::vector Bits; - -std::string toString (Bits& bits); - -class TheoryBV; - -/** - * The Bitblaster that manages the mapping between Nodes - * and their bitwise definition - * - */ -class Bitblaster { - - /** This class gets callbacks from minisat on propagations */ - class MinisatNotify : public prop::BVSatSolverInterface::Notify { - prop::CnfStream* d_cnf; - TheoryBV *d_bv; - public: - MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv) - : d_cnf(cnf) - , d_bv(bv) - {} - bool notify(prop::SatLiteral lit); - void notify(prop::SatClause& clause); - }; - - typedef __gnu_cxx::hash_map TermDefMap; - typedef __gnu_cxx::hash_set AtomSet; - - typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); - typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); - - // sat solver used for bitblasting and associated CnfStream - theory::OutputChannel* d_bvOutput; - prop::BVSatSolverInterface* d_satSolver; - prop::CnfStream* d_cnfStream; - - // caches and mappings - TermDefMap d_termCache; - AtomSet d_bitblastedAtoms; - - context::CDList d_assertedAtoms; /**< context dependent list storing the atoms - currently asserted by the DPLL SAT solver. */ - - /// helper methods - public: - bool hasBBAtom(TNode node); - private: - bool hasBBTerm(TNode node); - void getBBTerm(TNode node, Bits& bits); - - /// function tables for the various bitblasting strategies indexed by node kind - TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; - AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; - - // helper methods to initialize function tables - void initAtomBBStrategies(); - void initTermBBStrategies(); - - // returns a node that might be easier to bitblast - Node bbOptimize(TNode node); - - void addAtom(TNode atom); - // division is bitblasted in terms of constraints - // so it needs to use private bitblaster interface - void bbUdiv(TNode node, Bits& bits); - void bbUrem(TNode node, Bits& bits); -public: - void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division - void bbTerm(TNode node, Bits& bits); - void bbAtom(TNode node); - - Bitblaster(context::Context* c, bv::TheoryBV* bv); - ~Bitblaster(); - bool assertToSat(TNode node, bool propagate = true); - bool solve(bool quick_solve = false); - void getConflict(std::vector& conflict); - void explain(TNode atom, std::vector& explanation); - -private: - - - class Statistics { - public: - IntStat d_numTermClauses, d_numAtomClauses; - IntStat d_numTerms, d_numAtoms; - TimerStat d_bitblastTimer; - Statistics(); - ~Statistics(); - }; - - Statistics d_statistics; -}; - - - -} /* bv namespace */ - -} /* theory namespace */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__BV__SAT_H */ diff --git a/src/theory/bv/bv_solver_types.cpp b/src/theory/bv/bv_solver_types.cpp deleted file mode 100644 index 2589e5712..000000000 --- a/src/theory/bv/bv_solver_types.cpp +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \file bv_sat.cpp - ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** 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 "bv_solver_types.h" - -namespace CVC4 { -namespace theory { -namespace bv { - -#ifdef BV_MINISAT -using namespace BVMinisat; -SatLit neg(const SatLit& lit) { - return ~lit; -} - -SatLit mkLit(SatVar var) { - return BVMinisat::mkLit(var, false); -} - -SatVar mkVar(SatLit lit) { - return BVMinisat::var(lit); -} -bool polarity(SatLit lit) { - return !(BVMinisat::sign(lit)); -} - - -std::string toStringLit(SatLit lit) { - std::ostringstream os; - os << (polarity(lit) ? "" : "-") << var(lit) + 1; - return os.str(); -} -#endif - -#ifdef BV_PICOSAT - -SatLit mkLit(SatVar var) { - return var; -} -SatVar mkVar(SatLit lit) { - return (lit > 0 ? lit : -lit); -} -bool polarity(SatLit lit) { - return (lit > 0); -} - -SatLit neg(const SatLit& lit) { - return -lit; -} - -std::string toStringLit(SatLit lit) { - std::ostringstream os; - os << (lit < 0 ? "-" : "") << lit; - return os.str(); -} - - -#endif - -} -} -} diff --git a/src/theory/bv/bv_solver_types.h b/src/theory/bv/bv_solver_types.h deleted file mode 100644 index fb99ae4c6..000000000 --- a/src/theory/bv/bv_solver_types.h +++ /dev/null @@ -1,185 +0,0 @@ -//********************* */ -/*! \file bv_solver_types.h - ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Definitions of the SatSolver literal and clause types - ** - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__BV__SOLVER__TYPES_H -#define __CVC4__BV__SOLVER__TYPES_H - -#define BV_MINISAT -//#define BV_PICOSAT - -#ifdef BV_MINISAT /* BV_MINISAT if we are using the minisat solver for the theory of bitvectors*/ -#include "theory/bv/bvminisat/core/Solver.h" -#include "theory/bv/bvminisat/core/SolverTypes.h" -#include "theory/bv/bvminisat/simp/SimpSolver.h" -#endif /* BV_MINISAT */ - -#ifdef BV_PICOSAT /* BV_PICOSAT */ -#include "picosat/picosat.h" -#endif /* BV_PICOSAT */ - -#include "expr/node.h" -#include -#include -#include -#include -#include -#include "context/cdlist.h" -#include "util/stats.h" - - -namespace CVC4 { -namespace theory { -namespace bv { - -#endif /* BV_MINISAT */ - - - -// #ifdef BV_PICOSAT /* BV_PICOSAT */ -// /** -// * PICOSAT type-definitions -// * -// * -// */ - -// typedef int SatVar; -// typedef int SatLit; - -// std::string toStringLit(SatLit lit); - - -// SatLit neg(const SatLit& lit); - -// struct SatLitHash { -// static size_t hash (const SatLit& lit) { -// return (size_t) lit; -// } - -// }; - -// struct SatLitHashFunction { -// size_t operator()(SatLit lit) const { -// return (size_t) lit; -// } -// }; - -// struct SatLitLess{ -// static bool compare(const SatLit& x, const SatLit& y) -// { -// return x < y; -// } -// }; - -// #endif /* BV_PICOSAT */ - -// #ifdef BV_PICOSAT /* BV_PICOSAT */ - -// /** -// * Some helper functions that should be defined for each SAT solver supported -// * -// * -// * @return -// */ - -// SatLit mkLit(SatVar var); -// SatVar mkVar(SatLit lit); -// bool polarity(SatLit lit); - - -// /** -// * Wrapper to create the impression of a SatSolver class for Picosat -// * which is written in C -// */ - -// class SatSolver: public SatSolverInterface { -// int d_varCount; -// bool d_started; -// public: -// SatSolver() : -// d_varCount(0), -// d_started(false) -// { -// picosat_init(); /// call constructor -// picosat_enable_trace_generation(); // required for unsat cores -// } - -// ~SatSolver() { -// picosat_reset(); -// } - -// void addClause(const SatClause* cl) { -// Assert (cl); -// const SatClause& clause = *cl; -// for (unsigned i = 0; i < clause.size(); ++i ) { -// picosat_add(clause[i]); -// } -// picosat_add(0); // ends clause -// } - -// bool solve () { -// if(d_started) { -// picosat_remove_learned(100); -// } -// int res = picosat_sat(-1); // no decision limit -// // 0 UNKNOWN, 10 SATISFIABLE and 20 UNSATISFIABLE -// d_started = true; -// Assert (res == 10 || res == 20); -// return res == 10; -// } - -// bool solve(const context::CDList & assumps) { -// context::CDList::const_iterator it = assumps.begin(); -// for (; it!= assumps.end(); ++it) { -// picosat_assume(*it); -// } -// return solve (); -// } - -// SatVar newVar() { return ++d_varCount; } - -// void setUnremovable(SatLit lit) {}; - -// SatClause* getUnsatCore() { -// const int* failedAssumption = picosat_failed_assumptions(); -// Assert(failedAssumption); - -// SatClause* unsatCore = new SatClause(); -// while (*failedAssumption != 0) { -// SatLit lit = *failedAssumption; -// unsatCore->addLiteral(neg(lit)); -// ++failedAssumption; -// } -// unsatCore->sort(); -// return unsatCore; -// } -// }; - - -// #endif /* BV_PICOSAT */ - - - - -} /* bv namespace */ - -} /* theory namespace */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__BV__SOLVER__TYPES_H */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 07eb69c26..d005e9473 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -20,7 +20,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/valuation.h" -#include "theory/bv/bv_sat.h" +#include "theory/bv/bitblaster.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index bbc7a8f72..081fa7c2a 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -21,7 +21,7 @@ #include #include "theory/theory.h" -#include "theory/bv/bv_sat.h" +#include "theory/bv/bitblaster.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h"