mirror of
https://github.com/Z3Prover/z3
synced 2026-02-28 19:01:29 +00:00
working on pdr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
990b93c2fd
commit
bf0481c4d0
5 changed files with 236 additions and 193 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue