move more converters

src/ast/converters/CMakeLists.txt

@@ -1,8 +1,10 @@
 z3_add_component(converters
   SOURCES
+    equiv_proof_converter.cpp
+    generic_model_converter.cpp
     model_converter.cpp
     proof_converter.cpp
-    generic_model_converter.cpp
+    replace_proof_converter.cpp
   COMPONENT_DEPENDENCIES
     model
 )

src/ast/converters/equiv_proof_converter.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 #include "ast/ast_pp.h"
 #include "ast/scoped_proof.h"
 

src/ast/converters/equiv_proof_converter.h

@@ -23,7 +23,7 @@ Revision History:
 
 #pragma once
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 
 class equiv_proof_converter : public proof_converter {
     ast_manager&            m;

src/ast/converters/replace_proof_converter.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/expr_functors.h"
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"

src/muz/base/dl_util.h

@@ -24,7 +24,7 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "util/uint_set.h"
 #include "tactic/horn_subsume_model_converter.h"
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/substitution/substitution.h"
 #include "ast/rewriter/ast_counter.h"
 #include "util/statistics.h"

src/muz/transforms/dl_mk_array_blast.h

@@ -22,9 +22,9 @@ Revision History:
 #include "muz/base/dl_rule_set.h"
 #include "muz/base/dl_rule_transformer.h"
 #include "muz/transforms/dl_mk_interp_tail_simplifier.h"
-#include "tactic/equiv_proof_converter.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "ast/converters/equiv_proof_converter.h"
 
 namespace datalog {
 

src/muz/transforms/dl_mk_elim_term_ite.h

@@ -21,7 +21,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/base/dl_rule_set.h"
 #include "muz/base/dl_rule_transformer.h"
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 
 namespace datalog {
     class mk_elim_term_ite : public rule_transformer::plugin {

src/tactic/CMakeLists.txt

@@ -1,14 +1,12 @@
 z3_add_component(tactic
   SOURCES
     dependency_converter.cpp
-    equiv_proof_converter.cpp
     goal.cpp
     goal_num_occurs.cpp
     goal_shared_occs.cpp
     goal_util.cpp
     horn_subsume_model_converter.cpp
     probe.cpp
-    replace_proof_converter.cpp
     tactical.cpp
     tactic.cpp
   COMPONENT_DEPENDENCIES