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

register auxiliary constants from projection operation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-20 08:51:24 -07:00
parent 112fa16bc0
commit 276fdd0e97
8 changed files with 68 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_rewriter.cpp
View file

@ -864,11 +864,11 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
expr_ref_vector as(m()), bs(m());
if (a1 != b1 && isc1 && isc2) {
TRACE("seq", tout << s1 << " " << s2 << "\n";);
if (s1.length() <= s2.length()) {
if (s1.prefixof(s2)) {
if (a == a1) {
result = m().mk_true();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
m_util.str.get_concat(a, as);
@ -878,10 +878,12 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
bs[0] = m_util.str.mk_string(s2);
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1),
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_REWRITE_FULL;
}
else {
result = m().mk_false();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
}
@ -889,6 +891,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
if (s2.prefixof(s1)) {
if (b == b1) {
result = m().mk_false();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
m_util.str.get_concat(a, as);
@ -898,10 +901,12 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
as[0] = m_util.str.mk_string(s1);
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()),
m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1));
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_REWRITE_FULL;
}
else {
result = m().mk_false();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
}
@ -930,9 +935,6 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
if (i == as.size()) {
result = mk_and(eqs);
TRACE("seq", tout << result << "\n";);
if (m().is_true(result)) {
return BR_DONE;
}
return BR_REWRITE3;
}
SASSERT(i < as.size());

2
src/model/model_core.cpp
View file

@ -94,7 +94,7 @@ void model_core::unregister_decl(func_decl * d) {
m_manager.dec_ref(ec->get_data().m_value);
m_interp.remove(d);
m_const_decls.erase(d);
return;
return;
}
decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);

56
src/smt/proto_model/proto_model.cpp
View file

