diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/theory/bv/bitblast | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/bv/bitblast')
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.cpp | 50 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblast_strategies_template.h | 89 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblast_utils.h | 16 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 22 |
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(); |