mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

working on model extraction

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-11 12:53:51 -08:00
parent 9373e1b7f5
commit 5622b13ed3
4 changed files with 47 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -302,7 +302,7 @@ namespace euf {
if (mval != sval) {
if (r->bool_var() != sat::null_bool_var)
out << "b" << r->bool_var() << " ";
out << bpp(r) << " :=\neval: " << sval << "\nmval: " << mval << "\n";
out << bpp(r) << " :=\nvalue obtained from model: " << sval << "\nvalue of the root expression: " << mval << "\n";
continue;
}
if (!m.is_bool(val))
@ -310,7 +310,7 @@ namespace euf {
auto bval = s().value(r->bool_var());
bool tt = l_true == bval;
if (tt != m.is_true(sval))
out << bpp(r) << " :=\neval: " << sval << "\nmval: " << bval << "\n";
out << bpp(r) << " :=\nvalue according to model: " << sval << "\nvalue of Boolean literal: " << bval << "\n";
}
for (euf::enode* r : nodes)
if (r)
@ -357,6 +357,7 @@ namespace euf {
if (!tt && !mdl.is_true(e))
continue;
CTRACE("euf", first, display_validation_failure(tout, mdl, n););
CTRACE("euf", first, display(tout));
IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
(void)first;
first = false;

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

@ -93,18 +93,17 @@ namespace intblast {
for (auto const& [src, vi] : m_vars) {
auto const& [v, b] = vi;
verbose_stream() << "asserting " << mk_pp(v, m) << " < " << b << "\n";
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
}
verbose_stream() << "check\n";
m_solver->display(verbose_stream());
verbose_stream() << es << "\n";
IF_VERBOSE(10, verbose_stream() << "check\n";
m_solver->display(verbose_stream());
verbose_stream() << es << "\n");
lbool r = m_solver->check_sat(es);
verbose_stream() << "result " << r << "\n";
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
if (r == l_false) {
expr_ref_vector core(m);
@ -112,8 +111,13 @@ namespace intblast {
obj_map<expr, unsigned> e2index;
for (unsigned i = 0; i < es.size(); ++i)
e2index.insert(es.get(i), i);
for (auto e : core)
m_core.push_back(literals[e2index[e]]);
for (auto e : core) {
unsigned idx = e2index[e];
if (idx < literals.size())
m_core.push_back(literals[idx]);
else
m_core.push_back(ctx.mk_literal(e));
}
}
return r;
@ -128,7 +132,7 @@ namespace intblast {
return any_of(subterms::all(expr_ref(e, m)), [&](auto* p) { return bv.is_bv_sort(p->get_sort()); });
}
void solver::sorted_subterms(expr_ref_vector const& es, ptr_vector<expr>& sorted) {
void solver::sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted) {
expr_fast_mark1 visited;
for (expr* e : es) {
sorted.push_back(e);
@ -144,6 +148,28 @@ namespace intblast {
sorted.push_back(arg);
}
}
//
// Add ground equalities to ensure the model is valid with respect to the current case splits.
// This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal
// assignment from complete level.
// E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment.
// If intblast is SAT, then force the model and literal assignment on the rest of the literals.
//
if (!is_ground(e))
continue;
euf::enode* n = ctx.get_enode(e);
if (!n)
continue;
if (n == n->get_root())
continue;
expr* r = n->get_root()->get_expr();
es.push_back(m.mk_eq(e, r));
r = es.back();
if (!visited.is_marked(r)) {
visited.mark(r);
sorted.push_back(r);
}
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
@ -163,6 +189,7 @@ namespace intblast {
expr_ref_vector args(m);
sorted_subterms(es, todo);
for (expr* e : todo) {
if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
@ -402,8 +429,8 @@ namespace intblast {
}
TRACE("bv",
for (unsigned i = 0; i < es.size(); ++i)
tout << mk_pp(es.get(i), m) << " -> " << mk_pp(translated[es.get(i)], m) << "\n";
for (expr* e : es)
tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated[e], m) << "\n";
);
for (unsigned i = 0; i < es.size(); ++i)

3
src/sat/smt/intblast_solver.h
View file

@ -53,7 +53,8 @@ namespace intblast {
bool is_bv(sat::literal lit);
void translate(expr_ref_vector& es);
void sorted_subterms(expr_ref_vector const& es, ptr_vector<expr>& sorted);
void add_root_equations(expr_ref_vector& es, ptr_vector<expr>& sorted);
void sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted);
public:
solver(euf::solver& ctx);

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

@ -347,13 +347,13 @@ namespace polysat {
unsigned sz2 = sz - arg_sz;
var2pdd(expr2enode(e)->get_th_var(get_id()));
if (arg_sz == sz)
add_clause(eq_internalize(e, arg), false);
add_clause(eq_internalize(e, arg), nullptr);
else {
sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz)));
// arg < 0 ==> e = concat(arg, 1...1)
// arg >= 0 ==> e = concat(arg, 0...0)
add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), false);
add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);
add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), nullptr);
add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr);
}
}
@ -364,10 +364,10 @@ namespace polysat {
unsigned sz2 = sz - arg_sz;
var2pdd(expr2enode(e)->get_th_var(get_id()));
if (arg_sz == sz)
add_clause(eq_internalize(e, arg), false);
add_clause(eq_internalize(e, arg), nullptr);
else
// e = concat(arg, 0...0)
add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);
add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr);
}
void solver::internalize_div_rem(app* e, bool is_div) {