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

Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-16 12:03:50 +00:00
commit 928858452f
3 changed files with 33 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -110,6 +110,9 @@ public:
bool lo, s; bool lo, s;
expr* t1; expr* t1;
rational n; rational n;
if (!shared(t)) {
return;
}
if (is_bound(t, t1, lo, s, n)) { if (is_bound(t, t1, lo, s, n)) {
if (sign) { if (sign) {
// !(n <= t1) <=> t1 <= n - 1 // !(n <= t1) <=> t1 <= n - 1

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

@ -22,6 +22,27 @@ Notes:
#include"ast_ll_pp.h" #include"ast_ll_pp.h"
#include"ast_pp.h" #include"ast_pp.h"
class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier {
ast_manager& m;
obj_map<expr, expr*> m_assertions;
expr_ref_vector m_trail;
unsigned_vector m_scopes;
void assert_eq_val(expr * t, app * val, bool mk_scope);
void assert_eq_core(expr * t, app * val);
public:
ctx_propagate_assertions(ast_manager& m);
virtual ~ctx_propagate_assertions() {}
virtual void assert_expr(expr * t, bool sign);
virtual bool simplify(expr* t, expr_ref& result);
virtual void push();
virtual void pop(unsigned num_scopes);
virtual unsigned scope_level() const { return m_scopes.size(); }
virtual simplifier * translate(ast_manager & m);
};
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) {}
void ctx_propagate_assertions::assert_expr(expr * t, bool sign) { void ctx_propagate_assertions::assert_expr(expr * t, bool sign) {
@ -106,6 +127,10 @@ ctx_simplify_tactic::simplifier * ctx_propagate_assertions::translate(ast_manage
return alloc(ctx_propagate_assertions, m); return alloc(ctx_propagate_assertions, m);
} }
tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(ctx_simplify_tactic, m, alloc(ctx_propagate_assertions, m), p));
}
struct ctx_simplify_tactic::imp { struct ctx_simplify_tactic::imp {
struct cached_result { struct cached_result {
@ -152,8 +177,7 @@ struct ctx_simplify_tactic::imp {
~imp() { ~imp() {
pop(scope_level()); pop(scope_level());
SASSERT(scope_level() == 0); SASSERT(scope_level() == 0 && m_cache_undo.empty());
restore_cache(0);
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,
@ -202,8 +226,8 @@ struct ctx_simplify_tactic::imp {
} }
void cache_core(expr * from, expr * to) { void cache_core(expr * from, expr * to) {
TRACE("ctx_simplify_tactic_cache", tout << "caching\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";);
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";);
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));
@ -270,11 +294,11 @@ struct ctx_simplify_tactic::imp {
if (num_scopes == 0) if (num_scopes == 0)
return; return;
SASSERT(num_scopes <= scope_level()); SASSERT(num_scopes <= scope_level());
unsigned lvl = scope_level();
m_simp->pop(num_scopes); m_simp->pop(num_scopes);
// restore cache // restore cache
unsigned lvl = scope_level();
for (unsigned i = 0; i < num_scopes; i++) { for (unsigned i = 0; i < num_scopes; i++) {
restore_cache(lvl); restore_cache(lvl);
lvl--; lvl--;

25
src/tactic/core/ctx_simplify_tactic.h
View file

@ -65,30 +65,7 @@ public:
virtual void cleanup(); virtual void cleanup();
}; };
tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier {
ast_manager& m;
obj_map<expr, expr*> m_assertions;
expr_ref_vector m_trail;
unsigned_vector m_scopes;
void assert_eq_val(expr * t, app * val, bool mk_scope);
void assert_eq_core(expr * t, app * val);
public:
ctx_propagate_assertions(ast_manager& m);
virtual ~ctx_propagate_assertions() {}
virtual void assert_expr(expr * t, bool sign);
virtual bool simplify(expr* t, expr_ref& result);
virtual void push();
virtual void pop(unsigned num_scopes);
virtual unsigned scope_level() const { return m_scopes.size(); }
virtual simplifier * translate(ast_manager & m);
};
inline tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()) {
return clean(alloc(ctx_simplify_tactic, m, alloc(ctx_propagate_assertions, m), p));
}
/* /*
ADD_TACTIC("ctx-simplify", "apply contextual simplification rules.", "mk_ctx_simplify_tactic(m, p)") ADD_TACTIC("ctx-simplify", "apply contextual simplification rules.", "mk_ctx_simplify_tactic(m, p)")