theory/bv/bv_inequality_graph.cpp \
theory/bv/bitblast_strategies_template.h \
theory/bv/bitblaster_template.h \
- theory/bv/lazy_bitblaster.h \
- theory/bv/eager_bitblaster.h \
- theory/bv/aig_bitblaster.h \
+ theory/bv/lazy_bitblaster.cpp \
+ theory/bv/eager_bitblaster.cpp \
+ theory/bv/aig_bitblaster.cpp \
theory/bv/bv_eager_solver.h \
theory/bv/bv_eager_solver.cpp \
theory/bv/slicer.h \
--- /dev/null
+/********************* */
+/*! \file aig_bitblaster.cpp
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): lianah
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief
+ **
+ ** Bitblaster for the lazy bv solver.
+ **/
+
+#include "cvc4_private.h"
+#include "bitblaster_template.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_factory.h"
+#include "theory/bv/options.h"
+
+
+#ifdef CVC4_USE_ABC
+// Function is defined as static in ABC. Not sure how else to do this.
+static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
+
+extern "C" {
+extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+}
+
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template <> inline
+std::string toString<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) {
+ Unreachable("Don't know how to print AIG");
+}
+
+
+template <> inline
+Abc_Obj_t* mkTrue<Abc_Obj_t*>() {
+ return Abc_AigConst1(AigBitblaster::currentAigNtk());
+}
+
+template <> inline
+Abc_Obj_t* mkFalse<Abc_Obj_t*>() {
+ return Abc_ObjNot(mkTrue<Abc_Obj_t*>());
+}
+
+template <> inline
+Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) {
+ return Abc_ObjNot(a);
+}
+
+template <> inline
+Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ return Abc_AigOr(AigBitblaster::currentAigM(), a, b);
+}
+
+template <> inline
+Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
+ Assert (children.size());
+ if (children.size() == 1)
+ return children[0];
+
+ Abc_Obj_t* result = children[0];
+ for (unsigned i = 1; i < children.size(); ++i) {
+ result = Abc_AigOr(AigBitblaster::currentAigM(), result, children[i]);
+ }
+ return result;
+}
+
+
+template <> inline
+Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ return Abc_AigAnd(AigBitblaster::currentAigM(), a, b);
+}
+
+template <> inline
+Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
+ Assert (children.size());
+ if (children.size() == 1)
+ return children[0];
+
+ Abc_Obj_t* result = children[0];
+ for (unsigned i = 1; i < children.size(); ++i) {
+ result = Abc_AigAnd(AigBitblaster::currentAigM(), result, children[i]);
+ }
+ return result;
+}
+
+template <> inline
+Abc_Obj_t* mkXor<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ return Abc_AigXor(AigBitblaster::currentAigM(), a, b);
+}
+
+template <> inline
+Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ return mkNot(mkXor(a, b));
+}
+
+template <> inline
+Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
+ return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b);
+}
+
+} /* CVC4::theory::bv */
+} /* CVC4::theory */
+} /* CVC4 */
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+
+Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
+
+Abc_Ntk_t* AigBitblaster::currentAigNtk() {
+ if (!AigBitblaster::abcAigNetwork) {
+ Abc_Start();
+ abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
+ char pName[] = "CVC4::theory::bv::AigNetwork";
+ abcAigNetwork->pName = Extra_UtilStrsav(pName);
+ }
+
+ return abcAigNetwork;
+}
+
+
+Abc_Aig_t* AigBitblaster::currentAigM() {
+ return (Abc_Aig_t*)(currentAigNtk()->pManFunc);
+}
+
+AigBitblaster::AigBitblaster()
+ : TBitblaster<Abc_Obj_t*>()
+ , d_aigCache()
+ , d_bbAtoms()
+ , d_aigOutputNode(NULL)
+{
+ d_nullContext = new context::Context();
+ d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster");
+ MinisatEmptyNotify* notify = new MinisatEmptyNotify();
+ d_satSolver->setNotify(notify);
+}
+
+AigBitblaster::~AigBitblaster() {
+ Assert (abcAigNetwork == NULL);
+ delete d_nullContext;
+}
+
+Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
+ Assert (node.getType().isBoolean());
+ Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n";
+
+ if (hasAig(node))
+ return getAig(node);
+
+ Abc_Obj_t* result = NULL;
+
+ Debug("bitvector-aig") << "AigBitblaster::convertToAig " << node <<"\n";
+ switch (node.getKind()) {
+ case kind::AND:
+ {
+ result = bbFormula(node[0]);
+ for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+ Abc_Obj_t* child = bbFormula(node[i]);
+ result = mkAnd(result, child);
+ }
+ break;
+ }
+ case kind::OR:
+ {
+ result = bbFormula(node[0]);
+ for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+ Abc_Obj_t* child = bbFormula(node[i]);
+ result = mkOr(result, child);
+ }
+ break;
+ }
+ case kind::IFF:
+ {
+ Assert (node.getNumChildren() == 2);
+ Abc_Obj_t* child1 = bbFormula(node[0]);
+ Abc_Obj_t* child2 = bbFormula(node[1]);
+
+ result = mkIff(child1, child2);
+ break;
+ }
+ case kind::XOR:
+ {
+ result = bbFormula(node[0]);
+ for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+ Abc_Obj_t* child = bbFormula(node[i]);
+ result = mkXor(result, child);
+ }
+ break;
+ }
+ case kind::IMPLIES:
+ {
+ Assert (node.getNumChildren() == 2);
+ Abc_Obj_t* child1 = bbFormula(node[0]);
+ Abc_Obj_t* child2 = bbFormula(node[1]);
+
+ result = mkOr(mkNot(child1), child2);
+ break;
+ }
+ case kind::ITE:
+ {
+ Assert (node.getNumChildren() == 3);
+ Abc_Obj_t* a = bbFormula(node[0]);
+ Abc_Obj_t* b = bbFormula(node[1]);
+ Abc_Obj_t* c = bbFormula(node[2]);
+ result = mkIte(a, b, c);
+ break;
+ }
+ case kind::NOT:
+ {
+ Abc_Obj_t* child1 = bbFormula(node[0]);
+ result = mkNot(child1);
+ break;
+ }
+ case kind::CONST_BOOLEAN:
+ {
+ result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>();
+ break;
+ }
+ case kind::VARIABLE:
+ case kind::SKOLEM:
+ {
+ result = mkInput(node);
+ break;
+ }
+ default:
+ bbAtom(node);
+ result = getBBAtom(node);
+ }
+
+ cacheAig(node, result);
+ Debug("bitvector-aig") << "AigBitblaster::bbFormula done " << node << " => " << result <<"\n";
+ return result;
+}
+
+void AigBitblaster::bbAtom(TNode node) {
+ if (hasBBAtom(node)) {
+ return;
+ }
+
+ Debug("bitvector-bitblast") << "Bitblasting atom " << node <<"\n";
+
+ // the bitblasted definition of the atom
+ Node normalized = Rewriter::rewrite(node);
+ Abc_Obj_t* atom_bb = (d_atomBBStrategies[normalized.getKind()])(normalized, this);
+ storeBBAtom(node, atom_bb);
+ Debug("bitvector-bitblast") << "Done bitblasting atom " << node <<"\n";
+}
+
+void AigBitblaster::bbTerm(TNode node, Bits& bits) {
+ if (hasBBTerm(node)) {
+ getBBTerm(node, bits);
+ return;
+ }
+
+ Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
+ d_termBBStrategies[node.getKind()] (node, bits, this);
+
+ Assert (bits.size() == utils::getSize(node));
+ storeBBTerm(node, bits);
+}
+
+
+void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
+ Assert (!hasAig(node));
+ d_aigCache.insert(std::make_pair(node, aig));
+}
+bool AigBitblaster::hasAig(TNode node) {
+ return d_aigCache.find(node) != d_aigCache.end();
+}
+Abc_Obj_t* AigBitblaster::getAig(TNode node) {
+ Assert(hasAig(node));
+ Debug("bitvector-aig") << "AigSimplifer::getAig " << node << " => " << d_aigCache.find(node)->second <<"\n";
+ return d_aigCache.find(node)->second;
+}
+
+void AigBitblaster::makeVariable(TNode node, Bits& bits) {
+
+ for (unsigned i = 0; i < utils::getSize(node); ++i) {
+ Node bit = utils::mkBitOf(node, i);
+ Abc_Obj_t* input = mkInput(bit);
+ cacheAig(bit, input);
+ bits.push_back(input);
+ }
+}
+
+Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
+ Assert (!hasInput(input));
+ Assert(input.getKind() == kind::BITVECTOR_BITOF ||
+ (input.getType().isBoolean() &&
+ (input.getKind() == kind::VARIABLE ||
+ input.getKind() == kind::SKOLEM)));
+ Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
+ // d_aigCache.insert(std::make_pair(input, aig_input));
+ d_nodeToAigInput.insert(std::make_pair(input, aig_input));
+ Debug("bitvector-aig") << "AigSimplifer::mkInput " << input << " " << aig_input <<"\n";
+ return aig_input;
+}
+
+bool AigBitblaster::hasInput(TNode input) {
+ return d_nodeToAigInput.find(input) != d_nodeToAigInput.end();
+}
+
+bool AigBitblaster::solve(TNode node) {
+ // setting output of network to be the query
+ Assert (d_aigOutputNode == NULL);
+ Abc_Obj_t* query = bbFormula(node);
+ d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk());
+ Abc_ObjAddFanin(d_aigOutputNode, query);
+
+ simplifyAig();
+ convertToCnfAndAssert();
+ // no need to use abc anymore
+
+ TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime);
+ prop::SatValue result = d_satSolver->solve();
+
+ Assert (result != prop::SAT_VALUE_UNKNOWN);
+ return result == prop::SAT_VALUE_TRUE;
+}
+
+
+void addAliases(Abc_Frame_t* pAbc);
+
+void AigBitblaster::simplifyAig() {
+ TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime);
+
+ Abc_AigCleanup(currentAigM());
+ Assert (Abc_NtkCheck(currentAigNtk()));
+
+ const char* command = options::bitvectorAigSimplifications().c_str();
+ Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
+ Abc_FrameSetCurrentNetwork(pAbc, currentAigNtk());
+
+ addAliases(pAbc);
+ if ( Cmd_CommandExecute( pAbc, command ) ) {
+ fprintf( stdout, "Cannot execute command \"%s\".\n", command );
+ exit(-1);
+ }
+ abcAigNetwork = Abc_FrameReadNtk(pAbc);
+}
+
+
+void AigBitblaster::convertToCnfAndAssert() {
+ TimerStat::CodeTimer cnfConversionTimer(d_statistics.d_cnfConversionTime);
+
+ Aig_Man_t * pMan = NULL;
+ Cnf_Dat_t * pCnf = NULL;
+ assert( Abc_NtkIsStrash(currentAigNtk()) );
+
+ // convert to the AIG manager
+ pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );
+ Abc_Stop();
+
+ // // free old network
+ // Abc_NtkDelete(currentAigNtk());
+ // abcAigNetwork = NULL;
+
+ Assert (pMan != NULL);
+ Assert (Aig_ManCheck(pMan));
+ pCnf = Cnf_DeriveFast( pMan, 0 );
+
+ assertToSatSolver(pCnf);
+
+ Cnf_DataFree( pCnf );
+ Cnf_ManFree();
+ Aig_ManStop(pMan);
+}
+
+void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
+ unsigned numVariables = pCnf->nVars;
+ unsigned numClauses = pCnf->nClauses;
+
+ d_statistics.d_numVariables += numVariables;
+ d_statistics.d_numClauses += numClauses;
+
+ // create variables in the sat solver
+ std::vector<prop::SatVariable> sat_variables;
+ for (unsigned i = 0; i < numVariables; ++i) {
+ sat_variables.push_back(d_satSolver->newVar(false, false, false));
+ }
+
+ // construct clauses and add to sat solver
+ int * pLit, * pStop;
+ for (unsigned i = 0; i < numClauses; i++ ) {
+ prop::SatClause clause;
+ for (pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ ) {
+ int int_lit = Cnf_Lit2Var(*pLit);
+ Assert (int_lit != 0);
+ unsigned index = int_lit < 0? -int_lit : int_lit;
+ Assert (index - 1 < sat_variables.size());
+ prop::SatLiteral lit(sat_variables[index-1], int_lit < 0);
+ clause.push_back(lit);
+ }
+ d_satSolver->addClause(clause, false);
+ }
+}
+
+void addAliases(Abc_Frame_t* pAbc) {
+ std::vector<std::string> aliases;
+ aliases.push_back("alias b balance");
+ aliases.push_back("alias rw rewrite");
+ aliases.push_back("alias rwz rewrite -z");
+ aliases.push_back("alias rf refactor");
+ aliases.push_back("alias rfz refactor -z");
+ aliases.push_back("alias re restructure");
+ aliases.push_back("alias rez restructure -z");
+ aliases.push_back("alias rs resub");
+ aliases.push_back("alias rsz resub -z");
+ aliases.push_back("alias rsk6 rs -K 6");
+ aliases.push_back("alias rszk5 rsz -K 5");
+ aliases.push_back("alias bl b -l");
+ aliases.push_back("alias rwl rw -l");
+ aliases.push_back("alias rwzl rwz -l");
+ aliases.push_back("alias rwzl rwz -l");
+ aliases.push_back("alias rfl rf -l");
+ aliases.push_back("alias rfzl rfz -l");
+ aliases.push_back("alias brw \"b; rw\"");
+
+ for (unsigned i = 0; i < aliases.size(); ++i) {
+ if ( Cmd_CommandExecute( pAbc, aliases[i].c_str() ) ) {
+ fprintf( stdout, "Cannot execute command \"%s\".\n", aliases[i].c_str() );
+ exit(-1);
+ }
+ }
+}
+
+bool AigBitblaster::hasBBAtom(TNode atom) const {
+ return d_bbAtoms.find(atom) != d_bbAtoms.end();
+}
+
+void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
+ d_bbAtoms.insert(std::make_pair(atom, atom_bb));
+}
+
+Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
+ Assert (hasBBAtom(atom));
+ return d_bbAtoms.find(atom)->second;
+}
+
+AigBitblaster::Statistics::Statistics()
+ : d_numClauses("theory::bv::AigBitblaster::numClauses", 0)
+ , d_numVariables("theory::bv::AigBitblaster::numVariables", 0)
+ , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime")
+ , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
+ , d_solveTime("theory::bv::AigBitblaster::solveTime")
+{
+ StatisticsRegistry::registerStat(&d_numClauses);
+ StatisticsRegistry::registerStat(&d_numVariables);
+ StatisticsRegistry::registerStat(&d_simplificationTime);
+ StatisticsRegistry::registerStat(&d_cnfConversionTime);
+ StatisticsRegistry::registerStat(&d_solveTime);
+}
+
+AigBitblaster::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numClauses);
+ StatisticsRegistry::unregisterStat(&d_numVariables);
+ StatisticsRegistry::unregisterStat(&d_simplificationTime);
+ StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
+ StatisticsRegistry::unregisterStat(&d_solveTime);
+}
+
+#else // CVC4_USE_ABC
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template <> inline
+std::string toString<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) {
+ Unreachable("Don't know how to print AIG");
+}
+
+
+template <> inline
+Abc_Obj_t* mkTrue<Abc_Obj_t*>() {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkFalse<Abc_Obj_t*>() {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
+ Unreachable();
+ return NULL;
+}
+
+
+template <> inline
+Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkXor<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
+ Unreachable();
+ return NULL;
+}
+
+template <> inline
+Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
+ Unreachable();
+ return NULL;
+}
+
+} /* CVC4::theory::bv */
+} /* CVC4::theory */
+} /* CVC4 */
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
+
+Abc_Ntk_t* AigBitblaster::currentAigNtk() {
+ Unreachable();
+ return NULL;
+}
+
+
+Abc_Aig_t* AigBitblaster::currentAigM() {
+ Unreachable();
+ return NULL;
+}
+
+AigBitblaster::~AigBitblaster() {
+ Unreachable();
+}
+
+Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
+ Unreachable();
+ return NULL;
+}
+
+void AigBitblaster::bbAtom(TNode node) {
+ Unreachable();
+}
+
+void AigBitblaster::bbTerm(TNode node, Bits& bits) {
+ Unreachable();
+}
+
+
+void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
+ Unreachable();
+}
+bool AigBitblaster::hasAig(TNode node) {
+ Unreachable();
+ return false;
+}
+Abc_Obj_t* AigBitblaster::getAig(TNode node) {
+ Unreachable();
+ return NULL;
+}
+
+void AigBitblaster::makeVariable(TNode node, Bits& bits) {
+ Unreachable();
+}
+
+Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
+ Unreachable();
+ return NULL;
+}
+
+bool AigBitblaster::hasInput(TNode input) {
+ Unreachable();
+ return false;
+}
+
+bool AigBitblaster::solve(TNode node) {
+ Unreachable();
+ return false;
+}
+void AigBitblaster::simplifyAig() {
+ Unreachable();
+}
+
+void AigBitblaster::convertToCnfAndAssert() {
+ Unreachable();
+}
+
+void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
+ Unreachable();
+}
+bool AigBitblaster::hasBBAtom(TNode atom) const {
+ Unreachable();
+ return false;
+}
+
+void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
+ Unreachable();
+}
+
+Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
+ Unreachable();
+ return NULL;
+}
+
+AigBitblaster::Statistics::Statistics()
+ : d_numClauses("theory::bv::AigBitblaster::numClauses", 0)
+ , d_numVariables("theory::bv::AigBitblaster::numVariables", 0)
+ , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime")
+ , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
+ , d_solveTime("theory::bv::AigBitblaster::solveTime")
+{}
+
+AigBitblaster::Statistics::~Statistics() {}
+
+AigBitblaster::AigBitblaster() {
+ Unreachable();
+}
+#endif // CVC4_USE_ABC
+++ /dev/null
-/********************* */
-/*! \file aig_bitblaster.h
- ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): lianah
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief
- **
- ** Bitblaster for the lazy bv solver.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__AIG__BITBLASTER_H
-#define __CVC4__AIG__BITBLASTER_H
-
-
-#include "bitblaster_template.h"
-#include "prop/cnf_stream.h"
-#include "prop/sat_solver_factory.h"
-#include "theory/bv/options.h"
-
-
-#ifdef CVC4_USE_ABC
-// Function is defined as static in ABC. Not sure how else to do this.
-static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
-
-extern "C" {
-extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-}
-
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-template <> inline
-std::string toString<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) {
- Unreachable("Don't know how to print AIG");
-}
-
-
-template <> inline
-Abc_Obj_t* mkTrue<Abc_Obj_t*>() {
- return Abc_AigConst1(AigBitblaster::currentAigNtk());
-}
-
-template <> inline
-Abc_Obj_t* mkFalse<Abc_Obj_t*>() {
- return Abc_ObjNot(mkTrue<Abc_Obj_t*>());
-}
-
-template <> inline
-Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) {
- return Abc_ObjNot(a);
-}
-
-template <> inline
-Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- return Abc_AigOr(AigBitblaster::currentAigM(), a, b);
-}
-
-template <> inline
-Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
- Assert (children.size());
- if (children.size() == 1)
- return children[0];
-
- Abc_Obj_t* result = children[0];
- for (unsigned i = 1; i < children.size(); ++i) {
- result = Abc_AigOr(AigBitblaster::currentAigM(), result, children[i]);
- }
- return result;
-}
-
-
-template <> inline
-Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- return Abc_AigAnd(AigBitblaster::currentAigM(), a, b);
-}
-
-template <> inline
-Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
- Assert (children.size());
- if (children.size() == 1)
- return children[0];
-
- Abc_Obj_t* result = children[0];
- for (unsigned i = 1; i < children.size(); ++i) {
- result = Abc_AigAnd(AigBitblaster::currentAigM(), result, children[i]);
- }
- return result;
-}
-
-template <> inline
-Abc_Obj_t* mkXor<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- return Abc_AigXor(AigBitblaster::currentAigM(), a, b);
-}
-
-template <> inline
-Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- return mkNot(mkXor(a, b));
-}
-
-template <> inline
-Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
- return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b);
-}
-
-
-Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
-
-Abc_Ntk_t* AigBitblaster::currentAigNtk() {
- if (!AigBitblaster::abcAigNetwork) {
- Abc_Start();
- abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
- char pName[] = "CVC4::theory::bv::AigNetwork";
- abcAigNetwork->pName = Extra_UtilStrsav(pName);
- }
-
- return abcAigNetwork;
-}
-
-
-Abc_Aig_t* AigBitblaster::currentAigM() {
- return (Abc_Aig_t*)(currentAigNtk()->pManFunc);
-}
-
-AigBitblaster::AigBitblaster()
- : TBitblaster<Abc_Obj_t*>()
- , d_aigCache()
- , d_bbAtoms()
- , d_aigOutputNode(NULL)
-{
- d_nullContext = new context::Context();
- d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster");
- MinisatEmptyNotify* notify = new MinisatEmptyNotify();
- d_satSolver->setNotify(notify);
-}
-
-AigBitblaster::~AigBitblaster() {
- Assert (abcAigNetwork == NULL);
- delete d_nullContext;
-}
-
-Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
- Assert (node.getType().isBoolean());
- Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n";
-
- if (hasAig(node))
- return getAig(node);
-
- Abc_Obj_t* result = NULL;
-
- Debug("bitvector-aig") << "AigBitblaster::convertToAig " << node <<"\n";
- switch (node.getKind()) {
- case kind::AND:
- {
- result = bbFormula(node[0]);
- for (unsigned i = 1; i < node.getNumChildren(); ++i) {
- Abc_Obj_t* child = bbFormula(node[i]);
- result = mkAnd(result, child);
- }
- break;
- }
- case kind::OR:
- {
- result = bbFormula(node[0]);
- for (unsigned i = 1; i < node.getNumChildren(); ++i) {
- Abc_Obj_t* child = bbFormula(node[i]);
- result = mkOr(result, child);
- }
- break;
- }
- case kind::IFF:
- {
- Assert (node.getNumChildren() == 2);
- Abc_Obj_t* child1 = bbFormula(node[0]);
- Abc_Obj_t* child2 = bbFormula(node[1]);
-
- result = mkIff(child1, child2);
- break;
- }
- case kind::XOR:
- {
- result = bbFormula(node[0]);
- for (unsigned i = 1; i < node.getNumChildren(); ++i) {
- Abc_Obj_t* child = bbFormula(node[i]);
- result = mkXor(result, child);
- }
- break;
- }
- case kind::IMPLIES:
- {
- Assert (node.getNumChildren() == 2);
- Abc_Obj_t* child1 = bbFormula(node[0]);
- Abc_Obj_t* child2 = bbFormula(node[1]);
-
- result = mkOr(mkNot(child1), child2);
- break;
- }
- case kind::ITE:
- {
- Assert (node.getNumChildren() == 3);
- Abc_Obj_t* a = bbFormula(node[0]);
- Abc_Obj_t* b = bbFormula(node[1]);
- Abc_Obj_t* c = bbFormula(node[2]);
- result = mkIte(a, b, c);
- break;
- }
- case kind::NOT:
- {
- Abc_Obj_t* child1 = bbFormula(node[0]);
- result = mkNot(child1);
- break;
- }
- case kind::CONST_BOOLEAN:
- {
- result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>();
- break;
- }
- case kind::VARIABLE:
- case kind::SKOLEM:
- {
- result = mkInput(node);
- break;
- }
- default:
- bbAtom(node);
- result = getBBAtom(node);
- }
-
- cacheAig(node, result);
- Debug("bitvector-aig") << "AigBitblaster::bbFormula done " << node << " => " << result <<"\n";
- return result;
-}
-
-void AigBitblaster::bbAtom(TNode node) {
- if (hasBBAtom(node)) {
- return;
- }
-
- Debug("bitvector-bitblast") << "Bitblasting atom " << node <<"\n";
-
- // the bitblasted definition of the atom
- Node normalized = Rewriter::rewrite(node);
- Abc_Obj_t* atom_bb = (d_atomBBStrategies[normalized.getKind()])(normalized, this);
- storeBBAtom(node, atom_bb);
- Debug("bitvector-bitblast") << "Done bitblasting atom " << node <<"\n";
-}
-
-void AigBitblaster::bbTerm(TNode node, Bits& bits) {
- if (hasBBTerm(node)) {
- getBBTerm(node, bits);
- return;
- }
-
- Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
- d_termBBStrategies[node.getKind()] (node, bits, this);
-
- Assert (bits.size() == utils::getSize(node));
- storeBBTerm(node, bits);
-}
-
-
-void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
- Assert (!hasAig(node));
- d_aigCache.insert(std::make_pair(node, aig));
-}
-bool AigBitblaster::hasAig(TNode node) {
- return d_aigCache.find(node) != d_aigCache.end();
-}
-Abc_Obj_t* AigBitblaster::getAig(TNode node) {
- Assert(hasAig(node));
- Debug("bitvector-aig") << "AigSimplifer::getAig " << node << " => " << d_aigCache.find(node)->second <<"\n";
- return d_aigCache.find(node)->second;
-}
-
-void AigBitblaster::makeVariable(TNode node, Bits& bits) {
-
- for (unsigned i = 0; i < utils::getSize(node); ++i) {
- Node bit = utils::mkBitOf(node, i);
- Abc_Obj_t* input = mkInput(bit);
- cacheAig(bit, input);
- bits.push_back(input);
- }
-}
-
-Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
- Assert (!hasInput(input));
- Assert(input.getKind() == kind::BITVECTOR_BITOF ||
- (input.getType().isBoolean() &&
- (input.getKind() == kind::VARIABLE ||
- input.getKind() == kind::SKOLEM)));
- Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
- // d_aigCache.insert(std::make_pair(input, aig_input));
- d_nodeToAigInput.insert(std::make_pair(input, aig_input));
- Debug("bitvector-aig") << "AigSimplifer::mkInput " << input << " " << aig_input <<"\n";
- return aig_input;
-}
-
-bool AigBitblaster::hasInput(TNode input) {
- return d_nodeToAigInput.find(input) != d_nodeToAigInput.end();
-}
-
-bool AigBitblaster::solve(TNode node) {
- // setting output of network to be the query
- Assert (d_aigOutputNode == NULL);
- Abc_Obj_t* query = bbFormula(node);
- d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk());
- Abc_ObjAddFanin(d_aigOutputNode, query);
-
- simplifyAig();
- convertToCnfAndAssert();
- // no need to use abc anymore
-
- TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime);
- prop::SatValue result = d_satSolver->solve();
-
- Assert (result != prop::SAT_VALUE_UNKNOWN);
- return result == prop::SAT_VALUE_TRUE;
-}
-
-
-void addAliases(Abc_Frame_t* pAbc);
-
-void AigBitblaster::simplifyAig() {
- TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime);
-
- Abc_AigCleanup(currentAigM());
- Assert (Abc_NtkCheck(currentAigNtk()));
-
- const char* command = options::bitvectorAigSimplifications().c_str();
- Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
- Abc_FrameSetCurrentNetwork(pAbc, currentAigNtk());
-
- addAliases(pAbc);
- if ( Cmd_CommandExecute( pAbc, command ) ) {
- fprintf( stdout, "Cannot execute command \"%s\".\n", command );
- exit(-1);
- }
- abcAigNetwork = Abc_FrameReadNtk(pAbc);
-}
-
-
-void AigBitblaster::convertToCnfAndAssert() {
- TimerStat::CodeTimer cnfConversionTimer(d_statistics.d_cnfConversionTime);
-
- Aig_Man_t * pMan = NULL;
- Cnf_Dat_t * pCnf = NULL;
- assert( Abc_NtkIsStrash(currentAigNtk()) );
-
- // convert to the AIG manager
- pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );
- Abc_Stop();
-
- // // free old network
- // Abc_NtkDelete(currentAigNtk());
- // abcAigNetwork = NULL;
-
- Assert (pMan != NULL);
- Assert (Aig_ManCheck(pMan));
- pCnf = Cnf_DeriveFast( pMan, 0 );
-
- assertToSatSolver(pCnf);
-
- Cnf_DataFree( pCnf );
- Cnf_ManFree();
- Aig_ManStop(pMan);
-}
-
-void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
- unsigned numVariables = pCnf->nVars;
- unsigned numClauses = pCnf->nClauses;
-
- d_statistics.d_numVariables += numVariables;
- d_statistics.d_numClauses += numClauses;
-
- // create variables in the sat solver
- std::vector<prop::SatVariable> sat_variables;
- for (unsigned i = 0; i < numVariables; ++i) {
- sat_variables.push_back(d_satSolver->newVar(false, false, false));
- }
-
- // construct clauses and add to sat solver
- int * pLit, * pStop;
- for (unsigned i = 0; i < numClauses; i++ ) {
- prop::SatClause clause;
- for (pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ ) {
- int int_lit = Cnf_Lit2Var(*pLit);
- Assert (int_lit != 0);
- unsigned index = int_lit < 0? -int_lit : int_lit;
- Assert (index - 1 < sat_variables.size());
- prop::SatLiteral lit(sat_variables[index-1], int_lit < 0);
- clause.push_back(lit);
- }
- d_satSolver->addClause(clause, false);
- }
-}
-
-void addAliases(Abc_Frame_t* pAbc) {
- std::vector<std::string> aliases;
- aliases.push_back("alias b balance");
- aliases.push_back("alias rw rewrite");
- aliases.push_back("alias rwz rewrite -z");
- aliases.push_back("alias rf refactor");
- aliases.push_back("alias rfz refactor -z");
- aliases.push_back("alias re restructure");
- aliases.push_back("alias rez restructure -z");
- aliases.push_back("alias rs resub");
- aliases.push_back("alias rsz resub -z");
- aliases.push_back("alias rsk6 rs -K 6");
- aliases.push_back("alias rszk5 rsz -K 5");
- aliases.push_back("alias bl b -l");
- aliases.push_back("alias rwl rw -l");
- aliases.push_back("alias rwzl rwz -l");
- aliases.push_back("alias rwzl rwz -l");
- aliases.push_back("alias rfl rf -l");
- aliases.push_back("alias rfzl rfz -l");
- aliases.push_back("alias brw \"b; rw\"");
-
- for (unsigned i = 0; i < aliases.size(); ++i) {
- if ( Cmd_CommandExecute( pAbc, aliases[i].c_str() ) ) {
- fprintf( stdout, "Cannot execute command \"%s\".\n", aliases[i].c_str() );
- exit(-1);
- }
- }
-}
-
-bool AigBitblaster::hasBBAtom(TNode atom) const {
- return d_bbAtoms.find(atom) != d_bbAtoms.end();
-}
-
-void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
- d_bbAtoms.insert(std::make_pair(atom, atom_bb));
-}
-
-Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
- Assert (hasBBAtom(atom));
- return d_bbAtoms.find(atom)->second;
-}
-
-AigBitblaster::Statistics::Statistics()
- : d_numClauses("theory::bv::AigBitblaster::numClauses", 0)
- , d_numVariables("theory::bv::AigBitblaster::numVariables", 0)
- , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime")
- , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
- , d_solveTime("theory::bv::AigBitblaster::solveTime")
-{
- StatisticsRegistry::registerStat(&d_numClauses);
- StatisticsRegistry::registerStat(&d_numVariables);
- StatisticsRegistry::registerStat(&d_simplificationTime);
- StatisticsRegistry::registerStat(&d_cnfConversionTime);
- StatisticsRegistry::registerStat(&d_solveTime);
-}
-
-AigBitblaster::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numClauses);
- StatisticsRegistry::unregisterStat(&d_numVariables);
- StatisticsRegistry::unregisterStat(&d_simplificationTime);
- StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
- StatisticsRegistry::unregisterStat(&d_solveTime);
-}
-
-
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-
-#else // CVC4_USE_ABC
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-template <> inline
-std::string toString<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) {
- Unreachable("Don't know how to print AIG");
-}
-
-
-template <> inline
-Abc_Obj_t* mkTrue<Abc_Obj_t*>() {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkFalse<Abc_Obj_t*>() {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
- Unreachable();
- return NULL;
-}
-
-
-template <> inline
-Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkXor<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
- Unreachable();
- return NULL;
-}
-
-template <> inline
-Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
- Unreachable();
- return NULL;
-}
-
-
-Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
-
-Abc_Ntk_t* AigBitblaster::currentAigNtk() {
- Unreachable();
- return NULL;
-}
-
-
-Abc_Aig_t* AigBitblaster::currentAigM() {
- Unreachable();
- return NULL;
-}
-
-AigBitblaster::~AigBitblaster() {
- Unreachable();
-}
-
-Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
- Unreachable();
- return NULL;
-}
-
-void AigBitblaster::bbAtom(TNode node) {
- Unreachable();
-}
-
-void AigBitblaster::bbTerm(TNode node, Bits& bits) {
- Unreachable();
-}
-
-
-void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
- Unreachable();
-}
-bool AigBitblaster::hasAig(TNode node) {
- Unreachable();
- return false;
-}
-Abc_Obj_t* AigBitblaster::getAig(TNode node) {
- Unreachable();
- return NULL;
-}
-
-void AigBitblaster::makeVariable(TNode node, Bits& bits) {
- Unreachable();
-}
-
-Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
- Unreachable();
- return NULL;
-}
-
-bool AigBitblaster::hasInput(TNode input) {
- Unreachable();
- return false;
-}
-
-bool AigBitblaster::solve(TNode node) {
- Unreachable();
- return false;
-}
-void AigBitblaster::simplifyAig() {
- Unreachable();
-}
-
-void AigBitblaster::convertToCnfAndAssert() {
- Unreachable();
-}
-
-void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
- Unreachable();
-}
-bool AigBitblaster::hasBBAtom(TNode atom) const {
- Unreachable();
- return false;
-}
-
-void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
- Unreachable();
-}
-
-Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
- Unreachable();
- return NULL;
-}
-
-AigBitblaster::Statistics::Statistics()
- : d_numClauses("theory::bv::AigBitblaster::numClauses", 0)
- , d_numVariables("theory::bv::AigBitblaster::numVariables", 0)
- , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime")
- , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
- , d_solveTime("theory::bv::AigBitblaster::solveTime")
-{}
-
-AigBitblaster::Statistics::~Statistics() {}
-
-AigBitblaster::AigBitblaster() {
- Unreachable();
-}
-
-} // namespace bv
-} // namespace theory
-} // namespace CVC4
-
-
-#endif // CVC4_USE_ABC
-
-#endif // __CVC4__AIG__BITBLASTER_H
#include "bitblast_strategies_template.h"
#include "prop/sat_solver.h"
#include "theory/valuation.h"
+#include "theory/theory_registrar.h"
class Abc_Obj_t_;
typedef Abc_Obj_t_ Abc_Obj_t;
void collectModelInfo(TheoryModel* m, bool fullModel);
};
+class BitblastingRegistrar: public prop::Registrar {
+ EagerBitblaster* d_bitblaster;
+public:
+ BitblastingRegistrar(EagerBitblaster* bb)
+ : d_bitblaster(bb)
+ {}
+ void preRegister(Node n);
+}; /* class Registrar */
+
class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
#include "theory/bv/bv_eager_solver.h"
#include "theory/bv/bitblaster_template.h"
-#include "theory/bv/eager_bitblaster.h"
-#include "theory/bv/aig_bitblaster.h"
+#include "theory/bv/options.h"
using namespace std;
using namespace CVC4;
#include "theory/bv/bv_subtheory_bitblast.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/lazy_bitblaster.h"
+#include "theory/bv/bitblaster_template.h"
#include "theory/bv/bv_quick_check.h"
#include "theory/bv/options.h"
+#include "theory/bv/abstraction.h"
#include "theory/decision_attributes.h"
#include "decision/options.h"
--- /dev/null
+/********************* */
+/*! \file eager_bitblaster.cpp
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): lianah
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief
+ **
+ ** Bitblaster for the eager bv solver.
+ **/
+
+#include "cvc4_private.h"
+
+#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/options.h"
+#include "theory/theory_model.h"
+#include "theory/bv/theory_bv.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_factory.h"
+
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+void BitblastingRegistrar::preRegister(Node n) {
+ d_bitblaster->bbAtom(n);
+};
+
+EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
+ : TBitblaster<Node>()
+ , d_bv(theory_bv)
+ , d_bbAtoms()
+ , d_variables()
+{
+ d_bitblastingRegistrar = new BitblastingRegistrar(this);
+ d_nullContext = new context::Context();
+
+ d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
+ d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
+
+ MinisatEmptyNotify* notify = new MinisatEmptyNotify();
+ d_satSolver->setNotify(notify);
+}
+
+EagerBitblaster::~EagerBitblaster() {
+ delete d_cnfStream;
+ delete d_satSolver;
+ delete d_nullContext;
+ delete d_bitblastingRegistrar;
+}
+
+void EagerBitblaster::bbFormula(TNode node) {
+ d_cnfStream->convertAndAssert(node, false, false);
+}
+
+/**
+ * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
+ * NOTE: duplicate clauses are not detected because of marker literal
+ * @param node the atom to be bitblasted
+ *
+ */
+void EagerBitblaster::bbAtom(TNode node) {
+ node = node.getKind() == kind::NOT? node[0] : node;
+ if (node.getKind() == kind::BITVECTOR_BITOF)
+ return;
+ if (hasBBAtom(node)) {
+ return;
+ }
+
+ Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+
+ // the bitblasted definition of the atom
+ Node normalized = Rewriter::rewrite(node);
+ Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
+ Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
+ normalized;
+ // asserting that the atom is true iff the definition holds
+ Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+
+ AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
+ storeBBAtom(node, atom_definition);
+ d_cnfStream->convertAndAssert(atom_definition, false, false);
+}
+
+void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
+ // no need to store the definition for the lazy bit-blaster
+ d_bbAtoms.insert(atom);
+}
+
+bool EagerBitblaster::hasBBAtom(TNode atom) const {
+ return d_bbAtoms.find(atom) != d_bbAtoms.end();
+}
+
+void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
+ if (hasBBTerm(node)) {
+ getBBTerm(node, bits);
+ return;
+ }
+
+ Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+
+ d_termBBStrategies[node.getKind()] (node, bits, this);
+
+ Assert (bits.size() == utils::getSize(node));
+
+ storeBBTerm(node, bits);
+}
+
+void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
+ Assert(bits.size() == 0);
+ for (unsigned i = 0; i < utils::getSize(var); ++i) {
+ bits.push_back(utils::mkBitOf(var, i));
+ }
+ d_variables.insert(var);
+}
+
+Node EagerBitblaster::getBBAtom(TNode node) const {
+ return node;
+}
+
+
+/**
+ * Calls the solve method for the Sat Solver.
+ *
+ * @return true for sat, and false for unsat
+ */
+
+bool EagerBitblaster::solve() {
+ if (Trace.isOn("bitvector")) {
+ Trace("bitvector") << "EagerBitblaster::solve(). \n";
+ }
+ Debug("bitvector") << "EagerBitblaster::solve(). \n";
+ // TODO: clear some memory
+ // if (something) {
+ // NodeManager* nm= NodeManager::currentNM();
+ // Rewriter::garbageCollect();
+ // nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+ // }
+ return prop::SAT_VALUE_TRUE == d_satSolver->solve();
+}
+
+
+/**
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
+ *
+ * @return
+ */
+Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
+ if (!hasBBTerm(a)) {
+ Assert(isSharedTerm(a));
+ return Node();
+ }
+ Bits bits;
+ getBBTerm(a, bits);
+ Integer value(0);
+ for (int i = bits.size() -1; i >= 0; --i) {
+ prop::SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
+ prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+ bit_value = d_satSolver->value(bit);
+ Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+ } else {
+ // the bit is unconstrainted so we can give it an arbitrary value
+ bit_value = prop::SAT_VALUE_FALSE;
+ }
+ Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+ value = value * 2 + bit_int;
+ }
+ return utils::mkConst(BitVector(bits.size(), value));
+}
+
+
+void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+ TNodeSet::const_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") << "TLazyBitblaster::collectModelInfo (assert (= "
+ << var << " "
+ << const_value << "))\n";
+ m->assertEquality(var, const_value, true);
+ }
+ }
+ }
+}
+
+bool EagerBitblaster::isSharedTerm(TNode node) {
+ return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
+}
+++ /dev/null
-/********************* */
-/*! \file eager_bitblaster.h
- ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): lianah
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief
- **
- ** Bitblaster for the lazy bv solver.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__EAGER__BITBLASTER_H
-#define __CVC4__EAGER__BITBLASTER_H
-
-
-#include "theory/theory_registrar.h"
-#include "theory/bv/bitblaster_template.h"
-#include "theory/bv/options.h"
-#include "theory/theory_model.h"
-#include "prop/cnf_stream.h"
-#include "prop/sat_solver_factory.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-
-class BitblastingRegistrar: public prop::Registrar {
- EagerBitblaster* d_bitblaster;
-public:
- BitblastingRegistrar(EagerBitblaster* bb)
- : d_bitblaster(bb)
- {}
- void preRegister(Node n) {
- d_bitblaster->bbAtom(n);
- };
-
-};/* class Registrar */
-
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
- : TBitblaster<Node>()
- , d_bv(theory_bv)
- , d_bbAtoms()
- , d_variables()
-{
- d_bitblastingRegistrar = new BitblastingRegistrar(this);
- d_nullContext = new context::Context();
-
- d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
-
- MinisatEmptyNotify* notify = new MinisatEmptyNotify();
- d_satSolver->setNotify(notify);
-}
-
-EagerBitblaster::~EagerBitblaster() {
- delete d_cnfStream;
- delete d_satSolver;
- delete d_nullContext;
- delete d_bitblastingRegistrar;
-}
-
-void EagerBitblaster::bbFormula(TNode node) {
- d_cnfStream->convertAndAssert(node, false, false);
-}
-
-/**
- * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
- * NOTE: duplicate clauses are not detected because of marker literal
- * @param node the atom to be bitblasted
- *
- */
-void EagerBitblaster::bbAtom(TNode node) {
- node = node.getKind() == kind::NOT? node[0] : node;
- if (node.getKind() == kind::BITVECTOR_BITOF)
- return;
- if (hasBBAtom(node)) {
- return;
- }
-
- Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
-
- // the bitblasted definition of the atom
- Node normalized = Rewriter::rewrite(node);
- Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
- Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
- normalized;
- // asserting that the atom is true iff the definition holds
- Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
-
- AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
- storeBBAtom(node, atom_definition);
- d_cnfStream->convertAndAssert(atom_definition, false, false);
-}
-
-void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
- // no need to store the definition for the lazy bit-blaster
- d_bbAtoms.insert(atom);
-}
-
-bool EagerBitblaster::hasBBAtom(TNode atom) const {
- return d_bbAtoms.find(atom) != d_bbAtoms.end();
-}
-
-void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
- if (hasBBTerm(node)) {
- getBBTerm(node, bits);
- return;
- }
-
- Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
-
- d_termBBStrategies[node.getKind()] (node, bits, this);
-
- Assert (bits.size() == utils::getSize(node));
-
- storeBBTerm(node, bits);
-}
-
-void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
- Assert(bits.size() == 0);
- for (unsigned i = 0; i < utils::getSize(var); ++i) {
- bits.push_back(utils::mkBitOf(var, i));
- }
- d_variables.insert(var);
-}
-
-Node EagerBitblaster::getBBAtom(TNode node) const {
- return node;
-}
-
-
-/**
- * Calls the solve method for the Sat Solver.
- *
- * @return true for sat, and false for unsat
- */
-
-bool EagerBitblaster::solve() {
- if (Trace.isOn("bitvector")) {
- Trace("bitvector") << "EagerBitblaster::solve(). \n";
- }
- Debug("bitvector") << "EagerBitblaster::solve(). \n";
- // TODO: clear some memory
- // if (something) {
- // NodeManager* nm= NodeManager::currentNM();
- // Rewriter::garbageCollect();
- // nm->reclaimZombiesUntil(options::zombieHuntThreshold());
- // }
- return prop::SAT_VALUE_TRUE == d_satSolver->solve();
-}
-
-
-/**
- * Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned.
- *
- * @param a
- * @param fullModel whether to create a "full model," i.e., add
- * constants to equivalence classes that don't already have them
- *
- * @return
- */
-Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
- if (!hasBBTerm(a)) {
- Assert(isSharedTerm(a));
- return Node();
- }
- Bits bits;
- getBBTerm(a, bits);
- Integer value(0);
- for (int i = bits.size() -1; i >= 0; --i) {
- prop::SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
- prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
- bit_value = d_satSolver->value(bit);
- Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
- } else {
- // the bit is unconstrainted so we can give it an arbitrary value
- bit_value = prop::SAT_VALUE_FALSE;
- }
- Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
- value = value * 2 + bit_int;
- }
- return utils::mkConst(BitVector(bits.size(), value));
-}
-
-
-void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
- TNodeSet::const_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") << "TLazyBitblaster::collectModelInfo (assert (= "
- << var << " "
- << const_value << "))\n";
- m->assertEquality(var, const_value, true);
- }
- }
- }
-}
-
-bool EagerBitblaster::isSharedTerm(TNode node) {
- return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
-}
-
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-
-
-#endif
--- /dev/null
+/********************* */
+/*! \file lazy_bitblaster.cpp
+** \verbatim
+** Original author: Liana Hadarean
+** Major contributors: none
+** Minor contributors (to current version): lianah
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2013 New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief
+**
+** Bitblaster for the lazy bv solver.
+**/
+
+#include "cvc4_private.h"
+#include "bitblaster_template.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.h"
+#include "theory/bv/options.h"
+#include "theory/theory_model.h"
+#include "theory/bv/abstraction.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+
+TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
+ : TBitblaster<Node>()
+ , d_bv(bv)
+ , d_ctx(c)
+ , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(c))
+ , d_explanations(new(true) ExplanationMap(c))
+ , d_variables()
+ , d_bbAtoms()
+ , d_abstraction(NULL)
+ , d_emptyNotify(emptyNotify)
+ , d_name(name)
+ , d_statistics(name) {
+ d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
+ d_nullRegistrar = new prop::NullRegistrar();
+ d_nullContext = new context::Context();
+ d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+ d_nullRegistrar,
+ d_nullContext);
+
+ prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
+ (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
+ (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
+
+ d_satSolver->setNotify(notify);
+}
+
+void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
+ d_abstraction = abs;
+}
+
+TLazyBitblaster::~TLazyBitblaster() {
+ delete d_cnfStream;
+ delete d_nullRegistrar;
+ delete d_nullContext;
+ 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 TLazyBitblaster::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;
+
+ /// if we are using bit-vector abstraction bit-blast the original interpretation
+ if (options::bvAbstraction() &&
+ d_abstraction != NULL &&
+ d_abstraction->isAbstraction(node)) {
+ // node must be of the form P(args) = bv1
+ Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node));
+
+ Node atom_bb;
+ if (expansion.getKind() == kind::CONST_BOOLEAN) {
+ atom_bb = expansion;
+ } else {
+ Assert (expansion.getKind() == kind::AND);
+ std::vector<Node> atoms;
+ for (unsigned i = 0; i < expansion.getNumChildren(); ++i) {
+ Node normalized_i = Rewriter::rewrite(expansion[i]);
+ Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ?
+ Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](normalized_i, this)) :
+ normalized_i;
+ atoms.push_back(atom_i);
+ }
+ atom_bb = utils::mkAnd(atoms);
+ }
+ Assert (!atom_bb.isNull());
+ Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+ storeBBAtom(node, atom_bb);
+ d_cnfStream->convertAndAssert(atom_definition, false, false);
+ return;
+ }
+
+ // the bitblasted definition of the atom
+ Node normalized = Rewriter::rewrite(node);
+ Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
+ Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
+ normalized;
+ // asserting that the atom is true iff the definition holds
+ Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+ storeBBAtom(node, atom_bb);
+ d_cnfStream->convertAndAssert(atom_definition, false, false);
+}
+
+void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
+ // no need to store the definition for the lazy bit-blaster
+ d_bbAtoms.insert(atom);
+}
+
+bool TLazyBitblaster::hasBBAtom(TNode atom) const {
+ return d_bbAtoms.find(atom) != d_bbAtoms.end();
+}
+
+
+void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
+ Assert(bits.size() == 0);
+ for (unsigned i = 0; i < utils::getSize(var); ++i) {
+ bits.push_back(utils::mkBitOf(var, i));
+ }
+ d_variables.insert(var);
+}
+
+uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
+ 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, seen);
+ return size;
+}
+
+// cnf conversion ensures the atom represents itself
+Node TLazyBitblaster::getBBAtom(TNode node) const {
+ return node;
+}
+
+void TLazyBitblaster::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));
+
+ storeBBTerm(node, bits);
+}
+/// Public methods
+
+void TLazyBitblaster::addAtom(TNode atom) {
+ d_cnfStream->ensureLiteral(atom);
+ prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
+ d_satSolver->addMarkerLiteral(lit);
+}
+
+void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
+ prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
+
+ ++(d_statistics.d_numExplainedPropagations);
+ if (options::bvEagerExplanations()) {
+ Assert (d_explanations->find(lit) != d_explanations->end());
+ const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
+ for (unsigned i = 0; i < literal_explanation.size(); ++i) {
+ explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
+ }
+ return;
+ }
+
+ std::vector<prop::SatLiteral> literal_explanation;
+ d_satSolver->explain(lit, 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 TLazyBitblaster::propagate() {
+ return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
+}
+
+bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
+ // strip the not
+ TNode atom;
+ if (lit.getKind() == kind::NOT) {
+ atom = lit[0];
+ } else {
+ atom = lit;
+ }
+
+ Assert (hasBBAtom(atom));
+
+ prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
+
+ if(lit.getKind() == kind::NOT) {
+ markerLit = ~markerLit;
+ }
+
+ Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n";
+ Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n";
+
+ prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
+
+ d_assertedAtoms->push_back(markerLit);
+
+ return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN;
+}
+
+/**
+ * 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 TLazyBitblaster::solve() {
+ if (Trace.isOn("bitvector")) {
+ Trace("bitvector") << "TLazyBitblaster::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") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
+ return prop::SAT_VALUE_TRUE == d_satSolver->solve();
+}
+
+prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
+ if (Trace.isOn("bitvector")) {
+ Trace("bitvector") << "TLazyBitblaster::solveWithBudget() 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") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
+ return d_satSolver->solve(budget);
+}
+
+
+void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) {
+ prop::SatClause conflictClause;
+ d_satSolver->getUnsatCore(conflictClause);
+
+ for (unsigned i = 0; i < conflictClause.size(); i++) {
+ prop::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);
+ }
+}
+
+TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
+ d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0),
+ d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0),
+ d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0),
+ d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0),
+ d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0),
+ d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
+ d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
+{
+ StatisticsRegistry::registerStat(&d_numTermClauses);
+ StatisticsRegistry::registerStat(&d_numAtomClauses);
+ StatisticsRegistry::registerStat(&d_numTerms);
+ StatisticsRegistry::registerStat(&d_numAtoms);
+ StatisticsRegistry::registerStat(&d_numExplainedPropagations);
+ StatisticsRegistry::registerStat(&d_numBitblastingPropagations);
+ StatisticsRegistry::registerStat(&d_bitblastTimer);
+}
+
+
+TLazyBitblaster::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_numTermClauses);
+ StatisticsRegistry::unregisterStat(&d_numAtomClauses);
+ StatisticsRegistry::unregisterStat(&d_numTerms);
+ StatisticsRegistry::unregisterStat(&d_numAtoms);
+ StatisticsRegistry::unregisterStat(&d_numExplainedPropagations);
+ StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations);
+ StatisticsRegistry::unregisterStat(&d_bitblastTimer);
+}
+
+bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
+ if(options::bvEagerExplanations()) {
+ // compute explanation
+ if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
+ std::vector<prop::SatLiteral> literal_explanation;
+ d_lazyBB->d_satSolver->explain(lit, literal_explanation);
+ d_lazyBB->d_explanations->insert(lit, literal_explanation);
+ } else {
+ // we propagated it at a lower level
+ return true;
+ }
+ }
+ ++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
+ TNode atom = d_cnf->getNode(lit);
+ return d_bv->storePropagation(atom, SUB_BITBLAST);
+}
+
+void TLazyBitblaster::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 TLazyBitblaster::MinisatNotify::safePoint() {
+ d_bv->d_out->safePoint();
+}
+
+EqualityStatus TLazyBitblaster::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);
+ theory::EqualityStatus status = theory::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])) {
+ prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]);
+ prop::SatValue a_lit_value = d_satSolver->value(a_lit);
+ if (a_lit_value != prop::SAT_VALUE_UNKNOWN) {
+ prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]);
+ prop::SatValue b_lit_value = d_satSolver->value(b_lit);
+ if (b_lit_value != prop::SAT_VALUE_UNKNOWN) {
+ if (a_lit_value != b_lit_value) {
+ return theory::EQUALITY_FALSE_IN_MODEL;
+ }
+ } else {
+ status = theory::EQUALITY_UNKNOWN;
+ }
+ } {
+ status = theory::EQUALITY_UNKNOWN;
+ }
+ } else {
+ status = theory::EQUALITY_UNKNOWN;
+ }
+ }
+
+ return status;
+
+ } else {
+ return theory::EQUALITY_UNKNOWN;
+ }
+}
+
+
+bool TLazyBitblaster::isSharedTerm(TNode node) {
+ return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
+}
+
+bool TLazyBitblaster::hasValue(TNode a) {
+ Assert (hasBBTerm(a));
+ Bits bits;
+ getBBTerm(a, bits);
+ for (int i = bits.size() -1; i >= 0; --i) {
+ prop::SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
+ prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+ bit_value = d_satSolver->value(bit);
+ if (bit_value == prop::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 TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
+ if (!hasBBTerm(a)) {
+ Assert(isSharedTerm(a));
+ return Node();
+ }
+ Bits bits;
+ getBBTerm(a, bits);
+ Integer value(0);
+ for (int i = bits.size() -1; i >= 0; --i) {
+ prop::SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
+ prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+ bit_value = d_satSolver->value(bit);
+ Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+ } else {
+ // the bit is unconstrainted so we can give it an arbitrary value
+ bit_value = prop::SAT_VALUE_FALSE;
+ }
+ Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+ value = value * 2 + bit_int;
+ }
+ return utils::mkConst(BitVector(bits.size(), value));
+}
+
+void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+ TNodeSet::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") << "TLazyBitblaster::collectModelInfo (assert (= "
+ << var << " "
+ << const_value << "))\n";
+ m->assertEquality(var, const_value, true);
+ }
+ }
+ }
+}
+
+void TLazyBitblaster::clearSolver() {
+ Assert (d_ctx->getLevel() == 0);
+ delete d_satSolver;
+ delete d_cnfStream;
+ d_assertedAtoms->deleteSelf();
+ d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
+ d_explanations->deleteSelf();
+ d_explanations = new(true) ExplanationMap(d_ctx);
+ d_bbAtoms.clear();
+ d_variables.clear();
+ d_termCache.clear();
+
+ // recreate sat solver
+ d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
+ d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+ new prop::NullRegistrar(),
+ new context::Context());
+
+ prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
+ (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
+ (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
+ d_satSolver->setNotify(notify);
+}
+++ /dev/null
-/********************* */
-/*! \file lazy_bitblaster.h
-** \verbatim
-** Original author: Liana Hadarean
-** Major contributors: none
-** Minor contributors (to current version): lianah
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013 New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief
-**
-** Bitblaster for the lazy bv solver.
-**/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__LAZY__BITBLASTER_H
-#define __CVC4__LAZY__BITBLASTER_H
-
-
-#include "bitblaster_template.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.h"
-#include "theory/bv/options.h"
-#include "theory/theory_model.h"
-#include "theory/bv/abstraction.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
- : TBitblaster<Node>()
- , d_bv(bv)
- , d_ctx(c)
- , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(c))
- , d_explanations(new(true) ExplanationMap(c))
- , d_variables()
- , d_bbAtoms()
- , d_abstraction(NULL)
- , d_emptyNotify(emptyNotify)
- , d_name(name)
- , d_statistics(name) {
- d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
- d_nullRegistrar = new prop::NullRegistrar();
- d_nullContext = new context::Context();
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
- d_nullRegistrar,
- d_nullContext);
-
- prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
- (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
- (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
-
- d_satSolver->setNotify(notify);
-}
-
-void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
- d_abstraction = abs;
-}
-
-TLazyBitblaster::~TLazyBitblaster() {
- delete d_cnfStream;
- delete d_nullRegistrar;
- delete d_nullContext;
- 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 TLazyBitblaster::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;
-
- /// if we are using bit-vector abstraction bit-blast the original interpretation
- if (options::bvAbstraction() &&
- d_abstraction != NULL &&
- d_abstraction->isAbstraction(node)) {
- // node must be of the form P(args) = bv1
- Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node));
-
- Node atom_bb;
- if (expansion.getKind() == kind::CONST_BOOLEAN) {
- atom_bb = expansion;
- } else {
- Assert (expansion.getKind() == kind::AND);
- std::vector<Node> atoms;
- for (unsigned i = 0; i < expansion.getNumChildren(); ++i) {
- Node normalized_i = Rewriter::rewrite(expansion[i]);
- Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ?
- Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](normalized_i, this)) :
- normalized_i;
- atoms.push_back(atom_i);
- }
- atom_bb = utils::mkAnd(atoms);
- }
- Assert (!atom_bb.isNull());
- Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
- storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(atom_definition, false, false);
- return;
- }
-
- // the bitblasted definition of the atom
- Node normalized = Rewriter::rewrite(node);
- Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
- Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
- normalized;
- // asserting that the atom is true iff the definition holds
- Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
- storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(atom_definition, false, false);
-}
-
-void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
- // no need to store the definition for the lazy bit-blaster
- d_bbAtoms.insert(atom);
-}
-
-bool TLazyBitblaster::hasBBAtom(TNode atom) const {
- return d_bbAtoms.find(atom) != d_bbAtoms.end();
-}
-
-
-void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
- Assert(bits.size() == 0);
- for (unsigned i = 0; i < utils::getSize(var); ++i) {
- bits.push_back(utils::mkBitOf(var, i));
- }
- d_variables.insert(var);
-}
-
-uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
- 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, seen);
- return size;
-}
-
-// cnf conversion ensures the atom represents itself
-Node TLazyBitblaster::getBBAtom(TNode node) const {
- return node;
-}
-
-void TLazyBitblaster::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));
-
- storeBBTerm(node, bits);
-}
-/// Public methods
-
-void TLazyBitblaster::addAtom(TNode atom) {
- d_cnfStream->ensureLiteral(atom);
- prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
- d_satSolver->addMarkerLiteral(lit);
-}
-
-void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
- prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
-
- ++(d_statistics.d_numExplainedPropagations);
- if (options::bvEagerExplanations()) {
- Assert (d_explanations->find(lit) != d_explanations->end());
- const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
- for (unsigned i = 0; i < literal_explanation.size(); ++i) {
- explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
- }
- return;
- }
-
- std::vector<prop::SatLiteral> literal_explanation;
- d_satSolver->explain(lit, 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 TLazyBitblaster::propagate() {
- return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
-}
-
-bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
- // strip the not
- TNode atom;
- if (lit.getKind() == kind::NOT) {
- atom = lit[0];
- } else {
- atom = lit;
- }
-
- Assert (hasBBAtom(atom));
-
- prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
-
- if(lit.getKind() == kind::NOT) {
- markerLit = ~markerLit;
- }
-
- Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n";
- Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n";
-
- prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
-
- d_assertedAtoms->push_back(markerLit);
-
- return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN;
-}
-
-/**
- * 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 TLazyBitblaster::solve() {
- if (Trace.isOn("bitvector")) {
- Trace("bitvector") << "TLazyBitblaster::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") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
- return prop::SAT_VALUE_TRUE == d_satSolver->solve();
-}
-
-prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
- if (Trace.isOn("bitvector")) {
- Trace("bitvector") << "TLazyBitblaster::solveWithBudget() 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") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
- return d_satSolver->solve(budget);
-}
-
-
-void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) {
- prop::SatClause conflictClause;
- d_satSolver->getUnsatCore(conflictClause);
-
- for (unsigned i = 0; i < conflictClause.size(); i++) {
- prop::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);
- }
-}
-
-TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
- d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0),
- d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0),
- d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0),
- d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0),
- d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0),
- d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
- d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
-{
- StatisticsRegistry::registerStat(&d_numTermClauses);
- StatisticsRegistry::registerStat(&d_numAtomClauses);
- StatisticsRegistry::registerStat(&d_numTerms);
- StatisticsRegistry::registerStat(&d_numAtoms);
- StatisticsRegistry::registerStat(&d_numExplainedPropagations);
- StatisticsRegistry::registerStat(&d_numBitblastingPropagations);
- StatisticsRegistry::registerStat(&d_bitblastTimer);
-}
-
-
-TLazyBitblaster::Statistics::~Statistics() {
- StatisticsRegistry::unregisterStat(&d_numTermClauses);
- StatisticsRegistry::unregisterStat(&d_numAtomClauses);
- StatisticsRegistry::unregisterStat(&d_numTerms);
- StatisticsRegistry::unregisterStat(&d_numAtoms);
- StatisticsRegistry::unregisterStat(&d_numExplainedPropagations);
- StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations);
- StatisticsRegistry::unregisterStat(&d_bitblastTimer);
-}
-
-bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
- if(options::bvEagerExplanations()) {
- // compute explanation
- if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
- std::vector<prop::SatLiteral> literal_explanation;
- d_lazyBB->d_satSolver->explain(lit, literal_explanation);
- d_lazyBB->d_explanations->insert(lit, literal_explanation);
- } else {
- // we propagated it at a lower level
- return true;
- }
- }
- ++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
- TNode atom = d_cnf->getNode(lit);
- return d_bv->storePropagation(atom, SUB_BITBLAST);
-}
-
-void TLazyBitblaster::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 TLazyBitblaster::MinisatNotify::safePoint() {
- d_bv->d_out->safePoint();
-}
-
-EqualityStatus TLazyBitblaster::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);
- theory::EqualityStatus status = theory::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])) {
- prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]);
- prop::SatValue a_lit_value = d_satSolver->value(a_lit);
- if (a_lit_value != prop::SAT_VALUE_UNKNOWN) {
- prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]);
- prop::SatValue b_lit_value = d_satSolver->value(b_lit);
- if (b_lit_value != prop::SAT_VALUE_UNKNOWN) {
- if (a_lit_value != b_lit_value) {
- return theory::EQUALITY_FALSE_IN_MODEL;
- }
- } else {
- status = theory::EQUALITY_UNKNOWN;
- }
- } {
- status = theory::EQUALITY_UNKNOWN;
- }
- } else {
- status = theory::EQUALITY_UNKNOWN;
- }
- }
-
- return status;
-
- } else {
- return theory::EQUALITY_UNKNOWN;
- }
-}
-
-
-bool TLazyBitblaster::isSharedTerm(TNode node) {
- return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
-}
-
-bool TLazyBitblaster::hasValue(TNode a) {
- Assert (hasBBTerm(a));
- Bits bits;
- getBBTerm(a, bits);
- for (int i = bits.size() -1; i >= 0; --i) {
- prop::SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
- prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
- bit_value = d_satSolver->value(bit);
- if (bit_value == prop::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 TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
- if (!hasBBTerm(a)) {
- Assert(isSharedTerm(a));
- return Node();
- }
- Bits bits;
- getBBTerm(a, bits);
- Integer value(0);
- for (int i = bits.size() -1; i >= 0; --i) {
- prop::SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
- prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
- bit_value = d_satSolver->value(bit);
- Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
- } else {
- // the bit is unconstrainted so we can give it an arbitrary value
- bit_value = prop::SAT_VALUE_FALSE;
- }
- Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
- value = value * 2 + bit_int;
- }
- return utils::mkConst(BitVector(bits.size(), value));
-}
-
-void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
- TNodeSet::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") << "TLazyBitblaster::collectModelInfo (assert (= "
- << var << " "
- << const_value << "))\n";
- m->assertEquality(var, const_value, true);
- }
- }
- }
-}
-
-void TLazyBitblaster::clearSolver() {
- Assert (d_ctx->getLevel() == 0);
- delete d_satSolver;
- delete d_cnfStream;
- d_assertedAtoms->deleteSelf();
- d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
- d_explanations->deleteSelf();
- d_explanations = new(true) ExplanationMap(d_ctx);
- d_bbAtoms.clear();
- d_variables.clear();
- d_termCache.clear();
-
- // recreate sat solver
- d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
- new prop::NullRegistrar(),
- new context::Context());
-
- prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
- (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
- (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
- d_satSolver->setNotify(notify);
-}
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-#endif
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/bv/theory_bv.h"
-#include "theory/bv/eager_bitblaster.h"
+#include "theory/bv/bitblaster_template.h"
#include "expr/node.h"
#include "expr/node_manager.h"
#include "context/context.h"
projects / cvc5.git / commitdiff