mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

indentation

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-03 22:52:23 -07:00
parent b9ddb11701
commit b49ffb8a87
2 changed files with 97 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

132
src/sat/smt/arith_proof_checker.h
View file

@ -41,16 +41,19 @@ namespace arith {
m_coeff = 0; m_coeff = 0;
} }
}; };
ast_manager& m; ast_manager& m;
arith_util a; arith_util a;
vector<std::pair<rational, expr*>> m_todo; vector<std::pair<rational, expr*>> m_todo;
bool m_strict = false; bool m_strict = false;
row m_ineq; row m_ineq;
row m_conseq; row m_conseq;
vector<row> m_eqs; vector<row> m_eqs;
vector<row> m_ineqs; vector<row> m_ineqs;
vector<row> m_diseqs; vector<row> m_diseqs;
symbol m_farkas;
symbol m_implied_eq;
symbol m_bound;
void add(row& r, expr* v, rational const& coeff) { void add(row& r, expr* v, rational const& coeff) {
rational coeff1; rational coeff1;
@ -147,6 +150,8 @@ namespace arith {
m_todo.push_back({coeff*coeff1, e2}); m_todo.push_back({coeff*coeff1, e2});
else if (a.is_mul(e, e1, e2) && a.is_uminus(e1, e3) && a.is_numeral(e3, coeff1)) else if (a.is_mul(e, e1, e2) && a.is_uminus(e1, e3) && a.is_numeral(e3, coeff1))
m_todo.push_back({-coeff*coeff1, e2}); m_todo.push_back({-coeff*coeff1, e2});
else if (a.is_mul(e, e1, e2) && a.is_uminus(e2, e3) && a.is_numeral(e3, coeff1))
m_todo.push_back({ -coeff * coeff1, e1 });
else if (a.is_mul(e, e1, e2) && a.is_numeral(e2, coeff1)) else if (a.is_mul(e, e1, e2) && a.is_numeral(e2, coeff1))
m_todo.push_back({coeff*coeff1, e1}); m_todo.push_back({coeff*coeff1, e1});
else if (a.is_add(e)) else if (a.is_add(e))
@ -309,10 +314,14 @@ namespace arith {
rows.push_back(row()); rows.push_back(row());
return rows.back(); return rows.back();
} }
public: public:
proof_checker(ast_manager& m): m(m), a(m) {} proof_checker(ast_manager& m):
m(m),
a(m),
m_farkas("farkas"),
m_implied_eq("implied-eq"),
m_bound("bound") {}
~proof_checker() override {} ~proof_checker() override {}
@ -328,7 +337,8 @@ namespace arith {
bool add_ineq(rational const& coeff, expr* e, bool sign) { bool add_ineq(rational const& coeff, expr* e, bool sign) {
if (!m_diseqs.empty()) if (!m_diseqs.empty())
return add_literal(fresh(m_ineqs), abs(coeff), e, sign); return add_literal(fresh(m_ineqs), abs(coeff), e, sign);
return add_literal(m_ineq, abs(coeff), e, sign); else
return add_literal(m_ineq, abs(coeff), e, sign);
} }
bool add_conseq(rational const& coeff, expr* e, bool sign) { bool add_conseq(rational const& coeff, expr* e, bool sign) {
@ -374,60 +384,66 @@ namespace arith {
else else
pos.mark(e, true); pos.mark(e, true);
if (jst->get_name() == symbol("farkas")) { if (jst->get_name() != m_farkas &&
bool even = true; jst->get_name() != m_bound &&
rational coeff; jst->get_name() != m_implied_eq) {
expr* x, *y; IF_VERBOSE(0, verbose_stream() << "unhandled inference " << mk_pp(jst, m) << "\n");
for (expr* arg : *jst) {
if (even) {
if (!a.is_numeral(arg, coeff)) {
IF_VERBOSE(0, verbose_stream() << "not numeral " << mk_pp(jst, m) << "\n");
return false;
}
}
else {
bool sign = m.is_not(arg, arg);
if (a.is_le(arg) || a.is_lt(arg) || a.is_ge(arg) || a.is_gt(arg))
add_ineq(coeff, arg, sign);
else if (m.is_eq(arg, x, y)) {
if (sign)
add_diseq(x, y);
else
add_eq(x, y);
}
else
return false;
if (sign && !pos.is_marked(arg)) {
units.push_back(m.mk_not(arg));
pos.mark(arg, false);
}
else if (!sign && !neg.is_marked(arg)) {
units.push_back(arg);
neg.mark(arg, false);
}
}
even = !even;
}
if (check_farkas()) {
return true;
}
IF_VERBOSE(0, verbose_stream() << "did not check farkas\n" << mk_pp(jst, m) << "\n"; display(verbose_stream()); );
return false; return false;
} }
bool is_bound = jst->get_name() == m_bound;
bool even = true;
rational coeff;
expr* x, * y;
unsigned j = 0;
for (expr* arg : *jst) {
if (even) {
if (!a.is_numeral(arg, coeff)) {
IF_VERBOSE(0, verbose_stream() << "not numeral " << mk_pp(jst, m) << "\n");
return false;
}
}
else {
bool sign = m.is_not(arg, arg);
if (a.is_le(arg) || a.is_lt(arg) || a.is_ge(arg) || a.is_gt(arg)) {
if (is_bound && j + 1 == jst->get_num_args())
add_conseq(coeff, arg, sign);
else
add_ineq(coeff, arg, sign);
}
else if (m.is_eq(arg, x, y)) {
if (sign)
add_diseq(x, y);
else
add_eq(x, y);
}
else {
IF_VERBOSE(0, verbose_stream() << "not a recognized arithmetical relation " << mk_pp(arg, m) << "\n");
return false;
}
// todo: rules for bounds and implied-by if (sign && !pos.is_marked(arg)) {
units.push_back(m.mk_not(arg));
IF_VERBOSE(0, verbose_stream() << "did not check " << mk_pp(jst, m) << "\n"); pos.mark(arg, false);
}
else if (!sign && !neg.is_marked(arg)) {
units.push_back(arg);
neg.mark(arg, false);
}
}
even = !even;
++j;
}
if (check())
return true;
IF_VERBOSE(0, verbose_stream() << "did not check condition\n" << mk_pp(jst, m) << "\n"; display(verbose_stream()); );
return false; return false;
} }
void register_plugins(euf::proof_checker& pc) override { void register_plugins(euf::proof_checker& pc) override {
pc.register_plugin(symbol("farkas"), this); pc.register_plugin(m_farkas, this);
pc.register_plugin(symbol("bound"), this); pc.register_plugin(m_bound, this);
pc.register_plugin(symbol("implied-eq"), this); pc.register_plugin(m_implied_eq, this);
} }
}; };

48
src/sat/smt/bv_internalize.cpp
View file

@ -308,7 +308,6 @@ namespace bv {
euf::enode* n = bool_var2enode(l.var()); euf::enode* n = bool_var2enode(l.var());
if (!n->is_attached_to(get_id())) if (!n->is_attached_to(get_id()))
mk_var(n); mk_var(n);
set_bit_eh(v, l, idx); set_bit_eh(v, l, idx);
} }
@ -453,7 +452,9 @@ namespace bv {
* *
* Alternative axiomatization: * Alternative axiomatization:
* e = sum bit2bool(i,n)*2^i + 2^n * (div(e, 2^n)) * e = sum bit2bool(i,n)*2^i + 2^n * (div(e, 2^n))
* possibly term div(e,2^n) is not * possibly term div(e,2^n) is not correct with respect to adapted semantics?
* if not, use fresh variable or similar. Overall should be much beter.
* Note: based on superb question raised at workshop on 9/1/22.
*/ */
void solver::assert_int2bv_axiom(app* n) { void solver::assert_int2bv_axiom(app* n) {
expr* e = nullptr; expr* e = nullptr;
@ -534,27 +535,27 @@ namespace bv {
internalize_binary(a, bin); internalize_binary(a, bin);
} }
void solver::internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& iun) { void solver::internalize_interp(app* n, std::function<expr* (expr*, expr*)>& ibin, std::function<expr* (expr*)>& iun) {
bv_rewriter_params p(s().params()); bv_rewriter_params p(s().params());
expr* arg1 = n->get_arg(0); expr* arg1 = n->get_arg(0);
expr* arg2 = n->get_arg(1); expr* arg2 = n->get_arg(1);
mk_bits(get_th_var(n)); mk_bits(get_th_var(n));
sat::literal eq_lit; sat::literal eq_lit;
if (p.hi_div0()) { if (p.hi_div0()) {
eq_lit = eq_internalize(n, ibin(arg1, arg2)); eq_lit = eq_internalize(n, ibin(arg1, arg2));
add_unit(eq_lit); add_unit(eq_lit);
} }
else { else {
unsigned sz = bv.get_bv_size(n); unsigned sz = bv.get_bv_size(n);
expr_ref zero(bv.mk_numeral(0, sz), m); expr_ref zero(bv.mk_numeral(0, sz), m);
sat::literal eqZ = eq_internalize(arg2, zero); sat::literal eqZ = eq_internalize(arg2, zero);
sat::literal eqU = mk_literal(iun(arg1)); sat::literal eqU = mk_literal(iun(arg1));
sat::literal eqI = mk_literal(ibin(arg1, arg2)); sat::literal eqI = mk_literal(ibin(arg1, arg2));
add_clause(~eqZ, eqU); add_clause(~eqZ, eqU);
add_clause(eqZ, eqI); add_clause(eqZ, eqI);
ctx.add_aux(~eqZ, eqU); ctx.add_aux(~eqZ, eqU);
ctx.add_aux(eqZ, eqI); ctx.add_aux(eqZ, eqI);
} }
} }
void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) { void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {
@ -574,11 +575,9 @@ namespace bv {
init_bits(n, bits); init_bits(n, bits);
} }
void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) { void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(e->get_num_args() >= 1); SASSERT(e->get_num_args() >= 1);
expr_ref_vector bits(m), new_bits(m), arg_bits(m); expr_ref_vector bits(m), new_bits(m), arg_bits(m);
get_arg_bits(e, 0, bits); get_arg_bits(e, 0, bits);
for (unsigned i = 1; i < e->get_num_args(); ++i) { for (unsigned i = 1; i < e->get_num_args(); ++i) {
arg_bits.reset(); arg_bits.reset();
@ -658,7 +657,7 @@ namespace bv {
conc.push_back(arg); conc.push_back(arg);
expr_ref r(bv.mk_concat(conc), m); expr_ref r(bv.mk_concat(conc), m);
mk_bits(get_th_var(e)); mk_bits(get_th_var(e));
sat::literal eq_lit = eq_internalize(e, r); sat::literal eq_lit = eq_internalize(e, r);
add_unit(eq_lit); add_unit(eq_lit);
} }
@ -667,9 +666,8 @@ namespace bv {
expr* arg = nullptr; expr* arg = nullptr;
VERIFY(bv.is_bit2bool(n, arg, idx)); VERIFY(bv.is_bit2bool(n, arg, idx));
euf::enode* argn = expr2enode(arg); euf::enode* argn = expr2enode(arg);
if (!argn->is_attached_to(get_id())) { if (!argn->is_attached_to(get_id()))
mk_var(argn); mk_var(argn);
}
theory_var v_arg = argn->get_th_var(get_id()); theory_var v_arg = argn->get_th_var(get_id());
SASSERT(idx < get_bv_size(v_arg)); SASSERT(idx < get_bv_size(v_arg));
sat::literal lit = expr2literal(n); sat::literal lit = expr2literal(n);
@ -770,7 +768,7 @@ namespace bv {
e1 = bv.mk_bit2bool(o1, i); e1 = bv.mk_bit2bool(o1, i);
e2 = bv.mk_bit2bool(o2, i); e2 = bv.mk_bit2bool(o2, i);
literal eq = eq_internalize(e1, e2); literal eq = eq_internalize(e1, e2);
add_clause(eq, ~oeq); add_clause(eq, ~oeq);
eqs.push_back(~eq); eqs.push_back(~eq);
} }
TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";); TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);