@ -42,6 +42,11 @@ proto_model::proto_model(ast_manager & m, params_ref const & p):
void proto_model::register_aux_decl(func_decl * d, func_interp * fi) {
model_core::register_decl(d, fi);
TRACE("cleanup_bug", tout << "register " << d->get_name() << "\n";);
m_aux_decls.insert(d);
}
void proto_model::register_aux_decl(func_decl * d) {
m_aux_decls.insert(d);
}
@ -220,31 +225,29 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, fun
*/
void proto_model::cleanup() {
func_decl_set found_aux_fs;
decl2finterp::iterator it = m_finterp.begin();
decl2finterp::iterator end = m_finterp.end();
for (; it != end; ++it) {
func_interp * fi = (*it).m_value;
for (auto const& kv : m_finterp) {
func_interp * fi = kv.m_value;
cleanup_func_interp(fi, found_aux_fs);
}
TRACE("cleanup_bug",
for (func_decl* faux : m_aux_decls) {
tout << faux->get_name() << "\n";
});
// remove auxiliary declarations that are not used.
if (found_aux_fs.size() != m_aux_decls.size()) {
remove_aux_decls_not_in_set(m_decls, found_aux_fs);
remove_aux_decls_not_in_set(m_func_decls, found_aux_fs);
func_decl_set::iterator it2 = m_aux_decls.begin();
func_decl_set::iterator end2 = m_aux_decls.end();
for (; it2 != end2; ++it2) {
func_decl * faux = *it2;
for (func_decl* faux : m_aux_decls) {
if (!found_aux_fs.contains(faux)) {
TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";);
func_interp * fi = 0;
m_finterp.find(faux, fi);
SASSERT(fi != 0);
m_finterp.erase(faux);
m_manager.dec_ref(faux);
dealloc(fi);
unregister_decl(faux);
}
else {
TRACE("cleanup_bug", tout << "not eliminating " << faux->get_name() << "\n";);
}
}
m_aux_decls.swap(found_aux_fs);
}
@ -270,10 +273,8 @@ ptr_vector<expr> const & proto_model::get_universe(sort * s) const {
ptr_vector<expr> & tmp = const_cast<proto_model*>(this)->m_tmp;
tmp.reset();
obj_hashtable<expr> const & u = get_known_universe(s);
obj_hashtable<expr>::iterator it = u.begin();
obj_hashtable<expr>::iterator end = u.end();
for (; it != end; ++it)
tmp.push_back(*it);
for (expr * e : u)
tmp.push_back(e);
return tmp;
}
@ -356,10 +357,7 @@ bool proto_model::is_as_array(expr * v) const {
}
void proto_model::compress() {
ptr_vector<func_decl>::iterator it = m_func_decls.begin();
ptr_vector<func_decl>::iterator end = m_func_decls.end();
for (; it != end; ++it) {
func_decl * f = *it;
for (func_decl* f : m_func_decls) {
func_interp * fi = get_func_interp(f);
SASSERT(fi != 0);
fi->compress();
@ -412,17 +410,13 @@ model * proto_model::mk_model() {
TRACE("proto_model", tout << "mk_model\n"; model_v2_pp(tout, *this););
model * m = alloc(model, m_manager);
decl2expr::iterator it1 = m_interp.begin();
decl2expr::iterator end1 = m_interp.end();
for (; it1 != end1; ++it1) {
m->register_decl(it1->m_key, it1->m_value);
for (auto const& kv : m_interp) {
m->register_decl(kv.m_key, kv.m_value);
}
decl2finterp::iterator it2 = m_finterp.begin();
decl2finterp::iterator end2 = m_finterp.end();
for (; it2 != end2; ++it2) {
m->register_decl(it2->m_key, it2->m_value);
m_manager.dec_ref(it2->m_key);
for (auto const& kv : m_finterp) {
m->register_decl(kv.m_key, kv.m_value);
m_manager.dec_ref(kv.m_key);
}
m_finterp.reset(); // m took the ownership of the func_interp's

1
src/smt/proto_model/proto_model.h
View file

@ -84,6 +84,7 @@ public:
// Primitives for building models
//
void register_aux_decl(func_decl * f, func_interp * fi);
void register_aux_decl(func_decl * f);
void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
void compress();
void cleanup();

5
src/smt/smt_model_checker.cpp
View file

@ -89,10 +89,7 @@ namespace smt {
void model_checker::restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe) {
SASSERT(!universe.empty());
ptr_buffer<expr> eqs;
obj_hashtable<expr>::iterator it = universe.begin();
obj_hashtable<expr>::iterator end = universe.end();
for (; it != end; ++it) {
expr * e = *it;
for (expr * e : universe) {
eqs.push_back(m.mk_eq(sk, e));
}
expr_ref fml(m.mk_or(eqs.size(), eqs.c_ptr()), m);

21
src/smt/smt_model_finder.cpp
View file

@ -628,18 +628,14 @@ namespace smt {
ptr_vector<expr> const & exceptions = n->get_exceptions();
ptr_vector<node> const & avoid_set = n->get_avoid_set();
ptr_vector<expr>::const_iterator it1 = exceptions.begin();
ptr_vector<expr>::const_iterator end1 = exceptions.end();
for (; it1 != end1; ++it1) {
expr * val = eval(*it1, true);
for (expr* e : exceptions) {
expr * val = eval(e, true);
SASSERT(val != 0);
r.push_back(val);
}
ptr_vector<node>::const_iterator it2 = avoid_set.begin();
ptr_vector<node>::const_iterator end2 = avoid_set.end();
for (; it2 != end2; ++it2) {
node * n = (*it2)->get_root();
for (node* a : avoid_set) {
node * n = a->get_root();
if (!n->is_mono_proj() && n->get_else() != 0) {
expr * val = eval(n->get_else(), true);
SASSERT(val != 0);
@ -661,11 +657,9 @@ namespace smt {
expr * t_result = 0;
unsigned gen_result = UINT_MAX;
obj_map<expr, unsigned>::iterator it1 = elems.begin();
obj_map<expr, unsigned>::iterator end1 = elems.end();
for (; it1 != end1; ++it1) {
expr * t = (*it1).m_key;
unsigned gen = (*it1).m_value;
for (auto const& kv : elems) {
expr * t = kv.m_key;
unsigned gen = kv.m_value;
expr * t_val = eval(t, true);
SASSERT(t_val != 0);
ptr_buffer<expr>::const_iterator it2 = ex_vals.begin();
@ -699,6 +693,7 @@ namespace smt {
if (m_sort2k.find(s, r))
return r;
r = m_manager.mk_fresh_const("k", s);
m_model->register_aux_decl(r->get_decl());
m_sort2k.insert(s, r);
m_ks.push_back(r);
return r;

10
src/smt/theory_seq.cpp
View file

@ -3224,26 +3224,32 @@ void theory_seq::add_indexof_axiom(expr* i) {
/*
let r = replace(a, s, t)
a = "" => s = "" or r = a
contains(a, s) or r = a
s = "" => r = t+a
tightest_prefix(s, x)
(contains(a, s) -> r = xty & a = xsy) &
(!contains(a, s) -> r = a)
*/
void theory_seq::add_replace_axiom(expr* r) {
context& ctx = get_context();
expr* a = 0, *s = 0, *t = 0;
VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_indexof_left, a, s);
expr_ref y = mk_skolem(m_indexof_right, a, s);
expr_ref xty = mk_concat(x, t, y);
expr_ref xsy = mk_concat(x, s, y);
literal a_emp = mk_eq_empty(a, true);
literal s_emp = mk_eq_empty(s, true);
literal cnt = mk_literal(m_util.str.mk_contains(a, s));
literal a_emp = mk_eq_empty(a);
literal s_emp = mk_eq_empty(s);
add_axiom(~a_emp, s_emp, mk_seq_eq(r, a));
add_axiom(cnt, mk_seq_eq(r, a));
add_axiom(~s_emp, mk_seq_eq(r, mk_concat(t, a)));
add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(a, xsy));
add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(r, xty));
ctx.force_phase(cnt);
tightest_prefix(s, x);
}

49
src/smt/theory_str.cpp
View file

@ -166,14 +166,18 @@ namespace smt {
}
}
void theory_str::assert_axiom(expr * e) {
void theory_str::assert_axiom(expr * _e) {
if (opt_VerifyFinalCheckProgress) {
finalCheckProgressIndicator = true;
}
if (get_manager().is_true(e)) return;
TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
if (get_manager().is_true(_e)) return;
context & ctx = get_context();
ast_manager& m = get_manager();
TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;);
expr_ref e(_e, m);
th_rewriter rw(m);
rw(e);
if (!ctx.b_internalized(e)) {
ctx.internalize(e, false);
}
@ -1419,6 +1423,9 @@ namespace smt {
void theory_str::instantiate_axiom_Substr(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr* substrBase = 0;
expr* substrPos = 0;
expr* substrLen = 0;
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
@ -1429,12 +1436,7 @@ namespace smt {
TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
expr_ref substrBase(expr->get_arg(0), m);
expr_ref substrPos(expr->get_arg(1), m);
expr_ref substrLen(expr->get_arg(2), m);
SASSERT(substrBase);
SASSERT(substrPos);
SASSERT(substrLen);
VERIFY(u.str.is_extract(expr, substrBase, substrPos, substrLen));
expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m);
@ -1452,28 +1454,19 @@ namespace smt {
// len >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
expr_ref argumentsValid(mk_and(argumentsValid_terms), m);
SASSERT(argumentsValid);
ctx.internalize(argumentsValid, false);
// (pos+len) >= strlen(base)
// --> pos + len + -1*strlen(base) >= 0
expr_ref lenOutOfBounds(m_autil.mk_ge(
m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
zero), m);
SASSERT(lenOutOfBounds);
ctx.internalize(argumentsValid, false);
expr_ref argumentsValid = mk_and(argumentsValid_terms);
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
// ==> (Substr ...) = ""
expr_ref case1_premise(m.mk_not(argumentsValid), m);
SASSERT(case1_premise);
ctx.internalize(case1_premise, false);
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
SASSERT(case1_conclusion);
ctx.internalize(case1_conclusion, false);
expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m);
SASSERT(case1);
expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
// Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base)
// ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1
@ -1483,8 +1476,7 @@ namespace smt {
ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)),
ctx.mk_eq_atom(mk_strlen(t0), substrPos),
ctx.mk_eq_atom(expr, t1)), m);
expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
SASSERT(case2);
expr_ref case2(m.mk_implies(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
@ -1497,16 +1489,11 @@ namespace smt {
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
SASSERT(case3);
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
ctx.internalize(case1, false);
ctx.internalize(case2, false);
ctx.internalize(case3, false);
expr_ref finalAxiom(m.mk_and(case1, case2, case3), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
assert_axiom(case1);
assert_axiom(case2);
assert_axiom(case3);
}
void theory_str::instantiate_axiom_Replace(enode * e) {