3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

resurrecting assertion stack

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-01 12:37:24 -07:00
parent c9722a1313
commit 26ffee95fc
4 changed files with 477 additions and 2 deletions

View file

@ -114,6 +114,10 @@ public:
virtual unsigned get_num_steps() const {
return m_replacer.get_num_steps();
}
virtual void reset() {
m_replacer.reset();
}
};
expr_replacer * mk_default_expr_replacer(ast_manager & m) {
@ -149,6 +153,11 @@ public:
virtual unsigned get_num_steps() const {
return m_r.get_num_steps();
}
virtual void reset() {
m_r.reset();
}
};
expr_replacer * mk_expr_simp_replacer(ast_manager & m, params_ref const & p) {

View file

@ -43,8 +43,8 @@ public:
void reset_cancel() { set_cancel(false); }
virtual void set_cancel(bool f) = 0;
virtual unsigned get_num_steps() const { return 0; }
virtual void reset() = 0;
void apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t);
void apply_substitution(expr * s, expr * def, expr_ref & t);
};

View file

@ -0,0 +1,328 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
assertion_stack.cpp
Abstract:
Assertion stacks
Author:
Leonardo de Moura (leonardo) 2012-02-17
Revision History:
--*/
#include"assertion_stack.h"
#include"well_sorted.h"
#include"ast_smt2_pp.h"
#include"ref_util.h"
#include"expr_replacer.h"
assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled):
m_manager(m),
m_forbidden(m),
m_csubst(m, core_enabled) {
init(m.proofs_enabled(), models_enabled, core_enabled);
}
assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
m_manager(m),
m_forbidden(m),
m_csubst(m, core_enabled, proofs_enabled) {
init(proofs_enabled, models_enabled, core_enabled);
}
void assertion_stack::init(bool proofs_enabled, bool models_enabled, bool core_enabled) {
m_ref_count = 0;
m_models_enabled = models_enabled;
m_proofs_enabled = proofs_enabled;
m_core_enabled = core_enabled;
m_inconsistent = false;
m_form_qhead = 0;
}
assertion_stack::~assertion_stack() {
reset();
}
void assertion_stack::reset() {
m_inconsistent = false;
m_form_qhead = 0;
m_mc_qhead = 0;
dec_ref_collection_values(m_manager, m_forms);
dec_ref_collection_values(m_manager, m_proofs);
dec_ref_collection_values(m_manager, m_deps);
dec_ref_collection_values(m_manager, m_forbidden);
m_forbidden_set.reset();
dec_ref_collection_values(m_manager, m_mc);
m_mc_tag.reset();
m_csubst.reset();
m_scopes.reset();
}
void assertion_stack::expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) {
scoped_ptr<expr_replacer> r = mk_default_expr_replacer(m());
(*r)(f, new_f, new_pr, new_dep);
// new_pr is a proof for f == new_f
// new_dep are the dependencies for showing f == new_f
if (proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
}
if (unsat_core_enabled()) {
new_dep = m().mk_join(dep, new_dep);
}
}
void assertion_stack::push_back(expr * f, proof * pr, expr_dependency * d) {
if (m().is_true(f))
return;
if (m().is_false(f)) {
m_inconsistent = true;
}
else {
SASSERT(!m_inconsistent);
}
m().inc_ref(f);
m_forms.push_back(f);
if (proofs_enabled()) {
m().inc_ref(pr);
m_proofs.push_back(pr);
}
if (unsat_core_enabled()) {
m().inc_ref(d);
m_deps.push_back(d);
}
}
void assertion_stack::quick_process(bool save_first, expr * & f, expr_dependency * d) {
if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
if (!save_first) {
push_back(f, 0, d);
}
return;
}
typedef std::pair<expr *, bool> expr_pol;
sbuffer<expr_pol, 64> todo;
todo.push_back(expr_pol(f, true));
while (!todo.empty()) {
if (m_inconsistent)
return;
expr_pol p = todo.back();
expr * curr = p.first;
bool pol = p.second;
todo.pop_back();
if (pol && m().is_and(curr)) {
app * t = to_app(curr);
unsigned i = t->get_num_args();
while (i > 0) {
--i;
todo.push_back(expr_pol(t->get_arg(i), true));
}
}
else if (!pol && m().is_or(curr)) {
app * t = to_app(curr);
unsigned i = t->get_num_args();
while (i > 0) {
--i;
todo.push_back(expr_pol(t->get_arg(i), false));
}
}
else if (m().is_not(curr)) {
todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
}
else {
if (!pol)
curr = m().mk_not(curr);
if (save_first) {
f = curr;
save_first = false;
}
else {
push_back(curr, 0, d);
}
}
}
}
void assertion_stack::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
unsigned num = f->get_num_args();
for (unsigned i = 0; i < num; i++) {
if (m_inconsistent)
return;
slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr);
}
}
void assertion_stack::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
unsigned num = f->get_num_args();
for (unsigned i = 0; i < num; i++) {
if (m_inconsistent)
return;
expr * child = f->get_arg(i);
if (m().is_not(child)) {
expr * not_child = to_app(child)->get_arg(0);
slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
}
else {
expr_ref not_child(m());
not_child = m().mk_not(child);
slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
}
}
}
void assertion_stack::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
if (m().is_and(f))
process_and(save_first, to_app(f), pr, d, out_f, out_pr);
else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))
process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr);
else if (save_first) {
out_f = f;
out_pr = pr;
}
else {
push_back(f, pr, d);
}
}
void assertion_stack::slow_process(expr * f, proof * pr, expr_dependency * d) {
expr_ref out_f(m());
proof_ref out_pr(m());
slow_process(false, f, pr, d, out_f, out_pr);
}
void assertion_stack::assert_expr(expr * f, proof * pr, expr_dependency * d) {
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m());
expand(f, pr, d, new_f, new_pr, new_d);
if (proofs_enabled())
slow_process(f, pr, d);
else
quick_process(false, f, d);
}
#ifdef Z3DEBUG
// bool assertion_stack::is_expanded(expr * f) {
// }
#endif
void assertion_stack::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
SASSERT(i >= m_form_qhead);
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
if (proofs_enabled()) {
expr_ref out_f(m());
proof_ref out_pr(m());
slow_process(true, f, pr, d, out_f, out_pr);
if (!m_inconsistent) {
if (m().is_false(out_f)) {
push_back(out_f, out_pr, d);
}
else {
m().inc_ref(out_f);
m().dec_ref(m_forms[i]);
m_forms[i] = out_f;
m().inc_ref(out_pr);
m().dec_ref(m_proofs[i]);
m_proofs[i] = out_pr;
if (unsat_core_enabled()) {
m().inc_ref(d);
m().dec_ref(m_deps[i]);
m_deps[i] = d;
}
}
}
}
else {
quick_process(true, f, d);
if (!m_inconsistent) {
if (m().is_false(f)) {
push_back(f, 0, d);
}
else {
m().inc_ref(f);
m().dec_ref(m_forms[i]);
m_forms[i] = f;
if (unsat_core_enabled()) {
m().inc_ref(d);
m().dec_ref(m_deps[i]);
m_deps[i] = d;
}
}
}
}
}
void assertion_stack::expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
SASSERT(i >= m_form_qhead);
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m());
expand(f, pr, d, new_f, new_pr, new_d);
update(i, new_f, new_pr, new_d);
}
void assertion_stack::push() {
commit();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_forms_lim = m_forms.size();
s.m_forbidden_lim = m_forbidden.size();
s.m_mc_lim = m_mc.size();
s.m_inconsistent_old = m_inconsistent;
}
void assertion_stack::pop(unsigned num_scopes) {
}
void assertion_stack::commit() {
}
#define MC_TAG_EXTENSION 0
#define MC_TAG_FILTER 1
void assertion_stack::add_filter(func_decl * f) {
m().inc_ref(f);
m_mc.push_back(f);
m_mc_tag.push_back(MC_TAG_FILTER);
}
void assertion_stack::add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) {
}
void assertion_stack::convert(model_ref & m) {
}
void assertion_stack::display(std::ostream & out) const {
out << "(assertion-stack";
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
out << "\n ";
if (i == m_form_qhead)
out << "==>\n";
out << mk_ismt2_pp(form(i), m(), 2);
}
out << ")" << std::endl;
}
bool assertion_stack::is_well_sorted() const {
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
expr * t = form(i);
if (!::is_well_sorted(m(), t))
return false;
}
return true;
}

