summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblast')
-rw-r--r--src/theory/bv/bitblast/aig_bitblaster.cpp50
-rw-r--r--src/theory/bv/bitblast/bitblast_strategies_template.h89
-rw-r--r--src/theory/bv/bitblast/bitblast_utils.h16
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.cpp2
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.cpp22
5 files changed, 86 insertions, 93 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 3ed926f84..c2bc9e6e8 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -18,7 +18,7 @@
#include "theory/bv/bitblast/aig_bitblaster.h"
-#include "base/cvc4_check.h"
+#include "base/check.h"
#include "options/bv_options.h"
#include "prop/sat_solver_factory.h"
#include "smt/smt_statistics_registry.h"
@@ -46,7 +46,7 @@ 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");
+ Unreachable() << "Don't know how to print AIG";
}
@@ -72,7 +72,7 @@ Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
template <> inline
Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
- Assert (children.size());
+ Assert(children.size());
if (children.size() == 1)
return children[0];
@@ -91,7 +91,7 @@ Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
template <> inline
Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
- Assert (children.size());
+ Assert(children.size());
if (children.size() == 1)
return children[0];
@@ -172,7 +172,7 @@ AigBitblaster::AigBitblaster()
AigBitblaster::~AigBitblaster() {}
Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
- Assert (node.getType().isBoolean());
+ Assert(node.getType().isBoolean());
Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n";
if (hasAig(node))
@@ -211,7 +211,7 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
}
case kind::IMPLIES:
{
- Assert (node.getNumChildren() == 2);
+ Assert(node.getNumChildren() == 2);
Abc_Obj_t* child1 = bbFormula(node[0]);
Abc_Obj_t* child2 = bbFormula(node[1]);
@@ -220,7 +220,7 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
}
case kind::ITE:
{
- Assert (node.getNumChildren() == 3);
+ 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]);
@@ -241,7 +241,7 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
case kind::EQUAL:
{
if( node[0].getType().isBoolean() ){
- Assert (node.getNumChildren() == 2);
+ Assert(node.getNumChildren() == 2);
Abc_Obj_t* child1 = bbFormula(node[0]);
Abc_Obj_t* child2 = bbFormula(node[1]);
@@ -283,18 +283,18 @@ void AigBitblaster::bbTerm(TNode node, Bits& bits) {
getBBTerm(node, bits);
return;
}
- Assert( node.getType().isBitVector() );
+ Assert(node.getType().isBitVector());
Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
d_termBBStrategies[node.getKind()] (node, bits, this);
- Assert (bits.size() == utils::getSize(node));
+ Assert(bits.size() == utils::getSize(node));
storeBBTerm(node, bits);
}
void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
- Assert (!hasAig(node));
+ Assert(!hasAig(node));
d_aigCache.insert(std::make_pair(node, aig));
}
bool AigBitblaster::hasAig(TNode node) {
@@ -317,9 +317,9 @@ void AigBitblaster::makeVariable(TNode node, Bits& bits) {
}
Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
- Assert (!hasInput(input));
- Assert(input.getKind() == kind::BITVECTOR_BITOF ||
- (input.getType().isBoolean() && input.isVar()));
+ 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));
@@ -333,7 +333,7 @@ bool AigBitblaster::hasInput(TNode input) {
bool AigBitblaster::solve(TNode node) {
// setting output of network to be the query
- Assert (d_aigOutputNode == NULL);
+ Assert(d_aigOutputNode == NULL);
Abc_Obj_t* query = bbFormula(node);
d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk());
Abc_ObjAddFanin(d_aigOutputNode, query);
@@ -345,7 +345,7 @@ bool AigBitblaster::solve(TNode node) {
TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime);
prop::SatValue result = d_satSolver->solve();
- Assert (result != prop::SAT_VALUE_UNKNOWN);
+ Assert(result != prop::SAT_VALUE_UNKNOWN);
return result == prop::SAT_VALUE_TRUE;
}
@@ -356,7 +356,7 @@ void AigBitblaster::simplifyAig() {
TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime);
Abc_AigCleanup(currentAigM());
- Assert (Abc_NtkCheck(currentAigNtk()));
+ Assert(Abc_NtkCheck(currentAigNtk()));
const char* command = options::bitvectorAigSimplifications().c_str();
Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
@@ -376,8 +376,8 @@ void AigBitblaster::convertToCnfAndAssert() {
Aig_Man_t * pMan = NULL;
Cnf_Dat_t * pCnf = NULL;
- Assert( Abc_NtkIsStrash(currentAigNtk()) );
-
+ Assert(Abc_NtkIsStrash(currentAigNtk()));
+
// convert to the AIG manager
pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );
Abc_Stop();
@@ -385,9 +385,9 @@ void AigBitblaster::convertToCnfAndAssert() {
// // free old network
// Abc_NtkDelete(currentAigNtk());
// s_abcAigNetwork = NULL;
-
- Assert (pMan != NULL);
- Assert (Aig_ManCheck(pMan));
+
+ Assert(pMan != NULL);
+ Assert(Aig_ManCheck(pMan));
pCnf = Cnf_DeriveFast( pMan, 0 );
assertToSatSolver(pCnf);
@@ -416,9 +416,9 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
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);
+ Assert(int_lit != 0);
unsigned index = int_lit < 0? -int_lit : int_lit;
- Assert (index - 1 < sat_variables.size());
+ Assert(index - 1 < sat_variables.size());
prop::SatLiteral lit(sat_variables[index-1], int_lit < 0);
clause.push_back(lit);
}
@@ -464,7 +464,7 @@ void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
}
Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
- Assert (hasBBAtom(atom));
+ Assert(hasBBAtom(atom));
return d_bbAtoms.find(atom)->second;
}
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 9e668e258..047396506 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -50,7 +50,7 @@ T UndefinedAtomBBStrategy(TNode node, TBitblaster<T>* bb) {
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);
@@ -75,7 +75,7 @@ T AdderUltBB(TNode node, TBitblaster<T>* bb) {
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);
@@ -98,7 +98,7 @@ T DefaultUltBB(TNode node, TBitblaster<T>* bb) {
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;
@@ -139,7 +139,7 @@ T DefaultSltBB(TNode node, TBitblaster<T>* bb){
bb->bbTerm(node[0], a);
bb->bbTerm(node[1], b);
Assert(a.size() == b.size());
-
+
T res = sLessThanBB(a, b, false);
return res;
}
@@ -152,7 +152,7 @@ T DefaultSleBB(TNode node, TBitblaster<T>* bb){
bb->bbTerm(node[0], a);
bb->bbTerm(node[1], b);
Assert(a.size() == b.size());
-
+
T res = sLessThanBB(a, b, true);
return res;
}
@@ -204,13 +204,13 @@ 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));
+ Assert(bit == Integer(1));
bits.push_back(mkTrue<T>());
}
}
@@ -234,8 +234,8 @@ 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);
+
+ Assert(node.getKind() == kind::BITVECTOR_CONCAT);
for (int i = node.getNumChildren() -1 ; i >= 0; --i ) {
TNode current = node[i];
std::vector<T> current_bits;
@@ -245,7 +245,7 @@ void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
bits.push_back(current_bits[j]);
}
}
- Assert (bits.size() == utils::getSize(node));
+ Assert(bits.size() == utils::getSize(node));
if(Debug.isOn("bitvector-bb")) {
Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n";
}
@@ -254,9 +254,8 @@ void DefaultConcatBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
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);
+
+ Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0);
bb->bbTerm(node[0], bits);
std::vector<T> current;
@@ -267,15 +266,14 @@ void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
}
current.clear();
}
- Assert (bits.size() == utils::getSize(node));
+ 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);
+ Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0);
bb->bbTerm(node[0], bits);
std::vector<T> current;
@@ -286,15 +284,14 @@ void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
}
current.clear();
}
- Assert (bits.size() == utils::getSize(node));
+ 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);
+ Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0);
bb->bbTerm(node[0], bits);
std::vector<T> current;
@@ -305,21 +302,20 @@ void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
}
current.clear();
}
- Assert (bits.size() == utils::getSize(node));
+ 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);
+ 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());
-
+ Assert(lhs.size() == rhs.size());
+
for (unsigned i = 0; i < lhs.size(); ++i) {
bits.push_back(mkIff(lhs[i], rhs[i]));
}
@@ -342,7 +338,8 @@ 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);
+ 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);
@@ -359,8 +356,7 @@ void DefaultCompBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
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);
+ Assert(res.size() == 0 && node.getKind() == kind::BITVECTOR_MULT);
// if (node.getNumChildren() == 2) {
// std::vector<T> a;
@@ -401,8 +397,7 @@ void DefaultMultBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
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);
+ Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0);
bb->bbTerm(node[0], res);
@@ -415,7 +410,7 @@ void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
rippleCarryAdder(res, current, newres, mkFalse<T>());
res = newres;
}
-
+
Assert(res.size() == utils::getSize(node));
}
@@ -423,13 +418,12 @@ void DefaultPlusBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
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);
-
+ 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);
+ bb->bbTerm(node[1], b);
Assert(a.size() == b.size() && utils::getSize(node) == a.size());
// bvsub a b = adder(a, ~b, 1)
@@ -442,7 +436,7 @@ 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());
@@ -458,7 +452,7 @@ void DefaultNegBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
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);
+ Assert(q.size() == 0 && r.size() == 0);
if(rec_width == 0 || isZero(a)) {
makeZero(q, a.size());
@@ -788,7 +782,7 @@ void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
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));
}
@@ -801,7 +795,7 @@ void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
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));
}
@@ -814,7 +808,7 @@ void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
bb->bbTerm(node[0], cond);
bb->bbTerm(node[1], thenpart);
bb->bbTerm(node[2], elsepart);
-
+
Assert(cond.size() == 1);
Assert(thenpart.size() == elsepart.size());
@@ -826,9 +820,9 @@ void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
template <class T>
void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
- Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
+ 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);
@@ -837,7 +831,7 @@ void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
for (unsigned i = low; i <= high; ++i) {
bits.push_back(base_bits[i]);
}
- Assert (bits.size() == high - low + 1);
+ Assert(bits.size() == high - low + 1);
if(Debug.isOn("bitvector-bb")) {
Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
@@ -868,8 +862,7 @@ 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);
+ Assert(node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0);
std::vector<T> bits;
bb->bbTerm(node[0], bits);
@@ -884,8 +877,8 @@ void DefaultSignExtendBB (TNode node, std::vector<T>& res_bits, TBitblaster<T>*
for (unsigned i = 0 ; i < amount ; ++i ) {
res_bits.push_back(sign_bit);
}
-
- Assert (res_bits.size() == amount + bits.size());
+
+ Assert(res_bits.size() == amount + bits.size());
}
template <class T>
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index f2bee22e5..03e0aa349 100644
--- a/src/theory/bv/bitblast/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -81,7 +81,7 @@ Node mkOr<Node>(Node a, Node b) {
template <> inline
Node mkOr<Node>(const std::vector<Node>& children) {
- Assert (children.size());
+ Assert(children.size());
if (children.size() == 1)
return children[0];
return NodeManager::currentNM()->mkNode(kind::OR, children);
@@ -95,7 +95,7 @@ Node mkAnd<Node>(Node a, Node b) {
template <> inline
Node mkAnd<Node>(const std::vector<Node>& children) {
- Assert (children.size());
+ Assert(children.size());
if (children.size() == 1)
return children[0];
return NodeManager::currentNM()->mkNode(kind::AND, children);
@@ -123,7 +123,7 @@ Node mkIte<Node>(Node cond, Node a, Node b) {
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);
+ Assert(lo < b.size() && hi < b.size() && lo <= hi);
for (unsigned i = lo; i <= hi; ++i) {
dest.push_back(b[i]);
}
@@ -168,7 +168,7 @@ void inline lshift(std::vector<T>& bits, unsigned amount) {
template <class T>
void inline makeZero(std::vector<T>& bits, unsigned width) {
- Assert(bits.size() == 0);
+ Assert(bits.size() == 0);
for(unsigned i = 0; i < width; ++i) {
bits.push_back(mkFalse<T>());
}
@@ -188,7 +188,7 @@ void inline makeZero(std::vector<T>& bits, unsigned width) {
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]),
@@ -222,8 +222,8 @@ inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, s
template <class T>
T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
- Assert (a.size() && b.size());
-
+ Assert(a.size() && b.size());
+
T res = mkAnd(mkNot(a[0]), b[0]);
if(orEqual) {
@@ -240,7 +240,7 @@ T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
template <class T>
T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
- Assert (a.size() && b.size());
+ Assert(a.size() && b.size());
if (a.size() == 1) {
if(orEqual) {
return mkOr(mkIff(a[0], b[0]),
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 0d3d3b483..9d43355cc 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -60,7 +60,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
solver = prop::SatSolverFactory::createCryptoMinisat(
smtStatisticsRegistry(), "EagerBitblaster");
break;
- default: Unreachable("Unknown SAT solver type");
+ default: Unreachable() << "Unknown SAT solver type";
}
d_satSolver.reset(solver);
d_cnfStream.reset(
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 845fd399e..2018590f7 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -232,7 +232,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
getBBTerm(node, bits);
return;
}
- Assert( node.getType().isBitVector() );
+ Assert(node.getType().isBitVector());
d_bv->spendResource(options::bitblastStep());
Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
@@ -240,7 +240,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
d_termBBStrategies[node.getKind()] (node, bits,this);
- Assert (bits.size() == utils::getSize(node));
+ Assert(bits.size() == utils::getSize(node));
storeBBTerm(node, bits);
}
@@ -257,7 +257,7 @@ void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
++(d_statistics.d_numExplainedPropagations);
if (options::bvEagerExplanations()) {
- Assert (d_explanations->find(lit) != d_explanations->end());
+ 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]));
@@ -292,9 +292,9 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
} else {
atom = lit;
}
- Assert( utils::isBitblastAtom( atom ) );
+ Assert(utils::isBitblastAtom(atom));
- Assert (hasBBAtom(atom));
+ Assert(hasBBAtom(atom));
prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
@@ -483,7 +483,7 @@ bool TLazyBitblaster::isSharedTerm(TNode node) {
}
bool TLazyBitblaster::hasValue(TNode a) {
- Assert (hasBBTerm(a));
+ Assert(hasBBTerm(a));
Bits bits;
getBBTerm(a, bits);
for (int i = bits.size() -1; i >= 0; --i) {
@@ -522,7 +522,7 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
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);
+ Assert(bit_value != prop::SAT_VALUE_UNKNOWN);
} else {
if (!fullModel) return Node();
// unconstrained bits default to false
@@ -545,12 +545,12 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
if (d_variables.find(var) == d_variables.end())
continue;
- Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
+ Assert(Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
// only shared terms could not have been bit-blasted
- Assert (hasBBTerm(var) || isSharedTerm(var));
+ Assert(hasBBTerm(var) || isSharedTerm(var));
Node const_value = getModelFromSatSolver(var, true);
- Assert (const_value.isNull() || const_value.isConst());
+ Assert(const_value.isNull() || const_value.isConst());
if(const_value != Node()) {
Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
<< var << " "
@@ -565,7 +565,7 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
}
void TLazyBitblaster::clearSolver() {
- Assert (d_ctx->getLevel() == 0);
+ Assert(d_ctx->getLevel() == 0);
d_assertedAtoms->deleteSelf();
d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
d_explanations->deleteSelf();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback