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

ctx_simplify: remove virtual push() method

Browse source
This commit is contained in:
Nuno Lopes 2016-02-28 17:57:40 +00:00
parent 51687b2be7
commit e7a360ca08
3 changed files with 2 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -363,7 +363,7 @@ public:
return expr_has_bounds(t);
}
virtual void push() {
void push() {
TRACE("bv", tout << "push\n";);
unsigned sz = m_scopes.size();
m_scopes.resize(sz + 1);

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

@ -36,7 +36,7 @@ public:
virtual ~ctx_propagate_assertions() {}
virtual bool assert_expr(expr * t, bool sign);
virtual bool simplify(expr* t, expr_ref& result);
virtual void push();
void push();
virtual void pop(unsigned num_scopes);
virtual unsigned scope_level() const { return m_scopes.size(); }
virtual simplifier * translate(ast_manager & m);
@ -260,10 +260,6 @@ struct ctx_simplify_tactic::imp {
return m_simp->scope_level();
}
void push() {
m_simp->push();
}
void restore_cache(unsigned lvl) {
if (lvl >= m_cache_undo.size())
return;

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

@ -31,7 +31,6 @@ public:
virtual bool assert_expr(expr * t, bool sign) = 0;
virtual bool simplify(expr* t, expr_ref& result) = 0;
virtual bool may_simplify(expr* t) { return true; }
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
virtual simplifier * translate(ast_manager & m) = 0;
virtual unsigned scope_level() const = 0;