View file

@ -0,0 +1,138 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
assertion_stack.h
Abstract:
It should be viewed as the "goal" object for incremental solvers.
The main difference is the support of push/pop operations. Like a
goal, an assertion_stack contains expressions, their proofs (if
proof generation is enabled), and dependencies (if unsat core
generation is enabled).
The assertions on the stack are grouped by scope levels. Scoped
levels are created using push, and removed using pop.
Assertions may be "committed". Whenever a push is executed, all
"uncommitted" assertions are automatically committed.
Only uncommitted assertions can be simplified/reduced.
An assertion set has a limited model converter that only supports
definitions (for constant elimination) and filters (for fresh
symbols introduced by tactics).
Some tactics support assertion_stacks and can be applied to them.
However, a tactic can only access the assertions on the top level.
The assertion stack also informs the tactic which declarations
can't be eliminated since they occur in the already committed part.
Author:
Leonardo de Moura (leonardo) 2012-02-17
Revision History:
--*/
#ifndef _ASSERTION_STACK_H_
#define _ASSERTION_STACK_H_
#include"ast.h"
#include"model.h"
#include"expr_substitution.h"
class assertion_stack {
ast_manager & m_manager;
unsigned m_ref_count;
bool m_models_enabled; // model generation is enabled.
bool m_proofs_enabled; // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true
bool m_core_enabled; // unsat core extraction is enabled.
bool m_inconsistent;
ptr_vector<expr> m_forms;
ptr_vector<proof> m_proofs;
ptr_vector<expr_dependency> m_deps;
unsigned m_form_qhead; // position of first uncommitted assertion
unsigned m_mc_qhead;
// Set of declarations that can't be eliminated
obj_hashtable<func_decl> m_forbidden_set;
func_decl_ref_vector m_forbidden;
// Limited model converter support, it supports only extensions and filters.
// It should be viewed as combination of extension_model_converter and
// filter_model_converter for goals.
expr_substitution m_csubst; // substitution for eliminated constants
// Model converter is just two sequences: func_decl and tag.
// Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst.
// Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model.
ptr_vector<func_decl> m_mc;
char_vector m_mc_tag;
struct scope {
unsigned m_forms_lim;
unsigned m_forbidden_lim;
unsigned m_mc_lim;
bool m_inconsistent_old;
};
svector<scope> m_scopes;
void init(bool proofs_enabled, bool models_enabled, bool core_enabled);
void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep);
void push_back(expr * f, proof * pr, expr_dependency * d);
void quick_process(bool save_first, expr * & f, expr_dependency * d);
void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void slow_process(expr * f, proof * pr, expr_dependency * d);
public:
assertion_stack(ast_manager & m, bool models_enabled = true, bool core_enabled = true);
assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled);
~assertion_stack();
void reset();
void inc_ref() { ++m_ref_count; }
void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
ast_manager & m() const { return m_manager; }
bool models_enabled() const { return m_models_enabled; }
bool proofs_enabled() const { return m_proofs_enabled; }
bool unsat_core_enabled() const { return m_core_enabled; }
bool inconsistent() const { return m_inconsistent; }
unsigned size() const { return m_forms.size(); }
unsigned qhead() const { return m_form_qhead; }
expr * form(unsigned i) const { return m_forms[i]; }
proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m_proofs[i]) : 0; }
expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m_deps[i] : 0; }
void assert_expr(expr * f, proof * pr, expr_dependency * d);
void assert_expr(expr * f) {
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
}
void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
void expand_and_update(unsigned i, expr * f, proof * pr = 0, expr_dependency * d = 0);
void commit();
void push();
void pop(unsigned num_scopes);
unsigned scope_lvl() const { return m_scopes.size(); }
bool is_well_sorted() const;
bool is_forbidden(func_decl * f) const { return m_forbidden_set.contains(f); }
void add_filter(func_decl * f);
void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep);
void convert(model_ref & m);
void display(std::ostream & out) const;
};
#endif