3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

optimize model pruning

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-14 11:19:02 -07:00
commit bdad4e3bcb
5 changed files with 236 additions and 192 deletions

View file

@ -382,16 +382,15 @@ namespace pdr {
}
lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core) {
unsigned level = n.level();
expr* state = n.state();
TRACE("pdr",
tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n";
tout << mk_pp(n.state(), m) << "\n";);
ensure_level(n.level());
model_ref model;
ensure_level(level);
prop_solver::scoped_level _sl(m_solver, level);
TRACE("pdr", tout << "is-reachable: " << head()->get_name() << " level: " << level << "\n";
tout << mk_pp(state, m) << "\n";);
bool assumes_level;
lbool is_sat = m_solver.check_conjunction_as_assumptions(state, core, &model, assumes_level);
prop_solver::scoped_level _sl(m_solver, n.level());
m_solver.set_core(core);
m_solver.set_model(&model);
lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
if (is_sat == l_true && core) {
core->reset();
model2cube(*model, *core);
@ -411,7 +410,31 @@ namespace pdr {
}
tmp = pm.mk_and(conj);
prop_solver::scoped_level _sl(m_solver, level);
return m_solver.check_conjunction_as_assumptions(tmp, core, 0, assumes_level) == l_false;
m_solver.set_core(core);
lbool r = m_solver.check_conjunction_as_assumptions(tmp);
if (r == l_false) {
assumes_level = m_solver.assumes_level();
}
return r == l_false;
}
bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& lits, bool& assumes_level) {
manager& pm = get_pdr_manager();
expr_ref_vector conj(m), core(m);
expr_ref fml(m), states(m);
states = m.mk_not(pm.mk_and(lits));
mk_assumptions(head(), states, conj);
fml = pm.mk_and(conj);
prop_solver::scoped_level _sl(m_solver, level);
m_solver.set_core(&core);
m_solver.set_subset_based_core(true);
lbool res = m_solver.check_assumptions_and_formula(lits, fml);
if (res == l_false) {
lits.reset();
lits.append(core);
assumes_level = m_solver.assumes_level();
}
return res == l_false;
}
void pred_transformer::mk_assumptions(func_decl* head, expr* fml, expr_ref_vector& result) {
@ -425,7 +448,6 @@ namespace pdr {
for (unsigned i = 0; i < m_predicates.size(); i++) {
func_decl* d = m_predicates[i];
if (d == head) {
// tmp1 = (m_tag2rule.size() == 1)?fml:m.mk_implies(pred, fml);
tmp1 = m.mk_implies(pred, fml);
pm.formula_n2o(tmp1, tmp2, i);
result.push_back(tmp2);
@ -883,10 +905,21 @@ namespace pdr {
return result;
}
bool model_search::is_repeated(model_node& n) const {
model_node* p = n.parent();
while (p) {
if (p->state() == n.state()) {
return true;
}
p = p->parent();
}
return false;
}
void model_search::add_leaf(model_node& n) {
unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
++count;
if (count == 1) {
if (count == 1 || is_repeated(n)) {
set_leaf(n);
}
else {
@ -944,7 +977,6 @@ namespace pdr {
}
void model_search::erase_leaf(model_node& n) {
if (n.children().empty() && n.is_open()) {
std::deque<model_node*>::iterator
it = m_leaves.begin(),
@ -1619,7 +1651,7 @@ namespace pdr {
TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") << mk_pp(ncube, m) << "\n";);
n.pt().add_property(ncube, uses_level?n.level():infty_level);
CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1));
m_search.backtrack_level(uses_level && m_params.get_bool(":flexible-trace",false), n);
m_search.backtrack_level(uses_level && m_params.get_bool(":flexible-trace", false), n);
break;
}
case l_undef: {

View file

@ -139,6 +139,7 @@ namespace pdr {
lbool is_reachable(model_node& n, expr_ref_vector* core);
bool is_invariant(unsigned level, expr* co_state, bool inductive, bool& assumes_level, expr_ref_vector* core = 0);
bool check_inductive(unsigned level, expr_ref_vector& state, bool& assumes_level);
expr_ref get_formulas(unsigned level, bool add_axioms);
@ -235,6 +236,8 @@ namespace pdr {
model_node* next();
bool is_repeated(model_node& n) const;
void add_leaf(model_node& n); // add fresh node.
void set_leaf(model_node& n); // Set node as leaf, remove children.

View file

@ -99,31 +99,26 @@ namespace pdr {
}
ast_manager& m = core.get_manager();
TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; } "\n";);
unsigned num_failures = 0, i = 0, num_changes = 0;
unsigned num_failures = 0, i = 0, old_core_size = core.size();
ptr_vector<expr> processed;
while (i < core.size() && 1 < core.size() && (!m_failure_limit || num_failures <= m_failure_limit)) {
expr_ref lit(m), state(m);
expr_ref lit(m);
lit = core[i].get();
core[i] = m.mk_true();
state = m.mk_not(n.pt().get_pdr_manager().mk_and(core));
bool uses_level_tmp = false;
if (n.pt().is_invariant(n.level(), state, true, uses_level_tmp, 0)) {
core[i] = m.mk_true();
if (n.pt().check_inductive(n.level(), core, uses_level)) {
num_failures = 0;
core[i] = core.back();
core.pop_back();
TRACE("pdr", tout << "Remove: " << mk_pp(lit, m) << "\n";);
IF_VERBOSE(3, verbose_stream() << "remove: " << mk_pp(lit, m) << "\n";);
++num_changes;
uses_level = uses_level_tmp;
for (i = 0; i < core.size() && processed.contains(core[i].get()); ++i);
}
else {
IF_VERBOSE(3, verbose_stream() << "keep: " << mk_pp(lit, m) << "\n";);
core[i] = lit;
processed.push_back(lit);
++num_failures;
++i;
}
}
IF_VERBOSE(2, verbose_stream() << "changes: " << num_changes << " size: " << core.size() << "\n";);
TRACE("pdr", tout << "changes: " << num_changes << " index: " << i << " size: " << core.size() << "\n";);
IF_VERBOSE(2, verbose_stream() << "old size: " << old_core_size << " new size: " << core.size() << "\n";);
TRACE("pdr", tout << "old size: " << old_core_size << " new size: " << core.size() << "\n";);
}
//

View file

@ -28,6 +28,7 @@ Revision History:
#include "datatype_decl_plugin.h"
#include "pdr_farkas_learner.h"
#include "ast_smt2_pp.h"
#include "expr_replacer.h"
//
// Auxiliary structure to introduce propositional names for assumptions that are not
@ -42,36 +43,36 @@ namespace pdr {
ast_manager& m;
expr_ref_vector m_atoms;
expr_ref_vector m_assumptions;
obj_map<app,expr *> m_fresh2expr;
obj_map<expr, app*> m_expr2fresh;
obj_hashtable<expr> m_equivs;
unsigned m_num_fresh;
obj_map<app,expr *> m_proxies2expr;
obj_map<expr, app*> m_expr2proxies;
obj_hashtable<expr> m_implies;
unsigned m_num_proxies;
app * mk_fresh(expr* atom) {
app * mk_proxy(expr* literal) {
app* res;
SASSERT(!is_var(atom)); //it doesn't make sense to introduce names to variables
if (m_expr2fresh.find(atom, res)) {
SASSERT(!is_var(literal)); //it doesn't make sense to introduce names to variables
if (m_expr2proxies.find(literal, res)) {
return res;
}
SASSERT(s.m_fresh.size() >= m_num_fresh);
if (m_num_fresh == s.m_fresh.size()) {
SASSERT(s.m_proxies.size() >= m_num_proxies);
if (m_num_proxies == s.m_proxies.size()) {
std::stringstream name;
name << "pdr_proxy_" << s.m_fresh.size();
name << "pdr_proxy_" << s.m_proxies.size();
res = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort());
s.m_fresh.push_back(res);
s.m_proxies.push_back(res);
s.m_aux_symbols.insert(res->get_decl());
}
else {
res = s.m_fresh[m_num_fresh].get();
res = s.m_proxies[m_num_proxies].get();
}
++m_num_fresh;
m_expr2fresh.insert(atom, res);
m_fresh2expr.insert(res, atom);
expr_ref equiv(m.mk_or(atom, m.mk_not(res)), m);
s.m_ctx->assert_expr(equiv);
m_assumptions.push_back(equiv);
m_equivs.insert(equiv);
TRACE("pdr_verbose", tout << "name asserted " << mk_pp(equiv, m) << "\n";);
++m_num_proxies;
m_expr2proxies.insert(literal, res);
m_proxies2expr.insert(res, literal);
expr_ref implies(m.mk_or(m.mk_not(res), literal), m);
s.m_ctx->assert_expr(implies);
m_assumptions.push_back(implies);
m_implies.insert(implies);
TRACE("pdr_verbose", tout << "name asserted " << mk_pp(implies, m) << "\n";);
return res;
}
@ -84,7 +85,7 @@ namespace pdr {
m.is_not(lit, lit_core);
SASSERT(!m.is_true(lit));
if (!is_uninterp(lit_core) || to_app(lit_core)->get_num_args() != 0) {
conjs[i] = mk_fresh(lit);
conjs[i] = mk_proxy(lit);
}
}
m_assumptions.append(conjs);
@ -122,38 +123,64 @@ namespace pdr {
public:
safe_assumptions(prop_solver& s, expr_ref_vector const& assumptions):
s(s), m(s.m), m_atoms(assumptions), m_assumptions(m), m_num_fresh(0) {
s(s), m(s.m), m_atoms(assumptions), m_assumptions(m), m_num_proxies(0) {
mk_safe(m_atoms);
}
}
~safe_assumptions() {
}
expr_ref_vector const& atoms() const { return m_atoms; }
unsigned assumptions_size() const { return m_assumptions.size(); }
expr* assumptions(unsigned i) const { return m_assumptions[i]; }
~safe_assumptions() {
}
void undo_proxies(expr_ref_vector& es) {
expr_ref e(m);
expr* r;
for (unsigned i = 0; i < es.size(); ++i) {
e = es[i].get();
if (is_app(e) && m_proxies2expr.find(to_app(e), r)) {
es[i] = r;
}
}
}
void elim_proxies(expr_ref_vector& es) {
expr_substitution sub(m, false, m.proofs_enabled());
proof_ref pr(m);
if (m.proofs_enabled()) {
pr = m.mk_asserted(m.mk_true());
}
obj_map<app,expr*>::iterator it = m_proxies2expr.begin(), end = m_proxies2expr.end();
for (; it != end; ++it) {
sub.insert(it->m_key, m.mk_true(), pr);
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
rep->set_substitution(&sub);
replace_proxies(*rep, es);
}
private:
expr_ref_vector const& atoms() const { return m_atoms; }
unsigned assumptions_size() const { return m_assumptions.size(); }
expr* assumptions(unsigned i) const { return m_assumptions[i]; }
expr* undo_naming(expr* atom) {
if (m_equivs.contains(atom)) {
return m.mk_true();
}
SASSERT(is_app(atom)); //only apps can be used in safe cubes
m_fresh2expr.find(to_app(atom), atom);
return atom;
}
void undo_naming(expr_ref_vector& literals) {
for (unsigned i = 0; i < literals.size(); ++i) {
literals[i] = undo_naming(literals[i].get());
if (m.is_true(literals[i].get())) {
literals[i] = literals.back();
literals.pop_back();
--i;
}
}
}
void replace_proxies(expr_replacer& rep, expr_ref_vector& es) {
expr_ref e(m);
for (unsigned i = 0; i < es.size(); ++i) {
e = es[i].get();
if (m_implies.contains(e)) {
e = m.mk_true();
}
else {
rep(e);
}
es[i] = e;
if (m.is_true(e)) {
es[i] = es.back();
es.pop_back();
--i;
}
}
}
};
@ -166,7 +193,9 @@ namespace pdr {
m_ctx(pm.mk_fresh()),
m_pos_level_atoms(m),
m_neg_level_atoms(m),
m_fresh(m),
m_proxies(m),
m_core(0),
m_subset_based_core(false),
m_in_level(false)
{
m_ctx->assert_expr(m_pm.get_background());
@ -226,15 +255,11 @@ namespace pdr {
lbool prop_solver::check_safe_assumptions(
safe_assumptions& safe,
const expr_ref_vector& atoms,
expr_ref_vector* core,
model_ref * mdl,
bool& assumes_level)
const expr_ref_vector& atoms)
{
flet<bool> _model(m_fparams.m_model, mdl != 0);
flet<bool> _model(m_fparams.m_model, m_model != 0);
expr_ref_vector expr_atoms(m);
expr_atoms.append(atoms.size(), atoms.c_ptr());
assumes_level = false;
if (m_in_level) {
push_level_atoms(m_current_level, expr_atoms);
@ -246,120 +271,106 @@ namespace pdr {
tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n";
tout << result << "\n";);
if (result == l_true && mdl) {
m_ctx->get_model(*mdl);
TRACE("pdr_verbose", model_pp(tout, **mdl); );
if (result == l_true && m_model) {
m_ctx->get_model(*m_model);
TRACE("pdr_verbose", model_pp(tout, **m_model); );
}
unsigned core_size = m_ctx->get_unsat_core_size();
if (result == l_false && !core) {
if (result == l_false) {
unsigned core_size = m_ctx->get_unsat_core_size();
m_assumes_level = false;
for (unsigned i = 0; i < core_size; ++i) {
if (m_level_atoms_set.contains(m_ctx->get_unsat_core_expr(i))) {
assumes_level = true;
m_assumes_level = true;
break;
}
}
}
if (result == l_false && core && m.proofs_enabled()) {
proof_ref pr(m);
pr = m_ctx->get_proof();
IF_VERBOSE(21, verbose_stream() << mk_ismt2_pp(pr, m) << "\n";);
farkas_learner fl(m_fparams, m);
expr_ref_vector lemmas(m);
obj_hashtable<expr> bs;
for (unsigned i = 0; i < safe.assumptions_size(); ++i) {
bs.insert(safe.assumptions(i));
}
fl.get_lemmas(pr, bs, lemmas);
safe.undo_naming(lemmas);
fl.simplify_lemmas(lemmas);
IF_VERBOSE(2,
verbose_stream() << "Lemmas\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
});
core->reset();
core->append(lemmas);
return result;
if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) {
extract_theory_core(safe);
}
if (result == l_false && core) {
core->reset();
for (unsigned i = 0; i < core_size; ++i) {
expr * core_expr = m_ctx->get_unsat_core_expr(i);
SASSERT(is_app(core_expr));
if (m_level_atoms_set.contains(core_expr)) {
assumes_level = true;
continue;
}
if (m_ctx->is_aux_predicate(core_expr)) {
continue;
}
core->push_back(to_app(core_expr));
}
SASSERT(expr_atoms.size() >= core->size());
safe.undo_naming(*core);
TRACE("pdr",
tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n";
tout << "core_exprs: ";
for (unsigned i = 0; i < core_size; ++i) {
tout << mk_pp(m_ctx->get_unsat_core_expr(i), m) << " ";
}
tout << "\n";
tout << "core: " << mk_pp(m_pm.mk_and(*core), m) << "\n";
);
else if (result == l_false && m_core) {
extract_subset_core(safe);
SASSERT(expr_atoms.size() >= m_core->size());
}
m_core = 0;
m_model = 0;
m_subset_based_core = false;
return result;
}
lbool prop_solver::check_assumptions(
const expr_ref_vector & atoms,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level)
{
return check_assumptions_and_formula(atoms, m.mk_true(), core, mdl, assumes_level);
void prop_solver::extract_subset_core(safe_assumptions& safe) {
unsigned core_size = m_ctx->get_unsat_core_size();
m_core->reset();
for (unsigned i = 0; i < core_size; ++i) {
expr * core_expr = m_ctx->get_unsat_core_expr(i);
SASSERT(is_app(core_expr));
if (m_level_atoms_set.contains(core_expr)) {
continue;
}
if (m_ctx->is_aux_predicate(core_expr)) {
continue;
}
m_core->push_back(to_app(core_expr));
}
safe.undo_proxies(*m_core);
TRACE("pdr",
tout << "core_exprs: ";
for (unsigned i = 0; i < core_size; ++i) {
tout << mk_pp(m_ctx->get_unsat_core_expr(i), m) << " ";
}
tout << "\n";
tout << "core: " << mk_pp(m_pm.mk_and(*m_core), m) << "\n";
);
}
lbool prop_solver::check_conjunction_as_assumptions(
expr * conj,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level) {
void prop_solver::extract_theory_core(safe_assumptions& safe) {
proof_ref pr(m);
pr = m_ctx->get_proof();
IF_VERBOSE(21, verbose_stream() << mk_ismt2_pp(pr, m) << "\n";);
farkas_learner fl(m_fparams, m);
expr_ref_vector lemmas(m);
obj_hashtable<expr> bs;
for (unsigned i = 0; i < safe.assumptions_size(); ++i) {
bs.insert(safe.assumptions(i));
}
fl.get_lemmas(pr, bs, lemmas);
safe.elim_proxies(lemmas);
fl.simplify_lemmas(lemmas); // redundant
IF_VERBOSE(2,
verbose_stream() << "Lemmas\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
});
m_core->reset();
m_core->append(lemmas);
}
lbool prop_solver::check_assumptions(const expr_ref_vector & atoms)
{
return check_assumptions_and_formula(atoms, m.mk_true());
}
lbool prop_solver::check_conjunction_as_assumptions(expr * conj) {
expr_ref_vector asmp(m);
asmp.push_back(conj);
return check_assumptions(asmp, core, mdl, assumes_level);
return check_assumptions(asmp);
}
lbool prop_solver::check_assumptions_and_formula(
const expr_ref_vector & atoms,
expr * form,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level)
lbool prop_solver::check_assumptions_and_formula(const expr_ref_vector & atoms, expr * form)
{
pdr::smt_context::scoped _scoped(*m_ctx);
safe_assumptions safe(*this, atoms);
m_ctx->assert_expr(form);
CTRACE("pdr", !m.is_true(form), tout << "check with formula: " << mk_pp(form, m) << "\n";);
lbool res = check_safe_assumptions(safe, safe.atoms(), core, mdl, assumes_level);
if (res == l_false && core && m_try_minimize_core) {
unsigned sz = core->size();
bool assumes_level1 = false;
lbool res2 = check_safe_assumptions(safe, *core, core, mdl, assumes_level1);
if (res2 == l_false && sz > core->size()) {
assumes_level = assumes_level1;
IF_VERBOSE(1, verbose_stream() << "reduced core size from " << sz << " to " << core->size() << "\n";);
}
}
lbool res = check_safe_assumptions(safe, safe.atoms());
//
// we don't have to undo model naming, as from the model

View file

@ -33,6 +33,7 @@ Revision History:
namespace pdr {
class prop_solver {
private:
front_end_params& m_fparams;
ast_manager& m;
@ -44,7 +45,11 @@ namespace pdr {
app_ref_vector m_pos_level_atoms; // atoms used to identify level
app_ref_vector m_neg_level_atoms; //
obj_hashtable<expr> m_level_atoms_set;
app_ref_vector m_fresh; // predicates for assumptions
app_ref_vector m_proxies; // predicates for assumptions
expr_ref_vector* m_core;
model_ref* m_model;
bool m_subset_based_core;
bool m_assumes_level;
func_decl_set m_aux_symbols;
bool m_in_level;
unsigned m_current_level; // set when m_in_level
@ -55,13 +60,14 @@ namespace pdr {
void ensure_level(unsigned lvl);
class safe_assumptions;
void extract_theory_core(safe_assumptions& assumptions);
void extract_subset_core(safe_assumptions& assumptions);
lbool check_safe_assumptions(
safe_assumptions& assumptions,
expr_ref_vector const& atoms,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level);
expr_ref_vector const& atoms);
public:
@ -73,6 +79,11 @@ namespace pdr {
m_aux_symbols.contains(s) ||
m_ctx->is_aux_predicate(s);
}
void set_core(expr_ref_vector* core) { m_core = core; }
void set_model(model_ref* mdl) { m_model = mdl; }
void set_subset_based_core(bool f) { m_subset_based_core = f; }
bool assumes_level() const { return m_assumes_level; }
void add_level();
unsigned level_cnt() const;
@ -99,24 +110,16 @@ namespace pdr {
* If the conjunction of atoms is consistent with the solver state and o_model is non-zero,
* o_model will contain the "o" literals true in the assignment.
*/
lbool check_assumptions(
const expr_ref_vector & atoms,
expr_ref_vector * core, model_ref * mdl,
bool& assumes_level);
lbool check_assumptions(const expr_ref_vector & atoms);
lbool check_conjunction_as_assumptions(
expr * conj, expr_ref_vector * core,
model_ref * mdl, bool& assumes_level);
lbool check_conjunction_as_assumptions(expr * conj);
/**
* Like check_assumptions, except it also asserts an extra formula
*/
lbool check_assumptions_and_formula(
const expr_ref_vector & atoms,
expr * form,
expr_ref_vector * core,
model_ref * mdl,
bool& assumes_level);
expr * form);
void collect_statistics(statistics& st) const;