mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #3833

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 04:34:36 -07:00
parent bd59fceaec
commit dde0c9bd0d
7 changed files with 39 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast.h
View file

@ -1883,6 +1883,22 @@ public:
app * mk_app(func_decl * decl, unsigned num_args, expr * const * args);
app* mk_app(func_decl* decl, ref_vector<expr, ast_manager> const& args) {
return mk_app(decl, args.size(), args.c_ptr());
}
app* mk_app(func_decl* decl, ref_vector<app, ast_manager> const& args) {
return mk_app(decl, args.size(), (expr*const*)args.c_ptr());
}
app * mk_app(func_decl * decl, ptr_vector<expr> const& args) {
return mk_app(decl, args.size(), args.c_ptr());
}
app * mk_app(func_decl * decl, ptr_vector<app> const& args) {
return mk_app(decl, args.size(), (expr*const*)args.c_ptr());
}
app * mk_app(func_decl * decl, expr * const * args) {
return mk_app(decl, decl->get_arity(), args);
}

4
src/ast/expr_abstract.cpp
View file

@ -85,10 +85,10 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
unsigned new_base = base + q->get_num_decls();
for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i), result1);
result1 = expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i));
patterns.push_back(result1.get());
}
expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1);
result1 = expr_abstract(m, new_base, num_bound, bound, q->get_expr());
b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get());
m_pinned.push_back(b);
m_map.insert(curr, b);

2
src/ast/expr_abstract.h
View file

@ -34,6 +34,8 @@ public:
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
inline expr_ref expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n) { expr_ref r(m); expr_abstract(m, base, num_bound, bound, n, r); return r; }
inline expr_ref expr_abstract(expr_ref_vector const& bound, expr* n) { return expr_abstract(bound.m(), 0, bound.size(), bound.c_ptr(), n); }
inline expr_ref expr_abstract(app_ref_vector const& bound, expr* n) { return expr_abstract(bound.m(), 0, bound.size(), (expr*const*)bound.c_ptr(), n); }
expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);

2
src/muz/spacer/spacer_manager.cpp
View file

@ -94,7 +94,7 @@ void inductive_property::to_model(model_ref& md) const {
for (unsigned j = 0; j < sig.size(); ++j) {
sig_vars.push_back(m.mk_const(sig[sig.size() - j - 1]));
}
expr_ref q = expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop);
expr_ref q = expr_abstract(sig_vars, prop);
md->register_decl(ri.m_pred, q);
}
TRACE("spacer", tout << *md;);

27
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -67,8 +67,8 @@ namespace datalog {
void operator()(model_ref & old_model) override {
model_ref new_model = alloc(model, m);
for (unsigned i = 0; i < m_new_funcs.size(); ++i) {
func_decl* p = m_new_funcs[i].get();
func_decl* q = m_old_funcs[i].get();
func_decl* p = m_new_funcs.get(i);
func_decl* q = m_old_funcs.get(i);
expr_ref_vector const& sub = m_subst[i];
sort_ref_vector const& sorts = m_sorts[i];
bool_vector const& is_bound = m_bound[i];
@ -76,7 +76,6 @@ namespace datalog {
expr_ref body(m);
unsigned arity_q = q->get_arity();
SASSERT(0 < p->get_arity());
func_interp* g = alloc(func_interp, m, arity_q);
if (f) {
body = f->get_interp();
@ -88,11 +87,11 @@ namespace datalog {
for (unsigned i = 0; i < p->get_arity(); ++i) {
args.push_back(m.mk_var(i, p->get_domain(i)));
}
body = m.mk_app(p, args.size(), args.c_ptr());
body = m.mk_app(p, args);
}
// Create quantifier wrapper around body.
TRACE("dl", tout << mk_pp(body, m) << "\n";);
TRACE("dl", tout << body << "\n";);
// 1. replace variables by the compound terms from
// the original predicate.
expr_safe_replace rep(m);
@ -102,7 +101,7 @@ namespace datalog {
rep(body);
rep.reset();
TRACE("dl", tout << mk_pp(body, m) << "\n";);
TRACE("dl", tout << body << "\n";);
// 2. replace bound variables by constants.
expr_ref_vector consts(m), bound(m), _free(m);
svector<symbol> names;
@ -123,21 +122,21 @@ namespace datalog {
rep(body);
rep.reset();
TRACE("dl", tout << mk_pp(body, m) << "\n";);
TRACE("dl", tout << body << "\n";);
// 3. abstract and quantify those variables that should be bound.
expr_abstract(m, 0, bound.size(), bound.c_ptr(), body, body);
body = expr_abstract(bound, body);
body = m.mk_forall(names.size(), bound_sorts.c_ptr(), names.c_ptr(), body);
TRACE("dl", tout << mk_pp(body, m) << "\n";);
TRACE("dl", tout << body << "\n";);
// 4. replace remaining constants by variables.
for (unsigned i = 0; i < _free.size(); ++i) {
rep.insert(_free[i].get(), m.mk_var(i, m.get_sort(_free[i].get())));
unsigned j = 0;
for (expr* f : _free) {
rep.insert(f, m.mk_var(j++, m.get_sort(f)));
}
rep(body);
g->set_else(body);
TRACE("dl", tout << mk_pp(body, m) << "\n";);
new_model->register_decl(q, g);
new_model->register_decl(q, body);
TRACE("dl", tout << body << "\n";);
}
old_model = new_model;
}

11
src/qe/qe.cpp
View file

@ -2077,7 +2077,7 @@ namespace qe {
if (num_vars > 0) {
ptr_vector<sort> sorts;
vector<symbol> names;
ptr_vector<app> free_vars;
app_ref_vector free_vars(m);
for (unsigned i = 0; i < num_vars; ++i) {
contains_app contains_x(m, vars[i]);
if (contains_x(fml)) {
@ -2087,8 +2087,7 @@ namespace qe {
}
}
if (!free_vars.empty()) {
expr_ref tmp(m);
expr_abstract(m, 0, free_vars.size(), (expr*const*)free_vars.c_ptr(), fml, tmp);
expr_ref tmp = expr_abstract(free_vars, fml);
fml = m.mk_exists(free_vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1);
}
}
@ -2279,9 +2278,7 @@ namespace qe {
void expr_quant_elim::abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml) {
if (sz > 0) {
expr_ref tmp(m);
expr_abstract(m, 0, sz, bound, fml, tmp);
fml = tmp;
fml = expr_abstract(m, 0, sz, bound, fml);
}
}
@ -2620,7 +2617,7 @@ namespace qe {
}
var_shifter shift(m);
shift(result, vars.size(), result);
expr_abstract(m, 0, vars.size(), (expr*const*)vars.c_ptr(), result, result);
result = expr_abstract(vars, result);
TRACE("qe", tout << "abstracted" << mk_pp(result, m) << "\n";);
ptr_vector<sort> sorts;
svector<symbol> names;

2
src/tactic/goal.cpp
View file

@ -305,7 +305,7 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
}
}
else {
SASSERT(!m().proofs_enabled());
SASSERT(!proofs_enabled());
expr_ref fr(f, m());
quick_process(true, fr, d);
if (!m_inconsistent) {