This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
theory/builtin/type_enumerator.h \
theory/bv/abstraction.cpp \
theory/bv/abstraction.h \
- theory/bv/aig_bitblaster.cpp \
- theory/bv/bitblast_strategies_template.h \
- theory/bv/bitblast_utils.h \
- theory/bv/bitblaster_template.h \
+ theory/bv/bitblast/aig_bitblaster.cpp \
+ theory/bv/bitblast/aig_bitblaster.h \
+ theory/bv/bitblast/bitblast_strategies_template.h \
+ theory/bv/bitblast/bitblast_utils.h \
+ theory/bv/bitblast/bitblaster.h \
+ theory/bv/bitblast/eager_bitblaster.cpp \
+ theory/bv/bitblast/eager_bitblaster.h \
+ theory/bv/bitblast/lazy_bitblaster.cpp \
+ theory/bv/bitblast/lazy_bitblaster.h \
theory/bv/bv_eager_solver.cpp \
theory/bv/bv_eager_solver.h \
theory/bv/bv_inequality_graph.cpp \
theory/bv/bvgauss.h \
theory/bv/bvintropow2.cpp \
theory/bv/bvintropow2.h \
- theory/bv/eager_bitblaster.cpp \
- theory/bv/lazy_bitblaster.cpp \
theory/bv/slicer.cpp \
theory/bv/slicer.h \
theory/bv/theory_bv.cpp \
#include "proof/proof_utils.h"
#include "proof/sat_proof_implementation.h"
#include "prop/bvminisat/bvminisat.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/bitblaster.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_rewrite_rules.h"
+++ /dev/null
-/********************* */
-/*! \file aig_bitblaster.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief
- **
- ** Bitblaster for the lazy bv solver.
- **/
-
-#include "bitblaster_template.h"
-
-#include "cvc4_private.h"
-
-#include "base/cvc4_check.h"
-#include "options/bv_options.h"
-#include "prop/cnf_stream.h"
-#include "prop/sat_solver_factory.h"
-#include "smt/smt_statistics_registry.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();
- switch(options::bvSatSolver()) {
- case SAT_SOLVER_MINISAT: {
- prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext,
- smtStatisticsRegistry(),
- "AigBitblaster");
- MinisatEmptyNotify* notify = new MinisatEmptyNotify();
- minisat->setNotify(notify);
- d_satSolver = minisat;
- break;
- }
- case SAT_SOLVER_CRYPTOMINISAT:
- d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
- "AigBitblaster");
- break;
- default: CVC4_FATAL() << "Unknown SAT solver type";
- }
-}
-
-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::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::EQUAL:
- {
- if( node[0].getType().isBoolean() ){
- Assert (node.getNumChildren() == 2);
- Abc_Obj_t* child1 = bbFormula(node[0]);
- Abc_Obj_t* child2 = bbFormula(node[1]);
-
- result = mkIff(child1, child2);
- break;
- }
- //else, continue...
- }
- default:
- if( node.isVar() ){
- result = mkInput(node);
- }else{
- 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;
- }
- Assert( node.getType().isBitVector() );
-
- 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.isVar()));
- 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")
-{
- smtStatisticsRegistry()->registerStat(&d_numClauses);
- smtStatisticsRegistry()->registerStat(&d_numVariables);
- smtStatisticsRegistry()->registerStat(&d_simplificationTime);
- smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
- smtStatisticsRegistry()->registerStat(&d_solveTime);
-}
-
-AigBitblaster::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numClauses);
- smtStatisticsRegistry()->unregisterStat(&d_numVariables);
- smtStatisticsRegistry()->unregisterStat(&d_simplificationTime);
- smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
- smtStatisticsRegistry()->unregisterStat(&d_solveTime);
-}
-#endif // CVC4_USE_ABC
--- /dev/null
+/********************* */
+/*! \file aig_bitblaster.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief AIG bitblaster.
+ **
+ ** AIG bitblaster.
+ **/
+
+#include "cvc4_private.h"
+
+#include "theory/bv/bitblast/aig_bitblaster.h"
+
+#include "base/cvc4_check.h"
+#include "options/bv_options.h"
+#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
+
+#ifdef CVC4_USE_ABC
+
+extern "C" {
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "sat/cnf/cnf.h"
+
+extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters);
+}
+
+// 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;
+}
+
+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_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
+
+Abc_Ntk_t* AigBitblaster::currentAigNtk() {
+ if (!AigBitblaster::s_abcAigNetwork) {
+ Abc_Start();
+ s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
+ char pName[] = "CVC4::theory::bv::AigNetwork";
+ s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
+ }
+
+ return s_abcAigNetwork;
+}
+
+
+Abc_Aig_t* AigBitblaster::currentAigM() {
+ return (Abc_Aig_t*)(currentAigNtk()->pManFunc);
+}
+
+AigBitblaster::AigBitblaster()
+ : TBitblaster<Abc_Obj_t*>(),
+ d_nullContext(new context::Context()),
+ d_aigCache(),
+ d_bbAtoms(),
+ d_aigOutputNode(NULL)
+{
+ prop::SatSolver* solver = nullptr;
+ switch (options::bvSatSolver())
+ {
+ case SAT_SOLVER_MINISAT:
+ {
+ prop::BVSatSolverInterface* minisat =
+ prop::SatSolverFactory::createMinisat(
+ d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
+ MinisatEmptyNotify notify;
+ minisat->setNotify(¬ify);
+ solver = minisat;
+ break;
+ }
+ case SAT_SOLVER_CADICAL:
+ solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
+ "AigBitblaster");
+ break;
+ case SAT_SOLVER_CRYPTOMINISAT:
+ solver = prop::SatSolverFactory::createCryptoMinisat(
+ smtStatisticsRegistry(), "AigBitblaster");
+ break;
+ default: CVC4_FATAL() << "Unknown SAT solver type";
+ }
+ d_satSolver.reset(solver);
+}
+
+AigBitblaster::~AigBitblaster() {}
+
+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::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::EQUAL:
+ {
+ if( node[0].getType().isBoolean() ){
+ Assert (node.getNumChildren() == 2);
+ Abc_Obj_t* child1 = bbFormula(node[0]);
+ Abc_Obj_t* child2 = bbFormula(node[1]);
+
+ result = mkIff(child1, child2);
+ break;
+ }
+ //else, continue...
+ }
+ default:
+ if( node.isVar() ){
+ result = mkInput(node);
+ }else{
+ 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;
+ }
+ Assert( node.getType().isBitVector() );
+
+ 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.isVar()));
+ 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);
+ }
+ s_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());
+ // s_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")
+{
+ smtStatisticsRegistry()->registerStat(&d_numClauses);
+ smtStatisticsRegistry()->registerStat(&d_numVariables);
+ smtStatisticsRegistry()->registerStat(&d_simplificationTime);
+ smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->registerStat(&d_solveTime);
+}
+
+AigBitblaster::Statistics::~Statistics() {
+ smtStatisticsRegistry()->unregisterStat(&d_numClauses);
+ smtStatisticsRegistry()->unregisterStat(&d_numVariables);
+ smtStatisticsRegistry()->unregisterStat(&d_simplificationTime);
+ smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+#endif // CVC4_USE_ABC
--- /dev/null
+/********************* */
+/*! \file aig_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief AIG bitblaster.
+ **
+ ** AIG Bitblaster based on ABC.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "base/tls.h"
+
+class Abc_Obj_t_;
+typedef Abc_Obj_t_ Abc_Obj_t;
+
+class Abc_Ntk_t_;
+typedef Abc_Ntk_t_ Abc_Ntk_t;
+
+class Abc_Aig_t_;
+typedef Abc_Aig_t_ Abc_Aig_t;
+
+class Cnf_Dat_t_;
+typedef Cnf_Dat_t_ Cnf_Dat_t;
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class AigBitblaster : public TBitblaster<Abc_Obj_t*>
+{
+ public:
+ AigBitblaster();
+ ~AigBitblaster();
+
+ void makeVariable(TNode node, Bits& bits) override;
+ void bbTerm(TNode node, Bits& bits) override;
+ void bbAtom(TNode node) override;
+ Abc_Obj_t* bbFormula(TNode formula);
+ bool solve(TNode query);
+ static Abc_Aig_t* currentAigM();
+ static Abc_Ntk_t* currentAigNtk();
+
+ private:
+ typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
+ typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;
+
+ static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork;
+ std::unique_ptr<context::Context> d_nullContext;
+ std::unique_ptr<prop::SatSolver> d_satSolver;
+ TNodeAigMap d_aigCache;
+ NodeAigMap d_bbAtoms;
+
+ NodeAigMap d_nodeToAigInput;
+ // the thing we are checking for sat
+ Abc_Obj_t* d_aigOutputNode;
+
+ void addAtom(TNode atom);
+ void simplifyAig();
+ void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
+ Abc_Obj_t* getBBAtom(TNode atom) const override;
+ bool hasBBAtom(TNode atom) const override;
+ void cacheAig(TNode node, Abc_Obj_t* aig);
+ bool hasAig(TNode node);
+ Abc_Obj_t* getAig(TNode node);
+ Abc_Obj_t* mkInput(TNode input);
+ bool hasInput(TNode input);
+ void convertToCnfAndAssert();
+ void assertToSatSolver(Cnf_Dat_t* pCnf);
+ Node getModelFromSatSolver(TNode a, bool fullModel) override
+ {
+ Unreachable();
+ }
+
+ class Statistics
+ {
+ public:
+ IntStat d_numClauses;
+ IntStat d_numVariables;
+ TimerStat d_simplificationTime;
+ TimerStat d_cnfConversionTime;
+ TimerStat d_solveTime;
+ Statistics();
+ ~Statistics();
+ };
+
+ Statistics d_statistics;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+#endif // __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
--- /dev/null
+/********************* */
+/*! \file bitblast_strategies_template.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Aina Niemetz, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of bitblasting functions for various operators.
+ **
+ ** Implementation of bitblasting functions for various operators.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+
+#include <cmath>
+#include <ostream>
+
+#include "expr/node.h"
+#include "theory/bv/bitblast/bitblast_utils.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+namespace theory {
+namespace bv {
+
+/**
+ * Default Atom Bitblasting strategies:
+ *
+ * @param node the atom to be bitblasted
+ * @param bb the bitblaster
+ */
+
+template <class T>
+T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) {
+ Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+ << node.getKind() << "\n";
+ Unreachable();
+}
+
+
+template <class T>
+T DefaultEqBB(TNode node, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+
+ Assert(node.getKind() == kind::EQUAL);
+ std::vector<T> lhs, rhs;
+ bb->bbTerm(node[0], lhs);
+ bb->bbTerm(node[1], rhs);
+
+ Assert(lhs.size() == rhs.size());
+
+ std::vector<T> bits_eq;
+ for (unsigned i = 0; i < lhs.size(); i++) {
+ T bit_eq = mkIff(lhs[i], rhs[i]);
+ bits_eq.push_back(bit_eq);
+ }
+ T bv_eq = mkAnd(bits_eq);
+ return bv_eq;
+}
+
+template <class T>
+T AdderUltBB(TNode node, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_ULT);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+
+ // a < b <=> ~ (add(a, ~b, 1).carry_out)
+ std::vector<T> not_b;
+ negateBits(b, not_b);
+ T carry = mkTrue<T>();
+
+ for (unsigned i = 0 ; i < a.size(); ++i) {
+ carry = mkOr( mkAnd(a[i], not_b[i]),
+ mkAnd( mkXor(a[i], not_b[i]),
+ carry));
+ }
+ return mkNot(carry);
+}
+
+
+template <class T>
+T DefaultUltBB(TNode node, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_ULT);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+
+ // construct bitwise comparison
+ T res = uLessThanBB(a, b, false);
+ return res;
+}
+
+template <class T>
+T DefaultUleBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_ULE);
+ std::vector<T> a, b;
+
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+ // construct bitwise comparison
+ T res = uLessThanBB(a, b, true);
+ return res;
+}
+
+template <class T>
+T DefaultUgtBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ // should be rewritten
+ Unimplemented();
+}
+template <class T>
+T DefaultUgeBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ // should be rewritten
+ Unimplemented();
+}
+
+template <class T>
+T DefaultSltBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+
+ T res = sLessThanBB(a, b, false);
+ return res;
+}
+
+template <class T>
+T DefaultSleBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+
+ T res = sLessThanBB(a, b, true);
+ return res;
+}
+
+template <class T>
+T DefaultSgtBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ // should be rewritten
+ Unimplemented();
+}
+
+template <class T>
+T DefaultSgeBB(TNode node, TBitblaster<T>* bb){
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ // should be rewritten
+ Unimplemented();
+}
+
+
+/// Term bitblasting strategies
+
+/**
+ * Default Term Bitblasting strategies
+ *
+ * @param node the term to be bitblasted
+ * @param bits [output parameter] bits representing the new term
+ * @param bb the bitblaster in which the clauses are added
+ */
+template <class T>
+void UndefinedTermBBStrategy(TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+ << node.getKind() << "\n";
+ Unreachable();
+}
+
+template <class T>
+void DefaultVarBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Assert(bits.size() == 0);
+ bb->makeVariable(node, bits);
+
+ if(Debug.isOn("bitvector-bb")) {
+ Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << " with bits " << toString(bits);
+ }
+}
+
+template <class T>
+void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+ Assert(node.getKind() == kind::CONST_BITVECTOR);
+ Assert(bits.size() == 0);
+
+ for (unsigned i = 0; i < utils::getSize(node); ++i) {
+ Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
+ if(bit == Integer(0)){
+ bits.push_back(mkFalse<T>());
+ } else {
+ Assert (bit == Integer(1));
+ bits.push_back(mkTrue<T>());
+ }
+ }
+ if(Debug.isOn("bitvector-bb")) {
+ Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
+ }
+}
+
+
+template <class T>
+void DefaultNotBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_NOT);
+ Assert(bits.size() == 0);
+ std::vector<T> bv;
+ bb->bbTerm(node[0], bv);
+ negateBits(bv, bits);
+}
+
+template <class T>
+void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+ Assert(bits.size() == 0);
+
+ Assert (node.getKind() == kind::BITVECTOR_CONCAT);
+ for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
+ TNode current = node[i];
+ std::vector<T> current_bits;
+ bb->bbTerm(current, current_bits);
+
+ for(unsigned j = 0; j < utils::getSize(current); ++j) {
+ bits.push_back(current_bits[j]);
+ }
+ }
+ Assert (bits.size() == utils::getSize(node));
+ if(Debug.isOn("bitvector-bb")) {
+ Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
+ }
+}
+
+template <class T>
+void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+
+ Assert(node.getKind() == kind::BITVECTOR_AND &&
+ bits.size() == 0);
+
+ bb->bbTerm(node[0], bits);
+ std::vector<T> current;
+ for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+ bb->bbTerm(node[j], current);
+ for (unsigned i = 0; i < utils::getSize(node); ++i) {
+ bits[i] = mkAnd(bits[i], current[i]);
+ }
+ current.clear();
+ }
+ Assert (bits.size() == utils::getSize(node));
+}
+
+template <class T>
+void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+
+ Assert(node.getKind() == kind::BITVECTOR_OR &&
+ bits.size() == 0);
+
+ bb->bbTerm(node[0], bits);
+ std::vector<T> current;
+ for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+ bb->bbTerm(node[j], current);
+ for (unsigned i = 0; i < utils::getSize(node); ++i) {
+ bits[i] = mkOr(bits[i], current[i]);
+ }
+ current.clear();
+ }
+ Assert (bits.size() == utils::getSize(node));
+}
+
+template <class T>
+void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+
+ Assert(node.getKind() == kind::BITVECTOR_XOR &&
+ bits.size() == 0);
+
+ bb->bbTerm(node[0], bits);
+ std::vector<T> current;
+ for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+ bb->bbTerm(node[j], current);
+ for (unsigned i = 0; i < utils::getSize(node); ++i) {
+ bits[i] = mkXor(bits[i], current[i]);
+ }
+ current.clear();
+ }
+ Assert (bits.size() == utils::getSize(node));
+}
+
+template <class T>
+void DefaultXnorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+
+ Assert(node.getNumChildren() == 2 &&
+ node.getKind() == kind::BITVECTOR_XNOR &&
+ bits.size() == 0);
+ std::vector<T> lhs, rhs;
+ bb->bbTerm(node[0], lhs);
+ bb->bbTerm(node[1], rhs);
+ Assert(lhs.size() == rhs.size());
+
+ for (unsigned i = 0; i < lhs.size(); ++i) {
+ bits.push_back(mkIff(lhs[i], rhs[i]));
+ }
+}
+
+
+template <class T>
+void DefaultNandBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ Unimplemented();
+}
+template <class T>
+void DefaultNorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ Unimplemented();
+}
+template <class T>
+void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+
+ Assert(utils::getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+
+ std::vector<T> bit_eqs;
+ for (unsigned i = 0; i < a.size(); ++i) {
+ T eq = mkIff(a[i], b[i]);
+ bit_eqs.push_back(eq);
+ }
+ T a_eq_b = mkAnd(bit_eqs);
+ bits.push_back(a_eq_b);
+}
+
+template <class T>
+void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+ Assert(res.size() == 0 &&
+ node.getKind() == kind::BITVECTOR_MULT);
+
+ // if (node.getNumChildren() == 2) {
+ // std::vector<T> a;
+ // std::vector<T> b;
+ // bb->bbTerm(node[0], a);
+ // bb->bbTerm(node[1], b);
+ // unsigned bw = utils::getSize(node);
+ // unsigned thresh = bw % 2 ? bw/2 : bw/2 - 1;
+ // bool no_overflow = true;
+ // for (unsigned i = thresh; i < bw; ++i) {
+ // if (a[i] != mkFalse<T> || b[i] != mkFalse<T> ) {
+ // no_overflow = false;
+ // }
+ // }
+ // if (no_overflow) {
+ // shiftAddMultiplier();
+ // return;
+ // }
+
+ // }
+
+ std::vector<T> newres;
+ bb->bbTerm(node[0], res);
+ for(unsigned i = 1; i < node.getNumChildren(); ++i) {
+ std::vector<T> current;
+ bb->bbTerm(node[i], current);
+ newres.clear();
+ // constructs a simple shift and add multiplier building the result
+ // in res
+ shiftAddMultiplier(res, current, newres);
+ res = newres;
+ }
+ if(Debug.isOn("bitvector-bb")) {
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ }
+}
+
+template <class T>
+void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_PLUS &&
+ res.size() == 0);
+
+ bb->bbTerm(node[0], res);
+
+ std::vector<T> newres;
+
+ for(unsigned i = 1; i < node.getNumChildren(); ++i) {
+ std::vector<T> current;
+ bb->bbTerm(node[i], current);
+ newres.clear();
+ rippleCarryAdder(res, current, newres, mkFalse<T>());
+ res = newres;
+ }
+
+ Assert(res.size() == utils::getSize(node));
+}
+
+
+template <class T>
+void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_SUB &&
+ node.getNumChildren() == 2 &&
+ bits.size() == 0);
+
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size() && utils::getSize(node) == a.size());
+
+ // bvsub a b = adder(a, ~b, 1)
+ std::vector<T> not_b;
+ negateBits(b, not_b);
+ rippleCarryAdder(a, not_b, bits, mkTrue<T>());
+}
+
+template <class T>
+void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_NEG);
+
+ std::vector<T> a;
+ bb->bbTerm(node[0], a);
+ Assert(utils::getSize(node) == a.size());
+
+ // -a = add(~a, 0, 1).
+ std::vector<T> not_a;
+ negateBits(a, not_a);
+ std::vector<T> zero;
+ makeZero(zero, utils::getSize(node));
+
+ rippleCarryAdder(not_a, zero, bits, mkTrue<T>());
+}
+
+template <class T>
+void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) {
+ Assert( q.size() == 0 && r.size() == 0);
+
+ if(rec_width == 0 || isZero(a)) {
+ makeZero(q, a.size());
+ makeZero(r, a.size());
+ return;
+ }
+
+ std::vector<T> q1, r1;
+ std::vector<T> a1 = a;
+ rshift(a1, 1);
+
+ uDivModRec(a1, b, q1, r1, rec_width - 1);
+ // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd
+ lshift(q1, 1);
+ lshift(r1, 1);
+
+
+ T is_odd = mkIff(a[0], mkTrue<T>());
+ T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>());
+
+ std::vector<T> zero;
+ makeZero(zero, b.size());
+
+ std::vector<T> r1_shift_add;
+ // account for a being odd
+ rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd);
+ // now check if the remainder is greater than b
+ std::vector<T> not_b;
+ negateBits(b, not_b);
+ std::vector<T> r_minus_b;
+ T co1;
+ // use adder because we need r_minus_b anyway
+ co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue<T>());
+ // sign is true if r1 < b
+ T sign = mkNot(co1);
+
+ q1[0] = mkIte(sign, q1[0], mkTrue<T>());
+
+ // would be nice to have a high level ITE instead of bitwise
+ for(unsigned i = 0; i < a.size(); ++i) {
+ r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]);
+ }
+
+ // check if a < b
+
+ std::vector<T> a_minus_b;
+ T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue<T>());
+ // Node a_lt_b = a_minus_b.back();
+ T a_lt_b = mkNot(co2);
+
+ for(unsigned i = 0; i < a.size(); ++i) {
+ T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]);
+ T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]);
+ q.push_back(qval);
+ r.push_back(rval);
+ }
+
+}
+
+template <class T>
+void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb)
+{
+ Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node
+ << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0);
+
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+
+ std::vector<T> r;
+ uDivModRec(a, b, q, r, utils::getSize(node));
+ // adding a special case for division by 0
+ std::vector<T> iszero;
+ for (unsigned i = 0; i < b.size(); ++i)
+ {
+ iszero.push_back(mkIff(b[i], mkFalse<T>()));
+ }
+ T b_is_0 = mkAnd(iszero);
+
+ for (unsigned i = 0; i < q.size(); ++i)
+ {
+ q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
+ r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a
+ }
+
+ // cache the remainder in case we need it later
+ Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
+ kind::BITVECTOR_UREM_TOTAL, node[0], node[1]));
+ bb->storeBBTerm(remainder, r);
+}
+
+template <class T>
+void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb)
+{
+ Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node
+ << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0);
+
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+
+ std::vector<T> q;
+ uDivModRec(a, b, q, rem, utils::getSize(node));
+ // adding a special case for division by 0
+ std::vector<T> iszero;
+ for (unsigned i = 0; i < b.size(); ++i)
+ {
+ iszero.push_back(mkIff(b[i], mkFalse<T>()));
+ }
+ T b_is_0 = mkAnd(iszero);
+
+ for (unsigned i = 0; i < q.size(); ++i)
+ {
+ q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
+ rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a
+ }
+
+ // cache the quotient in case we need it later
+ Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
+ kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]));
+ bb->storeBBTerm(quotient, q);
+}
+
+template <class T>
+void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ Unimplemented();
+}
+template <class T>
+void DefaultSremBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ Unimplemented();
+}
+template <class T>
+void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ Unimplemented();
+}
+
+template <class T>
+void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
+{
+ Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node
+ << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+
+ // check for b < log2(n)
+ unsigned size = utils::getSize(node);
+ unsigned log2_size = std::ceil(log2((double)size));
+ Node a_size = utils::mkConst(size, size);
+ Node b_ult_a_size_node = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
+ // ensure that the inequality is bit-blasted
+ bb->bbAtom(b_ult_a_size_node);
+ T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+ std::vector<T> prev_res;
+ res = a;
+ // we only need to look at the bits bellow log2_a_size
+ for (unsigned s = 0; s < log2_size; ++s)
+ {
+ // barrel shift stage: at each stage you can either shift by 2^s bits
+ // or leave the previous stage untouched
+ prev_res = res;
+ unsigned threshold = pow(2, s);
+ for (unsigned i = 0; i < a.size(); ++i)
+ {
+ if (i < threshold)
+ {
+ // if b[s] is true then we must have shifted by at least 2^b bits so
+ // all bits bellow 2^s will be 0, otherwise just use previous shift
+ // value
+ res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
+ }
+ else
+ {
+ // if b[s]= 0, use previous value, otherwise shift by threshold bits
+ Assert(i >= threshold);
+ res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]);
+ }
+ }
+ }
+ prev_res = res;
+ for (unsigned i = 0; i < b.size(); ++i)
+ {
+ // this is fine because b_ult_a_size has been bit-blasted
+ res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
+ }
+
+ if (Debug.isOn("bitvector-bb"))
+ {
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ }
+}
+
+template <class T>
+void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
+{
+ Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node
+ << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+
+ // check for b < log2(n)
+ unsigned size = utils::getSize(node);
+ unsigned log2_size = std::ceil(log2((double)size));
+ Node a_size = utils::mkConst(size, size);
+ Node b_ult_a_size_node = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
+ // ensure that the inequality is bit-blasted
+ bb->bbAtom(b_ult_a_size_node);
+ T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+ res = a;
+ std::vector<T> prev_res;
+
+ for (unsigned s = 0; s < log2_size; ++s)
+ {
+ // barrel shift stage: at each stage you can either shift by 2^s bits
+ // or leave the previous stage untouched
+ prev_res = res;
+ int threshold = pow(2, s);
+ for (unsigned i = 0; i < a.size(); ++i)
+ {
+ if (i + threshold >= a.size())
+ {
+ // if b[s] is true then we must have shifted by at least 2^b bits so
+ // all bits above 2^s will be 0, otherwise just use previous shift value
+ res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
+ }
+ else
+ {
+ // if b[s]= 0, use previous value, otherwise shift by threshold bits
+ Assert(i + threshold < a.size());
+ res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]);
+ }
+ }
+ }
+
+ prev_res = res;
+ for (unsigned i = 0; i < b.size(); ++i)
+ {
+ // this is fine because b_ult_a_size has been bit-blasted
+ res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
+ }
+
+ if (Debug.isOn("bitvector-bb"))
+ {
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ }
+}
+
+template <class T>
+void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
+{
+ Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node
+ << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+
+ // check for b < n
+ unsigned size = utils::getSize(node);
+ unsigned log2_size = std::ceil(log2((double)size));
+ Node a_size = utils::mkConst(size, size);
+ Node b_ult_a_size_node = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
+ // ensure that the inequality is bit-blasted
+ bb->bbAtom(b_ult_a_size_node);
+ T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
+
+ res = a;
+ T sign_bit = a.back();
+ std::vector<T> prev_res;
+
+ for (unsigned s = 0; s < log2_size; ++s)
+ {
+ // barrel shift stage: at each stage you can either shift by 2^s bits
+ // or leave the previous stage untouched
+ prev_res = res;
+ int threshold = pow(2, s);
+ for (unsigned i = 0; i < a.size(); ++i)
+ {
+ if (i + threshold >= a.size())
+ {
+ // if b[s] is true then we must have shifted by at least 2^b bits so
+ // all bits above 2^s will be the sign bit, otherwise just use previous
+ // shift value
+ res[i] = mkIte(b[s], sign_bit, prev_res[i]);
+ }
+ else
+ {
+ // if b[s]= 0, use previous value, otherwise shift by threshold bits
+ Assert(i + threshold < a.size());
+ res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]);
+ }
+ }
+ }
+
+ prev_res = res;
+ for (unsigned i = 0; i < b.size(); ++i)
+ {
+ // this is fine because b_ult_a_size has been bit-blasted
+ res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit);
+ }
+
+ if (Debug.isOn("bitvector-bb"))
+ {
+ Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
+ }
+}
+
+template <class T>
+void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_ULTBV);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+
+ // construct bitwise comparison
+ res.push_back(uLessThanBB(a, b, false));
+}
+
+template <class T>
+void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_SLTBV);
+ std::vector<T> a, b;
+ bb->bbTerm(node[0], a);
+ bb->bbTerm(node[1], b);
+ Assert(a.size() == b.size());
+
+ // construct bitwise comparison
+ res.push_back(sLessThanBB(a, b, false));
+}
+
+template <class T>
+void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
+ Assert(node.getKind() == kind::BITVECTOR_ITE);
+ std::vector<T> cond, thenpart, elsepart;
+ bb->bbTerm(node[0], cond);
+ bb->bbTerm(node[1], thenpart);
+ bb->bbTerm(node[2], elsepart);
+
+ Assert(cond.size() == 1);
+ Assert(thenpart.size() == elsepart.size());
+
+ for (unsigned i = 0; i < thenpart.size(); ++i) {
+ // (~cond OR thenpart) AND (cond OR elsepart)
+ res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i])));
+ }
+}
+
+template <class T>
+void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
+ Assert(bits.size() == 0);
+
+ std::vector<T> base_bits;
+ bb->bbTerm(node[0], base_bits);
+ unsigned high = utils::getExtractHigh(node);
+ unsigned low = utils::getExtractLow(node);
+
+ for (unsigned i = low; i <= high; ++i) {
+ bits.push_back(base_bits[i]);
+ }
+ Assert (bits.size() == high - low + 1);
+
+ if(Debug.isOn("bitvector-bb")) {
+ Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+ Debug("bitvector-bb") << " with bits " << toString(bits);
+ }
+}
+
+
+template <class T>
+void DefaultRepeatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ // this should be rewritten
+ Unimplemented();
+}
+
+template <class T>
+void DefaultZeroExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
+
+ Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n";
+
+ // this should be rewritten
+ Unimplemented();
+
+}
+
+template <class T>
+void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
+ Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n";
+
+ Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
+ res_bits.size() == 0);
+
+ std::vector<T> bits;
+ bb->bbTerm(node[0], bits);
+
+ T sign_bit = bits.back();
+ unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+
+ for (unsigned i = 0; i < bits.size(); ++i ) {
+ res_bits.push_back(bits[i]);
+ }
+
+ for (unsigned i = 0 ; i < amount ; ++i ) {
+ res_bits.push_back(sign_bit);
+ }
+
+ Assert (res_bits.size() == amount + bits.size());
+}
+
+template <class T>
+void DefaultRotateRightBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+
+ Unimplemented();
+}
+
+template <class T>
+void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
+ Debug("bitvector") << "theory::bv:: Unimplemented kind "
+ << node.getKind() << "\n";
+ Unimplemented();
+}
+
+
+}
+}
+}
+
+#endif
--- /dev/null
+/********************* */
+/*! \file bitblast_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Paul Meng, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Various utility functions for bit-blasting.
+ **
+ ** Various utility functions for bit-blasting.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+
+
+#include <ostream>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template <class T> class TBitblaster;
+
+template <class T>
+std::string toString (const std::vector<T>& bits);
+
+template <> inline
+std::string toString<Node> (const std::vector<Node>& bits) {
+ std::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();
+}
+
+template <class T> T mkTrue();
+template <class T> T mkFalse();
+template <class T> T mkNot(T a);
+template <class T> T mkOr(T a, T b);
+template <class T> T mkOr(const std::vector<T>& a);
+template <class T> T mkAnd(T a, T b);
+template <class T> T mkAnd(const std::vector<T>& a);
+template <class T> T mkXor(T a, T b);
+template <class T> T mkIff(T a, T b);
+template <class T> T mkIte(T cond, T a, T b);
+
+
+template <> inline
+Node mkTrue<Node>() {
+ return NodeManager::currentNM()->mkConst<bool>(true);
+}
+
+template <> inline
+Node mkFalse<Node>() {
+ return NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+template <> inline
+Node mkNot<Node>(Node a) {
+ return NodeManager::currentNM()->mkNode(kind::NOT, a);
+}
+
+template <> inline
+Node mkOr<Node>(Node a, Node b) {
+ return NodeManager::currentNM()->mkNode(kind::OR, a, b);
+}
+
+template <> inline
+Node mkOr<Node>(const std::vector<Node>& children) {
+ Assert (children.size());
+ if (children.size() == 1)
+ return children[0];
+ return NodeManager::currentNM()->mkNode(kind::OR, children);
+}
+
+
+template <> inline
+Node mkAnd<Node>(Node a, Node b) {
+ return NodeManager::currentNM()->mkNode(kind::AND, a, b);
+}
+
+template <> inline
+Node mkAnd<Node>(const std::vector<Node>& children) {
+ Assert (children.size());
+ if (children.size() == 1)
+ return children[0];
+ return NodeManager::currentNM()->mkNode(kind::AND, children);
+}
+
+
+template <> inline
+Node mkXor<Node>(Node a, Node b) {
+ return NodeManager::currentNM()->mkNode(kind::XOR, a, b);
+}
+
+template <> inline
+Node mkIff<Node>(Node a, Node b) {
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+}
+
+template <> inline
+Node mkIte<Node>(Node cond, Node a, Node b) {
+ return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b);
+}
+
+/*
+ Various helper functions that get called by the bitblasting procedures
+ */
+
+template <class T>
+void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
+ Assert ( lo < b.size() && hi < b.size() && lo <= hi);
+ for (unsigned i = lo; i <= hi; ++i) {
+ dest.push_back(b[i]);
+ }
+}
+
+template <class T>
+void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
+ for(unsigned i = 0; i < bits.size(); ++i) {
+ negated_bits.push_back(mkNot(bits[i]));
+ }
+}
+
+template <class T>
+bool inline isZero(const std::vector<T>& bits) {
+ for(unsigned i = 0; i < bits.size(); ++i) {
+ if(bits[i] != mkFalse<T>()) {
+ return false;
+ }
+ }
+ return true;
+}
+
+template <class T>
+void inline rshift(std::vector<T>& bits, unsigned amount) {
+ for (unsigned i = 0; i < bits.size() - amount; ++i) {
+ bits[i] = bits[i+amount];
+ }
+ for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
+ bits[i] = mkFalse<T>();
+ }
+}
+
+template <class T>
+void inline lshift(std::vector<T>& bits, unsigned amount) {
+ for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
+ bits[i] = bits[i-amount];
+ }
+ for(unsigned i = 0; i < amount; ++i) {
+ bits[i] = mkFalse<T>();
+ }
+}
+
+template <class T>
+void inline makeZero(std::vector<T>& bits, unsigned width) {
+ Assert(bits.size() == 0);
+ for(unsigned i = 0; i < width; ++i) {
+ bits.push_back(mkFalse<T>());
+ }
+}
+
+
+/**
+ * Constructs a simple ripple carry adder
+ *
+ * @param a first term to be added
+ * @param b second term to be added
+ * @param res the result
+ * @param carry the carry-in bit
+ *
+ * @return the carry-out
+ */
+template <class T>
+T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
+ Assert(a.size() == b.size() && res.size() == 0);
+
+ for (unsigned i = 0 ; i < a.size(); ++i) {
+ T sum = mkXor(mkXor(a[i], b[i]), carry);
+ carry = mkOr( mkAnd(a[i], b[i]),
+ mkAnd( mkXor(a[i], b[i]),
+ carry));
+ res.push_back(sum);
+ }
+
+ return carry;
+}
+
+template <class T>
+inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, std::vector<T>& res) {
+
+ for (unsigned i = 0; i < a.size(); ++i) {
+ res.push_back(mkAnd(b[0], a[i]));
+ }
+
+ for(unsigned k = 1; k < res.size(); ++k) {
+ T carry_in = mkFalse<T>();
+ T carry_out;
+ for(unsigned j = 0; j < res.size() -k; ++j) {
+ T aj = mkAnd(b[k], a[j]);
+ carry_out = mkOr(mkAnd(res[j+k], aj),
+ mkAnd( mkXor(res[j+k], aj), carry_in));
+ res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
+ carry_in = carry_out;
+ }
+ }
+}
+
+template <class T>
+T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
+ Assert (a.size() && b.size());
+
+ T res = mkAnd(mkNot(a[0]), b[0]);
+
+ if(orEqual) {
+ res = mkOr(res, mkIff(a[0], b[0]));
+ }
+
+ for (unsigned i = 1; i < a.size(); ++i) {
+ // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
+ res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
+ mkAnd(mkNot(a[i]), b[i]));
+ }
+ return res;
+}
+
+template <class T>
+T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
+ Assert (a.size() && b.size());
+ if (a.size() == 1) {
+ if(orEqual) {
+ return mkOr(mkIff(a[0], b[0]),
+ mkAnd(a[0], mkNot(b[0])));
+ }
+
+ return mkAnd(a[0], mkNot(b[0]));
+ }
+ unsigned n = a.size() - 1;
+ std::vector<T> a1, b1;
+ extractBits(a, a1, 0, n-1);
+ extractBits(b, b1, 0, n-1);
+
+ // unsigned comparison of the first n-1 bits
+ T ures = uLessThanBB(a1, b1, orEqual);
+ T res = mkOr(// a b have the same sign
+ mkAnd(mkIff(a[n], b[n]),
+ ures),
+ // a is negative and b positive
+ mkAnd(a[n],
+ mkNot(b[n])));
+ return res;
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
--- /dev/null
+/********************* */
+/*! \file bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Tim King, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Wrapper around the SAT solver used for bitblasting
+ **
+ ** Wrapper around the SAT solver used for bitblasting.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+#include "expr/node.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/bitblast/bitblast_strategies_template.h"
+#include "theory/theory_registrar.h"
+#include "theory/valuation.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+
+/**
+ * The Bitblaster that manages the mapping between Nodes
+ * and their bitwise definition
+ *
+ */
+
+template <class T>
+class TBitblaster
+{
+ protected:
+ typedef std::vector<T> Bits;
+ typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
+
+ typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
+ typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);
+
+ // caches and mappings
+ TermDefMap d_termCache;
+ ModelCache d_modelCache;
+
+ BitVectorProof* d_bvp;
+
+ void initAtomBBStrategies();
+ void initTermBBStrategies();
+
+ protected:
+ /// function tables for the various bitblasting strategies indexed by node
+ /// kind
+ TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
+ AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+ virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
+
+ public:
+ TBitblaster();
+ virtual ~TBitblaster() {}
+ virtual void bbAtom(TNode node) = 0;
+ virtual void bbTerm(TNode node, Bits& bits) = 0;
+ virtual void makeVariable(TNode node, Bits& bits) = 0;
+ virtual T getBBAtom(TNode atom) const = 0;
+ virtual bool hasBBAtom(TNode atom) const = 0;
+ virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
+
+ bool hasBBTerm(TNode node) const;
+ void getBBTerm(TNode node, Bits& bits) const;
+ virtual void storeBBTerm(TNode term, const Bits& bits);
+ /**
+ * Return a constant representing the value of a in the model.
+ * If fullModel is true set unconstrained bits to 0. If not return
+ * NullNode() for a fully or partially unconstrained.
+ *
+ */
+ Node getTermModel(TNode node, bool fullModel);
+ void invalidateModelCache();
+};
+
+class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify
+{
+ public:
+ MinisatEmptyNotify() {}
+ bool notify(prop::SatLiteral lit) override { return true; }
+ void notify(prop::SatClause& clause) override {}
+ void spendResource(unsigned amount) override
+ {
+ NodeManager::currentResourceManager()->spendResource(amount);
+ }
+ void safePoint(unsigned amount) override {}
+};
+
+// Bitblaster implementation
+
+template <class T>
+void TBitblaster<T>::initAtomBBStrategies()
+{
+ for (int i = 0; i < kind::LAST_KIND; ++i)
+ {
+ d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
+ }
+ /// setting default bb strategies for atoms
+ d_atomBBStrategies[kind::EQUAL] = DefaultEqBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB<T>;
+ d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB<T>;
+}
+
+template <class T>
+void TBitblaster<T>::initTermBBStrategies()
+{
+ for (int i = 0; i < kind::LAST_KIND; ++i)
+ {
+ d_termBBStrategies[i] = DefaultVarBB<T>;
+ }
+ /// setting default bb strategies for terms:
+ d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy<T>;
+ d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy<T>;
+ d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
+ d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
+ d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
+ d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB<T>;
+}
+
+template <class T>
+TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL)
+{
+ initAtomBBStrategies();
+ initTermBBStrategies();
+}
+
+template <class T>
+bool TBitblaster<T>::hasBBTerm(TNode node) const
+{
+ return d_termCache.find(node) != d_termCache.end();
+}
+template <class T>
+void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const
+{
+ Assert(hasBBTerm(node));
+ bits = d_termCache.find(node)->second;
+}
+
+template <class T>
+void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits)
+{
+ d_termCache.insert(std::make_pair(node, bits));
+}
+
+template <class T>
+void TBitblaster<T>::invalidateModelCache()
+{
+ d_modelCache.clear();
+}
+
+template <class T>
+Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
+{
+ if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
+
+ if (node.isConst()) return node;
+
+ Node value = getModelFromSatSolver(node, false);
+ if (!value.isNull())
+ {
+ Debug("bv-equality-status")
+ << "TLazyBitblaster::getTermModel from SatSolver" << node << " => "
+ << value << "\n";
+ d_modelCache[node] = value;
+ Assert(value.isConst());
+ return value;
+ }
+
+ if (Theory::isLeafOf(node, theory::THEORY_BV))
+ {
+ // if it is a leaf may ask for fullModel
+ value = getModelFromSatSolver(node, true);
+ Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue"
+ << node << " => " << value << "\n";
+ Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel);
+ if (!value.isNull())
+ {
+ d_modelCache[node] = value;
+ }
+ return value;
+ }
+ Assert(node.getType().isBitVector());
+
+ NodeBuilder<> nb(node.getKind());
+ if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ nb << node.getOperator();
+ }
+
+ for (unsigned i = 0; i < node.getNumChildren(); ++i)
+ {
+ nb << getTermModel(node[i], fullModel);
+ }
+ value = nb;
+ value = Rewriter::rewrite(value);
+ Assert(value.isConst());
+ d_modelCache[node] = value;
+ Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value"
+ << node << " => " << value << "\n";
+ return value;
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif /* __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
--- /dev/null
+/********************* */
+/*! \file eager_bitblaster.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief
+ **
+ ** Bitblaster for the eager bv solver.
+ **/
+
+#include "cvc4_private.h"
+
+#include "theory/bv/bitblast/eager_bitblaster.h"
+
+#include "options/bv_options.h"
+#include "proof/bitvector_proof.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
+ : TBitblaster<Node>(),
+ d_satSolver(),
+ d_bitblastingRegistrar(new BitblastingRegistrar(this)),
+ d_nullContext(new context::Context()),
+ d_cnfStream(),
+ d_bv(theory_bv),
+ d_bbAtoms(),
+ d_variables(),
+ d_notify()
+{
+ prop::SatSolver *solver = nullptr;
+ switch (options::bvSatSolver())
+ {
+ case SAT_SOLVER_MINISAT:
+ {
+ prop::BVSatSolverInterface* minisat =
+ prop::SatSolverFactory::createMinisat(
+ d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster");
+ d_notify.reset(new MinisatEmptyNotify());
+ minisat->setNotify(d_notify.get());
+ solver = minisat;
+ break;
+ }
+ case SAT_SOLVER_CADICAL:
+ solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
+ "EagerBitblaster");
+ break;
+ case SAT_SOLVER_CRYPTOMINISAT:
+ solver = prop::SatSolverFactory::createCryptoMinisat(
+ smtStatisticsRegistry(), "EagerBitblaster");
+ break;
+ default: Unreachable("Unknown SAT solver type");
+ }
+ d_satSolver.reset(solver);
+ d_cnfStream.reset(
+ new prop::TseitinCnfStream(d_satSolver.get(),
+ d_bitblastingRegistrar.get(),
+ d_nullContext.get(),
+ options::proof(),
+ "EagerBitblaster"));
+}
+
+EagerBitblaster::~EagerBitblaster() {}
+
+void EagerBitblaster::bbFormula(TNode node) {
+ d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID,
+ TNode::null());
+}
+
+/**
+ * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
+ * NOTE: duplicate clauses are not detected because of marker literal
+ * @param node the atom to be bitblasted
+ *
+ */
+void EagerBitblaster::bbAtom(TNode node)
+{
+ node = node.getKind() == kind::NOT ? node[0] : node;
+ if (node.getKind() == kind::BITVECTOR_BITOF) return;
+ if (hasBBAtom(node))
+ {
+ return;
+ }
+
+ Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
+
+ // the bitblasted definition of the atom
+ Node normalized = Rewriter::rewrite(node);
+ Node atom_bb =
+ normalized.getKind() != kind::CONST_BOOLEAN
+ ? d_atomBBStrategies[normalized.getKind()](normalized, this)
+ : normalized;
+
+ if (!options::proof())
+ {
+ atom_bb = Rewriter::rewrite(atom_bb);
+ }
+
+ // asserting that the atom is true iff the definition holds
+ Node atom_definition =
+ NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb);
+
+ AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
+ storeBBAtom(node, atom_bb);
+ d_cnfStream->convertAndAssert(
+ atom_definition, false, false, RULE_INVALID, TNode::null());
+}
+
+void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
+ if (d_bvp) {
+ d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+ }
+ d_bbAtoms.insert(atom);
+}
+
+void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+ if (d_bvp) {
+ d_bvp->registerTermBB(node.toExpr());
+ }
+ d_termCache.insert(std::make_pair(node, bits));
+}
+
+bool EagerBitblaster::hasBBAtom(TNode atom) const {
+ return d_bbAtoms.find(atom) != d_bbAtoms.end();
+}
+
+void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
+ Assert(node.getType().isBitVector());
+
+ if (hasBBTerm(node)) {
+ getBBTerm(node, bits);
+ return;
+ }
+
+ d_bv->spendResource(options::bitblastStep());
+ Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
+
+ d_termBBStrategies[node.getKind()](node, bits, this);
+
+ Assert(bits.size() == utils::getSize(node));
+
+ storeBBTerm(node, bits);
+}
+
+void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
+ Assert(bits.size() == 0);
+ for (unsigned i = 0; i < utils::getSize(var); ++i) {
+ bits.push_back(utils::mkBitOf(var, i));
+ }
+ d_variables.insert(var);
+}
+
+Node EagerBitblaster::getBBAtom(TNode node) const { return node; }
+
+/**
+ * Calls the solve method for the Sat Solver.
+ *
+ * @return true for sat, and false for unsat
+ */
+
+bool EagerBitblaster::solve() {
+ if (Trace.isOn("bitvector")) {
+ Trace("bitvector") << "EagerBitblaster::solve(). \n";
+ }
+ Debug("bitvector") << "EagerBitblaster::solve(). \n";
+ // TODO: clear some memory
+ // if (something) {
+ // NodeManager* nm= NodeManager::currentNM();
+ // Rewriter::garbageCollect();
+ // nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+ // }
+ return prop::SAT_VALUE_TRUE == d_satSolver->solve();
+}
+
+/**
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
+ *
+ * @return
+ */
+Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
+ if (!hasBBTerm(a)) {
+ return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node();
+ }
+
+ Bits bits;
+ getBBTerm(a, bits);
+ Integer value(0);
+ for (int i = bits.size() - 1; i >= 0; --i) {
+ prop::SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
+ prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+ bit_value = d_satSolver->value(bit);
+ Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
+ } else {
+ if (!fullModel) return Node();
+ // unconstrained bits default to false
+ bit_value = prop::SAT_VALUE_FALSE;
+ }
+ Integer bit_int =
+ bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+ value = value * 2 + bit_int;
+ }
+ return utils::mkConst(bits.size(), value);
+}
+
+bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
+ TNodeSet::iterator it = d_variables.begin();
+ for (; it != d_variables.end(); ++it) {
+ TNode var = *it;
+ if (d_bv->isLeaf(var) || isSharedTerm(var) ||
+ (var.isVar() && var.getType().isBoolean())) {
+ // only shared terms could not have been bit-blasted
+ Assert(hasBBTerm(var) || isSharedTerm(var));
+
+ Node const_value = getModelFromSatSolver(var, true);
+
+ if (const_value != Node()) {
+ Debug("bitvector-model")
+ << "EagerBitblaster::collectModelInfo (assert (= " << var << " "
+ << const_value << "))\n";
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
+ }
+ }
+ }
+ return true;
+}
+
+void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
+ d_bvp = bvp;
+ d_satSolver->setProofLog(bvp);
+ bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
+}
+
+bool EagerBitblaster::isSharedTerm(TNode node) {
+ return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
+}
+
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file eager_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bitblaster for eager BV solver.
+ **
+ ** Bitblaster for the eager BV solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+
+#include <unordered_set>
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BitblastingRegistrar;
+class TheoryBV;
+
+class EagerBitblaster : public TBitblaster<Node>
+{
+ public:
+ EagerBitblaster(TheoryBV* theory_bv);
+ ~EagerBitblaster();
+
+ void addAtom(TNode atom);
+ void makeVariable(TNode node, Bits& bits) override;
+ void bbTerm(TNode node, Bits& bits) override;
+ void bbAtom(TNode node) override;
+ Node getBBAtom(TNode node) const override;
+ bool hasBBAtom(TNode atom) const override;
+ void bbFormula(TNode formula);
+ void storeBBAtom(TNode atom, Node atom_bb) override;
+ void storeBBTerm(TNode node, const Bits& bits) override;
+
+ bool assertToSat(TNode node, bool propagate = true);
+ bool solve();
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
+ void setProofLog(BitVectorProof* bvp);
+
+ private:
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ // sat solver used for bitblasting and associated CnfStream
+ std::unique_ptr<prop::SatSolver> d_satSolver;
+ std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
+ std::unique_ptr<context::Context> d_nullContext;
+ std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+ TheoryBV* d_bv;
+ TNodeSet d_bbAtoms;
+ TNodeSet d_variables;
+
+ // This is either an MinisatEmptyNotify or NULL.
+ std::unique_ptr<MinisatEmptyNotify> d_notify;
+
+ Node getModelFromSatSolver(TNode a, bool fullModel) override;
+ bool isSharedTerm(TNode node);
+};
+
+class BitblastingRegistrar : public prop::Registrar
+{
+ public:
+ BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {}
+ void preRegister(Node n) override { d_bitblaster->bbAtom(n); }
+
+ private:
+ EagerBitblaster* d_bitblaster;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+#endif // __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
--- /dev/null
+/********************* */
+/*! \file lazy_bitblaster.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Aina Niemetz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bitblaster for the lazy bv solver.
+ **
+ ** Bitblaster for the lazy bv solver.
+ **/
+
+#include "cvc4_private.h"
+
+#include "theory/bv/bitblast/lazy_bitblaster.h"
+
+#include "options/bv_options.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/bv/abstraction.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+#include "proof/bitvector_proof.h"
+#include "proof/proof_manager.h"
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+namespace {
+
+/* Determine the number of uncached nodes that a given node consists of. */
+uint64_t numNodes(TNode node, utils::NodeSet& seen)
+{
+ std::vector<TNode> stack;
+ uint64_t res = 0;
+
+ stack.push_back(node);
+ while (!stack.empty())
+ {
+ Node n = stack.back();
+ stack.pop_back();
+
+ if (seen.find(n) != seen.end()) continue;
+
+ res += 1;
+ seen.insert(n);
+ stack.insert(stack.end(), n.begin(), n.end());
+ }
+ return res;
+}
+}
+
+TLazyBitblaster::TLazyBitblaster(context::Context* c,
+ bv::TheoryBV* bv,
+ const std::string name,
+ bool emptyNotify)
+ : TBitblaster<Node>(),
+ d_bv(bv),
+ d_ctx(c),
+ d_nullRegistrar(new prop::NullRegistrar()),
+ d_nullContext(new context::Context()),
+ 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_fullModelAssertionLevel(c, 0),
+ d_name(name),
+ d_statistics(name)
+{
+ d_satSolver.reset(
+ prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
+
+ d_cnfStream.reset(
+ new prop::TseitinCnfStream(d_satSolver.get(),
+ d_nullRegistrar.get(),
+ d_nullContext.get(),
+ options::proof(),
+ "LazyBitblaster"));
+
+ d_satSolverNotify.reset(
+ d_emptyNotify
+ ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify()
+ : (prop::BVSatSolverInterface::Notify*)new MinisatNotify(
+ d_cnfStream.get(), bv, this));
+
+ d_satSolver->setNotify(d_satSolverNotify.get());
+}
+
+void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
+ d_abstraction = abs;
+}
+
+TLazyBitblaster::~TLazyBitblaster()
+{
+ d_assertedAtoms->deleteSelf();
+ d_explanations->deleteSelf();
+}
+
+
+/**
+ * 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)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ 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 = nm->mkNode(kind::EQUAL, node, atom_bb);
+ storeBBAtom(node, atom_bb);
+ d_cnfStream->convertAndAssert(
+ atom_definition, false, false, RULE_INVALID, TNode::null());
+ return;
+ }
+
+ // the bitblasted definition of the atom
+ Node normalized = Rewriter::rewrite(node);
+ Node atom_bb =
+ normalized.getKind() != kind::CONST_BOOLEAN
+ ? d_atomBBStrategies[normalized.getKind()](normalized, this)
+ : normalized;
+
+ if (!options::proof())
+ {
+ atom_bb = Rewriter::rewrite(atom_bb);
+ }
+
+ // asserting that the atom is true iff the definition holds
+ Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
+ storeBBAtom(node, atom_bb);
+ d_cnfStream->convertAndAssert(
+ atom_definition, false, false, RULE_INVALID, TNode::null());
+}
+
+void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
+ // No need to store the definition for the lazy bit-blaster (unless proofs are enabled).
+ if( d_bvp != NULL ){
+ d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+ }
+ d_bbAtoms.insert(atom);
+}
+
+void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+ if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
+ d_termCache.insert(std::make_pair(node, bits));
+}
+
+
+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;
+ if (!utils::isBitblastAtom(node)) { return 0; }
+ Node atom_bb =
+ Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
+ uint64_t size = 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;
+ }
+ Assert( node.getType().isBitVector() );
+
+ d_bv->spendResource(options::bitblastStep());
+ Debug("bitvector-bitblast") << "Bitblasting term " << 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( utils::isBitblastAtom( atom ) );
+
+ 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";
+ d_fullModelAssertionLevel.set(d_bv->numAssertions());
+ 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)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ 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 = nm->mkNode(kind::NOT, atom);
+ }
+ conflict.push_back(not_atom);
+ }
+}
+
+TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
+ d_numTermClauses(prefix + "::NumTermSatClauses", 0),
+ d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
+ d_numTerms(prefix + "::NumBitblastedTerms", 0),
+ d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
+ d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
+ d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
+ d_bitblastTimer(prefix + "::BitblastTimer")
+{
+ smtStatisticsRegistry()->registerStat(&d_numTermClauses);
+ smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
+ smtStatisticsRegistry()->registerStat(&d_numTerms);
+ smtStatisticsRegistry()->registerStat(&d_numAtoms);
+ smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
+ smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
+ smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
+}
+
+
+TLazyBitblaster::Statistics::~Statistics() {
+ smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
+ smtStatisticsRegistry()->unregisterStat(&d_numTerms);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
+ smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
+ smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
+ smtStatisticsRegistry()->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::spendResource(unsigned amount)
+{
+ d_bv->spendResource(amount);
+}
+
+void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount)
+{
+ d_bv->d_out->safePoint(amount);
+}
+
+EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
+{
+ int numAssertions = d_bv->numAssertions();
+ Debug("bv-equality-status")
+ << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n";
+ Debug("bv-equality-status")
+ << "BVSatSolver has full model? "
+ << (d_fullModelAssertionLevel.get() == numAssertions) << "\n";
+
+ // First check if it trivially rewrites to false/true
+ Node a_eq_b =
+ Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b));
+
+ if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
+ if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
+
+ if (d_fullModelAssertionLevel.get() != numAssertions)
+ {
+ return theory::EQUALITY_UNKNOWN;
+ }
+
+ // Check if cache is valid (invalidated in check and pops)
+ if (d_bv->d_invalidateModelCache.get())
+ {
+ invalidateModelCache();
+ }
+ d_bv->d_invalidateModelCache.set(false);
+
+ Node a_value = getTermModel(a, true);
+ Node b_value = getTermModel(b, true);
+
+ Assert(a_value.isConst() && b_value.isConst());
+
+ if (a_value == b_value)
+ {
+ Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n";
+ return theory::EQUALITY_TRUE_IN_MODEL;
+ }
+ Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n";
+ return theory::EQUALITY_FALSE_IN_MODEL;
+}
+
+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::getModelFromSatSolver(TNode a, bool fullModel) {
+ if (!hasBBTerm(a)) {
+ return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
+ }
+
+ Bits bits;
+ getBBTerm(a, bits);
+ Integer value(0);
+ for (int i = bits.size() -1; i >= 0; --i) {
+ prop::SatValue bit_value;
+ if (d_cnfStream->hasLiteral(bits[i])) {
+ prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+ bit_value = d_satSolver->value(bit);
+ Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+ } else {
+ if (!fullModel) return Node();
+ // unconstrained bits default to false
+ bit_value = prop::SAT_VALUE_FALSE;
+ }
+ Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+ value = value * 2 + bit_int;
+ }
+ return utils::mkConst(bits.size(), value);
+}
+
+bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
+ std::set<Node> termSet;
+ d_bv->computeRelevantTerms(termSet);
+
+ for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
+ TNode var = *it;
+ // not actually a leaf of the bit-vector theory
+ if (d_variables.find(var) == d_variables.end())
+ continue;
+
+ Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
+ // only shared terms could not have been bit-blasted
+ Assert (hasBBTerm(var) || isSharedTerm(var));
+
+ Node const_value = getModelFromSatSolver(var, true);
+ Assert (const_value.isNull() || const_value.isConst());
+ if(const_value != Node()) {
+ Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+ << var << " "
+ << const_value << "))\n";
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
+ d_bvp = bvp;
+ d_satSolver->setProofLog( bvp );
+ bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
+}
+
+void TLazyBitblaster::clearSolver() {
+ Assert (d_ctx->getLevel() == 0);
+ 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();
+
+ invalidateModelCache();
+ // recreate sat solver
+ d_satSolver.reset(
+ prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
+ d_cnfStream.reset(new prop::TseitinCnfStream(
+ d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get()));
+ d_satSolverNotify.reset(
+ d_emptyNotify
+ ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify()
+ : (prop::BVSatSolverInterface::Notify*)new MinisatNotify(
+ d_cnfStream.get(), d_bv, this));
+ d_satSolver->setNotify(d_satSolverNotify.get());
+}
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file lazy_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bitblaster for the lazy bv solver.
+ **
+ ** Bitblaster for the lazy bv solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "prop/cnf_stream.h"
+#include "prop/registrar.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/abstraction.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class TheoryBV;
+
+class TLazyBitblaster : public TBitblaster<Node>
+{
+ public:
+ void bbTerm(TNode node, Bits& bits) override;
+ void bbAtom(TNode node) override;
+ Node getBBAtom(TNode atom) const override;
+ void storeBBAtom(TNode atom, Node atom_bb) override;
+ void storeBBTerm(TNode node, const Bits& bits) override;
+ bool hasBBAtom(TNode atom) const override;
+
+ TLazyBitblaster(context::Context* c,
+ TheoryBV* bv,
+ const std::string name = "",
+ bool emptyNotify = false);
+ ~TLazyBitblaster();
+ /**
+ * Pushes the assumption literal associated with node to the SAT
+ * solver assumption queue.
+ *
+ * @param node assumption
+ * @param propagate run bcp or not
+ *
+ * @return false if a conflict detected
+ */
+ bool assertToSat(TNode node, bool propagate = true);
+ bool propagate();
+ bool solve();
+ prop::SatValue solveWithBudget(unsigned long conflict_budget);
+ void getConflict(std::vector<TNode>& conflict);
+ void explain(TNode atom, std::vector<TNode>& explanation);
+ void setAbstraction(AbstractionModule* abs);
+
+ theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+ /**
+ * Adds a constant value for each bit-blasted variable in the model.
+ *
+ * @param m the model
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
+ */
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
+ void setProofLog(BitVectorProof* bvp);
+
+ typedef TNodeSet::const_iterator vars_iterator;
+ vars_iterator beginVars() { return d_variables.begin(); }
+ vars_iterator endVars() { return d_variables.end(); }
+
+ /**
+ * Creates the bits corresponding to the variable (or non-bv term).
+ *
+ * @param var
+ */
+ void makeVariable(TNode var, Bits& bits) override;
+
+ bool isSharedTerm(TNode node);
+ uint64_t computeAtomWeight(TNode node, NodeSet& seen);
+ /**
+ * Deletes SatSolver and CnfCache, but maintains bit-blasting
+ * terms cache.
+ *
+ */
+ void clearSolver();
+
+ private:
+ typedef std::vector<Node> Bits;
+ typedef context::CDList<prop::SatLiteral> AssertionList;
+ typedef context::CDHashMap<prop::SatLiteral,
+ std::vector<prop::SatLiteral>,
+ prop::SatLiteralHashFunction>
+ ExplanationMap;
+ /** This class gets callbacks from minisat on propagations */
+ class MinisatNotify : public prop::BVSatSolverInterface::Notify
+ {
+ prop::CnfStream* d_cnf;
+ TheoryBV* d_bv;
+ TLazyBitblaster* d_lazyBB;
+
+ public:
+ MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv)
+ : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
+ {
+ }
+
+ bool notify(prop::SatLiteral lit) override;
+ void notify(prop::SatClause& clause) override;
+ void spendResource(unsigned amount) override;
+ void safePoint(unsigned amount) override;
+ };
+
+ TheoryBV* d_bv;
+ context::Context* d_ctx;
+
+ std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+ std::unique_ptr<context::Context> d_nullContext;
+ // sat solver used for bitblasting and associated CnfStream
+ std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
+ std::unique_ptr<prop::BVSatSolverInterface::Notify> d_satSolverNotify;
+ std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+ AssertionList*
+ d_assertedAtoms; /**< context dependent list storing the atoms
+ currently asserted by the DPLL SAT solver. */
+ ExplanationMap* d_explanations; /**< context dependent list of explanations
+ for the propagated literals. Only used when
+ bvEagerPropagate option enabled. */
+ TNodeSet d_variables;
+ TNodeSet d_bbAtoms;
+ AbstractionModule* d_abstraction;
+ bool d_emptyNotify;
+
+ // The size of the fact queue when we most recently called solve() in the
+ // bit-vector SAT solver. This is the level at which we should have
+ // a full model in the bv SAT solver.
+ context::CDO<int> d_fullModelAssertionLevel;
+
+ void addAtom(TNode atom);
+ bool hasValue(TNode a);
+ Node getModelFromSatSolver(TNode a, bool fullModel) override;
+
+ class Statistics
+ {
+ public:
+ IntStat d_numTermClauses, d_numAtomClauses;
+ IntStat d_numTerms, d_numAtoms;
+ IntStat d_numExplainedPropagations;
+ IntStat d_numBitblastingPropagations;
+ TimerStat d_bitblastTimer;
+ Statistics(const std::string& name);
+ ~Statistics();
+ };
+ std::string d_name;
+
+ // NOTE: d_statistics is public since d_bitblastTimer needs to be initalized
+ // prior to calling bbAtom. As it is now, the timer can't be initialized
+ // in bbAtom since the method is called recursively and the timer would
+ // be initialized multiple times, which is not allowed.
+ public:
+ Statistics d_statistics;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+#endif // __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+++ /dev/null
-/********************* */
-/*! \file bitblast_strategies_template.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Aina Niemetz, Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of bitblasting functions for various operators.
- **
- ** Implementation of bitblasting functions for various operators.
- **/
-
-#ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
-#define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
-
-#include <cmath>
-#include <ostream>
-
-#include "cvc4_private.h"
-#include "expr/node.h"
-#include "theory/bv/bitblast_utils.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/rewriter.h"
-
-namespace CVC4 {
-
-namespace theory {
-namespace bv {
-
-/**
- * Default Atom Bitblasting strategies:
- *
- * @param node the atom to be bitblasted
- * @param bb the bitblaster
- */
-
-template <class T>
-T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) {
- Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
- << node.getKind() << "\n";
- Unreachable();
-}
-
-
-template <class T>
-T DefaultEqBB(TNode node, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
-
- Assert(node.getKind() == kind::EQUAL);
- std::vector<T> lhs, rhs;
- bb->bbTerm(node[0], lhs);
- bb->bbTerm(node[1], rhs);
-
- Assert(lhs.size() == rhs.size());
-
- std::vector<T> bits_eq;
- for (unsigned i = 0; i < lhs.size(); i++) {
- T bit_eq = mkIff(lhs[i], rhs[i]);
- bits_eq.push_back(bit_eq);
- }
- T bv_eq = mkAnd(bits_eq);
- return bv_eq;
-}
-
-template <class T>
-T AdderUltBB(TNode node, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_ULT);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
-
- // a < b <=> ~ (add(a, ~b, 1).carry_out)
- std::vector<T> not_b;
- negateBits(b, not_b);
- T carry = mkTrue<T>();
-
- for (unsigned i = 0 ; i < a.size(); ++i) {
- carry = mkOr( mkAnd(a[i], not_b[i]),
- mkAnd( mkXor(a[i], not_b[i]),
- carry));
- }
- return mkNot(carry);
-}
-
-
-template <class T>
-T DefaultUltBB(TNode node, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_ULT);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
-
- // construct bitwise comparison
- T res = uLessThanBB(a, b, false);
- return res;
-}
-
-template <class T>
-T DefaultUleBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_ULE);
- std::vector<T> a, b;
-
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
- // construct bitwise comparison
- T res = uLessThanBB(a, b, true);
- return res;
-}
-
-template <class T>
-T DefaultUgtBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- // should be rewritten
- Unimplemented();
-}
-template <class T>
-T DefaultUgeBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- // should be rewritten
- Unimplemented();
-}
-
-template <class T>
-T DefaultSltBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
-
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
-
- T res = sLessThanBB(a, b, false);
- return res;
-}
-
-template <class T>
-T DefaultSleBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
-
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
-
- T res = sLessThanBB(a, b, true);
- return res;
-}
-
-template <class T>
-T DefaultSgtBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- // should be rewritten
- Unimplemented();
-}
-
-template <class T>
-T DefaultSgeBB(TNode node, TBitblaster<T>* bb){
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- // should be rewritten
- Unimplemented();
-}
-
-
-/// Term bitblasting strategies
-
-/**
- * Default Term Bitblasting strategies
- *
- * @param node the term to be bitblasted
- * @param bits [output parameter] bits representing the new term
- * @param bb the bitblaster in which the clauses are added
- */
-template <class T>
-void UndefinedTermBBStrategy(TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
- << node.getKind() << "\n";
- Unreachable();
-}
-
-template <class T>
-void DefaultVarBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Assert(bits.size() == 0);
- bb->makeVariable(node, bits);
-
- if(Debug.isOn("bitvector-bb")) {
- Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n";
- Debug("bitvector-bb") << " with bits " << toString(bits);
- }
-}
-
-template <class T>
-void DefaultConstBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
- Assert(node.getKind() == kind::CONST_BITVECTOR);
- Assert(bits.size() == 0);
-
- for (unsigned i = 0; i < utils::getSize(node); ++i) {
- Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
- if(bit == Integer(0)){
- bits.push_back(mkFalse<T>());
- } else {
- Assert (bit == Integer(1));
- bits.push_back(mkTrue<T>());
- }
- }
- if(Debug.isOn("bitvector-bb")) {
- Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
- }
-}
-
-
-template <class T>
-void DefaultNotBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_NOT);
- Assert(bits.size() == 0);
- std::vector<T> bv;
- bb->bbTerm(node[0], bv);
- negateBits(bv, bits);
-}
-
-template <class T>
-void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
- Assert(bits.size() == 0);
-
- Assert (node.getKind() == kind::BITVECTOR_CONCAT);
- for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
- TNode current = node[i];
- std::vector<T> current_bits;
- bb->bbTerm(current, current_bits);
-
- for(unsigned j = 0; j < utils::getSize(current); ++j) {
- bits.push_back(current_bits[j]);
- }
- }
- Assert (bits.size() == utils::getSize(node));
- if(Debug.isOn("bitvector-bb")) {
- Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
- }
-}
-
-template <class T>
-void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
-
- Assert(node.getKind() == kind::BITVECTOR_AND &&
- bits.size() == 0);
-
- bb->bbTerm(node[0], bits);
- std::vector<T> current;
- for(unsigned j = 1; j < node.getNumChildren(); ++j) {
- bb->bbTerm(node[j], current);
- for (unsigned i = 0; i < utils::getSize(node); ++i) {
- bits[i] = mkAnd(bits[i], current[i]);
- }
- current.clear();
- }
- Assert (bits.size() == utils::getSize(node));
-}
-
-template <class T>
-void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
-
- Assert(node.getKind() == kind::BITVECTOR_OR &&
- bits.size() == 0);
-
- bb->bbTerm(node[0], bits);
- std::vector<T> current;
- for(unsigned j = 1; j < node.getNumChildren(); ++j) {
- bb->bbTerm(node[j], current);
- for (unsigned i = 0; i < utils::getSize(node); ++i) {
- bits[i] = mkOr(bits[i], current[i]);
- }
- current.clear();
- }
- Assert (bits.size() == utils::getSize(node));
-}
-
-template <class T>
-void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
-
- Assert(node.getKind() == kind::BITVECTOR_XOR &&
- bits.size() == 0);
-
- bb->bbTerm(node[0], bits);
- std::vector<T> current;
- for(unsigned j = 1; j < node.getNumChildren(); ++j) {
- bb->bbTerm(node[j], current);
- for (unsigned i = 0; i < utils::getSize(node); ++i) {
- bits[i] = mkXor(bits[i], current[i]);
- }
- current.clear();
- }
- Assert (bits.size() == utils::getSize(node));
-}
-
-template <class T>
-void DefaultXnorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
-
- Assert(node.getNumChildren() == 2 &&
- node.getKind() == kind::BITVECTOR_XNOR &&
- bits.size() == 0);
- std::vector<T> lhs, rhs;
- bb->bbTerm(node[0], lhs);
- bb->bbTerm(node[1], rhs);
- Assert(lhs.size() == rhs.size());
-
- for (unsigned i = 0; i < lhs.size(); ++i) {
- bits.push_back(mkIff(lhs[i], rhs[i]));
- }
-}
-
-
-template <class T>
-void DefaultNandBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- Unimplemented();
-}
-template <class T>
-void DefaultNorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- Unimplemented();
-}
-template <class T>
-void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
-
- Assert(utils::getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
-
- std::vector<T> bit_eqs;
- for (unsigned i = 0; i < a.size(); ++i) {
- T eq = mkIff(a[i], b[i]);
- bit_eqs.push_back(eq);
- }
- T a_eq_b = mkAnd(bit_eqs);
- bits.push_back(a_eq_b);
-}
-
-template <class T>
-void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
- Assert(res.size() == 0 &&
- node.getKind() == kind::BITVECTOR_MULT);
-
- // if (node.getNumChildren() == 2) {
- // std::vector<T> a;
- // std::vector<T> b;
- // bb->bbTerm(node[0], a);
- // bb->bbTerm(node[1], b);
- // unsigned bw = utils::getSize(node);
- // unsigned thresh = bw % 2 ? bw/2 : bw/2 - 1;
- // bool no_overflow = true;
- // for (unsigned i = thresh; i < bw; ++i) {
- // if (a[i] != mkFalse<T> || b[i] != mkFalse<T> ) {
- // no_overflow = false;
- // }
- // }
- // if (no_overflow) {
- // shiftAddMultiplier();
- // return;
- // }
-
- // }
-
- std::vector<T> newres;
- bb->bbTerm(node[0], res);
- for(unsigned i = 1; i < node.getNumChildren(); ++i) {
- std::vector<T> current;
- bb->bbTerm(node[i], current);
- newres.clear();
- // constructs a simple shift and add multiplier building the result
- // in res
- shiftAddMultiplier(res, current, newres);
- res = newres;
- }
- if(Debug.isOn("bitvector-bb")) {
- Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
- }
-}
-
-template <class T>
-void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_PLUS &&
- res.size() == 0);
-
- bb->bbTerm(node[0], res);
-
- std::vector<T> newres;
-
- for(unsigned i = 1; i < node.getNumChildren(); ++i) {
- std::vector<T> current;
- bb->bbTerm(node[i], current);
- newres.clear();
- rippleCarryAdder(res, current, newres, mkFalse<T>());
- res = newres;
- }
-
- Assert(res.size() == utils::getSize(node));
-}
-
-
-template <class T>
-void DefaultSubBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_SUB &&
- node.getNumChildren() == 2 &&
- bits.size() == 0);
-
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size() && utils::getSize(node) == a.size());
-
- // bvsub a b = adder(a, ~b, 1)
- std::vector<T> not_b;
- negateBits(b, not_b);
- rippleCarryAdder(a, not_b, bits, mkTrue<T>());
-}
-
-template <class T>
-void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_NEG);
-
- std::vector<T> a;
- bb->bbTerm(node[0], a);
- Assert(utils::getSize(node) == a.size());
-
- // -a = add(~a, 0, 1).
- std::vector<T> not_a;
- negateBits(a, not_a);
- std::vector<T> zero;
- makeZero(zero, utils::getSize(node));
-
- rippleCarryAdder(not_a, zero, bits, mkTrue<T>());
-}
-
-template <class T>
-void uDivModRec(const std::vector<T>& a, const std::vector<T>& b, std::vector<T>& q, std::vector<T>& r, unsigned rec_width) {
- Assert( q.size() == 0 && r.size() == 0);
-
- if(rec_width == 0 || isZero(a)) {
- makeZero(q, a.size());
- makeZero(r, a.size());
- return;
- }
-
- std::vector<T> q1, r1;
- std::vector<T> a1 = a;
- rshift(a1, 1);
-
- uDivModRec(a1, b, q1, r1, rec_width - 1);
- // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd
- lshift(q1, 1);
- lshift(r1, 1);
-
-
- T is_odd = mkIff(a[0], mkTrue<T>());
- T one_if_odd = mkIte(is_odd, mkTrue<T>(), mkFalse<T>());
-
- std::vector<T> zero;
- makeZero(zero, b.size());
-
- std::vector<T> r1_shift_add;
- // account for a being odd
- rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd);
- // now check if the remainder is greater than b
- std::vector<T> not_b;
- negateBits(b, not_b);
- std::vector<T> r_minus_b;
- T co1;
- // use adder because we need r_minus_b anyway
- co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue<T>());
- // sign is true if r1 < b
- T sign = mkNot(co1);
-
- q1[0] = mkIte(sign, q1[0], mkTrue<T>());
-
- // would be nice to have a high level ITE instead of bitwise
- for(unsigned i = 0; i < a.size(); ++i) {
- r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]);
- }
-
- // check if a < b
-
- std::vector<T> a_minus_b;
- T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue<T>());
- // Node a_lt_b = a_minus_b.back();
- T a_lt_b = mkNot(co2);
-
- for(unsigned i = 0; i < a.size(); ++i) {
- T qval = mkIte(a_lt_b, mkFalse<T>(), q1[i]);
- T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]);
- q.push_back(qval);
- r.push_back(rval);
- }
-
-}
-
-template <class T>
-void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb)
-{
- Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node
- << "\n";
- Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0);
-
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
-
- std::vector<T> r;
- uDivModRec(a, b, q, r, utils::getSize(node));
- // adding a special case for division by 0
- std::vector<T> iszero;
- for (unsigned i = 0; i < b.size(); ++i)
- {
- iszero.push_back(mkIff(b[i], mkFalse<T>()));
- }
- T b_is_0 = mkAnd(iszero);
-
- for (unsigned i = 0; i < q.size(); ++i)
- {
- q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
- r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a
- }
-
- // cache the remainder in case we need it later
- Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
- kind::BITVECTOR_UREM_TOTAL, node[0], node[1]));
- bb->storeBBTerm(remainder, r);
-}
-
-template <class T>
-void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb)
-{
- Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node
- << "\n";
- Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0);
-
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
-
- std::vector<T> q;
- uDivModRec(a, b, q, rem, utils::getSize(node));
- // adding a special case for division by 0
- std::vector<T> iszero;
- for (unsigned i = 0; i < b.size(); ++i)
- {
- iszero.push_back(mkIff(b[i], mkFalse<T>()));
- }
- T b_is_0 = mkAnd(iszero);
-
- for (unsigned i = 0; i < q.size(); ++i)
- {
- q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
- rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a
- }
-
- // cache the quotient in case we need it later
- Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
- kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]));
- bb->storeBBTerm(quotient, q);
-}
-
-template <class T>
-void DefaultSdivBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- Unimplemented();
-}
-template <class T>
-void DefaultSremBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- Unimplemented();
-}
-template <class T>
-void DefaultSmodBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- Unimplemented();
-}
-
-template <class T>
-void DefaultShlBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
-{
- Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node
- << "\n";
- Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
-
- // check for b < log2(n)
- unsigned size = utils::getSize(node);
- unsigned log2_size = std::ceil(log2((double)size));
- Node a_size = utils::mkConst(size, size);
- Node b_ult_a_size_node = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
- // ensure that the inequality is bit-blasted
- bb->bbAtom(b_ult_a_size_node);
- T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
- std::vector<T> prev_res;
- res = a;
- // we only need to look at the bits bellow log2_a_size
- for (unsigned s = 0; s < log2_size; ++s)
- {
- // barrel shift stage: at each stage you can either shift by 2^s bits
- // or leave the previous stage untouched
- prev_res = res;
- unsigned threshold = pow(2, s);
- for (unsigned i = 0; i < a.size(); ++i)
- {
- if (i < threshold)
- {
- // if b[s] is true then we must have shifted by at least 2^b bits so
- // all bits bellow 2^s will be 0, otherwise just use previous shift
- // value
- res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
- }
- else
- {
- // if b[s]= 0, use previous value, otherwise shift by threshold bits
- Assert(i >= threshold);
- res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]);
- }
- }
- }
- prev_res = res;
- for (unsigned i = 0; i < b.size(); ++i)
- {
- // this is fine because b_ult_a_size has been bit-blasted
- res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
- }
-
- if (Debug.isOn("bitvector-bb"))
- {
- Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
- }
-}
-
-template <class T>
-void DefaultLshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
-{
- Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node
- << "\n";
- Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
-
- // check for b < log2(n)
- unsigned size = utils::getSize(node);
- unsigned log2_size = std::ceil(log2((double)size));
- Node a_size = utils::mkConst(size, size);
- Node b_ult_a_size_node = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
- // ensure that the inequality is bit-blasted
- bb->bbAtom(b_ult_a_size_node);
- T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
- res = a;
- std::vector<T> prev_res;
-
- for (unsigned s = 0; s < log2_size; ++s)
- {
- // barrel shift stage: at each stage you can either shift by 2^s bits
- // or leave the previous stage untouched
- prev_res = res;
- int threshold = pow(2, s);
- for (unsigned i = 0; i < a.size(); ++i)
- {
- if (i + threshold >= a.size())
- {
- // if b[s] is true then we must have shifted by at least 2^b bits so
- // all bits above 2^s will be 0, otherwise just use previous shift value
- res[i] = mkIte(b[s], mkFalse<T>(), prev_res[i]);
- }
- else
- {
- // if b[s]= 0, use previous value, otherwise shift by threshold bits
- Assert(i + threshold < a.size());
- res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]);
- }
- }
- }
-
- prev_res = res;
- for (unsigned i = 0; i < b.size(); ++i)
- {
- // this is fine because b_ult_a_size has been bit-blasted
- res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse<T>());
- }
-
- if (Debug.isOn("bitvector-bb"))
- {
- Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
- }
-}
-
-template <class T>
-void DefaultAshrBB(TNode node, std::vector<T>& res, TBitblaster<T>* bb)
-{
- Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node
- << "\n";
- Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
-
- // check for b < n
- unsigned size = utils::getSize(node);
- unsigned log2_size = std::ceil(log2((double)size));
- Node a_size = utils::mkConst(size, size);
- Node b_ult_a_size_node = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size));
- // ensure that the inequality is bit-blasted
- bb->bbAtom(b_ult_a_size_node);
- T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node);
-
- res = a;
- T sign_bit = a.back();
- std::vector<T> prev_res;
-
- for (unsigned s = 0; s < log2_size; ++s)
- {
- // barrel shift stage: at each stage you can either shift by 2^s bits
- // or leave the previous stage untouched
- prev_res = res;
- int threshold = pow(2, s);
- for (unsigned i = 0; i < a.size(); ++i)
- {
- if (i + threshold >= a.size())
- {
- // if b[s] is true then we must have shifted by at least 2^b bits so
- // all bits above 2^s will be the sign bit, otherwise just use previous
- // shift value
- res[i] = mkIte(b[s], sign_bit, prev_res[i]);
- }
- else
- {
- // if b[s]= 0, use previous value, otherwise shift by threshold bits
- Assert(i + threshold < a.size());
- res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]);
- }
- }
- }
-
- prev_res = res;
- for (unsigned i = 0; i < b.size(); ++i)
- {
- // this is fine because b_ult_a_size has been bit-blasted
- res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit);
- }
-
- if (Debug.isOn("bitvector-bb"))
- {
- Debug("bitvector-bb") << "with bits: " << toString(res) << "\n";
- }
-}
-
-template <class T>
-void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_ULTBV);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
-
- // construct bitwise comparison
- res.push_back(uLessThanBB(a, b, false));
-}
-
-template <class T>
-void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_SLTBV);
- std::vector<T> a, b;
- bb->bbTerm(node[0], a);
- bb->bbTerm(node[1], b);
- Assert(a.size() == b.size());
-
- // construct bitwise comparison
- res.push_back(sLessThanBB(a, b, false));
-}
-
-template <class T>
-void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "Bitblasting node " << node << "\n";
- Assert(node.getKind() == kind::BITVECTOR_ITE);
- std::vector<T> cond, thenpart, elsepart;
- bb->bbTerm(node[0], cond);
- bb->bbTerm(node[1], thenpart);
- bb->bbTerm(node[2], elsepart);
-
- Assert(cond.size() == 1);
- Assert(thenpart.size() == elsepart.size());
-
- for (unsigned i = 0; i < thenpart.size(); ++i) {
- // (~cond OR thenpart) AND (cond OR elsepart)
- res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i])));
- }
-}
-
-template <class T>
-void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
- Assert(bits.size() == 0);
-
- std::vector<T> base_bits;
- bb->bbTerm(node[0], base_bits);
- unsigned high = utils::getExtractHigh(node);
- unsigned low = utils::getExtractLow(node);
-
- for (unsigned i = low; i <= high; ++i) {
- bits.push_back(base_bits[i]);
- }
- Assert (bits.size() == high - low + 1);
-
- if(Debug.isOn("bitvector-bb")) {
- Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
- Debug("bitvector-bb") << " with bits " << toString(bits);
- }
-}
-
-
-template <class T>
-void DefaultRepeatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- // this should be rewritten
- Unimplemented();
-}
-
-template <class T>
-void DefaultZeroExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
-
- Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n";
-
- // this should be rewritten
- Unimplemented();
-
-}
-
-template <class T>
-void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>* bb) {
- Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n";
-
- Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
- res_bits.size() == 0);
-
- std::vector<T> bits;
- bb->bbTerm(node[0], bits);
-
- T sign_bit = bits.back();
- unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
-
- for (unsigned i = 0; i < bits.size(); ++i ) {
- res_bits.push_back(bits[i]);
- }
-
- for (unsigned i = 0 ; i < amount ; ++i ) {
- res_bits.push_back(sign_bit);
- }
-
- Assert (res_bits.size() == amount + bits.size());
-}
-
-template <class T>
-void DefaultRotateRightBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
-
- Unimplemented();
-}
-
-template <class T>
-void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Debug("bitvector") << "theory::bv:: Unimplemented kind "
- << node.getKind() << "\n";
- Unimplemented();
-}
-
-
-}
-}
-}
-
-#endif
+++ /dev/null
-/********************* */
-/*! \file bitblast_utils.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Paul Meng, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Various utility functions for bit-blasting.
- **
- ** Various utility functions for bit-blasting.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__BITBLAST__UTILS_H
-#define __CVC4__BITBLAST__UTILS_H
-
-
-#include <ostream>
-#include "expr/node.h"
-
-#ifdef CVC4_USE_ABC
-#include "base/main/main.h"
-#include "base/abc/abc.h"
-
-extern "C" {
-#include "sat/cnf/cnf.h"
-}
-#endif
-
-namespace CVC4 {
-
-namespace theory {
-namespace bv {
-
-template <class T> class TBitblaster;
-
-template <class T>
-std::string toString (const std::vector<T>& bits);
-
-template <> inline
-std::string toString<Node> (const std::vector<Node>& bits) {
- std::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();
-}
-
-template <class T> T mkTrue();
-template <class T> T mkFalse();
-template <class T> T mkNot(T a);
-template <class T> T mkOr(T a, T b);
-template <class T> T mkOr(const std::vector<T>& a);
-template <class T> T mkAnd(T a, T b);
-template <class T> T mkAnd(const std::vector<T>& a);
-template <class T> T mkXor(T a, T b);
-template <class T> T mkIff(T a, T b);
-template <class T> T mkIte(T cond, T a, T b);
-
-
-template <> inline
-Node mkTrue<Node>() {
- return NodeManager::currentNM()->mkConst<bool>(true);
-}
-
-template <> inline
-Node mkFalse<Node>() {
- return NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-template <> inline
-Node mkNot<Node>(Node a) {
- return NodeManager::currentNM()->mkNode(kind::NOT, a);
-}
-
-template <> inline
-Node mkOr<Node>(Node a, Node b) {
- return NodeManager::currentNM()->mkNode(kind::OR, a, b);
-}
-
-template <> inline
-Node mkOr<Node>(const std::vector<Node>& children) {
- Assert (children.size());
- if (children.size() == 1)
- return children[0];
- return NodeManager::currentNM()->mkNode(kind::OR, children);
-}
-
-
-template <> inline
-Node mkAnd<Node>(Node a, Node b) {
- return NodeManager::currentNM()->mkNode(kind::AND, a, b);
-}
-
-template <> inline
-Node mkAnd<Node>(const std::vector<Node>& children) {
- Assert (children.size());
- if (children.size() == 1)
- return children[0];
- return NodeManager::currentNM()->mkNode(kind::AND, children);
-}
-
-
-template <> inline
-Node mkXor<Node>(Node a, Node b) {
- return NodeManager::currentNM()->mkNode(kind::XOR, a, b);
-}
-
-template <> inline
-Node mkIff<Node>(Node a, Node b) {
- return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
-}
-
-template <> inline
-Node mkIte<Node>(Node cond, Node a, Node b) {
- return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b);
-}
-
-/*
- Various helper functions that get called by the bitblasting procedures
- */
-
-template <class T>
-void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
- Assert ( lo < b.size() && hi < b.size() && lo <= hi);
- for (unsigned i = lo; i <= hi; ++i) {
- dest.push_back(b[i]);
- }
-}
-
-template <class T>
-void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
- for(unsigned i = 0; i < bits.size(); ++i) {
- negated_bits.push_back(mkNot(bits[i]));
- }
-}
-
-template <class T>
-bool inline isZero(const std::vector<T>& bits) {
- for(unsigned i = 0; i < bits.size(); ++i) {
- if(bits[i] != mkFalse<T>()) {
- return false;
- }
- }
- return true;
-}
-
-template <class T>
-void inline rshift(std::vector<T>& bits, unsigned amount) {
- for (unsigned i = 0; i < bits.size() - amount; ++i) {
- bits[i] = bits[i+amount];
- }
- for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
- bits[i] = mkFalse<T>();
- }
-}
-
-template <class T>
-void inline lshift(std::vector<T>& bits, unsigned amount) {
- for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
- bits[i] = bits[i-amount];
- }
- for(unsigned i = 0; i < amount; ++i) {
- bits[i] = mkFalse<T>();
- }
-}
-
-template <class T>
-void inline makeZero(std::vector<T>& bits, unsigned width) {
- Assert(bits.size() == 0);
- for(unsigned i = 0; i < width; ++i) {
- bits.push_back(mkFalse<T>());
- }
-}
-
-
-/**
- * Constructs a simple ripple carry adder
- *
- * @param a first term to be added
- * @param b second term to be added
- * @param res the result
- * @param carry the carry-in bit
- *
- * @return the carry-out
- */
-template <class T>
-T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
- Assert(a.size() == b.size() && res.size() == 0);
-
- for (unsigned i = 0 ; i < a.size(); ++i) {
- T sum = mkXor(mkXor(a[i], b[i]), carry);
- carry = mkOr( mkAnd(a[i], b[i]),
- mkAnd( mkXor(a[i], b[i]),
- carry));
- res.push_back(sum);
- }
-
- return carry;
-}
-
-template <class T>
-inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, std::vector<T>& res) {
-
- for (unsigned i = 0; i < a.size(); ++i) {
- res.push_back(mkAnd(b[0], a[i]));
- }
-
- for(unsigned k = 1; k < res.size(); ++k) {
- T carry_in = mkFalse<T>();
- T carry_out;
- for(unsigned j = 0; j < res.size() -k; ++j) {
- T aj = mkAnd(b[k], a[j]);
- carry_out = mkOr(mkAnd(res[j+k], aj),
- mkAnd( mkXor(res[j+k], aj), carry_in));
- res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
- carry_in = carry_out;
- }
- }
-}
-
-template <class T>
-T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
- Assert (a.size() && b.size());
-
- T res = mkAnd(mkNot(a[0]), b[0]);
-
- if(orEqual) {
- res = mkOr(res, mkIff(a[0], b[0]));
- }
-
- for (unsigned i = 1; i < a.size(); ++i) {
- // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
- res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
- mkAnd(mkNot(a[i]), b[i]));
- }
- return res;
-}
-
-template <class T>
-T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
- Assert (a.size() && b.size());
- if (a.size() == 1) {
- if(orEqual) {
- return mkOr(mkIff(a[0], b[0]),
- mkAnd(a[0], mkNot(b[0])));
- }
-
- return mkAnd(a[0], mkNot(b[0]));
- }
- unsigned n = a.size() - 1;
- std::vector<T> a1, b1;
- extractBits(a, a1, 0, n-1);
- extractBits(b, b1, 0, n-1);
-
- // unsigned comparison of the first n-1 bits
- T ures = uLessThanBB(a1, b1, orEqual);
- T res = mkOr(// a b have the same sign
- mkAnd(mkIff(a[n], b[n]),
- ures),
- // a is negative and b positive
- mkAnd(a[n],
- mkNot(b[n])));
- return res;
-}
-
-
-}
-}
-}
-
-#endif
+++ /dev/null
-/********************* */
-/*! \file bitblaster_template.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Wrapper around the SAT solver used for bitblasting
- **
- ** Wrapper around the SAT solver used for bitblasting.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__BITBLASTER_TEMPLATE_H
-#define __CVC4__BITBLASTER_TEMPLATE_H
-
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
-
-#include "bitblast_strategies_template.h"
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "prop/sat_solver.h"
-#include "theory/theory_registrar.h"
-#include "theory/valuation.h"
-#include "util/resource_manager.h"
-
-class Abc_Obj_t_;
-typedef Abc_Obj_t_ Abc_Obj_t;
-
-class Abc_Ntk_t_;
-typedef Abc_Ntk_t_ Abc_Ntk_t;
-
-class Abc_Aig_t_;
-typedef Abc_Aig_t_ Abc_Aig_t;
-
-class Cnf_Dat_t_;
-typedef Cnf_Dat_t_ Cnf_Dat_t;
-
-
-namespace CVC4 {
-namespace prop {
-class CnfStream;
-class BVSatSolverInterface;
-class NullRegistrar;
-}
-
-namespace theory {
-class OutputChannel;
-class TheoryModel;
-
-namespace bv {
-
-class BitblastingRegistrar;
-
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-
-class AbstractionModule;
-
-/**
- * The Bitblaster that manages the mapping between Nodes
- * and their bitwise definition
- *
- */
-
-template <class T>
-class TBitblaster {
-protected:
- typedef std::vector<T> Bits;
- typedef std::unordered_map <Node, Bits, NodeHashFunction> TermDefMap;
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
-
- typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
- typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*);
-
- // caches and mappings
- TermDefMap d_termCache;
- ModelCache d_modelCache;
-
- BitVectorProof * d_bvp;
-
- void initAtomBBStrategies();
- void initTermBBStrategies();
-protected:
- /// function tables for the various bitblasting strategies indexed by node kind
- TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
- AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
- virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
-public:
- TBitblaster();
- virtual ~TBitblaster() {}
- virtual void bbAtom(TNode node) = 0;
- virtual void bbTerm(TNode node, Bits& bits) = 0;
- virtual void makeVariable(TNode node, Bits& bits) = 0;
- virtual T getBBAtom(TNode atom) const = 0;
- virtual bool hasBBAtom(TNode atom) const = 0;
- virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
-
-
- bool hasBBTerm(TNode node) const;
- void getBBTerm(TNode node, Bits& bits) const;
- virtual void storeBBTerm(TNode term, const Bits& bits);
- /**
- * Return a constant representing the value of a in the model.
- * If fullModel is true set unconstrained bits to 0. If not return
- * NullNode() for a fully or partially unconstrained.
- *
- */
- Node getTermModel(TNode node, bool fullModel);
- void invalidateModelCache();
-};
-
-
-class TheoryBV;
-
-class TLazyBitblaster : public TBitblaster<Node> {
- typedef std::vector<Node> Bits;
- typedef context::CDList<prop::SatLiteral> AssertionList;
- typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap;
- /** This class gets callbacks from minisat on propagations */
- class MinisatNotify : public prop::BVSatSolverInterface::Notify {
- prop::CnfStream* d_cnf;
- TheoryBV *d_bv;
- TLazyBitblaster* d_lazyBB;
- public:
- MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv)
- : d_cnf(cnf)
- , d_bv(bv)
- , d_lazyBB(lbv)
- {}
-
- bool notify(prop::SatLiteral lit) override;
- void notify(prop::SatClause& clause) override;
- void spendResource(unsigned amount) override;
- void safePoint(unsigned amount) override;
- };
-
- TheoryBV *d_bv;
- context::Context* d_ctx;
-
- prop::NullRegistrar* d_nullRegistrar;
- context::Context* d_nullContext;
- // sat solver used for bitblasting and associated CnfStream
- prop::BVSatSolverInterface* d_satSolver;
- prop::BVSatSolverInterface::Notify* d_satSolverNotify;
- prop::CnfStream* d_cnfStream;
-
- AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms
- currently asserted by the DPLL SAT solver. */
- ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
- Only used when bvEagerPropagate option enabled. */
- TNodeSet d_variables;
- TNodeSet d_bbAtoms;
- AbstractionModule* d_abstraction;
- bool d_emptyNotify;
-
- // The size of the fact queue when we most recently called solve() in the
- // bit-vector SAT solver. This is the level at which we should have
- // a full model in the bv SAT solver.
- context::CDO<int> d_fullModelAssertionLevel;
-
- void addAtom(TNode atom);
- bool hasValue(TNode a);
- Node getModelFromSatSolver(TNode a, bool fullModel) override;
-
- public:
- void bbTerm(TNode node, Bits& bits) override;
- void bbAtom(TNode node) override;
- Node getBBAtom(TNode atom) const override;
- void storeBBAtom(TNode atom, Node atom_bb) override;
- void storeBBTerm(TNode node, const Bits& bits) override;
- bool hasBBAtom(TNode atom) const override;
-
- TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
- ~TLazyBitblaster();
- /**
- * Pushes the assumption literal associated with node to the SAT
- * solver assumption queue.
- *
- * @param node assumption
- * @param propagate run bcp or not
- *
- * @return false if a conflict detected
- */
- bool assertToSat(TNode node, bool propagate = true);
- bool propagate();
- bool solve();
- prop::SatValue solveWithBudget(unsigned long conflict_budget);
- void getConflict(std::vector<TNode>& conflict);
- void explain(TNode atom, std::vector<TNode>& explanation);
- void setAbstraction(AbstractionModule* abs);
-
- theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
-
- /**
- * Adds a constant value for each bit-blasted variable in the model.
- *
- * @param m the model
- * @param fullModel whether to create a "full model," i.e., add
- * constants to equivalence classes that don't already have them
- */
- bool collectModelInfo(TheoryModel* m, bool fullModel);
- void setProofLog( BitVectorProof * bvp );
-
- typedef TNodeSet::const_iterator vars_iterator;
- vars_iterator beginVars() { return d_variables.begin(); }
- vars_iterator endVars() { return d_variables.end(); }
-
- /**
- * Creates the bits corresponding to the variable (or non-bv term).
- *
- * @param var
- */
- void makeVariable(TNode var, Bits& bits) override;
-
- bool isSharedTerm(TNode node);
- uint64_t computeAtomWeight(TNode node, NodeSet& seen);
- /**
- * Deletes SatSolver and CnfCache, but maintains bit-blasting
- * terms cache.
- *
- */
- void clearSolver();
-private:
-
- class Statistics {
- public:
- IntStat d_numTermClauses, d_numAtomClauses;
- IntStat d_numTerms, d_numAtoms;
- IntStat d_numExplainedPropagations;
- IntStat d_numBitblastingPropagations;
- TimerStat d_bitblastTimer;
- Statistics(const std::string& name);
- ~Statistics();
- };
- std::string d_name;
-public:
- Statistics d_statistics;
-};
-
-class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify {
-public:
- MinisatEmptyNotify() {}
- bool notify(prop::SatLiteral lit) override { return true; }
- void notify(prop::SatClause& clause) override {}
- void spendResource(unsigned amount) override
- {
- NodeManager::currentResourceManager()->spendResource(amount);
- }
- void safePoint(unsigned amount) override {}
-};
-
-
-class EagerBitblaster : public TBitblaster<Node> {
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- // sat solver used for bitblasting and associated CnfStream
- prop::SatSolver* d_satSolver;
- BitblastingRegistrar* d_bitblastingRegistrar;
- context::Context* d_nullContext;
- prop::CnfStream* d_cnfStream;
-
- theory::bv::TheoryBV* d_bv;
- TNodeSet d_bbAtoms;
- TNodeSet d_variables;
-
- // This is either an MinisatEmptyNotify or NULL.
- MinisatEmptyNotify* d_notify;
-
- Node getModelFromSatSolver(TNode a, bool fullModel) override;
- bool isSharedTerm(TNode node);
-
-public:
- EagerBitblaster(theory::bv::TheoryBV* theory_bv);
- ~EagerBitblaster();
-
- void addAtom(TNode atom);
- void makeVariable(TNode node, Bits& bits) override;
- void bbTerm(TNode node, Bits& bits) override;
- void bbAtom(TNode node) override;
- Node getBBAtom(TNode node) const override;
- bool hasBBAtom(TNode atom) const override;
- void bbFormula(TNode formula);
- void storeBBAtom(TNode atom, Node atom_bb) override;
- void storeBBTerm(TNode node, const Bits& bits) override;
-
- bool assertToSat(TNode node, bool propagate = true);
- bool solve();
- bool collectModelInfo(TheoryModel* m, bool fullModel);
- void setProofLog( BitVectorProof * bvp );
-};
-
-class BitblastingRegistrar: public prop::Registrar {
- EagerBitblaster* d_bitblaster;
-public:
- BitblastingRegistrar(EagerBitblaster* bb)
- : d_bitblaster(bb)
- {}
- void preRegister(Node n) override;
-}; /* class Registrar */
-
-class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
- typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
- typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
-
- static Abc_Ntk_t* abcAigNetwork;
- context::Context* d_nullContext;
- prop::SatSolver* d_satSolver;
- TNodeAigMap d_aigCache;
- NodeAigMap d_bbAtoms;
-
- NodeAigMap d_nodeToAigInput;
- // the thing we are checking for sat
- Abc_Obj_t* d_aigOutputNode;
-
- void addAtom(TNode atom);
- void simplifyAig();
- void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
- Abc_Obj_t* getBBAtom(TNode atom) const override;
- bool hasBBAtom(TNode atom) const override;
- void cacheAig(TNode node, Abc_Obj_t* aig);
- bool hasAig(TNode node);
- Abc_Obj_t* getAig(TNode node);
- Abc_Obj_t* mkInput(TNode input);
- bool hasInput(TNode input);
- void convertToCnfAndAssert();
- void assertToSatSolver(Cnf_Dat_t* pCnf);
- Node getModelFromSatSolver(TNode a, bool fullModel) override
- {
- Unreachable();
- }
-
- public:
- AigBitblaster();
- ~AigBitblaster();
-
- void makeVariable(TNode node, Bits& bits) override;
- void bbTerm(TNode node, Bits& bits) override;
- void bbAtom(TNode node) override;
- Abc_Obj_t* bbFormula(TNode formula);
- bool solve(TNode query);
- static Abc_Aig_t* currentAigM();
- static Abc_Ntk_t* currentAigNtk();
-
-private:
- class Statistics {
- public:
- IntStat d_numClauses;
- IntStat d_numVariables;
- TimerStat d_simplificationTime;
- TimerStat d_cnfConversionTime;
- TimerStat d_solveTime;
- Statistics();
- ~Statistics();
- };
-
- Statistics d_statistics;
-
-};
-
-
-// Bitblaster implementation
-
-template <class T> void TBitblaster<T>::initAtomBBStrategies() {
- for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
- d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
- }
- /// setting default bb strategies for atoms
- d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_ULE ] = DefaultUleBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_UGT ] = DefaultUgtBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_UGE ] = DefaultUgeBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_SLT ] = DefaultSltBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB<T>;
- d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB<T>;
-}
-
-template <class T> void TBitblaster<T>::initTermBBStrategies() {
- for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
- d_termBBStrategies[i] = DefaultVarBB<T>;
- }
- /// setting default bb strategies for terms:
- d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_AND ] = DefaultAndBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_OR ] = DefaultOrBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_XOR ] = DefaultXorBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_XNOR ] = DefaultXnorBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_NAND ] = DefaultNandBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_NOR ] = DefaultNorBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_COMP ] = DefaultCompBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_MULT ] = DefaultMultBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_ULTBV ] = DefaultUltbvBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_SLTBV ] = DefaultSltbvBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_ITE ] = DefaultIteBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ] = DefaultSignExtendBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB<T>;
- d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB<T>;
-}
-
-template <class T>
-TBitblaster<T>::TBitblaster()
- : d_termCache()
- , d_modelCache()
- , d_bvp( NULL )
-{
- initAtomBBStrategies();
- initTermBBStrategies();
-}
-
-template <class T>
-bool TBitblaster<T>::hasBBTerm(TNode node) const {
- return d_termCache.find(node) != d_termCache.end();
-}
-template <class T>
-void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const {
- Assert (hasBBTerm(node));
- bits = d_termCache.find(node)->second;
-}
-
-template <class T>
-void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits) {
- d_termCache.insert(std::make_pair(node, bits));
-}
-
-template <class T>
-void TBitblaster<T>::invalidateModelCache() {
- d_modelCache.clear();
-}
-
-template <class T>
-Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
- if (d_modelCache.find(node) != d_modelCache.end())
- return d_modelCache[node];
-
- if (node.isConst())
- return node;
-
- Node value = getModelFromSatSolver(node, false);
- if (!value.isNull()) {
- Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from SatSolver" << node <<" => " << value <<"\n";
- d_modelCache[node] = value;
- Assert (value.isConst());
- return value;
- }
-
- if (Theory::isLeafOf(node, theory::THEORY_BV)) {
- // if it is a leaf may ask for fullModel
- value = getModelFromSatSolver(node, true);
- Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
- Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel);
- if (!value.isNull()) {
- d_modelCache[node] = value;
- }
- return value;
- }
- Assert (node.getType().isBitVector());
-
- NodeBuilder<> nb(node.getKind());
- if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- nb << node.getOperator();
- }
-
- for (unsigned i = 0; i < node.getNumChildren(); ++i) {
- nb << getTermModel(node[i], fullModel);
- }
- value = nb;
- value = Rewriter::rewrite(value);
- Assert (value.isConst());
- d_modelCache[node] = value;
- Debug("bv-term-model")<< "TLazyBitblaster::getTermModel Building Value" << node <<" => " << value <<"\n";
- return value;
-}
-
-
-} /* bv namespace */
-
-} /* theory namespace */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4__BITBLASTER_H */
**/
#include "theory/bv/bv_eager_solver.h"
+
#include "options/bv_options.h"
#include "proof/bitvector_proof.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/aig_bitblaster.h"
+#include "theory/bv/bitblast/eager_bitblaster.h"
using namespace std;
#include "theory/bv/bv_quick_check.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/lazy_bitblaster.h"
#include "theory/bv/theory_bv_utils.h"
using namespace CVC4::prop;
** Algebraic solver.
**/
+#include "theory/bv/bv_subtheory_bitblast.h"
#include "decision/decision_attributes.h"
-#include "options/decision_options.h"
#include "options/bv_options.h"
+#include "options/decision_options.h"
+#include "proof/bitvector_proof.h"
+#include "proof/proof_manager.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/lazy_bitblaster.h"
#include "theory/bv/bv_quick_check.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
-#include "proof/proof_manager.h"
-#include "proof/bitvector_proof.h"
using namespace std;
using namespace CVC4::context;
#include <unordered_map>
-#include "theory/bv/bitblaster_template.h"
#include "theory/bv/bv_subtheory.h"
namespace CVC4 {
namespace theory {
namespace bv {
-class LazyBitblaster;
+class TLazyBitblaster;
class AbstractionModule;
class BVQuickCheck;
class QuickXPlain;
+++ /dev/null
-/********************* */
-/*! \file eager_bitblaster.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief
- **
- ** Bitblaster for the eager bv solver.
- **/
-
-#include "cvc4_private.h"
-
-#include "options/bv_options.h"
-#include "proof/bitvector_proof.h"
-#include "prop/cnf_stream.h"
-#include "prop/sat_solver_factory.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/bv/bitblaster_template.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/theory_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-void BitblastingRegistrar::preRegister(Node n) { d_bitblaster->bbAtom(n); }
-
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
- : TBitblaster<Node>(),
- d_satSolver(NULL),
- d_bitblastingRegistrar(NULL),
- d_nullContext(NULL),
- d_cnfStream(NULL),
- d_bv(theory_bv),
- d_bbAtoms(),
- d_variables(),
- d_notify(NULL) {
- d_bitblastingRegistrar = new BitblastingRegistrar(this);
- d_nullContext = new context::Context();
-
- switch (options::bvSatSolver())
- {
- case SAT_SOLVER_MINISAT:
- {
- prop::BVSatSolverInterface* minisat =
- prop::SatSolverFactory::createMinisat(
- d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
- d_notify = new MinisatEmptyNotify();
- minisat->setNotify(d_notify);
- d_satSolver = minisat;
- break;
- }
- case SAT_SOLVER_CADICAL:
- d_satSolver = prop::SatSolverFactory::createCadical(
- smtStatisticsRegistry(), "EagerBitblaster");
- break;
- case SAT_SOLVER_CRYPTOMINISAT:
- d_satSolver = prop::SatSolverFactory::createCryptoMinisat(
- smtStatisticsRegistry(), "EagerBitblaster");
- break;
- default: Unreachable("Unknown SAT solver type");
- }
-
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
- d_nullContext, options::proof(),
- "EagerBitblaster");
-
- d_bvp = NULL;
-}
-
-EagerBitblaster::~EagerBitblaster() {
- delete d_cnfStream;
- delete d_satSolver;
- delete d_notify;
- delete d_nullContext;
- delete d_bitblastingRegistrar;
-}
-
-void EagerBitblaster::bbFormula(TNode node) {
- d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID,
- TNode::null());
-}
-
-/**
- * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
- * NOTE: duplicate clauses are not detected because of marker literal
- * @param node the atom to be bitblasted
- *
- */
-void EagerBitblaster::bbAtom(TNode node)
-{
- node = node.getKind() == kind::NOT ? node[0] : node;
- if (node.getKind() == kind::BITVECTOR_BITOF) return;
- if (hasBBAtom(node))
- {
- return;
- }
-
- Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
-
- // the bitblasted definition of the atom
- Node normalized = Rewriter::rewrite(node);
- Node atom_bb =
- normalized.getKind() != kind::CONST_BOOLEAN
- ? d_atomBBStrategies[normalized.getKind()](normalized, this)
- : normalized;
-
- if (!options::proof())
- {
- atom_bb = Rewriter::rewrite(atom_bb);
- }
-
- // asserting that the atom is true iff the definition holds
- Node atom_definition =
- NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb);
-
- AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
- storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(
- atom_definition, false, false, RULE_INVALID, TNode::null());
-}
-
-void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
- if (d_bvp) {
- d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
- }
- d_bbAtoms.insert(atom);
-}
-
-void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
- if (d_bvp) {
- d_bvp->registerTermBB(node.toExpr());
- }
- d_termCache.insert(std::make_pair(node, bits));
-}
-
-bool EagerBitblaster::hasBBAtom(TNode atom) const {
- return d_bbAtoms.find(atom) != d_bbAtoms.end();
-}
-
-void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
- Assert(node.getType().isBitVector());
-
- if (hasBBTerm(node)) {
- getBBTerm(node, bits);
- return;
- }
-
- d_bv->spendResource(options::bitblastStep());
- Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
-
- d_termBBStrategies[node.getKind()](node, bits, this);
-
- Assert(bits.size() == utils::getSize(node));
-
- storeBBTerm(node, bits);
-}
-
-void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
- Assert(bits.size() == 0);
- for (unsigned i = 0; i < utils::getSize(var); ++i) {
- bits.push_back(utils::mkBitOf(var, i));
- }
- d_variables.insert(var);
-}
-
-Node EagerBitblaster::getBBAtom(TNode node) const { return node; }
-
-/**
- * Calls the solve method for the Sat Solver.
- *
- * @return true for sat, and false for unsat
- */
-
-bool EagerBitblaster::solve() {
- if (Trace.isOn("bitvector")) {
- Trace("bitvector") << "EagerBitblaster::solve(). \n";
- }
- Debug("bitvector") << "EagerBitblaster::solve(). \n";
- // TODO: clear some memory
- // if (something) {
- // NodeManager* nm= NodeManager::currentNM();
- // Rewriter::garbageCollect();
- // nm->reclaimZombiesUntil(options::zombieHuntThreshold());
- // }
- return prop::SAT_VALUE_TRUE == d_satSolver->solve();
-}
-
-/**
- * Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned.
- *
- * @param a
- * @param fullModel whether to create a "full model," i.e., add
- * constants to equivalence classes that don't already have them
- *
- * @return
- */
-Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
- if (!hasBBTerm(a)) {
- return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node();
- }
-
- Bits bits;
- getBBTerm(a, bits);
- Integer value(0);
- for (int i = bits.size() - 1; i >= 0; --i) {
- prop::SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
- prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
- bit_value = d_satSolver->value(bit);
- Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
- } else {
- if (!fullModel) return Node();
- // unconstrained bits default to false
- bit_value = prop::SAT_VALUE_FALSE;
- }
- Integer bit_int =
- bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
- value = value * 2 + bit_int;
- }
- return utils::mkConst(bits.size(), value);
-}
-
-bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
-{
- TNodeSet::iterator it = d_variables.begin();
- for (; it != d_variables.end(); ++it) {
- TNode var = *it;
- if (d_bv->isLeaf(var) || isSharedTerm(var) ||
- (var.isVar() && var.getType().isBoolean())) {
- // only shared terms could not have been bit-blasted
- Assert(hasBBTerm(var) || isSharedTerm(var));
-
- Node const_value = getModelFromSatSolver(var, true);
-
- if (const_value != Node()) {
- Debug("bitvector-model")
- << "EagerBitblaster::collectModelInfo (assert (= " << var << " "
- << const_value << "))\n";
- if (!m->assertEquality(var, const_value, true))
- {
- return false;
- }
- }
- }
- }
- return true;
-}
-
-void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
- d_bvp = bvp;
- d_satSolver->setProofLog(bvp);
- bvp->initCnfProof(d_cnfStream, d_nullContext);
-}
-
-bool EagerBitblaster::isSharedTerm(TNode node) {
- return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
-}
-
-} /* namespace CVC4::theory::bv; */
-} /* namespace CVC4::theory; */
-} /* namespace CVC4; */
+++ /dev/null
-/********************* */
-/*! \file lazy_bitblaster.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Aina Niemetz, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Bitblaster for the lazy bv solver.
- **
- ** Bitblaster for the lazy bv solver.
- **/
-
-#include "bitblaster_template.h"
-#include "cvc4_private.h"
-#include "options/bv_options.h"
-#include "prop/cnf_stream.h"
-#include "prop/sat_solver.h"
-#include "prop/sat_solver_factory.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/bv/abstraction.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
-#include "proof/bitvector_proof.h"
-#include "proof/proof_manager.h"
-#include "theory/bv/theory_bv_utils.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-namespace {
-
-/* Determine the number of uncached nodes that a given node consists of. */
-uint64_t numNodes(TNode node, utils::NodeSet& seen)
-{
- std::vector<TNode> stack;
- uint64_t res = 0;
-
- stack.push_back(node);
- while (!stack.empty())
- {
- Node n = stack.back();
- stack.pop_back();
-
- if (seen.find(n) != seen.end()) continue;
-
- res += 1;
- seen.insert(n);
- stack.insert(stack.end(), n.begin(), n.end());
- }
- return res;
-}
-}
-
-
-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_fullModelAssertionLevel(c, 0)
- , d_name(name)
- , d_statistics(name) {
-
- d_satSolver = prop::SatSolverFactory::createMinisat(
- c, smtStatisticsRegistry(), name);
- d_nullRegistrar = new prop::NullRegistrar();
- d_nullContext = new context::Context();
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
- d_nullRegistrar,
- d_nullContext,
- options::proof(),
- "LazyBitblaster");
-
- d_satSolverNotify = d_emptyNotify ?
- (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
- (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv,
- this);
-
- d_satSolver->setNotify(d_satSolverNotify);
-}
-
-void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
- d_abstraction = abs;
-}
-
-TLazyBitblaster::~TLazyBitblaster()
-{
- delete d_cnfStream;
- delete d_nullRegistrar;
- delete d_nullContext;
- delete d_satSolver;
- delete d_satSolverNotify;
- d_assertedAtoms->deleteSelf();
- d_explanations->deleteSelf();
-}
-
-
-/**
- * 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)
-{
- NodeManager* nm = NodeManager::currentNM();
- 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 = nm->mkNode(kind::EQUAL, node, atom_bb);
- storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(
- atom_definition, false, false, RULE_INVALID, TNode::null());
- return;
- }
-
- // the bitblasted definition of the atom
- Node normalized = Rewriter::rewrite(node);
- Node atom_bb =
- normalized.getKind() != kind::CONST_BOOLEAN
- ? d_atomBBStrategies[normalized.getKind()](normalized, this)
- : normalized;
-
- if (!options::proof())
- {
- atom_bb = Rewriter::rewrite(atom_bb);
- }
-
- // asserting that the atom is true iff the definition holds
- Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb);
- storeBBAtom(node, atom_bb);
- d_cnfStream->convertAndAssert(
- atom_definition, false, false, RULE_INVALID, TNode::null());
-}
-
-void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
- // No need to store the definition for the lazy bit-blaster (unless proofs are enabled).
- if( d_bvp != NULL ){
- d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
- }
- d_bbAtoms.insert(atom);
-}
-
-void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
- if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
- d_termCache.insert(std::make_pair(node, bits));
-}
-
-
-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;
- if (!utils::isBitblastAtom(node)) { return 0; }
- Node atom_bb =
- Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
- uint64_t size = 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;
- }
- Assert( node.getType().isBitVector() );
-
- d_bv->spendResource(options::bitblastStep());
- Debug("bitvector-bitblast") << "Bitblasting term " << 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( utils::isBitblastAtom( atom ) );
-
- 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";
- d_fullModelAssertionLevel.set(d_bv->numAssertions());
- 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)
-{
- NodeManager* nm = NodeManager::currentNM();
- 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 = nm->mkNode(kind::NOT, atom);
- }
- conflict.push_back(not_atom);
- }
-}
-
-TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
- d_numTermClauses(prefix + "::NumTermSatClauses", 0),
- d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
- d_numTerms(prefix + "::NumBitblastedTerms", 0),
- d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
- d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
- d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
- d_bitblastTimer(prefix + "::BitblastTimer")
-{
- smtStatisticsRegistry()->registerStat(&d_numTermClauses);
- smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
- smtStatisticsRegistry()->registerStat(&d_numTerms);
- smtStatisticsRegistry()->registerStat(&d_numAtoms);
- smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
- smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
- smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
-}
-
-
-TLazyBitblaster::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
- smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
- smtStatisticsRegistry()->unregisterStat(&d_numTerms);
- smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
- smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
- smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
- smtStatisticsRegistry()->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::spendResource(unsigned amount)
-{
- d_bv->spendResource(amount);
-}
-
-void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount)
-{
- d_bv->d_out->safePoint(amount);
-}
-
-EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
-{
- int numAssertions = d_bv->numAssertions();
- Debug("bv-equality-status")
- << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n";
- Debug("bv-equality-status")
- << "BVSatSolver has full model? "
- << (d_fullModelAssertionLevel.get() == numAssertions) << "\n";
-
- // First check if it trivially rewrites to false/true
- Node a_eq_b =
- Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b));
-
- if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
- if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
-
- if (d_fullModelAssertionLevel.get() != numAssertions)
- {
- return theory::EQUALITY_UNKNOWN;
- }
-
- // Check if cache is valid (invalidated in check and pops)
- if (d_bv->d_invalidateModelCache.get())
- {
- invalidateModelCache();
- }
- d_bv->d_invalidateModelCache.set(false);
-
- Node a_value = getTermModel(a, true);
- Node b_value = getTermModel(b, true);
-
- Assert(a_value.isConst() && b_value.isConst());
-
- if (a_value == b_value)
- {
- Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n";
- return theory::EQUALITY_TRUE_IN_MODEL;
- }
- Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n";
- return theory::EQUALITY_FALSE_IN_MODEL;
-}
-
-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::getModelFromSatSolver(TNode a, bool fullModel) {
- if (!hasBBTerm(a)) {
- return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
- }
-
- Bits bits;
- getBBTerm(a, bits);
- Integer value(0);
- for (int i = bits.size() -1; i >= 0; --i) {
- prop::SatValue bit_value;
- if (d_cnfStream->hasLiteral(bits[i])) {
- prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
- bit_value = d_satSolver->value(bit);
- Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
- } else {
- if (!fullModel) return Node();
- // unconstrained bits default to false
- bit_value = prop::SAT_VALUE_FALSE;
- }
- Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
- value = value * 2 + bit_int;
- }
- return utils::mkConst(bits.size(), value);
-}
-
-bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
-{
- std::set<Node> termSet;
- d_bv->computeRelevantTerms(termSet);
-
- for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
- TNode var = *it;
- // not actually a leaf of the bit-vector theory
- if (d_variables.find(var) == d_variables.end())
- continue;
-
- Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
- // only shared terms could not have been bit-blasted
- Assert (hasBBTerm(var) || isSharedTerm(var));
-
- Node const_value = getModelFromSatSolver(var, true);
- Assert (const_value.isNull() || const_value.isConst());
- if(const_value != Node()) {
- Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
- << var << " "
- << const_value << "))\n";
- if (!m->assertEquality(var, const_value, true))
- {
- return false;
- }
- }
- }
- return true;
-}
-
-void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
- d_bvp = bvp;
- d_satSolver->setProofLog( bvp );
- bvp->initCnfProof(d_cnfStream, d_nullContext);
-}
-
-void TLazyBitblaster::clearSolver() {
- Assert (d_ctx->getLevel() == 0);
- delete d_satSolver;
- delete d_satSolverNotify;
- 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();
-
- invalidateModelCache();
- // recreate sat solver
- d_satSolver = prop::SatSolverFactory::createMinisat(
- d_ctx, smtStatisticsRegistry());
- d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
- d_nullContext);
-
- d_satSolverNotify = d_emptyNotify ?
- (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
- (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv,
- this);
- d_satSolver->setNotify(d_satSolverNotify);
-}
-
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/bv/theory_bv.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/eager_bitblaster.h"
#include "expr/node.h"
#include "expr/node_manager.h"
#include "context/context.h"
projects / cvc5.git / commitdiff