mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into poly

Browse source
This commit is contained in:
Jakob Rath 2024-02-26 11:46:22 +01:00
commit 183e911a79
260 changed files with 4131 additions and 3248 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_cutset.cpp
View file

@ -273,7 +273,7 @@ namespace sat {
std::string cut::table2string(unsigned num_input, uint64_t table) {
std::ostringstream strm;
display_table(strm, num_input, table);
return strm.str();
return std::move(strm).str();
}

4
src/sat/sat_params.pyg
View file

@ -64,7 +64,7 @@ def_module_params('sat',
('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'),
('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'),
('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),
('ddfw.restart_base', UINT, 100000, 'number of flips used a starting point for hessitant restart backoff'),
('ddfw.restart_base', UINT, 100000, 'number of flips used a starting point for hesitant restart backoff'),
('ddfw.reinit_base', UINT, 10000, 'increment basis for geometric backoff scheme of re-initialization of weights'),
('ddfw.threads', UINT, 0, 'number of ddfw threads to run in parallel with sat solver'),
('prob_search', BOOL, False, 'use probsat local search instead of CDCL'),
@ -105,7 +105,7 @@ def_module_params('sat',
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
('lookahead_scores', BOOL, False, 'extract lookahead scores. A utility that can only be used from the DIMACS front-end'),
('lookahead.double', BOOL, True, 'enable doubld lookahead'),
('lookahead.double', BOOL, True, 'enable double lookahead'),
('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'),
('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),

2
src/sat/sat_solver.cpp
View file

@ -2280,7 +2280,7 @@ namespace sat {
<< std::setw(4) << m_stats.m_restart
<< mk_stat(*this)
<< " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
std::string str(strm.str());
std::string str = std::move(strm).str();
svector<size_t> nums;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;

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

@ -15,6 +15,8 @@ Author:
--*/
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include "ast/ast_util.h"
#include "ast/scoped_proof.h"
#include "sat/smt/euf_solver.h"
@ -43,8 +45,7 @@ namespace arith {
}
unsigned nv = get_num_vars();
for (unsigned v = 0; v < nv; ++v) {
auto t = get_tv(v);
auto vi = lp().external_to_column_index(v);
auto vi = lp().external_to_local(v);
out << "v" << v << " ";
if (is_bool(v)) {
euf::enode* n = var2enode(v);
@ -55,10 +56,10 @@ namespace arith {
}
}
else {
if (t.is_null())
if (vi == lp::null_lpvar)
out << "null";
else
out << (t.is_term() ? "t" : "j") << vi;
out << (lp().column_has_term(vi) ? "t" : "j") << vi;
if (m_nla && m_nla->use_nra_model() && is_registered_var(v)) {
scoped_anum an(m_nla->am());
m_nla->am().display(out << " = ", nl_value(v, an));
@ -242,4 +243,21 @@ namespace arith {
return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
}
bool solver::validate_conflict() {
scoped_ptr<::solver> vs = mk_smt2_solver(m, ctx.s().params(), symbol::null);
for (auto lit : m_core)
vs->assert_expr(ctx.literal2expr(lit));
for (auto [a, b] : m_eqs)
vs->assert_expr(m.mk_eq(a->get_expr(), b->get_expr()));
cancel_eh<reslimit> eh(m.limit());
scoped_timer timer(1000, &eh);
bool result = l_true != vs->check_sat();
CTRACE("arith", !result, vs->display(tout));
CTRACE("arith", !result, s().display(tout));
SASSERT(result);
return result;
}
}

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

@ -472,7 +472,7 @@ namespace arith {
bool _has_var = has_var(t);
mk_enode(t);
theory_var v = mk_evar(t);
if (!_has_var) {
svector<lpvar> vars;
for (expr* n : *t) {
@ -507,11 +507,11 @@ namespace arith {
}
else {
vi = lp().add_term(m_left_side, v);
SASSERT(lp::tv::is_term(vi));
SASSERT(lp().column_has_term(vi));
TRACE("arith_verbose",
tout << "v" << v << " := " << mk_pp(term, m)
<< " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";);
lp().print_term(lp().get_term(vi), tout) << "\n";);
}
}
return v;
@ -541,8 +541,6 @@ namespace arith {
rational const& r = m_columns[var];
if (!r.is_zero()) {
auto vi = register_theory_var_in_lar_solver(var);
if (lp::tv::is_term(vi))
vi = lp().map_term_index_to_column_index(vi);
m_left_side.push_back(std::make_pair(r, vi));
m_columns[var].reset();
}
@ -625,9 +623,6 @@ namespace arith {
return lp().external_to_local(v);
}
lp::tv solver::get_tv(theory_var v) const {
return lp::tv::raw(get_lpvar(v));
}
/**
\brief We must redefine this method, because theory of arithmetic contains

36
src/sat/smt/arith_sls.cpp
View file

@ -59,18 +59,10 @@ namespace arith {
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());
auto t2 = arg.j();
auto w = s.lp().local_to_external(t2);
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;
}
@ -81,12 +73,12 @@ namespace arith {
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())) {
lp::lpvar vj = s.lp().external_to_local(v);
SASSERT(vj != lp::null_lpvar);
if (!s.lp().is_base(vj)) {
rational new_value_(new_value, rational::i64());
lp::impq val(new_value_, rational::zero());
s.lp().set_value_for_nbasic_column(vj.index(), val);
s.lp().set_value_for_nbasic_column(vj, val);
}
}
@ -460,18 +452,18 @@ namespace arith {
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()) {
void sls::add_args(sat::bool_var bv, ineq& ineq, lp::lpvar t, theory_var v, int64_t sign) {
if (s.lp().column_has_term(t)) {
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());
auto t2 = arg.j();
auto w = s.lp().local_to_external(t2);
add_arg(bv, ineq, sign * to_numeral(arg.coeff()), w);
}
}
else
add_arg(bv, ineq, sign, s.lp().local_to_external(t.id()));
add_arg(bv, ineq, sign, s.lp().local_to_external(t));
}
void sls::init_bool_var(sat::bool_var bv) {
@ -480,7 +472,7 @@ namespace arith {
api_bound* b = nullptr;
s.m_bool_var2bound.find(bv, b);
if (b) {
auto t = b->tv();
auto t = b->column_index();
rational bound = b->get_value();
bool should_minus = false;
sls::ineq_kind op;
@ -503,8 +495,8 @@ namespace arith {
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);
lp::lpvar tu = s.get_column(u);
lp::lpvar tv = s.get_column(v);
auto& ineq = new_ineq(sls::ineq_kind::EQ, 0);
add_args(bv, ineq, tu, u, 1);
add_args(bv, ineq, tv, v, -1);

4
src/sat/smt/arith_sls.h
View file

@ -105,7 +105,7 @@ namespace arith {
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;
svector<std::pair<lp::lpvar, euf::theory_var>> m_terms;
bool m_dscore_mode = false;
@ -140,7 +140,7 @@ namespace arith {
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 add_args(sat::bool_var bv, ineq& ineq, lp::lpvar j, euf::theory_var v, int64_t sign);
void init_bool_var(sat::bool_var v);
void init_bool_var_assignment(sat::bool_var v);

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

@ -370,7 +370,7 @@ namespace arith {
void solver::refine_bound(theory_var v, const lp::implied_bound& be) {
lpvar vi = be.m_j;
if (lp::tv::is_term(vi))
if (lp().column_has_term(vi))
return;
expr_ref w(var2expr(v), m);
if (a.is_add(w) || a.is_numeral(w) || m.is_ite(w))
@ -418,7 +418,7 @@ namespace arith {
++m_stats.m_assert_upper;
inf_rational value = b.get_value(is_true);
if (propagate_eqs() && value.is_rational())
propagate_eqs(b.tv(), ci, k, b, value.get_rational());
propagate_eqs(b.column_index(), ci, k, b, value.get_rational());
#if 0
if (propagation_mode() != BP_NONE)
lp().add_column_rows_to_touched_rows(b.tv().id());
@ -426,30 +426,29 @@ namespace arith {
}
void solver::propagate_eqs(lp::tv t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) {
void solver::propagate_eqs(lp::lpvar t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) {
u_dependency* dep;
auto& dm = lp().dep_manager();
if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t.index(), dep, value)) {
if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t, dep, value)) {
fixed_var_eh(b.get_var(), dm.mk_join(dm.mk_leaf(ci1), dep), value);
}
else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t.index(), dep, value)) {
else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t, dep, value)) {
fixed_var_eh(b.get_var(), dm.mk_join(dm.mk_leaf(ci1), dep), value);
}
}
bool solver::set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower) {
if (tv.is_term()) {
lpvar ti = tv.id();
bool solver::set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower) {
if (lp().column_has_term(tv)) {
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
if (vec.size() <= ti) {
vec.resize(ti + 1, constraint_bound(UINT_MAX, rational()));
if (vec.size() <= tv) {
vec.resize(tv + 1, constraint_bound(UINT_MAX, rational()));
}
constraint_bound& b = vec[ti];
constraint_bound& b = vec[tv];
if (b.first == UINT_MAX || (is_lower ? b.second < v : b.second > v)) {
TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";);
m_history.push_back(vec[ti]);
ctx.push(history_trail<constraint_bound>(vec, ti, m_history));
TRACE("arith", tout << "tighter bound " << tv << "\n";);
m_history.push_back(vec[tv]);
ctx.push(history_trail<constraint_bound>(vec, tv, m_history));
b.first = ci;
b.second = v;
}
@ -461,10 +460,10 @@ namespace arith {
rational b;
u_dependency* dep = nullptr;
if (is_lower) {
return lp().has_lower_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v;
return lp().has_lower_bound(tv, dep, b, is_strict) && !is_strict && b == v;
}
else {
return lp().has_upper_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v;
return lp().has_upper_bound(tv, dep, b, is_strict) && !is_strict && b == v;
}
}
}
@ -772,7 +771,7 @@ namespace arith {
bool solver::has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
bool solver::has_bound(lpvar vi, u_dependency*& dep, rational const& bound, bool is_lower) {
if (lp::tv::is_term(vi)) {
if (lp().column_has_term(vi)) {
theory_var v = lp().local_to_external(vi);
rational val;
TRACE("arith", tout << lp().get_variable_name(vi) << " " << v << "\n";);
@ -782,9 +781,8 @@ namespace arith {
}
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
lpvar ti = lp::tv::unmask_term(vi);
if (vec.size() > ti) {
auto& [ci, coeff] = vec[ti];
if (vec.size() > vi) {
auto& [ci, coeff] = vec[vi];
if (ci == UINT_MAX)
return false;
dep = lp().dep_manager().mk_leaf(ci);
@ -876,11 +874,16 @@ namespace arith {
lp::impq solver::get_ivalue(theory_var v) const {
SASSERT(is_registered_var(v));
return m_solver->get_tv_ivalue(get_tv(v));
return m_solver->get_column_value(get_column(v));
}
lp::lpvar solver::get_column(theory_var v) const {
SASSERT(is_registered_var(v));
return m_solver->external_to_local(v);
}
rational solver::get_value(theory_var v) const {
return is_registered_var(v) ? m_solver->get_tv_value(get_tv(v)) : rational::zero();
return is_registered_var(v) ? m_solver->get_value(get_column(v)) : rational::zero();
}
void solver::random_update() {
@ -895,18 +898,18 @@ namespace arith {
if (is_bool(v))
continue;
ensure_column(v);
lp::column_index vj = lp().to_column_index(v);
SASSERT(!vj.is_null());
lp::lpvar vj = lp().external_to_local(v);
SASSERT(vj != lp::null_lpvar);
theory_var other = m_model_eqs.insert_if_not_there(v);
if (is_equal(v, other))
continue;
if (!lp().is_fixed(vj))
vars.push_back(vj.index());
if (!lp().column_is_fixed(vj))
vars.push_back(vj);
else if (!m_tmp_var_set.contains(other)) {
lp::column_index other_j = lp().to_column_index(other);
if (!lp().is_fixed(other_j)) {
lp::lpvar other_j = lp().external_to_local(other);
if (!lp().column_is_fixed(other_j)) {
m_tmp_var_set.insert(other);
vars.push_back(other_j.index());
vars.push_back(other_j);
}
}
}
@ -1068,14 +1071,14 @@ namespace arith {
nlsat::anum const& solver::nl_value(theory_var v, scoped_anum& r) const {
SASSERT(m_nla);
SASSERT(m_nla->use_nra_model());
auto t = get_tv(v);
if (!t.is_term()) {
m_nla->am().set(r, m_nla->am_value(t.id()));
auto t = get_column(v);
if (!lp().column_has_term(t)) {
m_nla->am().set(r, m_nla->am_value(t));
}
else {
m_todo_terms.push_back(std::make_pair(t, rational::one()));
TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";);
TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n";
TRACE("nl_value", tout << "v" << v << " " << t << "\n";);
TRACE("nl_value", tout << "v" << v << " := w" << t << "\n";
lp().print_term(lp().get_term(t), tout) << "\n";);
m_nla->am().set(r, 0);
@ -1090,14 +1093,14 @@ namespace arith {
m_nla->am().set(r1, c1.to_mpq());
m_nla->am().add(r, r1, r);
for (lp::lar_term::ival arg : term) {
auto wi = lp().column2tv(arg.column());
auto wi = arg.j();
c1 = arg.coeff() * wcoeff;
if (wi.is_term()) {
if (lp().column_has_term(wi)) {
m_todo_terms.push_back(std::make_pair(wi, c1));
}
else {
m_nla->am().set(r1, c1.to_mpq());
m_nla->am().mul(m_nla->am_value(wi.id()), r1, r1);
m_nla->am().mul(m_nla->am_value(wi), r1, r1);
m_nla->am().add(r1, r, r);
}
}
@ -1251,6 +1254,9 @@ namespace arith {
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 (ctx.get_config().m_arith_validate)
VERIFY(validate_conflict());
if (is_conflict) {
DEBUG_CODE(
for (literal c : m_core) VERIFY(s().value(c) == l_true);
@ -1390,17 +1396,17 @@ namespace arith {
TRACE("arith", lp().print_term(term, tout) << "\n";);
for (lp::lar_term::ival ti : term) {
theory_var w;
auto tv = lp().column2tv(ti.column());
if (tv.is_term()) {
auto tv = ti.j();
if (lp().column_has_term(tv)) {
lp::lar_term const& term1 = lp().get_term(tv);
rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2);
continue;
}
else {
w = lp().local_to_external(tv.id());
w = lp().local_to_external(tv);
SASSERT(w >= 0);
TRACE("arith", tout << (tv.id()) << ": " << w << "\n";);
TRACE("arith", tout << tv << ": " << w << "\n";);
}
rational c0(0);
coeffs.find(w, c0);
@ -1506,7 +1512,7 @@ namespace arith {
}
void solver::add_lemmas() {
if (m_nla->check_feasible()) {
if (m_nla->should_check_feasible()) {
auto is_sat = make_feasible();
if (l_false == is_sat) {
get_infeasibility_explanation_and_set_conflict();

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

@ -38,7 +38,7 @@ namespace euf {
namespace arith {
typedef ptr_vector<lp_api::bound<sat::literal>> lp_bounds;
typedef lp::var_index lpvar;
typedef lp::lpvar lpvar;
typedef euf::theory_var theory_var;
typedef euf::theory_id theory_id;
typedef euf::enode enode;
@ -245,7 +245,7 @@ namespace arith {
symbol m_farkas;
std_vector<lp::implied_bound> m_implied_bounds;
lp::lp_bound_propagator<solver> m_bp;
mutable vector<std::pair<lp::tv, rational>> m_todo_terms;
mutable vector<std::pair<lp::lpvar, rational>> m_todo_terms;
// lemmas
lp::explanation m_explanation;
@ -306,7 +306,7 @@ namespace arith {
bool reflect(expr* n) const;
lpvar get_lpvar(theory_var v) const;
lp::tv get_tv(theory_var v) const;
lp::lpvar get_column(theory_var v) const;
// axioms
void mk_div_axiom(expr* p, expr* q);
@ -348,7 +348,7 @@ namespace arith {
iterator end,
bool& found_compatible);
void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value);
void propagate_eqs(lp::lpvar t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value);
void propagate_basic_bounds(unsigned qhead);
void propagate_bounds_with_lp_solver();
void propagate_bound(literal lit, api_bound& b);
@ -362,9 +362,9 @@ namespace arith {
api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);
void fixed_var_eh(theory_var v1, u_dependency* dep, rational const& bound);
bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); }
bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); }
bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower);
bool set_upper_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); }
bool set_lower_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); }
bool set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower);
typedef std::pair<lp::constraint_index, rational> constraint_bound;
vector<constraint_bound> m_lower_terms;
@ -483,6 +483,7 @@ namespace arith {
arith_proof_hint const* explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
void explain_assumptions(lp::explanation const& e);
bool validate_conflict();
public:
solver(euf::solver& ctx, theory_id id);

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

@ -32,7 +32,7 @@ namespace array {
typedef sat::literal literal;
typedef sat::bool_var bool_var;
typedef sat::literal_vector literal_vector;
typedef union_find<solver, euf::solver> array_union_find;
typedef union_find<solver> array_union_find;
struct stats {

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

@ -191,8 +191,8 @@ namespace bv {
case OP_BAND: internalize_ac(mk_and); break;
case OP_BOR: internalize_ac(mk_or); break;
case OP_BXOR: internalize_ac(mk_xor); break;
case OP_BNAND: internalize_bin(mk_nand); break;
case OP_BNOR: internalize_bin(mk_nor); break;
case OP_BNAND: if_unary(mk_not); internalize_bin(mk_nand); break;
case OP_BNOR: if_unary(mk_not); internalize_bin(mk_nor); break;
case OP_BXNOR: if_unary(mk_not); internalize_bin(mk_xnor); break;
case OP_BCOMP: internalize_bin(mk_comp); break;
case OP_SIGN_EXT: internalize_pun(mk_sign_extend); break;

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

@ -49,7 +49,7 @@ namespace bv {
typedef std::pair<numeral, unsigned> value_sort_pair;
typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
typedef union_find<solver, euf::solver> bv_union_find;
typedef union_find<solver> bv_union_find;
typedef std::pair<theory_var, unsigned> var_pos;
friend class ackerman;

2
src/sat/smt/dt_solver.cpp
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Theory plugin for altegraic datatypes
Theory plugin for algebraic datatypes
Author:

4
src/sat/smt/dt_solver.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Theory plugin for altegraic datatypes
Theory plugin for algebraic datatypes
Author:
@ -36,7 +36,7 @@ namespace dt {
typedef sat::bool_var bool_var;
typedef sat::literal literal;
typedef sat::literal_vector literal_vector;
typedef union_find<solver, euf::solver> dt_union_find;
typedef union_find<solver> dt_union_find;
struct var_data {
ptr_vector<enode> m_recognizers; //!< recognizers of this equivalence class that are being watched.

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

@ -282,7 +282,7 @@ namespace euf {
}
void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
out << "Failed to validate b" << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
s().display(out);
euf::enode_vector nodes;
nodes.push_back(n);

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

@ -1113,7 +1113,7 @@ namespace euf {
if (b != sat::null_bool_var) {
r->m_bool_var2expr.setx(b, n->get_expr(), nullptr);
SASSERT(r->m.is_bool(n->get_sort()));
IF_VERBOSE(11, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n");
IF_VERBOSE(20, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n");
}
}
for (auto* s_orig : m_id2solver) {

2
src/sat/smt/intblast_solver.cpp
View file

@ -188,6 +188,7 @@ namespace intblast {
core.push_back(~lit);
return check_core(name, core, {});
}
lbool solver::check_propagation(char const* name, sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
sat::literal_vector core;
core.append(lits);
@ -300,7 +301,6 @@ namespace intblast {
return r;
}
lbool solver::check_solver_state() {
sat::literal_vector literals;

2
src/sat/smt/q_ematch.cpp
View file

@ -390,7 +390,7 @@ namespace q {
m_qs.log_instantiation(lits, &j);
euf::th_proof_hint* ph = nullptr;
if (ctx.use_drat())
ph = q_proof_hint::mk(ctx, j.m_generation, lits, j.m_clause.num_decls(), j.m_binding);
ph = q_proof_hint::mk(ctx, m_ematch, j.m_generation, lits, j.m_clause.num_decls(), j.m_binding);
m_qs.add_clause(lits, ph);
}

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

@ -90,6 +90,7 @@ namespace q {
unsigned_vector m_clause_queue;
euf::enode_pair_vector m_evidence;
bool m_enable_propagate = true;
symbol m_ematch = symbol("ematch");
euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding);
binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding);

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

@ -71,7 +71,7 @@ namespace q {
for (auto const& [qlit, fml, inst, generation] : m_instantiations) {
euf::solver::scoped_generation sg(ctx, generation + 1);
sat::literal lit = ~ctx.mk_literal(fml);
auto* ph = ctx.use_drat()? q_proof_hint::mk(ctx, generation, ~qlit, lit, inst.size(), inst.data()) : nullptr;
auto* ph = ctx.use_drat()? q_proof_hint::mk(ctx, m_mbqi, generation, ~qlit, lit, inst.size(), inst.data()) : nullptr;
m_qs.add_clause(~qlit, lit, ph);
m_qs.log_instantiation(~qlit, lit);
}

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

@ -72,6 +72,7 @@ namespace q {
unsigned m_max_choose_candidates = 10;
unsigned m_generation_bound = UINT_MAX;
unsigned m_generation_max = UINT_MAX;
symbol m_mbqi = symbol("mbqi");
typedef std::tuple<sat::literal, expr_ref, expr_ref_vector, unsigned> instantiation_t;
vector<instantiation_t> m_instantiations;
vector<mbp::def> m_defs;

10
src/sat/smt/q_solver.cpp
View file

@ -120,7 +120,6 @@ namespace q {
}
sat::literal solver::instantiate(quantifier* _q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var) {
sat::literal sk;
expr_ref tmp(m);
quantifier_ref q(_q, m);
expr_ref_vector vars(m);
@ -364,10 +363,10 @@ namespace q {
}
}
q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned generation, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) {
q_proof_hint* q_proof_hint::mk(euf::solver& s, symbol const& method, unsigned generation, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings) {
SASSERT(n > 0);
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, lits.size()));
q_proof_hint* ph = new (mem) q_proof_hint(generation, n, lits.size());
q_proof_hint* ph = new (mem) q_proof_hint(method, generation, n, lits.size());
for (unsigned i = 0; i < n; ++i)
ph->m_bindings[i] = bindings[i]->get_expr();
for (unsigned i = 0; i < lits.size(); ++i)
@ -375,10 +374,10 @@ namespace q {
return ph;
}
q_proof_hint* q_proof_hint::mk(euf::solver& s, unsigned generation, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) {
q_proof_hint* q_proof_hint::mk(euf::solver& s, symbol const& method, unsigned generation, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings) {
SASSERT(n > 0);
auto* mem = s.get_region().allocate(q_proof_hint::get_obj_size(n, 2));
q_proof_hint* ph = new (mem) q_proof_hint(generation, n, 2);
q_proof_hint* ph = new (mem) q_proof_hint(method, generation, n, 2);
for (unsigned i = 0; i < n; ++i)
ph->m_bindings[i] = bindings[i];
ph->m_literals[0] = l1;
@ -402,6 +401,7 @@ namespace q {
args.push_back(s.literal2expr(~m_literals[i]));
args.push_back(binding);
args.push_back(m.mk_app(symbol("gen"), 1, gens, range));
args.push_back(m.mk_const(m_method, range));
return m.mk_app(symbol("inst"), args.size(), args.data(), range);
}

8
src/sat/smt/q_solver.h
View file

@ -30,21 +30,23 @@ namespace euf {
namespace q {
struct q_proof_hint : public euf::th_proof_hint {
symbol m_method;
unsigned m_generation;
unsigned m_num_bindings;
unsigned m_num_literals;
sat::literal* m_literals;
expr* m_bindings[0];
q_proof_hint(unsigned g, unsigned b, unsigned l) {
q_proof_hint(symbol const& method, unsigned g, unsigned b, unsigned l) {
m_method = method;
m_generation = g;
m_num_bindings = b;
m_num_literals = l;
m_literals = reinterpret_cast<sat::literal*>(m_bindings + m_num_bindings);
}
static size_t get_obj_size(unsigned num_bindings, unsigned num_lits) { return sizeof(q_proof_hint) + num_bindings*sizeof(expr*) + num_lits*sizeof(sat::literal); }
static q_proof_hint* mk(euf::solver& s, unsigned generation, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings);
static q_proof_hint* mk(euf::solver& s, unsigned generation, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings);
static q_proof_hint* mk(euf::solver& s, symbol const& method, unsigned generation, sat::literal_vector const& lits, unsigned n, euf::enode* const* bindings);
static q_proof_hint* mk(euf::solver& s, symbol const& method, unsigned generation, sat::literal l1, sat::literal l2, unsigned n, expr* const* bindings);
expr* get_hint(euf::solver& s) const override;
};

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

@ -178,8 +178,10 @@ namespace user_solver {
void solver::propagate_consequence(prop_info const& prop) {
sat::literal lit = ctx.internalize(prop.m_conseq, false, false);
if (s().value(lit) != l_true) {
s().assign(lit, mk_justification(m_qhead));
auto j = mk_justification(m_qhead);
s().assign(lit, j);
++m_stats.m_num_propagations;
persist_clause(lit, j);
}
}
@ -188,9 +190,17 @@ namespace user_solver {
}
bool solver::unit_propagate() {
if (m_qhead == m_prop.size())
if (m_qhead == m_prop.size() && m_replay_qhead == m_clauses_to_replay.size())
return false;
force_push();
bool replayed = false;
if (m_replay_qhead < m_clauses_to_replay.size()) {
replayed = true;
ctx.push(value_trail<unsigned>(m_replay_qhead));
for (; m_replay_qhead < m_clauses_to_replay.size(); ++m_replay_qhead)
replay_clause(m_clauses_to_replay.get(m_replay_qhead));
}
ctx.push(value_trail<unsigned>(m_qhead));
unsigned np = m_stats.m_num_propagations;
for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) {
@ -200,7 +210,37 @@ namespace user_solver {
else
propagate_new_fixed(prop);
}
return np < m_stats.m_num_propagations;
return np < m_stats.m_num_propagations || replayed;
}
void solver::replay_clause(expr_ref_vector const& clause) {
sat::literal_vector lits;
for (expr* e : clause)
lits.push_back(ctx.mk_literal(e));
add_clause(lits);
}
void solver::persist_clause(sat::literal lit, sat::justification const& sj) {
if (!ctx.get_config().m_up_persist_clauses)
return;
expr_ref_vector clause(m);
auto idx = sj.get_ext_justification_idx();
auto& j = justification::from_index(idx);
auto const& prop = m_prop[j.m_propagation_index];
sat::literal_vector r;
for (unsigned id : prop.m_ids)
r.append(m_id2justification[id]);
for (auto lit : r)
clause.push_back(ctx.literal2expr(~lit));
for (auto const& [a,b] : prop.m_eqs)
clause.push_back(m.mk_not(m.mk_eq(a, b)));
clause.push_back(ctx.literal2expr(lit));
m_clauses_to_replay.push_back(clause);
if (m_replay_qhead + 1 < m_clauses_to_replay.size())
std::swap(m_clauses_to_replay[m_replay_qhead], m_clauses_to_replay[m_clauses_to_replay.size()-1]);
++m_replay_qhead;
}
void solver::collect_statistics(::statistics& st) const {

5
src/sat/smt/user_solver.h
View file

@ -77,6 +77,8 @@ namespace user_solver {
stats m_stats;
sat::bool_var m_next_split_var = sat::null_bool_var;
lbool m_next_split_phase = l_undef;
vector<expr_ref_vector> m_clauses_to_replay;
unsigned m_replay_qhead = 0;
struct justification {
unsigned m_propagation_index { 0 };
@ -105,6 +107,9 @@ namespace user_solver {
sat::bool_var enode_to_bool(euf::enode* n, unsigned idx);
void replay_clause(expr_ref_vector const& clause);
void persist_clause(sat::literal lit, sat::justification const& j);
public:
solver(euf::solver& ctx);