mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity

Merge branch 'master' into polysat

Browse source
This commit is contained in:
Jakob Rath 2023-05-26 15:58:09 +02:00
commit f54f33551e
308 changed files with 6606 additions and 18485 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/CMakeLists.txt
View file

@ -3,6 +3,7 @@ z3_add_component(sat_smt
arith_axioms.cpp
arith_diagnostics.cpp
arith_internalize.cpp
arith_sls.cpp
arith_solver.cpp
array_axioms.cpp
array_diagnostics.cpp
@ -21,6 +22,7 @@ z3_add_component(sat_smt
euf_ackerman.cpp
euf_internalize.cpp
euf_invariant.cpp
euf_local_search.cpp
euf_model.cpp
euf_proof.cpp
euf_proof_checker.cpp

11
src/sat/smt/arith_diagnostics.cpp
View file

@ -23,6 +23,17 @@ Author:
namespace arith {
void arith_proof_hint_builder::set_type(euf::solver& ctx, hint_type ty) {
ctx.push(value_trail<unsigned>(m_eq_tail));
ctx.push(value_trail<unsigned>(m_lit_tail));
m_ty = ty;
reset();
}
arith_proof_hint* arith_proof_hint_builder::mk(euf::solver& s) {
return new (s.get_region()) arith_proof_hint(m_ty, m_num_le, m_lit_head, m_lit_tail, m_eq_head, m_eq_tail);
}
std::ostream& solver::display(std::ostream& out) const {
lp().display(out);

6
src/sat/smt/arith_internalize.cpp
View file

@ -107,10 +107,12 @@ namespace arith {
e = a.mk_idiv0(x, y);
}
else if (a.is_rem(n, x, y)) {
e = a.mk_rem0(x, y);
n = a.mk_rem(x, a.mk_int(0));
e = a.mk_rem0(x, a.mk_int(0));
}
else if (a.is_mod(n, x, y)) {
e = a.mk_mod0(x, y);
n = a.mk_mod(x, a.mk_int(0));
e = a.mk_mod0(x, a.mk_int(0));
}
else if (a.is_power(n, x, y)) {
e = a.mk_power0(x, y);

650
src/sat/smt/arith_sls.cpp Normal file
View file

@ -0,0 +1,650 @@
/*++
Copyright (c) 2023 Microsoft Corporation
Module Name:
arith_local_search.cpp
Abstract:
Local search dispatch for SMT
Author:
Nikolaj Bjorner (nbjorner) 2023-02-07
--*/
#include "sat/sat_solver.h"
#include "sat/smt/arith_solver.h"
namespace arith {
sls::sls(solver& s):
s(s), m(s.m) {}
void sls::reset() {
m_bool_vars.reset();
m_vars.reset();
m_terms.reset();
}
void sls::save_best_values() {
for (unsigned v = 0; v < s.get_num_vars(); ++v)
m_vars[v].m_best_value = m_vars[v].m_value;
check_ineqs();
if (unsat().size() == 1) {
auto idx = *unsat().begin();
verbose_stream() << idx << "\n";
auto const& c = *m_bool_search->m_clauses[idx].m_clause;
verbose_stream() << c << "\n";
for (auto lit : c) {
bool_var bv = lit.var();
ineq* i = atom(bv);
if (i)
verbose_stream() << lit << ": " << *i << "\n";
}
verbose_stream() << "\n";
}
}
void sls::store_best_values() {
// first compute assignment to terms
// then update non-basic variables in tableau.
if (!unsat().empty())
return;
for (auto const& [t,v] : m_terms) {
int64_t val = 0;
lp::lar_term const& term = s.lp().get_term(t);
for (lp::lar_term::ival const& arg : term) {
auto t2 = s.lp().column2tv(arg.column());
auto w = s.lp().local_to_external(t2.id());
val += to_numeral(arg.coeff()) * m_vars[w].m_best_value;
}
if (v == 52) {
verbose_stream() << "update v" << v << " := " << val << "\n";
for (lp::lar_term::ival const& arg : term) {
auto t2 = s.lp().column2tv(arg.column());
auto w = s.lp().local_to_external(t2.id());
verbose_stream() << "v" << w << " := " << m_vars[w].m_best_value << " * " << to_numeral(arg.coeff()) << "\n";
}
}
m_vars[v].m_best_value = val;
}
for (unsigned v = 0; v < s.get_num_vars(); ++v) {
if (s.is_bool(v))
continue;
if (!s.lp().external_is_used(v))
continue;
int64_t new_value = m_vars[v].m_best_value;
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())) {
rational new_value_(new_value, rational::i64());
lp::impq val(new_value_, rational::zero());
s.lp().set_value_for_nbasic_column(vj.index(), val);
}
}
lbool r = s.make_feasible();
VERIFY (!unsat().empty() || r == l_true);
#if 0
if (unsat().empty())
s.m_num_conflicts = s.get_config().m_arith_propagation_threshold;
#endif
auto check_bool_var = [&](sat::bool_var bv) {
auto* ineq = m_bool_vars.get(bv, nullptr);
if (!ineq)
return;
api_bound* b = nullptr;
s.m_bool_var2bound.find(bv, b);
if (!b)
return;
auto bound = b->get_value();
theory_var v = b->get_var();
if (s.get_phase(bv) == m_bool_search->get_model()[bv])
return;
switch (b->get_bound_kind()) {
case lp_api::lower_t:
verbose_stream() << "v" << v << " " << bound << " <= " << s.get_value(v) << " " << m_vars[v].m_best_value << "\n";
break;
case lp_api::upper_t:
verbose_stream() << "v" << v << " " << bound << " >= " << s.get_value(v) << " " << m_vars[v].m_best_value << "\n";
break;
}
int64_t value = 0;
for (auto const& [coeff, v] : ineq->m_args) {
value += coeff * m_vars[v].m_best_value;
}
ineq->m_args_value = value;
verbose_stream() << *ineq << " dtt " << dtt(false, *ineq) << " phase " << s.get_phase(bv) << " model " << m_bool_search->get_model()[bv] << "\n";
for (auto const& [coeff, v] : ineq->m_args)
verbose_stream() << "v" << v << " := " << m_vars[v].m_best_value << "\n";
s.display(verbose_stream());
display(verbose_stream());
UNREACHABLE();
exit(0);
};
if (unsat().empty()) {
for (bool_var v = 0; v < s.s().num_vars(); ++v)
check_bool_var(v);
}
}
void sls::set(sat::ddfw* d) {
m_bool_search = d;
reset();
m_bool_vars.reserve(s.s().num_vars());
add_vars();
for (unsigned i = 0; i < d->num_clauses(); ++i)
for (sat::literal lit : *d->get_clause_info(i).m_clause)
init_bool_var(lit.var());
for (unsigned v = 0; v < s.s().num_vars(); ++v)
init_bool_var_assignment(v);
d->set(this);
}
// distance to true
int64_t sls::dtt(bool sign, int64_t args, ineq const& ineq) const {
switch (ineq.m_op) {
case ineq_kind::LE:
if (sign) {
if (args <= ineq.m_bound)
return ineq.m_bound - args + 1;
return 0;
}
if (args <= ineq.m_bound)
return 0;
return args - ineq.m_bound;
case ineq_kind::EQ:
if (sign) {
if (args == ineq.m_bound)
return 1;
return 0;
}
if (args == ineq.m_bound)
return 0;
return 1;
case ineq_kind::NE:
if (sign) {
if (args == ineq.m_bound)
return 0;
return 1;
}
if (args == ineq.m_bound)
return 1;
return 0;
case ineq_kind::LT:
if (sign) {
if (args < ineq.m_bound)
return ineq.m_bound - args;
return 0;
}
if (args < ineq.m_bound)
return 0;
return args - ineq.m_bound + 1;
default:
UNREACHABLE();
return 0;
}
}
//
// dtt is high overhead. It walks ineq.m_args
// m_vars[w].m_value can be computed outside and shared among calls
// different data-structures for storing coefficients
//
int64_t sls::dtt(bool sign, ineq const& ineq, var_t v, int64_t new_value) const {
for (auto const& [coeff, w] : ineq.m_args)
if (w == v)
return dtt(sign, ineq.m_args_value + coeff * (new_value - m_vars[v].m_value), ineq);
return 1;
}
int64_t sls::dtt(bool sign, ineq const& ineq, int64_t coeff, int64_t old_value, int64_t new_value) const {
return dtt(sign, ineq.m_args_value + coeff * (new_value - old_value), ineq);
}
bool sls::cm(bool old_sign, ineq const& ineq, var_t v, int64_t& new_value) {
for (auto const& [coeff, w] : ineq.m_args)
if (w == v)
return cm(old_sign, ineq, v, coeff, new_value);
return false;
}
bool sls::cm(bool old_sign, ineq const& ineq, var_t v, int64_t coeff, int64_t& new_value) {
SASSERT(ineq.is_true() != old_sign);
VERIFY(ineq.is_true() != old_sign);
auto bound = ineq.m_bound;
auto argsv = ineq.m_args_value;
bool solved = false;
int64_t delta = argsv - bound;
auto make_eq = [&]() {
SASSERT(delta != 0);
if (delta < 0)
new_value = value(v) + (abs(delta) + abs(coeff) - 1) / coeff;
else
new_value = value(v) - (delta + abs(coeff) - 1) / coeff;
solved = argsv + coeff * (new_value - value(v)) == bound;
if (!solved && abs(coeff) == 1) {
verbose_stream() << "did not solve equality " << ineq << " for " << v << "\n";
verbose_stream() << new_value << " " << value(v) << " delta " << delta << " lhs " << (argsv + coeff * (new_value - value(v))) << " bound " << bound << "\n";
UNREACHABLE();
}
return solved;
};
auto make_diseq = [&]() {
if (delta >= 0)
delta++;
else
delta--;
new_value = value(v) + (abs(delta) + abs(coeff) - 1) / coeff;
VERIFY(argsv + coeff * (new_value - value(v)) != bound);
return true;
};
if (!old_sign) {
switch (ineq.m_op) {
case ineq_kind::LE:
// args <= bound -> args > bound
SASSERT(argsv <= bound);
SASSERT(delta <= 0);
--delta;
new_value = value(v) + (abs(delta) + abs(coeff) - 1) / coeff;
VERIFY(argsv + coeff * (new_value - value(v)) > bound);
return true;
case ineq_kind::LT:
// args < bound -> args >= bound
SASSERT(argsv <= ineq.m_bound);
SASSERT(delta <= 0);
new_value = value(v) + (abs(delta) + abs(coeff) - 1) / coeff;
VERIFY(argsv + coeff * (new_value - value(v)) >= bound);
return true;
case ineq_kind::EQ:
return make_diseq();
case ineq_kind::NE:
return make_eq();
default:
UNREACHABLE();
break;
}
}
else {
switch (ineq.m_op) {
case ineq_kind::LE:
SASSERT(argsv > ineq.m_bound);
SASSERT(delta > 0);
new_value = value(v) - (delta + abs(coeff) - 1) / coeff;
VERIFY(argsv + coeff * (new_value - value(v)) <= bound);
return true;
case ineq_kind::LT:
SASSERT(argsv >= ineq.m_bound);
SASSERT(delta >= 0);
++delta;
new_value = value(v) - (abs(delta) + abs(coeff) - 1) / coeff;
VERIFY(argsv + coeff * (new_value - value(v)) < bound);
return true;
case ineq_kind::NE:
return make_diseq();
case ineq_kind::EQ:
return make_eq();
default:
UNREACHABLE();
break;
}
}
return false;
}
// flip on the first positive score
// it could be changed to flip on maximal positive score
// or flip on maximal non-negative score
// or flip on first non-negative score
bool sls::flip(bool sign, ineq const& ineq) {
int64_t new_value;
auto v = ineq.m_var_to_flip;
if (v == UINT_MAX) {
IF_VERBOSE(1, verbose_stream() << "no var to flip\n");
return false;
}
if (!cm(sign, ineq, v, new_value)) {
verbose_stream() << "no critical move for " << v << "\n";
return false;
}
update(v, new_value);
return true;
}
//
// dscore(op) = sum_c (dts(c,alpha) - dts(c,alpha_after)) * weight(c)
// TODO - use cached dts instead of computed dts
// cached dts has to be updated when the score of literals are updated.
//
double sls::dscore(var_t v, int64_t new_value) const {
double score = 0;
auto const& vi = m_vars[v];
for (auto const& [coeff, bv] : vi.m_bool_vars) {
sat::literal lit(bv, false);
for (auto cl : m_bool_search->get_use_list(lit))
score += (compute_dts(cl) - dts(cl, v, new_value)) * m_bool_search->get_weight(cl);
for (auto cl : m_bool_search->get_use_list(~lit))
score += (compute_dts(cl) - dts(cl, v, new_value)) * m_bool_search->get_weight(cl);
}
return score;
}
//
// cm_score is costly. It involves several cache misses.
// Note that
// - m_bool_search->get_use_list(lit).size() is "often" 1 or 2
// - dtt_old can be saved
//
int sls::cm_score(var_t v, int64_t new_value) {
int score = 0;
auto& vi = m_vars[v];
int64_t old_value = vi.m_value;
for (auto const& [coeff, bv] : vi.m_bool_vars) {
auto const& ineq = *atom(bv);
bool old_sign = sign(bv);
int64_t dtt_old = dtt(old_sign, ineq);
int64_t dtt_new = dtt(old_sign, ineq, coeff, old_value, new_value);
if ((dtt_old == 0) == (dtt_new == 0))
continue;
sat::literal lit(bv, old_sign);
if (dtt_old == 0)
// flip from true to false
lit.neg();
// lit flips form false to true:
for (auto cl : m_bool_search->get_use_list(lit)) {
auto const& clause = get_clause_info(cl);
if (!clause.is_true())
++score;
}
// ignore the situation where clause contains multiple literals using v
for (auto cl : m_bool_search->get_use_list(~lit)) {
auto const& clause = get_clause_info(cl);
if (clause.m_num_trues == 1)
--score;
}
}
return score;
}
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.var());
if (!ineq)
continue;
d2 = dtt(a.sign(), *ineq);
if (first)
d = d2, first = false;
else
d = std::min(d, d2);
if (d == 0)
break;
}
return d;
}
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.var());
if (!ineq)
continue;
d2 = dtt(lit.sign(), *ineq, v, new_value);
if (first)
d = d2, first = false;
else
d = std::min(d, d2);
if (d == 0)
break;
}
return d;
}
void sls::update(var_t v, int64_t new_value) {
auto& vi = m_vars[v];
auto old_value = vi.m_value;
for (auto const& [coeff, bv] : vi.m_bool_vars) {
auto& ineq = *atom(bv);
bool old_sign = sign(bv);
sat::literal lit(bv, old_sign);
SASSERT(is_true(lit));
ineq.m_args_value += coeff * (new_value - old_value);
int64_t dtt_new = dtt(old_sign, ineq);
if (dtt_new != 0)
m_bool_search->flip(bv);
SASSERT(dtt(sign(bv), ineq) == 0);
}
vi.m_value = new_value;
}
void sls::add_vars() {
SASSERT(m_vars.empty());
for (unsigned v = 0; v < s.get_num_vars(); ++v) {
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, int64_t const& bound) {
auto* i = alloc(ineq);
i->m_bound = bound;
i->m_op = op;
return *i;
}
void sls::add_arg(sat::bool_var bv, 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_bool_vars.push_back({ c, bv});
}
int64_t sls::to_numeral(rational const& r) {
if (r.is_int64())
return r.get_int64();
return 0;
}
void sls::add_args(sat::bool_var bv, 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);
m_terms.push_back({t,v});
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(bv, ineq, sign * to_numeral(arg.coeff()), w);
}
}
else
add_arg(bv, ineq, sign, s.lp().local_to_external(t.id()));
}
void sls::init_bool_var(sat::bool_var bv) {
if (m_bool_vars.get(bv, nullptr))
return;
api_bound* b = nullptr;
s.m_bool_var2bound.find(bv, b);
if (b) {
auto t = b->tv();
rational bound = b->get_value();
bool should_minus = false;
sls::ineq_kind op;
should_minus = b->get_bound_kind() == lp_api::bound_kind::lower_t;
op = sls::ineq_kind::LE;
if (should_minus)
bound.neg();
auto& ineq = new_ineq(op, to_numeral(bound));
add_args(bv, ineq, t, b->get_var(), should_minus ? -1 : 1);
m_bool_vars.set(bv, &ineq);
m_bool_search->set_external(bv);
return;
}
expr* e = s.bool_var2expr(bv);
expr* l = nullptr, * r = nullptr;
if (e && m.is_eq(e, l, r) && s.a.is_int_real(l)) {
theory_var u = s.get_th_var(l);
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(sls::ineq_kind::EQ, 0);
add_args(bv, ineq, tu, u, 1);
add_args(bv, ineq, tv, v, -1);
m_bool_vars.set(bv, &ineq);
m_bool_search->set_external(bv);
return;
}
}
void sls::init_bool_var_assignment(sat::bool_var v) {
auto* ineq = m_bool_vars.get(v, nullptr);
if (ineq && is_true(sat::literal(v, false)) != (dtt(false, *ineq) == 0))
m_bool_search->flip(v);
}
void sls::init_search() {
on_restart();
}
void sls::finish_search() {
store_best_values();
}
void sls::flip(sat::bool_var v) {
sat::literal lit(v, !sign(v));
SASSERT(!is_true(lit));
auto const* ineq = atom(v);
if (!ineq)
IF_VERBOSE(0, verbose_stream() << "no inequality for variable " << v << "\n");
if (!ineq)
return;
SASSERT(ineq->is_true() == lit.sign());
flip(sign(v), *ineq);
}
double sls::reward(sat::bool_var v) {
if (m_dscore_mode)
return dscore_reward(v);
else
return dtt_reward(v);
}
double sls::dtt_reward(sat::bool_var bv0) {
bool sign0 = sign(bv0);
auto* ineq = atom(bv0);
if (!ineq)
return -1;
int64_t new_value;
double max_result = -1;
for (auto const & [coeff, x] : ineq->m_args) {
if (!cm(sign0, *ineq, x, coeff, new_value))
continue;
double result = 0;
auto old_value = m_vars[x].m_value;
for (auto const& [coeff, bv] : m_vars[x].m_bool_vars) {
result += m_bool_search->reward(bv);
continue;
bool old_sign = sign(bv);
auto dtt_old = dtt(old_sign, *atom(bv));
auto dtt_new = dtt(old_sign, *atom(bv), coeff, old_value, new_value);
if ((dtt_new == 0) != (dtt_old == 0))
result += m_bool_search->reward(bv);
}
if (result > max_result) {
max_result = result;
ineq->m_var_to_flip = x;
}
}
return max_result;
}
double sls::dscore_reward(sat::bool_var bv) {
m_dscore_mode = false;
bool old_sign = sign(bv);
sat::literal litv(bv, old_sign);
auto* ineq = atom(bv);
if (!ineq)
return 0;
SASSERT(ineq->is_true() != old_sign);
int64_t new_value;
for (auto const& [coeff, v] : ineq->m_args) {
double result = 0;
if (cm(old_sign, *ineq, v, coeff, new_value))
result = dscore(v, new_value);
// just pick first positive, or pick a max?
if (result > 0) {
ineq->m_var_to_flip = v;
return result;
}
}
return 0;
}
// switch to dscore mode
void sls::on_rescale() {
m_dscore_mode = true;
}
void sls::on_save_model() {
save_best_values();
}
void sls::on_restart() {
for (unsigned v = 0; v < s.s().num_vars(); ++v)
init_bool_var_assignment(v);
check_ineqs();
}
void sls::check_ineqs() {
auto check_bool_var = [&](sat::bool_var bv) {
auto const* ineq = atom(bv);
if (!ineq)
return;
int64_t d = dtt(sign(bv), *ineq);
sat::literal lit(bv, sign(bv));
if (is_true(lit) != (d == 0)) {
verbose_stream() << "invalid assignment " << bv << " " << *ineq << "\n";
}
VERIFY(is_true(lit) == (d == 0));
};
for (unsigned v = 0; v < s.get_num_vars(); ++v)
check_bool_var(v);
}
std::ostream& sls::display(std::ostream& out) const {
for (bool_var bv = 0; bv < s.s().num_vars(); ++bv) {
auto const* ineq = atom(bv);
if (!ineq)
continue;
out << bv << " " << *ineq << "\n";
}
for (unsigned v = 0; v < s.get_num_vars(); ++v) {
if (s.is_bool(v))
continue;
out << "v" << v << " := " << m_vars[v].m_value << " " << m_vars[v].m_best_value << "\n";
}
return out;
}
}

