}
SatValue BVMinisatSatSolver::solve(){
+ ++d_statistics.d_statCallsToSolve;
return toSatLiteralValue(d_minisat->solve());
}
return result;
}
-// SatValue BVMinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions, bool only_bcp){
-// ++d_solveCount;
-// ++d_statistics.d_statCallsToSolve;
-
-// Debug("sat::minisat") << "Solve with assumptions ";
-// context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
-// BVMinisat::vec<BVMinisat::Lit> assump;
-// for(; it!= assumptions.end(); ++it) {
-// SatLiteral lit = *it;
-// Debug("sat::minisat") << lit <<" ";
-// assump.push(toMinisatLit(lit));
-// }
-// Debug("sat::minisat") <<"\n";
-
-// clock_t begin, end;
-// begin = clock();
-// d_minisat->setOnlyBCP(only_bcp);
-// SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
-// end = clock();
-// d_statistics.d_statSolveTime = d_statistics.d_statSolveTime.getData() + (end - begin)/(double)CLOCKS_PER_SEC;
-// return result;
-// }
-
-
void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
// TODO add assertion to check the call was after an unsat call
for (int i = 0; i < d_minisat->conflict.size(); ++i) {
TNode urem = fact[0];
TNode result = fact[1];
TNode divisor = urem[1];
- Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor);
- Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div);
+ Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
+ Node divisor_eq_0 = mkNode(kind::EQUAL,
+ divisor,
+ mkConst(BitVector(getSize(divisor), 0u)));
+ Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
lemma(split);
}
if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
TNode urem = fact[1];
TNode result = fact[0];
TNode divisor = urem[1];
- Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor);
- Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div);
+ Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
+ Node divisor_eq_0 = mkNode(kind::EQUAL,
+ divisor,
+ mkConst(BitVector(getSize(divisor), 0u)));
+ Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
lemma(split);
}
}
SubEliminate,
SltEliminate,
SleEliminate,
+ UleEliminate,
CompEliminate,
RepeatEliminate,
RotateLeftEliminate,
ExtractNot,
ExtractArith,
ExtractArith2,
+ ExtractSignExtend,
DoubleNeg,
NegMult,
NegSub,
AndSimplify,
OrSimplify,
XorSimplify,
- UleEliminate,
+ BitwiseSlicing,
// rules to simplify bitblasting
BBPlusNeg
};
case UltOne : out << "UltOne"; return out;
case SltZero : out << "SltZero"; return out;
case ZeroUlt : out << "ZeroUlt"; return out;
- case UleEliminate : out << "UleEliminate"; return out;
+ case UleEliminate : out << "UleEliminate"; return out;
+ case BitwiseSlicing : out << "BitwiseSlicing"; return out;
+ case ExtractSignExtend : out << "ExtractSignExtend"; return out;
default:
Unreachable();
}
return utils::mkNode(kind::BITVECTOR_NOT, a);
}
+/**
+ * ExtractSignExtend
+ *
+ * (sign_extend k x) [i:j] => pushes extract in
+ *
+ * @return
+ */
+
+template<> inline
+bool RewriteRule<ExtractSignExtend>::applies(TNode node) {
+ if (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
+ return true;
+ }
+ return false;
+}
+
+template<> inline
+Node RewriteRule<ExtractSignExtend>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << node << ")" << std::endl;
+ TNode extendee = node[0][0];
+ unsigned extendee_size = utils::getSize(extendee);
+
+ unsigned high = utils::getExtractHigh(node);
+ unsigned low = utils::getExtractLow(node);
+
+ Node resultNode;
+ // extract falls on extendee
+ if (high < extendee_size) {
+ resultNode = utils::mkExtract(extendee, high, low);
+ } else if (low < extendee_size && high >= extendee_size) {
+ // if extract overlaps sign extend and extendee
+ Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low);
+ unsigned new_ammount = high - extendee_size + 1;
+ resultNode = utils::mkSignExtend(low_extract, new_ammount);
+ } else {
+ // extract only over sign extend
+ Assert (low >= extendee_size);
+ unsigned top = utils::getSize(extendee) - 1;
+ Node most_significant_bit = utils::mkExtract(extendee, top, top);
+ std::vector<Node> bits;
+ for (unsigned i = 0; i < high - low + 1; ++i) {
+ bits.push_back(most_significant_bit);
+ }
+ resultNode = utils::mkNode(kind::BITVECTOR_CONCAT, bits);
+ }
+ Debug("bv-rewrite") << " =>" << resultNode << std::endl;
+ return resultNode;
+}
+
+
+
/**
* ExtractArith
*
}
+/**
+ * BitwiseSlicing
+ *
+ * (a bvand c) ==> (concat (bvand a[i0:j0] c0) ... (bvand a[in:jn] cn))
+ * where c0,..., cn are maximally continuous substrings of 0 or 1 in the constant c
+ *
+ * Note: this rule assumes AndSimplify has already been called on the node
+ */
+template<> inline
+bool RewriteRule<BitwiseSlicing>::applies(TNode node) {
+ if ((node.getKind() != kind::BITVECTOR_AND &&
+ node.getKind() != kind::BITVECTOR_OR &&
+ node.getKind() != kind::BITVECTOR_XOR) ||
+ utils::getSize(node) == 1)
+ return false;
+
+ for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+ if (node[i].getKind() == kind::CONST_BITVECTOR) {
+ BitVector constant = node[i].getConst<BitVector>();
+ // we do not apply the rule if the constant is all 0s or all 1s
+ if (constant == BitVector(utils::getSize(node), 0u))
+ return false;
+
+ for (unsigned i = 0; i < constant.getSize(); ++i) {
+ if (!constant.isBitSet(i))
+ return true;
+ }
+ }
+ }
+ return false;
+}
+template<> inline
+Node RewriteRule<BitwiseSlicing>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl;
+ // get the constant
+ bool found_constant = false;
+ TNode constant;
+ std::vector<Node> other_children;
+ for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+ if (node[i].getKind() == kind::CONST_BITVECTOR) {
+ constant = node[i];
+ Assert (!found_constant);
+ found_constant = true;
+ } else {
+ other_children.push_back(node[i]);
+ }
+ }
+ Assert (found_constant && other_children.size() == node.getNumChildren() - 1);
-// template<> inline
-// bool RewriteRule<AndSimplify>::applies(TNode node) {
-// return (node.getKind() == kind::BITVECTOR_AND);
-// }
-
-// template<> inline
-// Node RewriteRule<AndSimplify>::apply(TNode node) {
-// Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
-// return resultNode;
-// }
+ Node other = utils::mkNode(node.getKind(), other_children);
+
+ BitVector bv_constant = constant.getConst<BitVector>();
+ std::vector<Node> concat_children;
+ int start = bv_constant.getSize() - 1;
+ int end = start;
+ for (int i = end - 1; i >= 0; --i) {
+ if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i)) {
+ Node other_extract = utils::mkExtract(other, end, start);
+ Node const_extract = utils::mkExtract(constant, end, start);
+ Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract);
+ concat_children.push_back(bitwise_op);
+ start = end = i;
+ } else {
+ start--;
+ }
+ if (i == 0) {
+ Node other_extract = utils::mkExtract(other, end, 0);
+ Node const_extract = utils::mkExtract(constant, end, 0);
+ Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract);
+ concat_children.push_back(bitwise_op);
+ }
+ }
+ Node result = utils::mkNode(kind::BITVECTOR_CONCAT, concat_children);
+ Debug("bv-rewrite") << " =>" << result << std::endl;
+ return result;
+}
// template<> inline
// bool RewriteRule<>::applies(TNode node) {
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
+ // if (RewriteRule<ExtractSignExtend>::applies(node)) {
+ // resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
+ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ // }
+
if (RewriteRule<ExtractBitwise>::applies(node)) {
resultNode = RewriteRule<ExtractBitwise>::run<false>(node);
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>,
- RewriteRule<AndSimplify>
- // RewriteRule<EvalAnd>,
- // RewriteRule<BitwiseIdemp>,
- // //RewriteRule<BitwiseSlice>, -> might need rw again
- // RewriteRule<AndZero>,
- // RewriteRule<AndOne>
+ RewriteRule<AndSimplify>//,
+ // RewriteRule<BitwiseSlicing>
>::apply(node);
+ if (resultNode.getKind() != node.getKind()) {
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
return RewriteResponse(REWRITE_DONE, resultNode);
}
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>,
- RewriteRule<OrSimplify>
+ RewriteRule<OrSimplify>//,
+ // RewriteRule<BitwiseSlicing>
>::apply(node);
+
+ if (resultNode.getKind() != node.getKind()) {
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
return RewriteResponse(REWRITE_DONE, resultNode);
}
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>, // flatten the expression
RewriteRule<XorSimplify>, // simplify duplicates and constants
- RewriteRule<XorZero> // checks if the constant part is zero and eliminates it
+ RewriteRule<XorZero>//, // checks if the constant part is zero and eliminates it
+ // RewriteRule<BitwiseSlicing>
>::apply(node);
// this simplification introduces new terms and might require further
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
+ if (resultNode.getKind() != node.getKind()) {
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
return RewriteResponse(REWRITE_DONE, resultNode);
}
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>, // flattens and sorts
- RewriteRule<MultSimplify> // multiplies constant part and checks for 0
+ RewriteRule<MultSimplify>, // multiplies constant part and checks for 0
+ RewriteRule<MultPow2> // replaces multiplication by a power of 2 by a shift
>::apply(node);
// only apply if every subterm was already rewritten
if(resultNode == node) {
return RewriteResponse(REWRITE_DONE, resultNode);
}
- return RewriteResponse(REWRITE_DONE, resultNode);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) {
inline Node mkNode(Kind kind, std::vector<Node>& children) {
+ Assert (children.size() > 0);
if (children.size() == 1) {
return children[0];
}
}
+inline Node mkSignExtend(TNode node, unsigned ammount) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node signExtendOp = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount));
+ return nm->mkNode(signExtendOp, node);
+}
+
inline Node mkExtract(TNode node, unsigned high, unsigned low) {
Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
std::vector<Node> children;
projects / cvc5.git / commitdiff