mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix sign of constant in pb constraint

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-24 20:28:56 -07:00
parent b82b53dc34
commit fefd00aa49
1 changed files with 2 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -29,39 +29,6 @@ Notes:
struct pb2bv_rewriter::imp { struct pb2bv_rewriter::imp {
struct argc_t {
expr* m_arg;
rational m_coeff;
argc_t():m_arg(0), m_coeff(0) {}
argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
};
struct argc_gt {
bool operator()(argc_t const& a, argc_t const& b) const {
return a.m_coeff > b.m_coeff;
}
};
struct argc_entry {
unsigned m_index;
rational m_k;
expr* m_value;
argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
argc_entry():m_index(0), m_k(0), m_value(0) {}
struct eq {
bool operator()(argc_entry const& a, argc_entry const& b) const {
return a.m_index == b.m_index && a.m_k == b.m_k;
}
};
struct hash {
unsigned operator()(argc_entry const& a) const {
return a.m_index ^ a.m_k.hash();
}
};
};
typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
ast_manager& m; ast_manager& m;
params_ref m_params; params_ref m_params;
expr_ref_vector m_lemmas; expr_ref_vector m_lemmas;
@ -121,6 +88,7 @@ struct pb2bv_rewriter::imp {
TRACE("pb", TRACE("pb",
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " "; tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
} }
switch (is_le) { switch (is_le) {
case l_true: tout << "<= "; break; case l_true: tout << "<= "; break;
@ -338,7 +306,7 @@ struct pb2bv_rewriter::imp {
return is_pb(a->get_arg(0), -mul); return is_pb(a->get_arg(0), -mul);
case OP_NUM: case OP_NUM:
VERIFY(au.is_numeral(a, r)); VERIFY(au.is_numeral(a, r));
m_k += mul * r; m_k -= mul * r;
return true; return true;
case OP_MUL: case OP_MUL:
if (sz != 2) { if (sz != 2) {