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 \
**/
#include "bitblast_strategies.h"
-#include "bv_sat.h"
+#include "bitblaster.h"
#include "prop/sat_solver.h"
#include "theory/booleans/theory_bool_rewriter.h"
--- /dev/null
+/********************* */
+/*! \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<bool>() ? "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<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::current()->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 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<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 ] = 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*/
--- /dev/null
+/********************* */
+/*! \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 <vector>
+#include <list>
+#include <iostream>
+#include <math.h>
+#include <ext/hash_map>
+
+#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<Node> 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 <Node, Bits, TNodeHashFunction > TermDefMap;
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> 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<prop::SatLiteral> 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<TNode>& conflict);
+ void explain(TNode atom, std::vector<TNode>& 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 */
+++ /dev/null
-/********************* */
-/*! \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<bool>() ? "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<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::current()->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 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<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 ] = 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*/
+++ /dev/null
-/********************* */
-/*! \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 <vector>
-#include <list>
-#include <iostream>
-#include <math.h>
-#include <ext/hash_map>
-
-#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<Node> 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 <Node, Bits, TNodeHashFunction > TermDefMap;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> 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<prop::SatLiteral> 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<TNode>& conflict);
- void explain(TNode atom, std::vector<TNode>& 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 */
+++ /dev/null
-/********************* */
-/*! \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
-
-}
-}
-}
+++ /dev/null
-//********************* */
-/*! \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 <vector>
-#include <list>
-#include <iostream>
-#include <math.h>
-#include <ext/hash_map>
-#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<SatLit> & assumps) {
-// context::CDList<SatLit>::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 */
#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;
#include <cxxtest/TestSuite.h>
#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"
projects / cvc5.git / commitdiff