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

move ctx_propagate_assertions class to .cpp file

Browse source
This commit is contained in:
Nuno Lopes 2016-02-16 09:34:45 +00:00
parent 07953342ac
commit 98c5a5c86c
2 changed files with 26 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

25
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 {

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)")