mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4d05a11144
commit
4fcc4d07ae
12 changed files with 139 additions and 49 deletions
|
|
@ -1573,12 +1573,14 @@ namespace z3 {
|
|||
else {
|
||||
r = Z3_mk_fpa_abs(a.ctx(), a);
|
||||
}
|
||||
a.check_error();
|
||||
return expr(a.ctx(), r);
|
||||
}
|
||||
inline expr sqrt(expr const & a, expr const& rm) {
|
||||
check_context(a, rm);
|
||||
assert(a.is_fpa());
|
||||
Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
|
||||
a.check_error();
|
||||
return expr(a.ctx(), r);
|
||||
}
|
||||
inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
|
||||
|
|
|
|||
|
|
@ -269,7 +269,8 @@ func_decl_info::func_decl_info(family_id family_id, decl_kind k, unsigned num_pa
|
|||
m_pairwise(false),
|
||||
m_injective(false),
|
||||
m_idempotent(false),
|
||||
m_skolem(false) {
|
||||
m_skolem(false),
|
||||
m_lambda(false) {
|
||||
}
|
||||
|
||||
bool func_decl_info::operator==(func_decl_info const & info) const {
|
||||
|
|
@ -281,20 +282,22 @@ bool func_decl_info::operator==(func_decl_info const & info) const {
|
|||
m_chainable == info.m_chainable &&
|
||||
m_pairwise == info.m_pairwise &&
|
||||
m_injective == info.m_injective &&
|
||||
m_skolem == info.m_skolem;
|
||||
m_skolem == info.m_skolem &&
|
||||
m_lambda == info.m_lambda;
|
||||
}
|
||||
|
||||
std::ostream & operator<<(std::ostream & out, func_decl_info const & info) {
|
||||
operator<<(out, static_cast<decl_info const&>(info));
|
||||
out << " :left-assoc " << info.is_left_associative();
|
||||
out << " :right-assoc " << info.is_right_associative();
|
||||
out << " :flat-associative " << info.is_flat_associative();
|
||||
out << " :commutative " << info.is_commutative();
|
||||
out << " :chainable " << info.is_chainable();
|
||||
out << " :pairwise " << info.is_pairwise();
|
||||
out << " :injective " << info.is_injective();
|
||||
out << " :idempotent " << info.is_idempotent();
|
||||
out << " :skolem " << info.is_skolem();
|
||||
if (info.is_left_associative()) out << " :left-assoc ";
|
||||
if (info.is_right_associative()) out << " :right-assoc ";
|
||||
if (info.is_flat_associative()) out << " :flat-associative ";
|
||||
if (info.is_commutative()) out << " :commutative ";
|
||||
if (info.is_chainable()) out << " :chainable ";
|
||||
if (info.is_pairwise()) out << " :pairwise ";
|
||||
if (info.is_injective()) out << " :injective ";
|
||||
if (info.is_idempotent()) out << " :idempotent ";
|
||||
if (info.is_skolem()) out << " :skolem ";
|
||||
if (info.is_lambda()) out << " :lambda ";
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
@ -1713,6 +1716,20 @@ bool ast_manager::are_distinct(expr* a, expr* b) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
void ast_manager::add_lambda_def(func_decl* f, quantifier* q) {
|
||||
m_lambda_defs.insert(f, q);
|
||||
f->get_info()->set_lambda(true);
|
||||
inc_ref(q);
|
||||
}
|
||||
|
||||
quantifier* ast_manager::is_lambda_def(func_decl* f) {
|
||||
if (f->get_info() && f->get_info()->is_lambda()) {
|
||||
return m_lambda_defs[f];
|
||||
}
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
|
||||
func_decl* ast_manager::get_rec_fun_decl(quantifier* q) const {
|
||||
SASSERT(is_rec_fun_def(q));
|
||||
return to_app(to_app(q->get_pattern(0))->get_arg(0))->get_decl();
|
||||
|
|
@ -1901,6 +1918,10 @@ void ast_manager::delete_node(ast * n) {
|
|||
func_decl* f = to_func_decl(n);
|
||||
if (f->m_info != nullptr && !m_debug_ref_count) {
|
||||
func_decl_info * info = f->get_info();
|
||||
if (info->is_lambda()) {
|
||||
push_dec_ref(m_lambda_defs[f]);
|
||||
m_lambda_defs.remove(f);
|
||||
}
|
||||
info->del_eh(*this);
|
||||
dealloc(info);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -398,6 +398,7 @@ struct func_decl_info : public decl_info {
|
|||
bool m_injective:1;
|
||||
bool m_idempotent:1;
|
||||
bool m_skolem:1;
|
||||
bool m_lambda:1;
|
||||
|
||||
func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr);
|
||||
~func_decl_info() {}
|
||||
|
|
@ -412,6 +413,7 @@ struct func_decl_info : public decl_info {
|
|||
bool is_injective() const { return m_injective; }
|
||||
bool is_idempotent() const { return m_idempotent; }
|
||||
bool is_skolem() const { return m_skolem; }
|
||||
bool is_lambda() const { return m_lambda; }
|
||||
|
||||
void set_associative(bool flag = true) { m_left_assoc = flag; m_right_assoc = flag; }
|
||||
void set_left_associative(bool flag = true) { m_left_assoc = flag; }
|
||||
|
|
@ -423,6 +425,7 @@ struct func_decl_info : public decl_info {
|
|||
void set_injective(bool flag = true) { m_injective = flag; }
|
||||
void set_idempotent(bool flag = true) { m_idempotent = flag; }
|
||||
void set_skolem(bool flag = true) { m_skolem = flag; }
|
||||
void set_lambda(bool flag = true) { m_lambda = flag; }
|
||||
|
||||
bool operator==(func_decl_info const & info) const;
|
||||
|
||||
|
|
@ -641,6 +644,7 @@ public:
|
|||
bool is_pairwise() const { return get_info() != nullptr && get_info()->is_pairwise(); }
|
||||
bool is_injective() const { return get_info() != nullptr && get_info()->is_injective(); }
|
||||
bool is_skolem() const { return get_info() != nullptr && get_info()->is_skolem(); }
|
||||
bool is_lambda() const { return get_info() != nullptr && get_info()->is_lambda(); }
|
||||
bool is_idempotent() const { return get_info() != nullptr && get_info()->is_idempotent(); }
|
||||
unsigned get_arity() const { return m_arity; }
|
||||
sort * get_domain(unsigned idx) const { SASSERT(idx < get_arity()); return m_domain[idx]; }
|
||||
|
|
@ -1522,6 +1526,7 @@ protected:
|
|||
family_id m_user_sort_family_id;
|
||||
family_id m_arith_family_id;
|
||||
ast_table m_ast_table;
|
||||
obj_map<func_decl, quantifier*> m_lambda_defs;
|
||||
id_gen m_expr_id_gen;
|
||||
id_gen m_decl_id_gen;
|
||||
sort * m_bool_sort;
|
||||
|
|
@ -1651,6 +1656,8 @@ public:
|
|||
|
||||
bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; }
|
||||
bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; }
|
||||
void add_lambda_def(func_decl* f, quantifier* q);
|
||||
quantifier* is_lambda_def(func_decl* f);
|
||||
func_decl* get_rec_fun_decl(quantifier* q) const;
|
||||
|
||||
symbol const& rec_fun_qid() const { return m_rec_fun; }
|
||||
|
|
|
|||
|
|
@ -122,9 +122,9 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe
|
|||
sort * range = m.get_sort(e);
|
||||
func_decl * new_skolem_decl = m.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.c_ptr(), range);
|
||||
app * n = m.mk_app(new_skolem_decl, new_args.size(), new_args.c_ptr());
|
||||
TRACE("mk_definition_bug", tout << "gen_name: " << mk_ismt2_pp(n, m) << "\n";
|
||||
for (unsigned i = 0; i < var_sorts.size(); i++) tout << mk_pp(var_sorts[i], m) << " ";
|
||||
tout << "\n";);
|
||||
if (is_lambda(e)) {
|
||||
m.add_lambda_def(new_skolem_decl, to_quantifier(e));
|
||||
}
|
||||
return n;
|
||||
}
|
||||
|
||||
|
|
@ -203,7 +203,7 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var
|
|||
// NB. The pattern is incomplete.
|
||||
// consider store(a, i, v) == \lambda j . if i = j then v else a[j]
|
||||
// the instantiation rules for store(a, i, v) are:
|
||||
// sotre(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
|
||||
// store(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
|
||||
// The first pattern is not included.
|
||||
// TBD use a model-based scheme for exracting instantiations instead of
|
||||
// using multi-patterns.
|
||||
|
|
|
|||
|
|
@ -27,7 +27,6 @@ Notes:
|
|||
#include "ast/act_cache.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
#include "ast/normal_forms/name_exprs.h"
|
||||
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
|
||||
/**
|
||||
|
|
@ -754,8 +753,7 @@ struct nnf::imp {
|
|||
if (fr.m_i == 0) {
|
||||
fr.m_i = 1;
|
||||
if (is_lambda(q)) {
|
||||
if (!visit(q->get_expr(), fr.m_pol, true))
|
||||
return false;
|
||||
// skip
|
||||
}
|
||||
else if (is_forall(q) == fr.m_pol) {
|
||||
if (!visit(q->get_expr(), fr.m_pol, true))
|
||||
|
|
@ -769,19 +767,9 @@ struct nnf::imp {
|
|||
}
|
||||
|
||||
if (is_lambda(q)) {
|
||||
expr * new_expr = m_result_stack.back();
|
||||
quantifier * new_q = m.update_quantifier(q, new_expr);
|
||||
proof * new_q_pr = nullptr;
|
||||
m_result_stack.push_back(q);
|
||||
if (proofs_enabled()) {
|
||||
// proof * new_expr_pr = m_result_pr_stack.back();
|
||||
new_q_pr = m.mk_rewrite(q, new_q); // TBD use new_expr_pr
|
||||
}
|
||||
|
||||
m_result_stack.pop_back();
|
||||
m_result_stack.push_back(new_q);
|
||||
if (proofs_enabled()) {
|
||||
m_result_pr_stack.pop_back();
|
||||
m_result_pr_stack.push_back(new_q_pr);
|
||||
m_result_pr_stack.push_back(nullptr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true;
|
||||
|
|
@ -949,7 +937,6 @@ void nnf::get_param_descrs(param_descrs & r) {
|
|||
imp::get_param_descrs(r);
|
||||
}
|
||||
|
||||
|
||||
void nnf::reset() {
|
||||
m_imp->reset();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -535,14 +535,14 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::internalize_lambda(quantifier * q) {
|
||||
UNREACHABLE();
|
||||
|
||||
#if 0
|
||||
UNREACHABLE();
|
||||
#else
|
||||
TRACE("internalize_quantifier", tout << mk_pp(q, m_manager) << "\n";);
|
||||
SASSERT(is_lambda(q));
|
||||
app_ref lam_name(m_manager.mk_fresh_const("lambda", m_manager.get_sort(q)), m_manager);
|
||||
enode * e = mk_enode(lam_name, true, false, false);
|
||||
expr_ref eq(m_manager), lam_app(m_manager);
|
||||
app_ref eq(m_manager), lam_app(m_manager);
|
||||
expr_ref_vector vars(m_manager);
|
||||
vars.push_back(lam_name);
|
||||
unsigned sz = q->get_num_decls();
|
||||
|
|
@ -553,9 +553,11 @@ namespace smt {
|
|||
lam_app = autil.mk_select(vars.size(), vars.c_ptr());
|
||||
eq = m_manager.mk_eq(lam_app, q->get_expr());
|
||||
quantifier_ref fa(m_manager);
|
||||
expr * patterns[1] = { m_manager.mk_pattern(lam_name) };
|
||||
expr * patterns[1] = { m_manager.mk_pattern(lam_app) };
|
||||
fa = m_manager.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m_manager.lambda_def_qid(), symbol::null, 1, patterns);
|
||||
internalize_quantifier(fa, true);
|
||||
if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name);
|
||||
m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
|
||||
#endif
|
||||
}
|
||||
|
||||
|
|
@ -938,7 +940,7 @@ namespace smt {
|
|||
e->mark_as_interpreted();
|
||||
TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
|
||||
TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);
|
||||
m_app2enode.setx(id, e, 0);
|
||||
m_app2enode.setx(id, e, nullptr);
|
||||
m_e_internalized_stack.push_back(n);
|
||||
m_trail_stack.push_back(&m_mk_enode_trail);
|
||||
m_enodes.push_back(e);
|
||||
|
|
|
|||
|
|
@ -272,9 +272,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
// traverse all enodes that are associated with fresh values...
|
||||
unsigned sz = roots.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
enode * r = roots[i];
|
||||
for (enode* r : roots) {
|
||||
model_value_proc * proc = root2proc[r];
|
||||
SASSERT(proc);
|
||||
if (!proc->is_fresh())
|
||||
|
|
@ -282,9 +280,7 @@ namespace smt {
|
|||
process_source(source(r), roots, root2proc, colors, already_traversed, todo, sorted_sources);
|
||||
}
|
||||
|
||||
sz = roots.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
enode * r = roots[i];
|
||||
for (enode * r : roots) {
|
||||
process_source(source(r), roots, root2proc, colors, already_traversed, todo, sorted_sources);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -230,6 +230,7 @@ namespace smt {
|
|||
m_stats.m_num_extensionality++;
|
||||
}
|
||||
|
||||
|
||||
bool theory_array::internalize_atom(app * atom, bool) {
|
||||
return internalize_term(atom);
|
||||
}
|
||||
|
|
@ -297,12 +298,11 @@ namespace smt {
|
|||
|
||||
void theory_array::new_eq_eh(theory_var v1, theory_var v2) {
|
||||
m_find.merge(v1, v2);
|
||||
#if 0
|
||||
if (is_lambda(get_enode(v1)->get_owner()) ||
|
||||
is_lambda(get_enode(v2)->get_owner())) {
|
||||
instantiate_extensionality(get_enode(v1), get_enode(v2));
|
||||
enode* n1 = get_enode(v1), *n2 = get_enode(v2);
|
||||
if (n1->get_owner()->get_decl()->is_lambda() ||
|
||||
n2->get_owner()->get_decl()->is_lambda()) {
|
||||
assert_congruent(n1, n2);
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
void theory_array::new_diseq_eh(theory_var v1, theory_var v2) {
|
||||
|
|
|
|||
|
|
@ -88,6 +88,7 @@ namespace smt {
|
|||
bool instantiate_axiom2b(enode * select, enode * store);
|
||||
void instantiate_axiom1(enode * store);
|
||||
void instantiate_extensionality(enode * a1, enode * a2);
|
||||
void instantiate_congruent(enode * a1, enode * a2);
|
||||
bool instantiate_axiom2b_for(theory_var v);
|
||||
|
||||
virtual final_check_status assert_delayed_axioms();
|
||||
|
|
|
|||
|
|
@ -300,6 +300,20 @@ namespace smt {
|
|||
m_extensionality_todo.push_back(std::make_pair(n1, n2));
|
||||
return true;
|
||||
}
|
||||
|
||||
void theory_array_base::assert_congruent(enode * a1, enode * a2) {
|
||||
TRACE("array", tout << "congruent: #" << a1->get_owner_id() << " #" << a2->get_owner_id() << "\n";);
|
||||
SASSERT(is_array_sort(a1));
|
||||
SASSERT(is_array_sort(a2));
|
||||
context & ctx = get_context();
|
||||
if (a1->get_owner_id() > a2->get_owner_id())
|
||||
std::swap(a1, a2);
|
||||
enode * nodes[2] = { a1, a2 };
|
||||
if (!ctx.add_fingerprint(this, 1, 2, nodes))
|
||||
return; // axiom was already instantiated
|
||||
m_congruent_todo.push_back(std::make_pair(a1, a2));
|
||||
}
|
||||
|
||||
|
||||
void theory_array_base::assert_extensionality_core(enode * n1, enode * n2) {
|
||||
app * e1 = n1->get_owner();
|
||||
|
|
@ -338,8 +352,59 @@ namespace smt {
|
|||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
/**
|
||||
\brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars)
|
||||
*/
|
||||
void theory_array_base::assert_congruent_core(enode * n1, enode * n2) {
|
||||
app * e1 = n1->get_owner();
|
||||
app * e2 = n2->get_owner();
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
sort* s = m.get_sort(e1);
|
||||
unsigned dimension = get_array_arity(s);
|
||||
literal n1_eq_n2 = mk_eq(e1, e2, true);
|
||||
ctx.mark_as_relevant(n1_eq_n2);
|
||||
expr_ref_vector args1(m), args2(m);
|
||||
expr_ref f1 = instantiate_lambda(e1);
|
||||
expr_ref f2 = instantiate_lambda(e2);
|
||||
args1.push_back(f1);
|
||||
args2.push_back(f2);
|
||||
svector<symbol> names;
|
||||
sort_ref_vector sorts(m);
|
||||
for (unsigned i = 0; i < dimension; i++) {
|
||||
sort * srt = get_array_domain(s, i);
|
||||
sorts.push_back(srt);
|
||||
names.push_back(symbol(i));
|
||||
expr * k = m.mk_var(dimension - i - 1, srt);
|
||||
args1.push_back(k);
|
||||
args2.push_back(k);
|
||||
}
|
||||
expr * sel1 = mk_select(dimension+1, args1.c_ptr());
|
||||
expr * sel2 = mk_select(dimension+1, args2.c_ptr());
|
||||
expr * eq = m.mk_eq(sel1, sel2);
|
||||
expr_ref q(m.mk_forall(dimension, sorts.c_ptr(), names.c_ptr(), eq), m);
|
||||
ctx.get_rewriter()(q);
|
||||
if (!ctx.b_internalized(q)) {
|
||||
ctx.internalize(q, true);
|
||||
}
|
||||
literal fa_eq = ctx.get_literal(q);
|
||||
ctx.mark_as_relevant(fa_eq);
|
||||
assert_axiom(~n1_eq_n2, fa_eq);
|
||||
}
|
||||
|
||||
expr_ref theory_array_base::instantiate_lambda(app* e) {
|
||||
ast_manager& m = get_manager();
|
||||
quantifier * q = m.is_lambda_def(e->get_decl());
|
||||
expr_ref f(e, m);
|
||||
if (q) {
|
||||
var_subst sub(m, false);
|
||||
f = sub(q, e->get_num_args(), e->get_args());
|
||||
}
|
||||
return f;
|
||||
}
|
||||
|
||||
bool theory_array_base::can_propagate() {
|
||||
return !m_axiom1_todo.empty() || !m_axiom2_todo.empty() || !m_extensionality_todo.empty();
|
||||
return !m_axiom1_todo.empty() || !m_axiom2_todo.empty() || !m_extensionality_todo.empty() || !m_congruent_todo.empty();
|
||||
}
|
||||
|
||||
void theory_array_base::propagate() {
|
||||
|
|
@ -352,7 +417,10 @@ namespace smt {
|
|||
m_axiom2_todo.reset();
|
||||
for (unsigned i = 0; i < m_extensionality_todo.size(); i++)
|
||||
assert_extensionality_core(m_extensionality_todo[i].first, m_extensionality_todo[i].second);
|
||||
for (unsigned i = 0; i < m_congruent_todo.size(); i++)
|
||||
assert_congruent_core(m_congruent_todo[i].first, m_congruent_todo[i].second);
|
||||
m_extensionality_todo.reset();
|
||||
m_congruent_todo.reset();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -522,6 +590,7 @@ namespace smt {
|
|||
m_axiom1_todo.reset();
|
||||
m_axiom2_todo.reset();
|
||||
m_extensionality_todo.reset();
|
||||
m_congruent_todo.reset();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -66,6 +66,7 @@ namespace smt {
|
|||
ptr_vector<enode> m_axiom1_todo;
|
||||
enode_pair_vector m_axiom2_todo;
|
||||
enode_pair_vector m_extensionality_todo;
|
||||
enode_pair_vector m_congruent_todo;
|
||||
scoped_ptr<theory_array_bapa> m_bapa;
|
||||
|
||||
void assert_axiom(unsigned num_lits, literal * lits);
|
||||
|
|
@ -79,6 +80,10 @@ namespace smt {
|
|||
void assert_extensionality_core(enode * a1, enode * a2);
|
||||
bool assert_extensionality(enode * a1, enode * a2);
|
||||
|
||||
expr_ref instantiate_lambda(app* e);
|
||||
void assert_congruent_core(enode * a1, enode * a2);
|
||||
void assert_congruent(enode * a1, enode * a2);
|
||||
|
||||
// --------------------------------------------------
|
||||
// Array sort -> extensionality skolems
|
||||
//
|
||||
|
|
|
|||
|
|
@ -3429,7 +3429,7 @@ public:
|
|||
}
|
||||
|
||||
app_ref mk_obj(theory_var v) {
|
||||
lp::var_index vi = m_theory_var2var_index[v];
|
||||
lp::var_index vi = get_var_index(v);
|
||||
bool is_int = a.is_int(get_enode(v)->get_owner());
|
||||
if (m_solver->is_term(vi)) {
|
||||
return mk_term(m_solver->get_term(vi), is_int);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue