From 98c5a5c86c0f137a02afbce2399583a84d3cb3d0 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Feb 2016 09:34:45 +0000 Subject: [PATCH] move ctx_propagate_assertions class to .cpp file --- src/tactic/core/ctx_simplify_tactic.cpp | 25 +++++++++++++++++++++++++ src/tactic/core/ctx_simplify_tactic.h | 25 +------------------------ 2 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index efaae3c40..95be200a8 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -22,6 +22,27 @@ Notes: #include"ast_ll_pp.h" #include"ast_pp.h" + +class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier { + ast_manager& m; + obj_map 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) {} 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); } +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 cached_result { diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index d72f54a83..fccb25d3b 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -65,30 +65,7 @@ public: virtual void cleanup(); }; - -class ctx_propagate_assertions : public ctx_simplify_tactic::simplifier { - ast_manager& m; - obj_map 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)); -} +tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("ctx-simplify", "apply contextual simplification rules.", "mk_ctx_simplify_tactic(m, p)")