mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

simplifications noticed by trying #4147

Browse source 
The change masks possible bugs in smt.threads and arrays.
This commit is contained in:
Nikolaj Bjorner 2020-04-29 10:15:54 -07:00
parent 7cfd16c7f9
commit 3fc001baea
4 changed files with 25 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/seq_axioms.cpp
View file

@ -563,16 +563,15 @@ void seq_axioms::add_itos_axiom(expr* e) {
/**
stoi(s) >= -1
stoi("") = -1
stoi(s) >= 0 => len(s) > 0
stoi(s) >= 0 => is_digit(nth(s,0))
*/
void seq_axioms::add_stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
literal ge0 = mk_ge(e, 0);
expr* s = nullptr;
VERIFY (seq.str.is_stoi(e, s));
add_axiom(mk_ge(e, -1)); // stoi(s) >= -1
add_axiom(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1))); // s = "" => stoi(s) = -1
literal ge0 = mk_ge(e, 0);
add_axiom(~ge0, is_digit(mk_nth(s, 0))); // stoi(s) >= 0 => is_digit(nth(s,0))
}
@ -614,9 +613,9 @@ void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
expr_ref len = mk_len(s);
literal ge0 = mk_ge(e, 0);
literal lek = mk_le(len, k);
add_axiom(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1)
add_axiom(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
add_axiom(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
add_axiom(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1)
add_axiom(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
add_axiom(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
for (unsigned i = 1; i < k; ++i) {
// len(s) <= i => stoi(s, i) = stoi(s, i - 1)

2
src/smt/smt_parallel.cpp
View file

@ -183,7 +183,7 @@ namespace smt {
}
};
// for debugging: num_threads = 1;
// for debugging: num_threads = 1;
while (true) {
vector<std::thread> threads(num_threads);

21
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -15,6 +15,16 @@ Author:
Notes:
Implement the inference rule
n = V |- F[n] = F[x]
--------------------
F[x] = F[V]
where n is an uninterpreted variable (fresh for F[x])
and V is a value (true or false) and x is a subterm
(different from V).
--*/
#include "smt/tactic/ctx_solver_simplify_tactic.h"
@ -184,9 +194,14 @@ protected:
if (cache.contains(e)) {
goto done;
}
if (m.is_true(e) || m.is_false(e)) {
res = e;
goto done;
}
if (m.is_bool(e) && simplify_bool(n, res)) {
TRACE("ctx_solver_simplify_tactic",
tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
TRACE("ctx_solver_simplify_tactic",
m_solver.display(tout) << "\n";
tout << "simplified: " << mk_pp(n, m) << "\n" << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
goto done;
}
if (!is_app(e)) {
@ -214,7 +229,7 @@ protected:
args.push_back(arg);
}
}
else if (!n2) {
else if (!n2 && !m.is_value(arg)) {
n2 = mk_fresh(id, m.get_sort(arg));
trail.push_back(n2);
todo.push_back(expr_pos(self_pos, ++child_id, i, arg));

3
src/tactic/core/distribute_forall_tactic.cpp
View file

@ -15,6 +15,7 @@ Author:
--*/
#include "tactic/tactical.h"
#include "ast/ast_util.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/var_subst.h"
@ -46,7 +47,7 @@ class distribute_forall_tactic : public tactic {
expr_ref_buffer new_args(m);
for (unsigned i = 0; i < num_args; i++) {
expr * arg = or_e->get_arg(i);
expr * not_arg = m.mk_not(arg);
expr * not_arg = mk_not(m, arg);
quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, not_arg);
new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));