mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fixing 2267

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-06 15:31:55 +02:00
parent 16af728fbe
commit 28ce701e17
15 changed files with 174 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_model.cpp
View file

@ -162,7 +162,9 @@ extern "C" {
model * _m = to_model_ref(m);
params_ref p;
ast_manager& mgr = mk_c(c)->m();
if (!_m->has_solver()) {
_m->set_solver(alloc(api::seq_expr_solver, mgr, p));
}
expr_ref result(mgr);
model::scoped_model_completion _scm(*_m, model_completion);
result = (*_m)(to_expr(t));

8
src/ast/ast.h
View file

@ -1846,6 +1846,14 @@ public:
return mk_func_decl(name, 2, d, range, assoc, comm, false);
}
bool is_considered_uninterpreted(func_decl* f) {
if (f->get_family_id() == null_family_id) {
return true;
}
decl_plugin* p = get_plugin(f->get_family_id());
return !p || p->is_considered_uninterpreted(f);
}
app * mk_app(func_decl * decl, unsigned num_args, expr * const * args);
app * mk_app(func_decl * decl, expr * const * args) {

1
src/ast/rewriter/seq_rewriter.h
View file

@ -167,6 +167,7 @@ public:
static void get_param_descrs(param_descrs & r) {}
void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
bool has_solver() { return m_re2aut.has_solver(); }
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);

5
src/math/interval/interval.h
View file

@ -234,6 +234,11 @@ public:
bool check_invariant(interval const & n) const;
/**
\brief b <- k
*/
void set(numeral const& k, interval & b);
/**
\brief b <- -a
*/

10
src/math/interval/interval_def.h
View file

