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

updated sat solver for cores

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-29 14:38:17 -07:00
parent 0e9511b597
commit 2b1af8fd50
9 changed files with 92 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/opt/inc_sat_solver.cpp
View file

@ -62,6 +62,7 @@ public:
proof_converter_ref pc;
model_converter_ref mc;
expr_dependency_ref core(m);
obj_map<expr, sat::literal> dep2asm;
if (!m_fmls.empty()) {
goal_ref g = alloc(goal, m);
@ -86,7 +87,7 @@ public:
}
g = result[0];
TRACE("opt", g->display(tout););
m_goal2sat(*g, m_params, m_solver, m_map);
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm);
}
lbool r = m_solver.check();

8
src/sat/sat_solver.cpp
View file

@ -699,7 +699,11 @@ namespace sat {
init_search();
init_assumptions(num_lits, lits);
propagate(false);
if (inconsistent()) return l_false;
if (inconsistent()) {
if (tracking_assumptions())
resolve_conflict();
return l_false;
}
cleanup();
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
m_restart_threshold = m_config.m_burst_search;
@ -867,6 +871,7 @@ namespace sat {
m_assumptions.push_back(l);
mk_clause(1, &l);
}
TRACE("sat", display(tout););
}
void solver::reinit_assumptions() {
@ -1564,7 +1569,6 @@ namespace sat {
literal l = m_trail[idx];
if (is_marked(l.var()))
break;
SASSERT(idx > 0);
idx--;
}

9
src/sat/tactic/atom2bool_var.cpp
View file

@ -90,8 +90,17 @@ struct collect_boolean_interface_proc {
template<typename T>
void operator()(T const & g) {
unsigned sz = g.size();
ptr_vector<expr> deps;
for (unsigned i = 0; i < sz; i++) {
process(g.form(i));
if (g.dep(i)) {
deps.reset();
m.linearize(g.dep(i), deps);
for (unsigned j = 0; j < deps.size(); ++j) {
quick_for_each_expr(proc, tvisited, deps[j]);
}
}
}
}

53
src/sat/tactic/goal2sat.cpp
View file

@ -35,6 +35,7 @@ Notes:
#include"for_each_expr.h"
#include"model_v2_pp.h"
#include"tactic.h"
#include"ast_pp.h"
struct goal2sat::imp {
struct frame {
@ -52,15 +53,19 @@ struct goal2sat::imp {
obj_hashtable<expr> m_interface_vars;
sat::solver & m_solver;
atom2bool_var & m_map;
dep2asm_map & m_dep2asm;
sat::bool_var m_true;
bool m_ite_extra;
unsigned long long m_max_memory;
volatile bool m_cancel;
expr_ref_vector m_trail;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map):
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm):
m(_m),
m_solver(s),
m_map(map) {
m_map(map),
m_dep2asm(dep2asm),
m_trail(m) {
updt_params(p);
m_cancel = false;
m_true = sat::null_bool_var;
@ -360,39 +365,55 @@ struct goal2sat::imp {
SASSERT(m_result_stack.empty());
}
void add_assumption(expr* d, expr* literal_d) {
void insert_dep(expr* dep, bool sign) {
expr_ref new_dep(m), fml(m);
if (is_uninterp_const(dep)) {
new_dep = dep;
}
else {
new_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
m_trail.push_back(new_dep);
m_interface_vars.insert(new_dep);
fml = m.mk_iff(new_dep, dep);
process(fml);
}
convert_atom(new_dep, false, false);
sat::literal lit = m_result_stack.back();
m_dep2asm.insert(dep, sign?(~lit):lit);
m_result_stack.pop_back();
}
void operator()(goal const & g) {
m_interface_vars.reset();
collect_boolean_interface(g, m_interface_vars);
unsigned size = g.size();
expr_ref f(m), d_new(m);
ptr_vector<expr> deps;
expr_ref_vector fmls(m);
for (unsigned idx = 0; idx < size; idx++) {
f = g.form(idx);
TRACE("sat", tout << "Formula: " << mk_pp(f, m) << "\n";);
// Add assumptions.
if (g.dep(idx)) {
expr_dependency * dep = g.dep(idx);
deps.reset();
m.linearize(dep, deps);
fmls.reset();
m.linearize(g.dep(idx), deps);
fmls.push_back(f);
for (unsigned i = 0; i < deps.size(); ++i) {
expr * d = deps[i];
expr * d1;
SASSERT(m.is_bool(d));
if (is_uninterp_const(d)) {
add_assumption(d, d);
}
else if (m.is_not(d, d1) && is_uninterp_const(d1)) {
add_assumption(d, d);
if (m.is_not(d, d1)) {
insert_dep(d1, true);
fmls.push_back(d1);
}
else {
// create fresh variable, map back to dependency.
add_assumption(d, d_new);
insert_dep(d, false);
fmls.push_back(m.mk_not(d));
}
}
f = m.mk_or(fmls.size(), fmls.c_ptr());
TRACE("sat", tout << mk_pp(f, m) << "\n";);
}
process(f);
}
@ -465,8 +486,8 @@ struct goal2sat::scoped_set_imp {
}
};
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m) {
imp proc(g.m(), p, t, m);
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm) {
imp proc(g.m(), p, t, m, dep2asm);
scoped_set_imp set(this, &proc);
proc(g);
}

4
src/sat/tactic/goal2sat.h
View file

@ -41,6 +41,8 @@ class goal2sat {
public:
goal2sat();
typedef obj_map<expr, sat::literal> dep2asm_map;
static void collect_param_descrs(param_descrs & r);
static bool has_unsupported_bool(goal const & s);
@ -55,7 +57,7 @@ public:
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
*/
void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m);
void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm);
void set_cancel(bool f);
};

37
src/sat/tactic/sat_tactic.cpp
View file

@ -52,7 +52,9 @@ class sat_tactic : public tactic {
g->elim_redundancies();
atom2bool_var map(m);
m_goal2sat(*g, m_params, m_solver, map);
obj_map<expr, sat::literal> dep2asm;
sat::literal_vector assumptions;
m_goal2sat(*g, m_params, m_solver, map, dep2asm);
TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
atom2bool_var::iterator it = map.begin();
atom2bool_var::iterator end = map.end();
@ -66,10 +68,21 @@ class sat_tactic : public tactic {
CASSERT("sat_solver", m_solver.check_invariant());
IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
TRACE("sat_dimacs", m_solver.display_dimacs(tout););
lbool r = m_solver.check();
dep2assumptions(dep2asm, assumptions);
lbool r = m_solver.check(assumptions.size(), assumptions.c_ptr());
if (r == l_false) {
g->assert_expr(m.mk_false(), 0, 0);
expr_dependency * lcore = 0;
if (produce_core) {
sat::literal_vector const& core = m_solver.get_core();
u_map<expr*> asm2dep;
mk_asm2dep(dep2asm, asm2dep);
for (unsigned i = 0; i < core.size(); ++i) {
sat::literal lit = core[i];
expr* dep = asm2dep.find(lit.index());
lcore = m.mk_join(lcore, m.mk_leaf(dep));
}
}
g->assert_expr(m.mk_false(), 0, lcore);
}
else if (r == l_true && !map.interpreted_atoms()) {
// register model
@ -115,6 +128,22 @@ class sat_tactic : public tactic {
m_sat2goal.set_cancel(f);
m_solver.set_cancel(f);
}
void dep2assumptions(obj_map<expr, sat::literal>& dep2asm,
sat::literal_vector& assumptions) {
obj_map<expr, sat::literal>::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
assumptions.push_back(it->m_value);
}
}
void mk_asm2dep(obj_map<expr, sat::literal>& dep2asm,
u_map<expr*>& lit2asm) {
obj_map<expr, sat::literal>::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
lit2asm.insert(it->m_value.index(), it->m_key);
}
}
};
struct scoped_set_imp {

1
src/shell/dimacs_frontend.cpp
View file

@ -155,7 +155,6 @@ unsigned read_dimacs(char const * file_name) {
g_solver = &solver2;
sat::literal_vector assumptions;
track_clauses(solver, solver2, assumptions, tracking_clauses);
solver2.display(std::cout);
r = g_solver->check(assumptions.size(), assumptions.c_ptr());
}
else {

1
src/tactic/probe.cpp
View file

@ -289,7 +289,6 @@ struct is_non_qfbv_predicate {
return;
if (is_uninterp_const(n))
return;
throw found();
}
};

4
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -105,7 +105,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
cond(mk_is_qfbv_probe(),
cond(mk_is_qfbv_eq_probe(),
and_then(mk_bv1_blaster_tactic(m),
using_params(smt, solver_p)),
using_params(sat, solver_p)),
and_then(mk_bit_blaster_tactic(m),
when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
and_then(using_params(and_then(mk_simplify_tactic(m),
@ -126,7 +126,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
tactic * new_sat = cond(mk_produce_proofs_probe(),
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
mk_sat_tactic(m));