From b49ffb8a87782b1119fe6e088d51ec5afb802813 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Sep 2022 22:52:23 -0700 Subject: [PATCH] indentation --- src/sat/smt/arith_proof_checker.h | 132 +++++++++++++++++------------- src/sat/smt/bv_internalize.cpp | 48 ++++++----- 2 files changed, 97 insertions(+), 83 deletions(-) diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h index d067303a5..1a8a8df27 100644 --- a/src/sat/smt/arith_proof_checker.h +++ b/src/sat/smt/arith_proof_checker.h @@ -41,16 +41,19 @@ namespace arith { m_coeff = 0; } }; - + ast_manager& m; - arith_util a; + arith_util a; vector> m_todo; - bool m_strict = false; - row m_ineq; - row m_conseq; - vector m_eqs; - vector m_ineqs; - vector m_diseqs; + bool m_strict = false; + row m_ineq; + row m_conseq; + vector m_eqs; + vector m_ineqs; + vector m_diseqs; + symbol m_farkas; + symbol m_implied_eq; + symbol m_bound; void add(row& r, expr* v, rational const& coeff) { rational coeff1; @@ -147,6 +150,8 @@ namespace arith { 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)) 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)) m_todo.push_back({coeff*coeff1, e1}); else if (a.is_add(e)) @@ -309,10 +314,14 @@ namespace arith { rows.push_back(row()); return rows.back(); } - 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 {} @@ -328,7 +337,8 @@ namespace arith { bool add_ineq(rational const& coeff, expr* e, bool sign) { if (!m_diseqs.empty()) 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) { @@ -374,60 +384,66 @@ namespace arith { else pos.mark(e, true); - if (jst->get_name() == symbol("farkas")) { - bool even = true; - rational coeff; - expr* x, *y; - 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()); ); + if (jst->get_name() != m_farkas && + jst->get_name() != m_bound && + jst->get_name() != m_implied_eq) { + IF_VERBOSE(0, verbose_stream() << "unhandled inference " << mk_pp(jst, m) << "\n"); 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_VERBOSE(0, verbose_stream() << "did not check " << mk_pp(jst, m) << "\n"); + 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; + ++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; } void register_plugins(euf::proof_checker& pc) override { - pc.register_plugin(symbol("farkas"), this); - pc.register_plugin(symbol("bound"), this); - pc.register_plugin(symbol("implied-eq"), this); + pc.register_plugin(m_farkas, this); + pc.register_plugin(m_bound, this); + pc.register_plugin(m_implied_eq, this); } }; diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 6d2dc683a..4cc161829 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -308,7 +308,6 @@ namespace bv { euf::enode* n = bool_var2enode(l.var()); if (!n->is_attached_to(get_id())) mk_var(n); - set_bit_eh(v, l, idx); } @@ -453,7 +452,9 @@ namespace bv { * * Alternative axiomatization: * 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) { expr* e = nullptr; @@ -534,27 +535,27 @@ namespace bv { internalize_binary(a, bin); } - void solver::internalize_interp(app* n, std::function& ibin, std::function& iun) { + void solver::internalize_interp(app* n, std::function& ibin, std::function& iun) { bv_rewriter_params p(s().params()); expr* arg1 = n->get_arg(0); expr* arg2 = n->get_arg(1); mk_bits(get_th_var(n)); - sat::literal eq_lit; + sat::literal eq_lit; if (p.hi_div0()) { eq_lit = eq_internalize(n, ibin(arg1, arg2)); - add_unit(eq_lit); - } - else { - unsigned sz = bv.get_bv_size(n); - expr_ref zero(bv.mk_numeral(0, sz), m); - sat::literal eqZ = eq_internalize(arg2, zero); - sat::literal eqU = mk_literal(iun(arg1)); - sat::literal eqI = mk_literal(ibin(arg1, arg2)); - add_clause(~eqZ, eqU); - add_clause(eqZ, eqI); - ctx.add_aux(~eqZ, eqU); - ctx.add_aux(eqZ, eqI); - } + add_unit(eq_lit); + } + else { + unsigned sz = bv.get_bv_size(n); + expr_ref zero(bv.mk_numeral(0, sz), m); + sat::literal eqZ = eq_internalize(arg2, zero); + sat::literal eqU = mk_literal(iun(arg1)); + sat::literal eqI = mk_literal(ibin(arg1, arg2)); + add_clause(~eqZ, eqU); + add_clause(eqZ, eqI); + ctx.add_aux(~eqZ, eqU); + ctx.add_aux(eqZ, eqI); + } } void solver::internalize_unary(app* n, std::function& fn) { @@ -574,11 +575,9 @@ namespace bv { init_bits(n, bits); } - void solver::internalize_binary(app* e, std::function& fn) { 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); for (unsigned i = 1; i < e->get_num_args(); ++i) { arg_bits.reset(); @@ -658,7 +657,7 @@ namespace bv { conc.push_back(arg); expr_ref r(bv.mk_concat(conc), m); 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); } @@ -667,9 +666,8 @@ namespace bv { expr* arg = nullptr; VERIFY(bv.is_bit2bool(n, arg, idx)); euf::enode* argn = expr2enode(arg); - if (!argn->is_attached_to(get_id())) { - mk_var(argn); - } + if (!argn->is_attached_to(get_id())) + mk_var(argn); theory_var v_arg = argn->get_th_var(get_id()); SASSERT(idx < get_bv_size(v_arg)); sat::literal lit = expr2literal(n); @@ -770,7 +768,7 @@ namespace bv { e1 = bv.mk_bit2bool(o1, i); e2 = bv.mk_bit2bool(o2, i); literal eq = eq_internalize(e1, e2); - add_clause(eq, ~oeq); + add_clause(eq, ~oeq); eqs.push_back(~eq); } TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);