@ -664,6 +664,16 @@ bool interval_manager<C>::check_invariant(interval const & n) const {
return true;
}
template<typename C>
void interval_manager<C>::set(numeral const& k, interval & b) {
set_lower_is_inf(b, false);
set_upper_is_inf(b, false);
m().set(lower(b), k);
m().set(upper(b), k);
set_lower_is_open(b, false);
set_upper_is_open(b, false);
}
template<typename C>
void interval_manager<C>::set(interval & t, interval const & s) {
if (&t == &const_cast<interval&>(s))

32
src/model/func_interp.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "ast/ast_smt2_pp.h"
#include "ast/ast_util.h"
#include "model/func_interp.h"
#include "ast/array_decl_plugin.h"
func_entry::func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result):
m_args_are_values(true),
@ -316,6 +317,37 @@ bool func_interp::is_identity() const {
return (sz.size() == m_entries.size() + 1);
}
expr_ref func_interp::get_array_interp(sort_ref_vector const& domain) const {
if (m_else == nullptr)
return expr_ref(m_manager);
if (!is_ground(m_else)) {
return expr_ref(m_manager);
}
array_util autil(m_manager);
sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_manager.get_sort(m_else)), m_manager);
expr_ref r(autil.mk_const_array(A, m_else), m_manager);
expr_ref_vector args(m_manager);
for (func_entry * curr : m_entries) {
expr * res = curr->get_result();
if (m_else == res) {
continue;
}
args.reset();
args.push_back(r);
for (unsigned i = 0; i < m_arity; i++) {
expr* arg = curr->get_arg(i);
if (!is_ground(arg)) {
return expr_ref(m_manager);
}
args.push_back(arg);
}
args.push_back(res);
r = autil.mk_store(args.size(), args.c_ptr());
}
return r;
}
expr * func_interp::get_interp_core() const {
if (m_else == nullptr)
return nullptr;

2
src/model/func_interp.h
View file

@ -112,6 +112,8 @@ public:
expr * get_interp() const;
expr_ref get_array_interp(sort_ref_vector const& domain) const;
func_interp * translate(ast_translation & translator) const;
private:

16
src/model/model.cpp
View file

@ -401,15 +401,25 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
continue;
}
fi = nullptr;
new_t = nullptr;
sort_ref_vector domain(m);
if (autil.is_as_array(a)) {
func_decl* f = autil.get_as_array_func_decl(a);
// only expand auxiliary definitions that occur once.
if (can_inline_def(ts, f)) {
fi = get_func_interp(f);
for (sort* s : *f) {
domain.push_back(s);
}
new_t = fi->get_array_interp(domain);
TRACE("model", tout << new_t << "\n";);
}
}
if (fi && fi->get_interp()) {
if (new_t) {
// noop
}
else if (fi && fi->get_interp()) {
f = autil.get_as_array_func_decl(a);
expr_ref_vector sargs(m);
sort_ref_vector vars(m);
@ -484,6 +494,10 @@ void model::set_solver(expr_solver* s) {
m_mev.set_solver(s);
}
bool model::has_solver() {
return m_mev.has_solver();
}
expr_ref_vector model::operator()(expr_ref_vector const& ts) {
expr_ref_vector rs(m);
for (expr* t : ts) rs.push_back((*this)(t));

1
src/model/model.h
View file

@ -95,6 +95,7 @@ public:
bool is_false(expr* t);
bool is_true(expr_ref_vector const& ts);
void reset_eval_cache();
bool has_solver();
void set_solver(expr_solver* solver);
class scoped_model_completion {

4
src/model/model_evaluator.cpp
View file

@ -695,3 +695,7 @@ bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_co
void model_evaluator::set_solver(expr_solver* solver) {
m_imp->m_cfg.m_seq_rw.set_solver(solver);
}
bool model_evaluator::has_solver() {
return m_imp->m_cfg.m_seq_rw.has_solver();
}

1
src/model/model_evaluator.h
View file

@ -57,6 +57,7 @@ public:
bool is_true(expr_ref_vector const& ts);
void set_solver(expr_solver* solver);
bool has_solver();
/**
* best effort evaluator of extensional array equality.

10
src/model/model_smt2_pp.cpp
View file

@ -194,11 +194,13 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
ptr_buffer<format> f_entry_conds;
ptr_buffer<func_decl> func_decls;
sort_fun_decls(m, md, func_decls);
for (unsigned i = 0; i < func_decls.size(); i++) {
func_decl * f = func_decls[i];
for (func_decl * f : func_decls) {
if (recfun_util.is_defined(f) && !recfun_util.is_generated(f)) {
continue;
}
if (!m.is_considered_uninterpreted(f)) {
continue;
}
func_interp * f_i = md.get_func_interp(f);
SASSERT(f->get_arity() == f_i->get_arity());
format_ref body(fm(m));
@ -216,8 +218,8 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
}
TRACE("model_smt2_pp", for (unsigned i = 0; i < var_names.size(); i++) tout << var_names[i] << "\n";);
f_var_names.reset();
for (unsigned i = 0; i < f->get_arity(); i++)
f_var_names.push_back(mk_string(m, var_names[i].bare_str()));
for (auto const& vn : var_names)
f_var_names.push_back(mk_string(m, vn.bare_str()));
f_arg_decls.reset();
for (unsigned i = 0; i < f->get_arity(); i++) {
format_ref f_domain(fm(m));

49
src/smt/theory_array_base.cpp
View file

@ -34,11 +34,7 @@ namespace smt {
void theory_array_base::found_unsupported_op(expr * n) {
if (!get_context().get_fparams().m_array_fake_support && !m_found_unsupported_op) {
//array_util autil(get_manager());
//func_decl* f = 0;
//if (autil.is_as_array(n, f) && f->is_skolem()) return;
TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_found_unsupported_op));
m_found_unsupported_op = true;
}
@ -266,10 +262,7 @@ namespace smt {
m_array_value.reset();
// populate m_array_value if the select(a, i) parent terms of r1
enode_vector::const_iterator it = r1->begin_parents();
enode_vector::const_iterator end = r1->end_parents();
for (; it != end; ++it) {
enode* parent = *it;
for (enode* parent : r1->get_const_parents()) {
if (parent->is_cgr() &&
ctx.is_relevant(parent) &&
is_select(parent->get_owner()) &&
@ -278,10 +271,7 @@ namespace smt {
}
}
// traverse select(a, i) parent terms of r2 trying to find a match.
it = r2->begin_parents();
end = r2->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
for (enode * parent : r2->get_const_parents()) {
enode * other;
if (parent->is_cgr() &&
ctx.is_relevant(parent) &&
@ -712,10 +702,7 @@ namespace smt {
for (theory_var v = 0; v < num_vars; ++v) {
enode * r = get_enode(v)->get_root();
if (is_representative(v) && get_context().is_relevant(r)) {
enode_vector::iterator it = r->begin_parents();
enode_vector::iterator end = r->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
for (enode * parent : r->get_const_parents()) {
if (parent->get_cg() == parent &&
get_context().is_relevant(parent) &&
is_select(parent) &&
@ -735,10 +722,7 @@ namespace smt {
if (!get_context().is_relevant(r)) {
return;
}
ptr_vector<enode>::const_iterator it = r->begin_parents();
ptr_vector<enode>::const_iterator end = r->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
for (enode * parent : r->get_const_parents()) {
if (get_context().is_relevant(parent) &&
is_store(parent) &&
parent->get_arg(0)->get_root() == r) {
@ -770,10 +754,7 @@ namespace smt {
void theory_array_base::propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo) {
select_set * sel_set = get_select_set(r);
select_set::iterator it2 = sel_set->begin();
select_set::iterator end2 = sel_set->end();
for (; it2 != end2; ++it2) {
enode * sel = *it2;
for (enode* sel : *sel_set) {
SASSERT(is_select(sel));
propagate_select_to_store_parents(r, sel, todo);
}
@ -781,10 +762,7 @@ namespace smt {
void theory_array_base::propagate_selects() {
enode_pair_vector todo;
enode_vector::const_iterator it = m_selects_domain.begin();
enode_vector::const_iterator end = m_selects_domain.end();
for (; it != end; ++it) {
enode * r = *it;
for (enode * r : m_selects_domain) {
propagate_selects_to_store_parents(r, todo);
}
for (unsigned qhead = 0; qhead < todo.size(); qhead++) {
@ -901,6 +879,10 @@ namespace smt {
}
};
bool theory_array_base::include_func_interp(func_decl* f) {
return is_decl_of(f, get_id(), OP_ARRAY_EXT);
}
model_value_proc * theory_array_base::mk_value(enode * n, model_generator & m) {
SASSERT(get_context().is_relevant(n));
theory_var v = n->get_th_var(get_id());
@ -948,10 +930,7 @@ namespace smt {
m_selects.find(n->get_root(), sel_set);
if (sel_set != nullptr) {
ptr_buffer<enode> args;
select_set::iterator it = sel_set->begin();
select_set::iterator end = sel_set->end();
for (; it != end; ++it) {
enode * select = *it;
for (enode * select : *sel_set) {
args.reset();
unsigned num = select->get_num_args();
for (unsigned j = 1; j < num; ++j)
@ -963,10 +942,8 @@ namespace smt {
TRACE("array",
tout << mk_pp(n->get_root()->get_owner(), get_manager()) << "\n";
if (sel_set) {
select_set::iterator it = sel_set->begin();
select_set::iterator end = sel_set->end();
for (; it != end; ++it) {
tout << "#" << (*it)->get_root()->get_owner()->get_id() << " " << mk_pp((*it)->get_owner(), get_manager()) << "\n";
for (enode* s : *sel_set) {
tout << "#" << s->get_root()->get_owner()->get_id() << " " << mk_pp(s->get_owner(), get_manager()) << "\n";
}
}
if (else_val_n) {

2
src/smt/theory_array_base.h
View file

@ -194,7 +194,7 @@ namespace smt {
select_set * get_select_set(enode * n);
void finalize_model(model_generator & m) override;
model_value_proc * mk_value(enode * n, model_generator & m) override;
bool include_func_interp(func_decl* f) override;
public:
theory_array_base(ast_manager & m);
~theory_array_base() override { restore_sorts(0); }

73
src/smt/theory_seq.cpp
View file

@ -13,7 +13,76 @@ Author:
Nikolaj Bjorner (nbjorner) 2015-6-12
Revision History:
Outline:
A cascading sequence of solvers:
- simplify_and_solve_eqs
- canonize equality
- solve_unit_eq: x = t, where x not in t.
- solve_binary_eq: xa = bx -> a = b, xa = bx
- solve_nth_eq: x = unit(nth(x,0)).unit(nth(x,1)).unit(nth(x,2)...unit(nth(x,n-1))
- solve_itos: itos(i) = "" -> i < 0
- check_contains
- (f,dep) = canonize(contains(a, b))
lit := |b| > |a|
f := true -> conflict
f := false -> solved
value(lit) = l_true -> solved
f := s = t -> dep -> s != t
f := f1 & f2 -> dep -> ~f1 | ~f2
f := f1 | f2 -> dep -> ~f1 & ~f2
- solve_nqs
- s_i = t_i, d_i <- solve(s = t)
- create literals for s_i = t_i
- if one of created literals is false, done.
- conflict if all created literals are true
- fixed_length
- len(s) = k -> s = unit(nth(0,s)).unit(nth(1,s))....unit(nth(n-1,s))
- len_based_split
s = x.xs t = y.ys, len(x) = len(y) -> x = y & xs = ys
s = x.xs t = y.ys, len(x) = len(y) + offset -> y = x*Z, Z*xs = ys
s = x.x'.xs, t = y.y'.ys, len(xs) = len(ys) -> xs = ys
- check_int_string
e := itos(n), len(e) = v, v > 0 ->
n := stoi(e), len(e) = v, v > 0 ->
- n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
- n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
- n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
- 10^k <= n < 10^{k+1}-1 => len(e) => k
- reduce_length_eq
x1...xn = y1...ym, len(x1...xk) = len(y1...yj) -> x1...xk = y1..yj, x{k+1}..xn = y{j+1}..ym
- branch_unit_variable
len(x) = n -> x = unit(a1)unit(a2)...unit(a_n)
- branch_binary_variable
x ++ units1 = units2 ++ y -> x is prefix of units2 or x = units2 ++ y1, y = y1 ++ y2, y2 = units2
- branch_variable
- branch_variable_mb
s = xs, t = ys, each x_i, y_j has a length.
based on length comparisons decompose into smaller equalities.
- branch_variable_eq
cycle through branch options
- branch_ternary_variable1
- branch_ternary_variable2
- check_length_coherence
len(e) >= lo => e = unit(nth(0,e)).unit(nth(1,e))....unit(nth(lo-1,e)).seq
len(e) <= lo => seq = empty
len(e) <= hi => len(seq) <= hi - lo
- check_extensionality
--*/
@ -454,8 +523,6 @@ bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
if (ls.empty() || !is_var(ls[0])) {
return false;
}
//std::function<bool(expr*)> is_unit = [&](expr* elem) { return m_util.str.is_unit(elem); }
//return rs.forall(is_unit);
for (auto const& elem : rs) {
if (!m_util.str.is_unit(elem)) {