From 102eee77dcd955a0b938d198444312d46c3e0a34 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Feb 2023 20:12:01 -0800 Subject: [PATCH] patch regressions Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/hoist_rewriter.cpp | 2 +- src/sat/smt/arith_sls.cpp | 127 ++++++++++++------------- src/sat/smt/arith_sls.h | 42 ++++---- src/tactic/core/tseitin_cnf_tactic.cpp | 5 +- 4 files changed, 88 insertions(+), 88 deletions(-) diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp index b86f1eb47..2329fd527 100644 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ b/src/ast/rewriter/hoist_rewriter.cpp @@ -35,7 +35,7 @@ expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) { } expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) { - if (m_rewriter) + if (false && m_rewriter) return m_rewriter->mk_or(args); else return ::mk_or(args); diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp index 79e6aec54..d7a85cdb1 100644 --- a/src/sat/smt/arith_sls.cpp +++ b/src/sat/smt/arith_sls.cpp @@ -62,12 +62,12 @@ namespace arith { // first compute assignment to terms // then update non-basic variables in tableau. for (auto const& [t, v] : m_terms) { - rational val; + int64_t val; lp::lar_term const& term = s.lp().get_term(t); for (lp::lar_term::ival arg : term) { auto t2 = s.lp().column2tv(arg.column()); auto w = s.lp().local_to_external(t2.id()); - val += arg.coeff() * value(w); + val += to_numeral(arg.coeff()) * value(w); } update(v, val); } @@ -77,15 +77,18 @@ namespace arith { continue; if (!s.lp().external_is_used(v)) continue; - rational old_value = s.is_registered_var(v) ? s.get_ivalue(v).x : rational::zero(); - rational new_value = value(v); + int64_t old_value = 0; + if (s.is_registered_var(v)) + old_value = to_numeral(s.get_ivalue(v).x); + int64_t new_value = value(v); if (old_value == new_value) continue; s.ensure_column(v); lp::column_index vj = s.lp().to_column_index(v); SASSERT(!vj.is_null()); if (!s.lp().is_base(vj.index())) { - lp::impq val(new_value); + rational new_value_(new_value, rational::i64()); + lp::impq val(new_value_, rational::zero()); s.lp().set_value_for_nbasic_column(vj.index(), val); } } @@ -120,31 +123,31 @@ namespace arith { } // distance to true - rational sls::dtt(rational const& args, ineq const& ineq) const { + int64_t sls::dtt(int64_t args, ineq const& ineq) const { switch (ineq.m_op) { case ineq_kind::LE: if (args <= ineq.m_bound) - return rational::zero(); + return 0; return args - ineq.m_bound; case ineq_kind::EQ: if (args == ineq.m_bound) - return rational::zero(); - return rational::one(); + return 0; + return 1; case ineq_kind::NE: if (args == ineq.m_bound) - return rational::one(); - return rational::zero(); + return 1; + return 0; case ineq_kind::LT: if (args < ineq.m_bound) - return rational::zero(); + return 0; return args - ineq.m_bound + 1; default: UNREACHABLE(); - return rational::zero(); + return 0; } } - rational sls::dtt(ineq const& ineq, var_t v, rational const& new_value) const { + int64_t sls::dtt(ineq const& ineq, var_t v, int64_t new_value) const { auto new_args_value = ineq.m_args_value; for (auto const& [coeff, w] : ineq.m_args) { if (w == v) { @@ -156,18 +159,18 @@ namespace arith { } // critical move - bool sls::cm(ineq const& ineq, var_t v, rational& new_value) { + bool sls::cm(ineq const& ineq, var_t v, int64_t& new_value) { SASSERT(!ineq.is_true()); - auto delta = ineq.m_args_value - ineq.m_bound; + int64_t delta = ineq.m_args_value - ineq.m_bound; if (ineq.m_op == ineq_kind::NE || ineq.m_op == ineq_kind::LT) delta--; for (auto const& [coeff, w] : ineq.m_args) { if (w == v) { if (coeff > 0) - new_value = value(v) - abs(ceil(delta / coeff)); + new_value = value(v) - abs((delta + coeff - 1)/ coeff); else - new_value = value(v) + abs(floor(delta / coeff)); + new_value = value(v) + abs(delta) / -coeff; switch (ineq.m_op) { case ineq_kind::LE: @@ -199,7 +202,7 @@ namespace arith { bool sls::flip(unsigned cl) { auto const& clause = get_clause(cl); - rational new_value; + int64_t new_value; for (literal lit : clause) { if (is_true(lit)) continue; @@ -246,7 +249,7 @@ namespace arith { bool sls::flip_dscore(unsigned cl) { auto const& clause = get_clause(cl); - rational new_value, min_value, min_score(-1); + int64_t new_value, min_value, min_score(-1); var_t min_var = UINT_MAX; for (auto lit : clause) { auto const* ineq = atom(lit); @@ -254,7 +257,7 @@ namespace arith { continue; for (auto const& [coeff, v] : ineq->m_args) { if (cm(*ineq, v, new_value)) { - rational score = dscore(v, new_value); + int64_t score = dscore(v, new_value); if (UINT_MAX == min_var || score < min_score) { min_var = v; min_value = new_value; @@ -290,22 +293,22 @@ namespace arith { // TODO - use cached dts instead of computed dts // cached dts has to be updated when the score of literals are updated. // - rational sls::dscore(var_t v, rational const& new_value) const { + int64_t sls::dscore(var_t v, int64_t new_value) const { auto const& vi = m_vars[v]; - rational score(0); + int64_t score(0); for (auto const& [coeff, lit] : vi.m_literals) for (auto cl : m_bool_search->get_use_list(lit)) - score += (compute_dts(cl) - dts(cl, v, new_value)) * rational(get_weight(cl)); + score += (compute_dts(cl) - dts(cl, v, new_value)) * int64_t(get_weight(cl)); return score; } - int sls::cm_score(var_t v, rational const& new_value) { + int sls::cm_score(var_t v, int64_t new_value) { int score = 0; auto& vi = m_vars[v]; for (auto const& [coeff, lit] : vi.m_literals) { auto const& ineq = *atom(lit); - rational dtt_old = dtt(ineq); - rational dtt_new = dtt(ineq, v, new_value); + int64_t dtt_old = dtt(ineq); + int64_t dtt_new = dtt(ineq, v, new_value); for (auto cl : m_bool_search->get_use_list(lit)) { auto const& clause = get_clause_info(cl); if (!clause.is_true()) { @@ -322,8 +325,8 @@ namespace arith { return score; } - rational sls::compute_dts(unsigned cl) const { - rational d(1), d2; + int64_t sls::compute_dts(unsigned cl) const { + int64_t d(1), d2; bool first = true; for (auto a : get_clause(cl)) { auto const* ineq = atom(a); @@ -340,8 +343,8 @@ namespace arith { return d; } - rational sls::dts(unsigned cl, var_t v, rational const& new_value) const { - rational d(1), d2; + int64_t sls::dts(unsigned cl, var_t v, int64_t new_value) const { + int64_t d(1), d2; bool first = true; for (auto lit : get_clause(cl)) { auto const* ineq = atom(lit); @@ -358,28 +361,17 @@ namespace arith { return d; } - void sls::update(var_t v, rational const& new_value) { + void sls::update(var_t v, int64_t new_value) { auto& vi = m_vars[v]; auto const& old_value = vi.m_value; for (auto const& [coeff, lit] : vi.m_literals) { auto& ineq = *atom(lit); - rational dtt_old = dtt(ineq); ineq.m_args_value += coeff * (new_value - old_value); - rational dtt_new = dtt(ineq); - if ((dtt_new == 0) == is_true(lit)) { - dtt(ineq) = dtt_new; - continue; - } - VERIFY((dtt_old == 0) == is_true(lit)); - VERIFY(!(dtt_new == 0 && dtt_new < dtt_old) || !is_true(lit)); - VERIFY(!(dtt_old == 0 && dtt_new > dtt_old) || is_true(lit)); - if (dtt_new == 0 && dtt_new < dtt_old) // flip from false to true - m_bool_search->flip(lit.var()); - else if (dtt_old == 0 && dtt_old < dtt_new) // flip from true to false - m_bool_search->flip(lit.var()); - dtt(ineq) = dtt_new; - - VERIFY((dtt_new == 0) == is_true(lit)); + int64_t dtt_new = dtt(ineq); + if ((dtt_new == 0) != is_true(lit)) + m_bool_search->flip(lit.var()); + + SASSERT((dtt_new == 0) == is_true(lit)); } vi.m_value = new_value; } @@ -387,21 +379,20 @@ namespace arith { void sls::add_vars() { SASSERT(m_vars.empty()); for (unsigned v = 0; v < s.get_num_vars(); ++v) { - rational value = s.is_registered_var(v) ? s.get_ivalue(v).x : rational::zero(); - value = s.is_int(v) ? ceil(value) : value; + int64_t value = s.is_registered_var(v) ? to_numeral(s.get_ivalue(v).x) : 0; auto k = s.is_int(v) ? sls::var_kind::INT : sls::var_kind::REAL; m_vars.push_back({ value, value, k, {} }); } } - sls::ineq& sls::new_ineq(ineq_kind op, rational const& bound) { + sls::ineq& sls::new_ineq(ineq_kind op, int64_t const& bound) { auto* i = alloc(ineq); i->m_bound = bound; i->m_op = op; return *i; } - void sls::add_arg(sat::literal lit, ineq& ineq, rational const& c, var_t v) { + void sls::add_arg(sat::literal lit, ineq& ineq, int64_t const& c, var_t v) { ineq.m_args.push_back({ c, v }); ineq.m_args_value += c * value(v); m_vars[v].m_literals.push_back({ c, lit }); @@ -426,36 +417,42 @@ namespace arith { bool has_hi = s.lp().has_upper_bound(vi.index(), ci, hi, is_strict_hi); if (has_lo && has_hi && lo == hi) { - auto& ineq = new_ineq(sls::ineq_kind::EQ, lo); + auto& ineq = new_ineq(sls::ineq_kind::EQ, to_numeral(lo)); sat::literal lit(bvars++); - add_arg(lit, ineq, rational::one(), v); + add_arg(lit, ineq, 1, v); add_ineq(lit, ineq); continue; } if (has_lo) { - auto& ineq = new_ineq(is_strict_lo ? sls::ineq_kind::LT : sls::ineq_kind::LE, -lo); + auto& ineq = new_ineq(is_strict_lo ? sls::ineq_kind::LT : sls::ineq_kind::LE, to_numeral(-lo)); sat::literal lit(bvars++); - add_arg(lit, ineq, -rational::one(), v); + add_arg(lit, ineq, -1, v); add_ineq(lit, ineq); } if (has_hi) { - auto& ineq = new_ineq(is_strict_hi ? sls::ineq_kind::LT : sls::ineq_kind::LE, hi); + auto& ineq = new_ineq(is_strict_hi ? sls::ineq_kind::LT : sls::ineq_kind::LE, to_numeral(hi)); sat::literal lit(bvars++); - add_arg(lit, ineq, rational::one(), v); + add_arg(lit, ineq, 1, v); add_ineq(lit, ineq); } } } + int64_t sls::to_numeral(rational const& r) { + if (r.is_int64()) + return r.get_int64(); + return 0; + } - void sls::add_args(sat::literal lit, ineq& ineq, lp::tv t, theory_var v, rational sign) { + + void sls::add_args(sat::literal lit, ineq& ineq, lp::tv t, theory_var v, int64_t sign) { if (t.is_term()) { lp::lar_term const& term = s.lp().get_term(t); for (lp::lar_term::ival arg : term) { auto t2 = s.lp().column2tv(arg.column()); auto w = s.lp().local_to_external(t2.id()); - add_arg(lit, ineq, sign * arg.coeff(), w); + add_arg(lit, ineq, sign * to_numeral(arg.coeff()), w); } } else @@ -489,9 +486,9 @@ namespace arith { } if (should_minus) bound.neg(); - auto& ineq = new_ineq(op, bound); + auto& ineq = new_ineq(op, to_numeral(bound)); - add_args(lit, ineq, t, b->get_var(), should_minus ? rational::minus_one() :rational::one()); + add_args(lit, ineq, t, b->get_var(), should_minus ? -1 : 1); m_literals.set(lit.index(), &ineq); return; } @@ -503,9 +500,9 @@ namespace arith { theory_var v = s.get_th_var(r); lp::tv tu = s.get_tv(u); lp::tv tv = s.get_tv(v); - auto& ineq = new_ineq(lit.sign() ? sls::ineq_kind::NE : sls::ineq_kind::EQ, rational::zero()); - add_args(lit, ineq, tu, u, rational::one()); - add_args(lit, ineq, tv, v, -rational::one()); + auto& ineq = new_ineq(lit.sign() ? sls::ineq_kind::NE : sls::ineq_kind::EQ, 0); + add_args(lit, ineq, tu, u, 1); + add_args(lit, ineq, tv, v, -1); m_literals.set(lit.index(), &ineq); return; } diff --git a/src/sat/smt/arith_sls.h b/src/sat/smt/arith_sls.h index 9a4cfcd81..9682376be 100644 --- a/src/sat/smt/arith_sls.h +++ b/src/sat/smt/arith_sls.h @@ -58,10 +58,10 @@ namespace arith { public: // encode args <= bound, args = bound, args < bound struct ineq { - vector> m_args; + vector> m_args; ineq_kind m_op = ineq_kind::LE; - rational m_bound; - rational m_args_value; + int64_t m_bound; + int64_t m_args_value; bool is_true() const { switch (m_op) { @@ -94,15 +94,15 @@ namespace arith { private: struct var_info { - rational m_value; - rational m_best_value; + int64_t m_value; + int64_t m_best_value; var_kind m_kind = var_kind::INT; - vector> m_literals; + vector> m_literals; }; struct clause { unsigned m_weight = 1; - rational m_dts = rational::one(); + int64_t m_dts = 1; }; solver& s; @@ -137,27 +137,29 @@ namespace arith { bool flip_dscore(); bool flip_dscore(unsigned cl); bool flip(unsigned cl); - rational dtt(ineq const& ineq) const { return dtt(ineq.m_args_value, ineq); } - rational dtt(rational const& args, ineq const& ineq) const; - rational dtt(ineq const& ineq, var_t v, rational const& new_value) const; - rational dts(unsigned cl, var_t v, rational const& new_value) const; - rational compute_dts(unsigned cl) const; - bool cm(ineq const& ineq, var_t v, rational& new_value); - int cm_score(var_t v, rational const& new_value); - void update(var_t v, rational const& new_value); + int64_t dtt(ineq const& ineq) const { return dtt(ineq.m_args_value, ineq); } + int64_t dtt(int64_t args, ineq const& ineq) const; + int64_t dtt(ineq const& ineq, var_t v, int64_t new_value) const; + int64_t dts(unsigned cl, var_t v, int64_t new_value) const; + int64_t compute_dts(unsigned cl) const; + bool cm(ineq const& ineq, var_t v, int64_t& new_value); + int cm_score(var_t v, int64_t new_value); + void update(var_t v, int64_t new_value); void paws(); - rational dscore(var_t v, rational const& new_value) const; + int64_t dscore(var_t v, int64_t new_value) const; void save_best_values(); void add_vars(); - sls::ineq& new_ineq(ineq_kind op, rational const& bound); - void add_arg(sat::literal lit, ineq& ineq, rational const& c, var_t v); + sls::ineq& new_ineq(ineq_kind op, int64_t const& bound); + void add_arg(sat::literal lit, ineq& ineq, int64_t const& c, var_t v); void add_bounds(sat::literal_vector& bounds); - void add_args(sat::literal lit, ineq& ineq, lp::tv t, euf::theory_var v, rational sign); + void add_args(sat::literal lit, ineq& ineq, lp::tv t, euf::theory_var v, int64_t sign); void init_literal(sat::literal lit); void init_bool_var_assignment(sat::bool_var v); void init_literal_assignment(sat::literal lit); - rational value(var_t v) const { return m_vars[v].m_value; } + int64_t value(var_t v) const { return m_vars[v].m_value; } + int64_t to_numeral(rational const& r); + public: sls(solver& s); lbool operator ()(bool_vector& phase); diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index ec03849bc..411b8aa6e 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -141,7 +141,7 @@ class tseitin_cnf_tactic : public tactic { sign = !sign; goto start; case OP_OR: - case OP_AND: + // case OP_AND: l = nullptr; m_cache.find(to_app(n), l); SASSERT(l != 0); @@ -188,7 +188,7 @@ class tseitin_cnf_tactic : public tactic { goto start; } case OP_OR: - case OP_AND: + // case OP_AND: visited = false; push_frame(to_app(n)); return; @@ -202,6 +202,7 @@ class tseitin_cnf_tactic : public tactic { case OP_XOR: case OP_IMPLIES: case OP_DISTINCT: + case OP_AND: throw_op_not_handled(); default: return;