170
src/sat/smt/arith_sls.h Normal file
View file

@ -0,0 +1,170 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
arith_local_search.h
Abstract:
Theory plugin for arithmetic local search
Author:
Nikolaj Bjorner (nbjorner) 2020-09-08
--*/
#pragma once
#include "util/obj_pair_set.h"
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.h"
#include "math/lp/indexed_value.h"
#include "math/lp/lar_solver.h"
#include "math/lp/nla_solver.h"
#include "math/lp/lp_types.h"
#include "math/lp/lp_api.h"
#include "math/polynomial/algebraic_numbers.h"
#include "math/polynomial/polynomial.h"
#include "sat/smt/sat_th.h"
#include "sat/sat_ddfw.h"
namespace arith {
class solver;
// local search portion for arithmetic
class sls : public sat::local_search_plugin {
enum class ineq_kind { EQ, LE, LT, NE };
enum class var_kind { INT, REAL };
typedef unsigned var_t;
typedef unsigned atom_t;
struct config {
double cb = 0.0;
unsigned L = 20;
unsigned t = 45;
unsigned max_no_improve = 500000;
double sp = 0.0003;
};
struct stats {
unsigned m_num_flips = 0;
};
public:
// encode args <= bound, args = bound, args < bound
struct ineq {
vector<std::pair<int64_t, var_t>> m_args;
ineq_kind m_op = ineq_kind::LE;
int64_t m_bound;
int64_t m_args_value;
unsigned m_var_to_flip = UINT_MAX;
bool is_true() const {
switch (m_op) {
case ineq_kind::LE:
return m_args_value <= m_bound;
case ineq_kind::EQ:
return m_args_value == m_bound;
case ineq_kind::NE:
return m_args_value != m_bound;
default:
return m_args_value < m_bound;
}
}
std::ostream& display(std::ostream& out) const {
bool first = true;
for (auto const& [c, v] : m_args)
out << (first ? "" : " + ") << c << " * v" << v, first = false;
switch (m_op) {
case ineq_kind::LE:
return out << " <= " << m_bound << "(" << m_args_value << ")";
case ineq_kind::EQ:
return out << " == " << m_bound << "(" << m_args_value << ")";
case ineq_kind::NE:
return out << " != " << m_bound << "(" << m_args_value << ")";
default:
return out << " < " << m_bound << "(" << m_args_value << ")";
}
}
};
private:
struct var_info {
int64_t m_value;
int64_t m_best_value;
var_kind m_kind = var_kind::INT;
svector<std::pair<int64_t, sat::bool_var>> m_bool_vars;
};
solver& s;
ast_manager& m;
sat::ddfw* m_bool_search = nullptr;
stats m_stats;
config m_config;
scoped_ptr_vector<ineq> m_bool_vars;
vector<var_info> m_vars;
svector<std::pair<lp::tv, euf::theory_var>> m_terms;
bool m_dscore_mode = false;
indexed_uint_set& unsat() { return m_bool_search->unsat_set(); }
unsigned num_clauses() const { return m_bool_search->num_clauses(); }
sat::clause& get_clause(unsigned idx) { return *get_clause_info(idx).m_clause; }
sat::clause const& get_clause(unsigned idx) const { return *get_clause_info(idx).m_clause; }
sat::ddfw::clause_info& get_clause_info(unsigned idx) { return m_bool_search->get_clause_info(idx); }
sat::ddfw::clause_info const& get_clause_info(unsigned idx) const { return m_bool_search->get_clause_info(idx); }
bool is_true(sat::literal lit) { return lit.sign() != m_bool_search->get_value(lit.var()); }
bool sign(sat::bool_var v) const { return !m_bool_search->get_value(v); }
void reset();
ineq* atom(sat::bool_var bv) const { return m_bool_vars[bv]; }
bool flip(bool sign, ineq const& ineq);
int64_t dtt(bool sign, ineq const& ineq) const { return dtt(sign, ineq.m_args_value, ineq); }
int64_t dtt(bool sign, int64_t args_value, ineq const& ineq) const;
int64_t dtt(bool sign, ineq const& ineq, var_t v, int64_t new_value) const;
int64_t dtt(bool sign, ineq const& ineq, int64_t coeff, int64_t old_value, 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(bool sign, ineq const& ineq, var_t v, int64_t& new_value);
bool cm(bool sign, ineq const& ineq, var_t v, int64_t coeff, int64_t& new_value);
int cm_score(var_t v, int64_t new_value);
void update(var_t v, int64_t new_value);
double dscore_reward(sat::bool_var v);
double dtt_reward(sat::bool_var v);
double dscore(var_t v, int64_t new_value) const;
void save_best_values();
void store_best_values();
void add_vars();
sls::ineq& new_ineq(ineq_kind op, int64_t const& bound);
void add_arg(sat::bool_var bv, ineq& ineq, int64_t const& c, var_t v);
void add_args(sat::bool_var bv, ineq& ineq, lp::tv t, euf::theory_var v, int64_t sign);
void init_bool_var(sat::bool_var v);
void init_bool_var_assignment(sat::bool_var v);
int64_t value(var_t v) const { return m_vars[v].m_value; }
int64_t to_numeral(rational const& r);
void check_ineqs();
std::ostream& display(std::ostream& out) const;
public:
sls(solver& s);
~sls() override {}
void set(sat::ddfw* d);
void init_search() override;
void finish_search() override;
void flip(sat::bool_var v) override;
double reward(sat::bool_var v) override;
void on_rescale() override;
void on_save_model() override;
void on_restart() override;
};
inline std::ostream& operator<<(std::ostream& out, sls::ineq const& ineq) {
return ineq.display(out);
}
}

9
src/sat/smt/arith_solver.cpp
View file

@ -24,6 +24,7 @@ namespace arith {
solver::solver(euf::solver& ctx, theory_id id) :
th_euf_solver(ctx, symbol("arith"), id),
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_local_search(*this),
m_resource_limit(*this),
m_bp(*this),
a(m),
@ -100,8 +101,7 @@ namespace arith {
return false;
switch (lbl) {
case l_false:
TRACE("arith", tout << "propagation conflict\n";);
case l_false:
get_infeasibility_explanation_and_set_conflict();
break;
case l_true:
@ -381,9 +381,9 @@ namespace arith {
void solver::assert_bound(bool is_true, api_bound& b) {
TRACE("arith", tout << b << "\n";);
lp::constraint_index ci = b.get_constraint(is_true);
lp().activate(ci);
TRACE("arith", tout << b << " " << is_infeasible() << "\n";);
if (is_infeasible())
return;
lp::lconstraint_kind k = bound2constraint_kind(b.is_int(), b.get_bound_kind(), is_true);
@ -1065,6 +1065,7 @@ namespace arith {
TRACE("pcs", tout << lp().constraints(););
auto status = lp().find_feasible_solution();
TRACE("arith_verbose", display(tout););
TRACE("arith", tout << status << "\n");
switch (status) {
case lp::lp_status::INFEASIBLE:
return l_false;
@ -1201,7 +1202,7 @@ namespace arith {
TRACE("arith",
tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n";
for (literal c : m_core) tout << literal2expr(c) << "\n";
for (literal c : m_core) tout << c << ": " << literal2expr(c) << "\n";
for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";);
if (is_conflict) {

32
src/sat/smt/arith_solver.h
View file

@ -19,9 +19,7 @@ Author:
#include "util/obj_pair_set.h"
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.h"
#include "math/lp/lp_solver.h"
#include "math/lp/lp_primal_simplex.h"
#include "math/lp/lp_dual_simplex.h"
#include "math/lp/indexed_value.h"
#include "math/lp/lar_solver.h"
#include "math/lp/nla_solver.h"
@ -30,6 +28,8 @@ Author:
#include "math/polynomial/algebraic_numbers.h"
#include "math/polynomial/polynomial.h"
#include "sat/smt/sat_th.h"
#include "sat/smt/arith_sls.h"
#include "sat/sat_ddfw.h"
namespace euf {
class solver;
@ -78,12 +78,7 @@ namespace arith {
m_eq_tail++;
}
public:
void set_type(euf::solver& ctx, hint_type ty) {
ctx.push(value_trail<unsigned>(m_eq_tail));
ctx.push(value_trail<unsigned>(m_lit_tail));
m_ty = ty;
reset();
}
void set_type(euf::solver& ctx, hint_type ty);
void set_num_le(unsigned n) { m_num_le = n; }
void add_eq(euf::enode* a, euf::enode* b) { add(a, b, true); }
void add_diseq(euf::enode* a, euf::enode* b) { add(a, b, false); }
@ -96,15 +91,13 @@ namespace arith {
}
std::pair<rational, literal> const& lit(unsigned i) const { return m_literals[i]; }
std::tuple<enode*, enode*, bool> const& eq(unsigned i) const { return m_eqs[i]; }
arith_proof_hint* mk(euf::solver& s) {
return new (s.get_region()) arith_proof_hint(m_ty, m_num_le, m_lit_head, m_lit_tail, m_eq_head, m_eq_tail);
}
arith_proof_hint* mk(euf::solver& s);
};
class solver : public euf::th_euf_solver {
friend struct arith_proof_hint;
friend class sls;
struct scope {
unsigned m_bounds_lim;
@ -144,7 +137,7 @@ namespace arith {
};
int_hashtable<var_value_hash, var_value_eq> m_model_eqs;
bool m_new_eq { false };
bool m_new_eq = false;
// temporary values kept during internalization
@ -197,6 +190,8 @@ namespace arith {
coeffs().pop_back();
}
};
sls m_local_search;
typedef vector<std::pair<rational, lpvar>> var_coeffs;
vector<rational> m_columns;
@ -233,10 +228,10 @@ namespace arith {
unsigned m_asserted_qhead = 0;
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
unsigned m_assume_eq_head{ 0 };
unsigned m_assume_eq_head = 0;
lp::u_set m_tmp_var_set;
unsigned m_num_conflicts{ 0 };
unsigned m_num_conflicts = 0;
lp_api::stats m_stats;
svector<scope> m_scopes;
@ -515,6 +510,8 @@ namespace arith {
bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
bool has_unhandled() const override { return m_not_handled != nullptr; }
void set_bool_search(sat::ddfw* ddfw) override { m_local_search.set(ddfw); }
// bounds and equality propagation callbacks
lp::lar_solver& lp() { return *m_solver; }
lp::lar_solver const& lp() const { return *m_solver; }
@ -523,4 +520,7 @@ namespace arith {
void consume(rational const& v, lp::constraint_index j);
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational& bval) const;
};
}

50
src/sat/smt/euf_local_search.cpp Normal file
View file

@ -0,0 +1,50 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_local_search.cpp
Abstract:
Local search dispatch for SMT
Author:
Nikolaj Bjorner (nbjorner) 2023-02-07
--*/
#include "sat/sat_solver.h"
#include "sat/sat_ddfw.h"
#include "sat/smt/euf_solver.h"
namespace euf {
lbool solver::local_search(bool_vector& phase) {
scoped_limits scoped_rl(m.limit());
sat::ddfw bool_search;
bool_search.reinit(s(), phase);
bool_search.updt_params(s().params());
bool_search.set_seed(rand());
scoped_rl.push_child(&(bool_search.rlimit()));
for (auto* th : m_solvers)
th->set_bool_search(&bool_search);
bool_search.check(0, nullptr, nullptr);
auto const& mdl = bool_search.get_model();
for (unsigned i = 0; i < mdl.size(); ++i)
phase[i] = mdl[i] == l_true;
if (bool_search.unsat_set().empty()) {
enable_trace("arith");
enable_trace("sat");
enable_trace("euf");
TRACE("sat", s().display(tout));
}
return bool_search.unsat_set().empty() ? l_true : l_undef;
}
}

5
src/sat/smt/euf_model.cpp
View file

@ -67,7 +67,7 @@ namespace euf {
m_qmodel = mdl;
}
void solver::update_model(model_ref& mdl) {
void solver::update_model(model_ref& mdl, bool validate) {
TRACE("model", tout << "create model\n";);
if (m_qmodel) {
mdl = m_qmodel;
@ -87,7 +87,8 @@ namespace euf {
for (auto* mb : m_solvers)
mb->finalize_model(*mdl);
TRACE("model", tout << "created model " << *mdl << "\n";);
validate_model(*mdl);
if (validate)
validate_model(*mdl);
}
bool solver::include_func_interp(func_decl* f) {

6
src/sat/smt/euf_proof_checker.cpp
View file

@ -28,7 +28,7 @@ Author:
#include "sat/smt/bv_theory_checker.h"
#include "sat/smt/distinct_theory_checker.h"
#include "sat/smt/tseitin_theory_checker.h"
#include "params/solver_params.hpp"
namespace euf {
@ -388,8 +388,8 @@ namespace euf {
m_sat_solver.updt_params(m_params);
m_drat.updt_config();
m_rup = symbol("rup");
sat_params sp(m_params);
m_check_rup = sp.smt_proof_check_rup();
solver_params sp(m_params);
m_check_rup = sp.proof_check_rup();
}
void smt_proof_checker::ensure_solver() {

2
src/sat/smt/euf_proof_checker.h
View file

@ -35,7 +35,7 @@ namespace euf {
virtual bool check(app* jst) = 0;
virtual expr_ref_vector clause(app* jst) = 0;
virtual void register_plugins(theory_checker& pc) = 0;
virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { v.reset(); v.append(this->clause(jst)); return false; }
virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { v.append(this->clause(jst)); return false; }
};
class theory_checker {

23
src/sat/smt/euf_solver.cpp
View file

@ -349,6 +349,20 @@ namespace euf {
si.uncache(literal(v, true));
}
bool solver::decide(bool_var& var, lbool& phase) {
for (auto const& th : m_solvers)
if (th->decide(var, phase))
return true;
return false;
}
bool solver::get_case_split(bool_var& var, lbool& phase) {
for (auto const& th : m_solvers)
if (th->get_case_split(var, phase))
return true;
return false;
}
void solver::asserted(literal l) {
m_relevancy.asserted(l);
if (!m_relevancy.is_relevant(l))
@ -478,8 +492,13 @@ namespace euf {
m_ackerman->cg_conflict_eh(a, b);
switch (s().value(lit)) {
case l_true:
if (n->merge_tf() && !m.is_value(n->get_root()->get_expr()))
m_egraph.merge(n, ante, to_ptr(lit));
if (!n->merge_tf())
break;
if (m.is_value(n->get_root()->get_expr()))
break;
if (!ante)
ante = mk_true();
m_egraph.merge(n, ante, to_ptr(lit));
break;
case l_undef:
case l_false:

21
src/sat/smt/euf_solver.h
View file

@ -100,6 +100,14 @@ namespace euf {
scope(unsigned l) : m_var_lim(l) {}
};
struct local_search_config {
double cb = 0.0;
unsigned L = 20;
unsigned t = 45;
unsigned max_no_improve = 500000;
double sp = 0.0003;
};
size_t* to_ptr(sat::literal l) { return TAG(size_t*, reinterpret_cast<size_t*>((size_t)(l.index() << 4)), 1); }
size_t* to_ptr(size_t jst) { return TAG(size_t*, reinterpret_cast<size_t*>(jst), 2); }
@ -119,6 +127,7 @@ namespace euf {
sat::sat_internalizer& si;
relevancy m_relevancy;
smt_params m_config;
local_search_config m_ls_config;
euf::egraph m_egraph;
trail_stack m_trail;
stats m_stats;
@ -251,7 +260,7 @@ namespace euf {
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
constraint& lit_constraint(enode* n);
constraint& lit_constraint(enode* n);
// user propagator
void check_for_user_propagator() {
@ -339,6 +348,7 @@ namespace euf {
void add_assumptions(sat::literal_set& assumptions) override;
bool tracking_assumptions() override;
std::string reason_unknown() override { return m_reason_unknown; }
lbool local_search(bool_vector& phase) override;
void propagate(literal lit, ext_justification_idx idx);
bool propagate(enode* a, enode* b, ext_justification_idx idx);
@ -359,6 +369,8 @@ namespace euf {
void add_explain(size_t* p) { m_explain.push_back(p); }
void reset_explain() { m_explain.reset(); }
void set_eliminated(bool_var v) override;
bool decide(bool_var& var, lbool& phase) override;
bool get_case_split(bool_var& var, lbool& phase) override;
void asserted(literal l) override;
sat::check_result check() override;
void push() override;
@ -486,7 +498,7 @@ namespace euf {
// model construction
void save_model(model_ref& mdl);
void update_model(model_ref& mdl);
void update_model(model_ref& mdl, bool validate);
obj_map<expr, enode*> const& values2root();
void model_updated(model_ref& mdl);
expr* node2value(enode* n) const;
@ -531,6 +543,10 @@ namespace euf {
check_for_user_propagator();
m_user_propagator->register_created(ceh);
}
void user_propagate_register_decide(user_propagator::decide_eh_t& ceh) {
check_for_user_propagator();
m_user_propagator->register_decide(ceh);
}
void user_propagate_register_expr(expr* e) {
check_for_user_propagator();
m_user_propagator->add_expr(e);
@ -552,4 +568,3 @@ namespace euf {
inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) {
return s.display(out);
}

9
src/sat/smt/pb_internalize.cpp
View file

@ -41,6 +41,11 @@ namespace pb {
SASSERT(m_pb.is_pb(e));
app* t = to_app(e);
rational k = m_pb.get_k(t);
if (!root && is_app(e)) {
sat::literal lit = si.get_cached(to_app(e));
if (lit != sat::null_literal)
return sign ? ~lit : lit;
}
switch (t->get_decl_kind()) {
case OP_AT_MOST_K:
return convert_at_most_k(t, k, root, sign);
@ -119,7 +124,7 @@ namespace pb {
else {
bool_var v = s().add_var(true);
literal lit(v, sign);
add_pb_ge(v, sign, wlits, k.get_unsigned());
add_pb_ge(v, false, wlits, k.get_unsigned());
TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";);
return lit;
}
@ -146,7 +151,7 @@ namespace pb {
else {
sat::bool_var v = s().add_var(true);
sat::literal lit(v, sign);
add_pb_ge(v, sign, wlits, k.get_unsigned());
add_pb_ge(v, false, wlits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
return lit;
}

20
src/sat/smt/pb_solver.cpp
View file

@ -2039,7 +2039,7 @@ namespace pb {
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) simplify(*m_constraints[i]);
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) simplify(*m_learned[i]);
init_use_lists();
remove_unused_defs();
// remove_unused_defs();
set_non_external();
elim_pure();
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
@ -2528,8 +2528,13 @@ namespace pb {
}
void solver::remove_unused_defs() {
if (incremental_mode()) return;
if (incremental_mode())
return;
// remove constraints where indicator literal isn't used.
NOT_IMPLEMENTED_YET();
// TODO: #6675
// need to add this inequality to the model reconstruction
// stack in order to produce correct models.
for (constraint* cp : m_constraints) {
constraint& c = *cp;
literal lit = c.lit();
@ -2853,19 +2858,20 @@ namespace pb {
void solver::subsumes(pbc& p1, literal lit) {
for (constraint* c : m_cnstr_use_list[lit.index()]) {
if (c == &p1 || c->was_removed()) continue;
bool s = false;
if (c == &p1 || c->was_removed() || c->lit() != sat::null_literal)
continue;
bool sub = false;
switch (c->tag()) {
case pb::tag_t::card_t:
s = subsumes(p1, c->to_card());
sub = subsumes(p1, c->to_card());
break;
case pb::tag_t::pb_t:
s = subsumes(p1, c->to_pb());
sub = subsumes(p1, c->to_pb());
break;
default:
break;
}
if (s) {
if (sub) {
++m_stats.m_num_pb_subsumes;
set_non_learned(p1);
remove_constraint(*c, "subsumed");

5
src/sat/smt/q_mbi.cpp
View file

@ -357,8 +357,7 @@ namespace q {
return expr_ref(m);
}
else if (!(*p)(*m_model, vars, fmls)) {
TRACE("q", tout << "theory projection failed\n");
return expr_ref(m);
TRACE("q", tout << "theory projection failed - use value\n");
}
}
for (app* v : vars) {
@ -636,7 +635,7 @@ namespace q {
if (m_model)
return;
m_model = alloc(model, m);
ctx.update_model(m_model);
ctx.update_model(m_model, false);
}
void mbqi::init_solver() {

1
src/sat/smt/sat_internalizer.h
View file

@ -26,6 +26,7 @@ namespace sat {
virtual literal internalize(expr* e) = 0;
virtual bool_var to_bool_var(expr* e) = 0;
virtual bool_var add_bool_var(expr* e) = 0;
virtual literal get_cached(app* t) const = 0;
virtual bool is_cached(app* t, literal l) const = 0;
virtual void cache(app* t, literal l) = 0;
virtual void uncache(literal l) = 0;

12
src/sat/smt/sat_th.h
View file

@ -18,6 +18,7 @@ Author:
#include "util/top_sort.h"
#include "sat/smt/sat_smt.h"
#include "sat/sat_ddfw.h"
#include "ast/euf/euf_egraph.h"
#include "model/model.h"
#include "smt/params/smt_params.h"
@ -136,6 +137,17 @@ namespace euf {
sat::status status() const { return sat::status::th(false, get_id()); }
/**
* Local search interface
*/
virtual void set_bool_search(sat::ddfw* ddfw) {}
virtual void set_bounds_begin() {}
virtual void set_bounds_end(unsigned num_literals) {}
virtual void set_bounds(enode* n) {}
};
class th_proof_hint : public sat::proof_hint {

15
src/sat/smt/user_solver.cpp
View file

@ -21,7 +21,7 @@ Author:
namespace user_solver {
solver::solver(euf::solver& ctx) :
th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))
th_euf_solver(ctx, symbol(user_propagator::plugin::name()), ctx.get_manager().mk_family_id(user_propagator::plugin::name()))
{}
solver::~solver() {
@ -92,24 +92,24 @@ namespace user_solver {
euf::enode* original_enode = bool_var2enode(var);
if (!is_attached_to_var(original_enode))
if (!original_enode || !is_attached_to_var(original_enode))
return false;
unsigned new_bit = 0; // ignored; currently no bv-support
expr* e = bool_var2expr(var);
expr* e = original_enode->get_expr();
m_decide_eh(m_user_context, this, &e, &new_bit, &phase);
euf::enode* new_enode = ctx.get_enode(e);
if (original_enode == new_enode)
if (original_enode == new_enode || new_enode->bool_var() == sat::null_bool_var)
return false;
var = new_enode->bool_var();
return true;
}
bool solver::get_case_split(sat::bool_var& var, lbool &phase){
bool solver::get_case_split(sat::bool_var& var, lbool& phase){
if (!m_next_split_expr)
return false;
@ -123,9 +123,12 @@ namespace user_solver {
void solver::asserted(sat::literal lit) {
if (!m_fixed_eh)
return;
force_push();
auto* n = bool_var2enode(lit.var());
euf::theory_var v = n->get_th_var(get_id());
if (!m_id2justification.get(v, sat::literal_vector()).empty())
// the core merged variables. We already issued the respective fixed callback for an equated variable
return;
force_push();
sat::literal_vector lits;
lits.push_back(lit);
m_id2justification.setx(v, lits, sat::literal_vector());