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

fix #2127 fix #2128

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-09 08:23:22 -08:00
parent b17c946acb
commit d2d42f9810
5 changed files with 63 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/array_decl_plugin.cpp
View file

@ -571,6 +571,11 @@ func_decl * array_recognizers::get_as_array_func_decl(expr * n) const {
return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast());
}
func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const {
SASSERT(is_as_array(f));
return to_func_decl(f->get_parameter(0).get_ast());
}
array_util::array_util(ast_manager& m):
array_recognizers(m.mk_family_id("array")),
m_manager(m) {

2
src/ast/array_decl_plugin.h
View file

@ -149,7 +149,9 @@ public:
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
func_decl * get_as_array_func_decl(expr * n) const;
func_decl * get_as_array_func_decl(func_decl* f) const;
};
class array_util : public array_recognizers {

24
src/model/model_evaluator.cpp
View file

@ -40,6 +40,7 @@ Revision History:
struct evaluator_cfg : public default_rewriter_cfg {
ast_manager & m;
model_core & m_model;
params_ref m_params;
bool_rewriter m_b_rw;
arith_rewriter m_a_rw;
bv_rewriter m_bv_rw;
@ -59,6 +60,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
m(m),
m_model(md),
m_params(p),
m_b_rw(m),
// We must allow customers to set parameters for arithmetic rewriter/evaluator.
// In particular, the maximum degree of algebraic numbers that will be evaluated.
@ -200,6 +202,26 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_REWRITE1;
}
}
if (st == BR_FAILED && num == 0 && m_ar.is_as_array(f)) {
func_decl* g = nullptr;
VERIFY(m_ar.is_as_array(f, g));
expr* def = nullptr;
quantifier* q = nullptr;
proof* def_pr = nullptr;
if (get_macro(g, def, q, def_pr)) {
sort_ref_vector vars(m);
svector<symbol> var_names;
for (unsigned i = 0; i < g->get_arity(); ++i) {
var_names.push_back(symbol(i));
vars.push_back(g->get_domain(g->get_arity() - i - 1));
}
result = m.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), def);
model_evaluator ev(m_model, m_params);
result = ev(result);
return BR_DONE;
}
}
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
return st;
}
@ -222,7 +244,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);

3
src/sat/sat_simplifier.cpp
View file

@ -1032,7 +1032,7 @@ namespace sat {
}
void insert(literal l) {
VERIFY(process_var(l.var()));
SASSERT(process_var(l.var()));
m_queue.insert(l);
}
@ -1075,6 +1075,7 @@ namespace sat {
}
void insert_queue() {
m_queue.reset();
unsigned num_vars = s.s.num_vars();
for (bool_var v = 0; v < num_vars; v++) {
if (process_var(v)) {

34
src/smt/theory_seq.cpp
View file

@ -2873,9 +2873,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
ctx.get_assignment(i_lt_len_s) == l_true) {
len = m_autil.mk_int(1);
lits.append(2, _lits);
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
return true;
}
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
}
else if (is_pre(e, s, i)) {
expr_ref zero(m_autil.mk_int(0), m);
@ -2887,9 +2887,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
ctx.get_assignment(i_lt_len_s) == l_true) {
len = i;
lits.append(2, _lits);
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
return true;
}
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
}
else if (is_post(e, s, l)) {
expr_ref zero(m_autil.mk_int(0), m);
@ -2900,9 +2900,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
ctx.get_assignment(l_le_len_s) == l_true) {
len = l;
lits.append(2, _lits);
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
return true;
}
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
}
else if (is_skolem(m_tail, e)) {
// e = tail(s, l), len(s) > l => len(tail(s, l)) = len(s) - l - 1
@ -4942,6 +4942,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
*/
void theory_seq::add_at_axiom(expr* e) {
TRACE("seq", tout << "at-axiom: " << mk_pp(e, m) << "\n";);
expr* s = nullptr, *i = nullptr;
VERIFY(m_util.str.is_at(e, s, i));
expr_ref zero(m_autil.mk_int(0), m);
@ -5082,9 +5083,36 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";);
m_new_propagation = true;
++m_stats.m_add_axiom;
#if 0
static unsigned level = 0;
if (level == 0) {
level++;
disable_trace("seq");
kernel k(m, ctx.get_fparams());
expr_ref tmp(m);
for (literal lit: lits) {
ctx.literal2expr(~lit, tmp);
k.assert_expr(tmp);
}
lbool r = k.check();
enable_trace("seq");
if (r == l_true) {
k.display(std::cout); std::cout << "\n";
TRACE("seq", k.display(tout << "sat\n"); tout << "\n";);
}
level--;
}
#endif
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
#if 0
void theory_seq::dump_axiom(literal_vector const& lits) {
display_lemma_as_smt_problem(std::cout << "; lemma\n", lits.size(), lits.c_ptr());
}
#endif
expr_ref theory_seq::coalesce_chars(expr* const& e) {
context& ctx = get_context();
expr* s;