From 4df172e9711c198d81ec382625ea819e2cb703ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Dec 2012 08:14:44 -0800 Subject: [PATCH] Fix file name (use same naming convention) Signed-off-by: Leonardo de Moura --- src/tactic/core/ctx_simplify_tactic.cpp | 4 ++-- .../{num_occurs_goal.cpp => goal_num_occurs.cpp} | 6 +++--- src/tactic/{num_occurs_goal.h => goal_num_occurs.h} | 10 +++++----- 3 files changed, 10 insertions(+), 10 deletions(-) rename src/tactic/{num_occurs_goal.cpp => goal_num_occurs.cpp} (75%) rename src/tactic/{num_occurs_goal.h => goal_num_occurs.h} (64%) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index cca21b90e..831efa087 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include"ctx_simplify_tactic.h" #include"mk_simplified_app.h" -#include"num_occurs_goal.h" +#include"goal_num_occurs.h" #include"cooperate.h" #include"ast_ll_pp.h" #include"ast_smt2_pp.h" @@ -51,7 +51,7 @@ struct ctx_simplify_tactic::imp { unsigned m_scope_lvl; unsigned m_depth; unsigned m_num_steps; - num_occurs_goal m_occs; + goal_num_occurs m_occs; mk_simplified_app m_mk_app; unsigned long long m_max_memory; unsigned m_max_depth; diff --git a/src/tactic/num_occurs_goal.cpp b/src/tactic/goal_num_occurs.cpp similarity index 75% rename from src/tactic/num_occurs_goal.cpp rename to src/tactic/goal_num_occurs.cpp index adc412434..6c94e307c 100644 --- a/src/tactic/num_occurs_goal.cpp +++ b/src/tactic/goal_num_occurs.cpp @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - num_occurs_goal.cpp + goal_num_occurs.cpp Abstract: @@ -15,10 +15,10 @@ Author: Revision History: --*/ -#include"num_occurs_goal.h" +#include"goal_num_occurs.h" #include"goal.h" -void num_occurs_goal::operator()(goal const & g) { +void goal_num_occurs::operator()(goal const & g) { expr_fast_mark1 visited; unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { diff --git a/src/tactic/num_occurs_goal.h b/src/tactic/goal_num_occurs.h similarity index 64% rename from src/tactic/num_occurs_goal.h rename to src/tactic/goal_num_occurs.h index 5e6e0cc94..33a25e03f 100644 --- a/src/tactic/num_occurs_goal.h +++ b/src/tactic/goal_num_occurs.h @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - num_occurs_goal.h + goal_num_occurs.h Abstract: @@ -15,16 +15,16 @@ Author: Revision History: --*/ -#ifndef _NUM_OCCURS_GOAL_H_ -#define _NUM_OCCURS_GOAL_H_ +#ifndef _GOAL_NUM_OCCURS_H_ +#define _GOAL_NUM_OCCURS_H_ #include"num_occurs.h" class goal; -class num_occurs_goal : public num_occurs { +class goal_num_occurs : public num_occurs { public: - num_occurs_goal(bool ignore_ref_count1 = false, bool ignore_quantifiers = false): + goal_num_occurs(bool ignore_ref_count1 = false, bool ignore_quantifiers = false): num_occurs(ignore_ref_count1, ignore_quantifiers) { }