mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-11-04 15:19:19 +00:00
commit e700460645
3 changed files with 55 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/mk_util.py
View file

@ -82,7 +82,7 @@ Z3PY_SRC_DIR=None
VS_PROJ = False VS_PROJ = False
TRACE = False TRACE = False
DOTNET_ENABLED=False DOTNET_ENABLED=False
DOTNET_KEY_FILE=None DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
JAVA_ENABLED=False JAVA_ENABLED=False
ML_ENABLED=False ML_ENABLED=False
PYTHON_INSTALL_ENABLED=False PYTHON_INSTALL_ENABLED=False
@ -1591,7 +1591,7 @@ class DotNetDLLComponent(Component):
elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): elif os.path.isfile(os.path.join(self.src_dir, self.key_file)):
self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file))
else: else:
print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.dll_name, self.key_file)) print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
self.key_file = None self.key_file = None
if not self.key_file is None: if not self.key_file is None:

42
src/ast/rewriter/bool_rewriter.cpp
View file

@ -581,38 +581,40 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n"; TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n";
tout << t << " " << e << " " << val << "\n";); tout << t << " " << e << " " << val << "\n";);
result = m().mk_false(); result = m().mk_false();
} }
else if (t == val && e == val) { else if (t == val && e == val) {
result = m().mk_true(); result = m().mk_true();
} }
else if (t == val) { else if (t == val) {
result = cond; result = cond;
} }
else { else {
SASSERT(e == val); SASSERT(e == val);
mk_not(cond, result); mk_not(cond, result);
} }
return BR_DONE; return BR_DONE;
} }
if (m().is_value(t)) { if (m_ite_extra_rules) {
if (val == t) { if (m().is_value(t)) {
result = m().mk_or(cond, m().mk_eq(val, e)); if (val == t) {
result = m().mk_or(cond, m().mk_eq(val, e));
}
else {
mk_not(cond, result);
result = m().mk_and(result, m().mk_eq(val, e));
}
return BR_REWRITE2;
} }
else { if (m().is_value(e)) {
mk_not(cond, result); if (val == e) {
result = m().mk_and(result, m().mk_eq(val, e)); mk_not(cond, result);
result = m().mk_or(result, m().mk_eq(val, t));
}
else {
result = m().mk_and(cond, m().mk_eq(val, t));
}
return BR_REWRITE2;
} }
return BR_REWRITE2;
}
if (m().is_value(e)) {
if (val == e) {
mk_not(cond, result);
result = m().mk_or(result, m().mk_eq(val, t));
}
else {
result = m().mk_and(cond, m().mk_eq(val, t));
}
return BR_REWRITE2;
} }
expr* cond2, *t2, *e2; expr* cond2, *t2, *e2;
if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {

60
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -46,7 +46,7 @@ public:
ctx_propagate_assertions::ctx_propagate_assertions(ast_manager& m): m(m), m_trail(m) {} ctx_propagate_assertions::ctx_propagate_assertions(ast_manager& m): m(m), m_trail(m) {}
bool ctx_propagate_assertions::assert_expr(expr * t, bool sign) { bool ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
expr * p = t; expr * p = t;
while (m.is_not(t, t)) { while (m.is_not(t, t)) {
sign = !sign; sign = !sign;
@ -83,8 +83,8 @@ void ctx_propagate_assertions::assert_eq_core(expr * t, app * val) {
// because the simplifier stopped at depth m_max_depth // because the simplifier stopped at depth m_max_depth
return; return;
} }
CTRACE("assert_eq_bug", m_assertions.contains(t), CTRACE("assert_eq_bug", m_assertions.contains(t),
tout << "t:\n" << mk_ismt2_pp(t, m) << "\nval:\n" << mk_ismt2_pp(val, m) << "\n"; tout << "t:\n" << mk_ismt2_pp(t, m) << "\nval:\n" << mk_ismt2_pp(val, m) << "\n";
expr * old_val = 0; expr * old_val = 0;
m_assertions.find(t, old_val); m_assertions.find(t, old_val);
@ -114,11 +114,11 @@ void ctx_propagate_assertions::pop(unsigned num_scopes) {
m_trail.pop_back(); m_trail.pop_back();
} }
SASSERT(m_trail.size() == old_trail_size); SASSERT(m_trail.size() == old_trail_size);
m_scopes.shrink(scope_lvl - num_scopes); m_scopes.shrink(scope_lvl - num_scopes);
} }
bool ctx_simplify_tactic::simplifier::shared(expr * t) const { bool ctx_simplify_tactic::simplifier::shared(expr * t) const {
SASSERT(m_occs); SASSERT(m_occs);
return t->get_ref_count() > 1 && m_occs->get_num_occs(t) > 1; return t->get_ref_count() > 1 && m_occs->get_num_occs(t) > 1;
} }
@ -139,7 +139,7 @@ struct ctx_simplify_tactic::imp {
unsigned m_lvl; unsigned m_lvl;
cached_result * m_next; cached_result * m_next;
cached_result(expr * t, unsigned lvl, cached_result * next): cached_result(expr * t, unsigned lvl, cached_result * next):
m_to(t), m_to(t),
m_lvl(lvl), m_lvl(lvl),
m_next(next) { m_next(next) {
} }
@ -156,7 +156,7 @@ struct ctx_simplify_tactic::imp {
small_object_allocator m_allocator; small_object_allocator m_allocator;
svector<cache_cell> m_cache; svector<cache_cell> m_cache;
vector<ptr_vector<expr> > m_cache_undo; vector<ptr_vector<expr> > m_cache_undo;
unsigned m_depth; unsigned m_depth;
unsigned m_num_steps; unsigned m_num_steps;
goal_num_occurs m_occs; goal_num_occurs m_occs;
mk_simplified_app m_mk_app; mk_simplified_app m_mk_app;
@ -183,7 +183,7 @@ struct ctx_simplify_tactic::imp {
dealloc(m_simp); dealloc(m_simp);
DEBUG_CODE({ DEBUG_CODE({
for (unsigned i = 0; i < m_cache.size(); i++) { for (unsigned i = 0; i < m_cache.size(); i++) {
CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from,
tout << "i: " << i << "\n" << mk_ismt2_pp(m_cache[i].m_from, m) << "\n"; tout << "i: " << i << "\n" << mk_ismt2_pp(m_cache[i].m_from, m) << "\n";
tout << "m_result: " << m_cache[i].m_result << "\n"; tout << "m_result: " << m_cache[i].m_result << "\n";
if (m_cache[i].m_result) tout << "lvl: " << m_cache[i].m_result->m_lvl << "\n";); if (m_cache[i].m_result) tout << "lvl: " << m_cache[i].m_result->m_lvl << "\n";);
@ -209,7 +209,7 @@ struct ctx_simplify_tactic::imp {
throw tactic_exception(m.limit().get_cancel_msg()); throw tactic_exception(m.limit().get_cancel_msg());
} }
bool shared(expr * t) const { bool shared(expr * t) const {
TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";); TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";);
return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1; return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1;
} }
@ -233,7 +233,7 @@ struct ctx_simplify_tactic::imp {
unsigned id = from->get_id(); unsigned id = from->get_id();
TRACE("ctx_simplify_tactic_cache", tout << "caching " << id << " @ " << scope_level() << "\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";); TRACE("ctx_simplify_tactic_cache", tout << "caching " << id << " @ " << scope_level() << "\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";);
m_cache.reserve(id+1); m_cache.reserve(id+1);
cache_cell & cell = m_cache[id]; cache_cell & cell = m_cache[id];
void * mem = m_allocator.allocate(sizeof(cached_result)); void * mem = m_allocator.allocate(sizeof(cached_result));
if (cell.m_from == 0) { if (cell.m_from == 0) {
// new_entry // new_entry
@ -243,7 +243,7 @@ struct ctx_simplify_tactic::imp {
m.inc_ref(to); m.inc_ref(to);
} }
else { else {
// update // update
cell.m_result = new (mem) cached_result(to, scope_level(), cell.m_result); cell.m_result = new (mem) cached_result(to, scope_level(), cell.m_result);
m.inc_ref(to); m.inc_ref(to);
} }
@ -255,7 +255,7 @@ struct ctx_simplify_tactic::imp {
if (shared(from)) if (shared(from))
cache_core(from, to); cache_core(from, to);
} }
unsigned scope_level() const { unsigned scope_level() const {
return m_simp->scope_level(); return m_simp->scope_level();
} }
@ -276,7 +276,7 @@ struct ctx_simplify_tactic::imp {
m.dec_ref(cell.m_result->m_to); m.dec_ref(cell.m_result->m_to);
cached_result * to_delete = cell.m_result; cached_result * to_delete = cell.m_result;
SASSERT(to_delete->m_lvl == lvl); SASSERT(to_delete->m_lvl == lvl);
TRACE("ctx_simplify_tactic_cache", tout << "uncaching: " << to_delete->m_lvl << "\n" << TRACE("ctx_simplify_tactic_cache", tout << "uncaching: " << to_delete->m_lvl << "\n" <<
mk_ismt2_pp(key, m) << "\n--->\n" << mk_ismt2_pp(to_delete->m_to, m) << "\nrestoring:\n"; mk_ismt2_pp(key, m) << "\n--->\n" << mk_ismt2_pp(to_delete->m_to, m) << "\nrestoring:\n";
if (to_delete->m_next) tout << mk_ismt2_pp(to_delete->m_next->m_to, m); else tout << "<null>"; if (to_delete->m_next) tout << mk_ismt2_pp(to_delete->m_next->m_to, m); else tout << "<null>";
tout << "\n";); tout << "\n";);
@ -287,7 +287,7 @@ struct ctx_simplify_tactic::imp {
} }
m_allocator.deallocate(sizeof(cached_result), to_delete); m_allocator.deallocate(sizeof(cached_result), to_delete);
} }
keys.reset(); keys.reset();
} }
void pop(unsigned num_scopes) { void pop(unsigned num_scopes) {
@ -295,7 +295,7 @@ struct ctx_simplify_tactic::imp {
return; return;
SASSERT(num_scopes <= scope_level()); SASSERT(num_scopes <= scope_level());
unsigned lvl = scope_level(); unsigned lvl = scope_level();
m_simp->pop(num_scopes); m_simp->pop(num_scopes);
// restore cache // restore cache
@ -339,7 +339,7 @@ struct ctx_simplify_tactic::imp {
} }
m_num_steps++; m_num_steps++;
m_depth++; m_depth++;
if (m.is_or(t)) if (m.is_or(t))
simplify_or_and<true>(to_app(t), r); simplify_or_and<true>(to_app(t), r);
else if (m.is_and(t)) else if (m.is_and(t))
simplify_or_and<false>(to_app(t), r); simplify_or_and<false>(to_app(t), r);
@ -351,7 +351,7 @@ struct ctx_simplify_tactic::imp {
SASSERT(r.get() != 0); SASSERT(r.get() != 0);
TRACE("ctx_simplify_tactic_detail", tout << "result:\n" << mk_bounded_pp(t, m) << "\n---->\n" << mk_bounded_pp(r, m) << "\n";); TRACE("ctx_simplify_tactic_detail", tout << "result:\n" << mk_bounded_pp(t, m) << "\n---->\n" << mk_bounded_pp(r, m) << "\n";);
} }
template<bool OR> template<bool OR>
void simplify_or_and(app * t, expr_ref & r) { void simplify_or_and(app * t, expr_ref & r) {
// go forwards // go forwards
@ -374,7 +374,7 @@ struct ctx_simplify_tactic::imp {
continue; continue;
} }
if ((OR && m.is_true(new_arg)) || if ((OR && m.is_true(new_arg)) ||
(!OR && m.is_false(new_arg))) { (!OR && m.is_false(new_arg))) {
r = new_arg; r = new_arg;
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
cache(t, r); cache(t, r);
@ -403,7 +403,7 @@ struct ctx_simplify_tactic::imp {
continue; continue;
} }
if ((OR && m.is_true(new_arg)) || if ((OR && m.is_true(new_arg)) ||
(!OR && m.is_false(new_arg))) { (!OR && m.is_false(new_arg))) {
r = new_arg; r = new_arg;
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
cache(t, r); cache(t, r);
@ -428,7 +428,7 @@ struct ctx_simplify_tactic::imp {
} }
cache(t, r); cache(t, r);
} }
void simplify_ite(app * ite, expr_ref & r) { void simplify_ite(app * ite, expr_ref & r) {
expr * c = ite->get_arg(0); expr * c = ite->get_arg(0);
expr * t = ite->get_arg(1); expr * t = ite->get_arg(1);
@ -467,8 +467,8 @@ struct ctx_simplify_tactic::imp {
} }
else { else {
expr * args[3] = { new_c.get(), new_t.get(), new_e.get() }; expr * args[3] = { new_c.get(), new_t.get(), new_e.get() };
TRACE("ctx_simplify_tactic_ite_bug", TRACE("ctx_simplify_tactic_ite_bug",
tout << "mk_ite\n" << mk_ismt2_pp(new_c.get(), m) << "\n" << mk_ismt2_pp(new_t.get(), m) tout << "mk_ite\n" << mk_ismt2_pp(new_c.get(), m) << "\n" << mk_ismt2_pp(new_t.get(), m)
<< "\n" << mk_ismt2_pp(new_e.get(), m) << "\n";); << "\n" << mk_ismt2_pp(new_e.get(), m) << "\n";);
m_mk_app(ite->get_decl(), 3, args, r); m_mk_app(ite->get_decl(), 3, args, r);
} }
@ -529,7 +529,7 @@ struct ctx_simplify_tactic::imp {
unsigned sz = g.size(); unsigned sz = g.size();
expr_ref r(m); expr_ref r(m);
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
m_depth = 0; m_depth = 0;
simplify(g.form(i), r); simplify(g.form(i), r);
if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) { if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) {
r = m.mk_false(); r = m.mk_false();
@ -538,6 +538,8 @@ struct ctx_simplify_tactic::imp {
} }
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
m_occs(g);
// go backwards // go backwards
sz = g.size(); sz = g.size();
for (unsigned i = sz; !g.inconsistent() && i > 0; ) { for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
@ -590,7 +592,7 @@ struct ctx_simplify_tactic::imp {
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";); IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";);
SASSERT(g.is_well_sorted()); SASSERT(g.is_well_sorted());
} }
}; };
ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p): ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p):
@ -618,9 +620,9 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
r.insert("propagate_eq", CPK_BOOL, "(default: false) enable equality propagation from bounds."); r.insert("propagate_eq", CPK_BOOL, "(default: false) enable equality propagation from bounds.");
} }
void ctx_simplify_tactic::operator()(goal_ref const & in, void ctx_simplify_tactic::operator()(goal_ref const & in,
goal_ref_buffer & result, goal_ref_buffer & result,
model_converter_ref & mc, model_converter_ref & mc,
proof_converter_ref & pc, proof_converter_ref & pc,
expr_dependency_ref & core) { expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0; mc = 0; pc = 0; core = 0;
@ -628,12 +630,12 @@ void ctx_simplify_tactic::operator()(goal_ref const & in,
in->inc_depth(); in->inc_depth();
result.push_back(in.get()); result.push_back(in.get());
} }
void ctx_simplify_tactic::cleanup() { void ctx_simplify_tactic::cleanup() {
ast_manager & m = m_imp->m; ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_imp->m_simp->translate(m), m_params); imp * d = alloc(imp, m, m_imp->m_simp->translate(m), m_params);
std::swap(d, m_imp); std::swap(d, m_imp);
dealloc(d); dealloc(d);
} }