From 0a4446ae269bfb28f6cba1c2a234b9c5e5527389 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Oct 2012 22:14:35 -0700 Subject: [PATCH] reorganizing the code Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 34 +++++++++---------- .../ufbv_strategy/ufbv_strategy.cpp | 0 .../ufbv_strategy/ufbv_strategy.h | 0 .../array_property_expander.cpp | 0 .../array_property/array_property_expander.h | 0 .../array_property_recognizer.cpp | 0 .../array_property_recognizer.h | 0 src/{ => ast}/macros/macro_finder.cpp | 0 src/{ => ast}/macros/macro_finder.h | 0 src/{ => ast}/macros/macro_manager.cpp | 0 src/{ => ast}/macros/macro_manager.h | 0 src/{ => ast}/macros/macro_substitution.cpp | 0 src/{ => ast}/macros/macro_substitution.h | 0 src/{ => ast}/macros/macro_util.cpp | 0 src/{ => ast}/macros/macro_util.h | 0 src/{ => ast}/macros/quasi_macros.cpp | 0 src/{ => ast}/macros/quasi_macros.h | 0 src/{ => ast}/pattern/pattern_inference.cpp | 0 src/{ => ast}/pattern/pattern_inference.h | 0 src/{ => ast}/proof_checker/proof_checker.cpp | 0 src/{ => ast}/proof_checker/proof_checker.h | 0 src/{ => ast}/rewriter/arith_rewriter.cpp | 0 src/{ => ast}/rewriter/arith_rewriter.h | 0 src/{ => ast}/rewriter/array_rewriter.cpp | 0 src/{ => ast}/rewriter/array_rewriter.h | 0 src/{ => ast}/rewriter/bool_rewriter.cpp | 0 src/{ => ast}/rewriter/bool_rewriter.h | 0 src/{ => ast}/rewriter/bv_rewriter.cpp | 0 src/{ => ast}/rewriter/bv_rewriter.h | 0 src/{ => ast}/rewriter/datatype_rewriter.cpp | 0 src/{ => ast}/rewriter/datatype_rewriter.h | 0 src/{ => ast}/rewriter/der.cpp | 0 src/{ => ast}/rewriter/der.h | 0 src/{ => ast}/rewriter/dl_rewriter.cpp | 0 src/{ => ast}/rewriter/dl_rewriter.h | 0 src/{ => ast}/rewriter/expr_replacer.cpp | 0 src/{ => ast}/rewriter/expr_replacer.h | 0 src/{ => ast}/rewriter/factor_rewriter.cpp | 0 src/{ => ast}/rewriter/factor_rewriter.h | 0 src/{ => ast}/rewriter/float_rewriter.cpp | 0 src/{ => ast}/rewriter/float_rewriter.h | 0 src/{ => ast}/rewriter/mk_simplified_app.cpp | 0 src/{ => ast}/rewriter/mk_simplified_app.h | 0 src/{ => ast}/rewriter/poly_rewriter.h | 0 src/{ => ast}/rewriter/poly_rewriter_def.h | 0 src/{ => ast}/rewriter/quant_hoist.cpp | 0 src/{ => ast}/rewriter/quant_hoist.h | 0 src/{ => ast}/rewriter/rewriter.cpp | 0 src/{ => ast}/rewriter/rewriter.h | 0 src/{ => ast}/rewriter/rewriter.txt | 0 src/{ => ast}/rewriter/rewriter_def.h | 0 src/{ => ast}/rewriter/rewriter_types.h | 0 src/{ => ast}/rewriter/th_rewriter.cpp | 0 src/{ => ast}/rewriter/th_rewriter.h | 0 src/{ => ast}/rewriter/var_subst.cpp | 0 src/{ => ast}/rewriter/var_subst.h | 0 src/{ => ast}/simplifier/README | 0 .../simplifier/arith_simplifier_params.cpp | 0 .../simplifier/arith_simplifier_params.h | 0 .../simplifier/arith_simplifier_plugin.cpp | 0 .../simplifier/arith_simplifier_plugin.h | 0 .../simplifier/array_simplifier_plugin.cpp | 0 .../simplifier/array_simplifier_plugin.h | 0 src/{ => ast}/simplifier/base_simplifier.h | 0 .../simplifier/basic_simplifier_plugin.cpp | 0 .../simplifier/basic_simplifier_plugin.h | 0 src/{ => ast}/simplifier/bit2int.cpp | 0 src/{ => ast}/simplifier/bit2int.h | 0 src/{ => ast}/simplifier/bv_elim.cpp | 0 src/{ => ast}/simplifier/bv_elim.h | 0 .../simplifier/bv_simplifier_params.h | 0 .../simplifier/bv_simplifier_plugin.cpp | 0 .../simplifier/bv_simplifier_plugin.h | 0 .../simplifier/datatype_simplifier_plugin.cpp | 0 .../simplifier/datatype_simplifier_plugin.h | 0 .../simplifier/distribute_forall.cpp | 0 src/{ => ast}/simplifier/distribute_forall.h | 0 src/{ => ast}/simplifier/elim_bounds.cpp | 0 src/{ => ast}/simplifier/elim_bounds.h | 0 src/{ => ast}/simplifier/inj_axiom.cpp | 0 src/{ => ast}/simplifier/inj_axiom.h | 0 .../simplifier/maximise_ac_sharing.cpp | 0 .../simplifier/maximise_ac_sharing.h | 0 .../simplifier/poly_simplifier_plugin.cpp | 0 .../simplifier/poly_simplifier_plugin.h | 0 src/{ => ast}/simplifier/pull_ite_tree.cpp | 0 src/{ => ast}/simplifier/pull_ite_tree.h | 0 src/{ => ast}/simplifier/push_app_ite.cpp | 0 src/{ => ast}/simplifier/push_app_ite.h | 0 src/{ => ast}/simplifier/simplifier.cpp | 0 src/{ => ast}/simplifier/simplifier.h | 0 .../simplifier/simplifier_plugin.cpp | 0 src/{ => ast}/simplifier/simplifier_plugin.h | 0 .../simplifier/theory_array_params.h | 0 src/{ => ast}/substitution/expr_offset.h | 0 src/{ => ast}/substitution/expr_offset_map.h | 0 src/{ => ast}/substitution/matcher.cpp | 0 src/{ => ast}/substitution/matcher.h | 0 src/{ => ast}/substitution/substitution.cpp | 0 src/{ => ast}/substitution/substitution.h | 0 .../substitution/substitution_tree.cpp | 0 .../substitution/substitution_tree.h | 0 src/{ => ast}/substitution/unifier.cpp | 0 src/{ => ast}/substitution/unifier.h | 0 src/{ => ast}/substitution/var_offset_map.h | 0 src/{ => tactic}/aig/aig.cpp | 0 src/{ => tactic}/aig/aig.h | 0 src/{ => tactic}/aig/aig_tactic.cpp | 0 src/{ => tactic}/aig/aig_tactic.h | 0 src/{ => tactic}/arith_tactics/add_bounds.cpp | 0 src/{ => tactic}/arith_tactics/add_bounds.h | 0 .../arith_tactics/add_bounds_tactic.cpp | 0 .../arith_tactics/add_bounds_tactic.h | 0 .../arith_tactics/bound_manager.cpp | 0 .../arith_tactics/bound_manager.h | 0 .../arith_tactics/bound_propagator.cpp | 0 .../arith_tactics/bound_propagator.h | 0 .../arith_tactics/bv2int_rewriter.cpp | 0 .../arith_tactics/bv2int_rewriter.h | 0 .../arith_tactics/bv2real_rewriter.cpp | 0 .../arith_tactics/bv2real_rewriter.h | 0 .../arith_tactics/degree_shift_tactic.cpp | 0 .../arith_tactics/degree_shift_tactic.h | 0 .../arith_tactics/diff_neq_tactic.cpp | 0 .../arith_tactics/diff_neq_tactic.h | 0 .../arith_tactics/elim_term_ite_strategy.cpp | 0 .../arith_tactics/elim_term_ite_strategy.h | 0 .../arith_tactics/factor_tactic.cpp | 0 .../arith_tactics/factor_tactic.h | 0 .../arith_tactics/fix_dl_var_tactic.cpp | 0 .../arith_tactics/fix_dl_var_tactic.h | 0 src/{ => tactic}/arith_tactics/fm_tactic.cpp | 0 src/{ => tactic}/arith_tactics/fm_tactic.h | 0 .../arith_tactics/lia2pb_tactic.cpp | 0 .../arith_tactics/lia2pb_tactic.h | 0 .../arith_tactics/linear_equation.cpp | 0 .../arith_tactics/linear_equation.h | 0 src/{ => tactic}/arith_tactics/lu.cpp | 0 src/{ => tactic}/arith_tactics/lu.h | 0 src/{ => tactic}/arith_tactics/mip_tactic.cpp | 0 src/{ => tactic}/arith_tactics/mip_tactic.h | 0 .../arith_tactics/nla2bv_tactic.cpp | 0 .../arith_tactics/nla2bv_tactic.h | 0 .../arith_tactics/normalize_bounds_tactic.cpp | 0 .../arith_tactics/normalize_bounds_tactic.h | 0 .../arith_tactics/pb2bv_model_converter.cpp | 0 .../arith_tactics/pb2bv_model_converter.h | 0 .../arith_tactics/pb2bv_tactic.cpp | 0 src/{ => tactic}/arith_tactics/pb2bv_tactic.h | 0 .../arith_tactics/probe_arith.cpp | 0 src/{ => tactic}/arith_tactics/probe_arith.h | 0 .../arith_tactics/propagate_ineqs_tactic.cpp | 0 .../arith_tactics/propagate_ineqs_tactic.h | 0 .../arith_tactics/purify_arith_tactic.cpp | 0 .../arith_tactics/purify_arith_tactic.h | 0 .../arith_tactics/recover_01_tactic.cpp | 0 .../arith_tactics/recover_01_tactic.h | 0 src/{ => tactic}/arith_tactics/smt_arith.cpp | 0 src/{ => tactic}/arith_tactics/smt_arith.h | 0 .../arith_tactics/smt_formula_compiler.cpp | 0 .../arith_tactics/smt_formula_compiler.h | 0 .../arith_tactics/smt_solver_exp.cpp | 0 .../arith_tactics/smt_solver_exp.h | 0 .../arith_tactics/smt_solver_strategy.cpp | 0 .../arith_tactics/smt_solver_strategy.h | 0 .../arith_tactics/smt_solver_types.h | 0 .../bit_blaster/bit_blaster.cpp | 0 src/{bv => tactic}/bit_blaster/bit_blaster.h | 0 .../bit_blaster_model_converter.cpp | 0 .../bit_blaster/bit_blaster_model_converter.h | 0 .../bit_blaster/bit_blaster_rewriter.cpp | 0 .../bit_blaster/bit_blaster_rewriter.h | 0 .../bit_blaster/bit_blaster_tpl.h | 0 .../bit_blaster/bit_blaster_tpl_def.h | 0 .../bit_blaster/bv1_blaster_tactic.cpp | 0 .../bit_blaster/bv1_blaster_tactic.h | 0 .../bit_blaster/eager_bit_blaster.cpp | 0 .../bit_blaster/eager_bit_blaster.h | 0 .../bv_tactics}/bit_blaster_tactic.cpp | 0 .../bv_tactics}/bit_blaster_tactic.h | 0 .../bv_tactics}/bv_size_reduction_tactic.cpp | 0 .../bv_tactics}/bv_size_reduction_tactic.h | 0 .../bv_tactics}/max_bv_sharing_tactic.cpp | 0 .../bv_tactics}/max_bv_sharing_tactic.h | 0 .../core_tactics/cofactor_elim_term_ite.cpp | 0 .../core_tactics/cofactor_elim_term_ite.h | 0 .../core_tactics/cofactor_term_ite_tactic.cpp | 0 .../core_tactics/cofactor_term_ite_tactic.h | 0 .../core_tactics/ctx_simplify_tactic.cpp | 0 .../core_tactics/ctx_simplify_tactic.h | 0 src/{ => tactic}/core_tactics/der_tactic.cpp | 0 src/{ => tactic}/core_tactics/der_tactic.h | 0 .../core_tactics/distribute_forall_tactic.cpp | 0 .../core_tactics/distribute_forall_tactic.h | 0 .../core_tactics/elim_term_ite_tactic.cpp | 0 .../core_tactics/elim_term_ite_tactic.h | 0 .../core_tactics/elim_uncnstr_tactic.cpp | 0 .../core_tactics/elim_uncnstr_tactic.h | 0 src/{ => tactic}/core_tactics/nnf_tactic.cpp | 0 src/{ => tactic}/core_tactics/nnf_tactic.h | 0 src/{ => tactic}/core_tactics/occf_tactic.cpp | 0 src/{ => tactic}/core_tactics/occf_tactic.h | 0 .../core_tactics/propagate_values_tactic.cpp | 0 .../core_tactics/propagate_values_tactic.h | 0 .../core_tactics/reduce_args_tactic.cpp | 0 .../core_tactics/reduce_args_tactic.h | 0 .../core_tactics/simplify_tactic.cpp | 0 .../core_tactics/simplify_tactic.h | 0 .../core_tactics/solve_eqs_tactic.cpp | 0 .../core_tactics/solve_eqs_tactic.h | 0 .../core_tactics/split_clause_tactic.cpp | 0 .../core_tactics/split_clause_tactic.h | 0 .../core_tactics/symmetry_reduce_tactic.cpp | 0 .../core_tactics/symmetry_reduce_tactic.h | 0 .../core_tactics/tseitin_cnf_tactic.cpp | 0 .../core_tactics/tseitin_cnf_tactic.h | 0 src/{ => tactic}/fpa/fpa2bv_converter.cpp | 0 src/{ => tactic}/fpa/fpa2bv_converter.h | 0 src/{ => tactic}/fpa/fpa2bv_tactic.cpp | 0 src/{ => tactic}/fpa/fpa2bv_tactic.h | 0 src/{ => tactic}/fpa/qffpa_tactic.cpp | 0 src/{ => tactic}/fpa/qffpa_tactic.h | 0 src/{ => tactic}/portfolio/default_tactic.cpp | 0 src/{ => tactic}/portfolio/default_tactic.h | 0 .../portfolio/install_tactics.cpp | 0 src/{ => tactic}/portfolio/install_tactics.h | 0 .../portfolio/smt_strategic_solver.cpp | 0 .../portfolio/smt_strategic_solver.h | 0 src/{bv => tactic}/sls_tactic/sls_strategy.h | 0 src/{bv => tactic}/sls_tactic/sls_tactic.cpp | 0 src/{bv => tactic}/sls_tactic/sls_tactic.h | 0 .../smtlogic_tactics/nra_tactic.cpp | 0 .../smtlogic_tactics/nra_tactic.h | 0 .../smtlogic_tactics/qfaufbv_tactic.cpp | 0 .../smtlogic_tactics/qfaufbv_tactic.h | 0 .../smtlogic_tactics/qfauflia_tactic.cpp | 0 .../smtlogic_tactics/qfauflia_tactic.h | 0 .../smtlogic_tactics/qfbv_tactic.cpp | 0 .../smtlogic_tactics/qfbv_tactic.h | 0 .../smtlogic_tactics/qfidl_tactic.cpp | 0 .../smtlogic_tactics/qfidl_tactic.h | 0 .../smtlogic_tactics/qflia_tactic.cpp | 0 .../smtlogic_tactics/qflia_tactic.h | 0 .../smtlogic_tactics/qflra_tactic.cpp | 0 .../smtlogic_tactics/qflra_tactic.h | 0 .../smtlogic_tactics/qfnia_tactic.cpp | 0 .../smtlogic_tactics/qfnia_tactic.h | 0 .../smtlogic_tactics/qfnra_tactic.cpp | 0 .../smtlogic_tactics/qfnra_tactic.h | 0 .../smtlogic_tactics/qfuf_tactic.cpp | 0 .../smtlogic_tactics/qfuf_tactic.h | 0 .../smtlogic_tactics/qfufbv_tactic.cpp | 0 .../smtlogic_tactics/qfufbv_tactic.h | 0 .../smtlogic_tactics/quant_tactics.cpp | 0 .../smtlogic_tactics/quant_tactics.h | 0 255 files changed, 17 insertions(+), 17 deletions(-) rename src/{bv => assertion_set}/ufbv_strategy/ufbv_strategy.cpp (100%) rename src/{bv => assertion_set}/ufbv_strategy/ufbv_strategy.h (100%) rename src/{ => ast}/array_property/array_property_expander.cpp (100%) rename src/{ => ast}/array_property/array_property_expander.h (100%) rename src/{ => ast}/array_property/array_property_recognizer.cpp (100%) rename src/{ => ast}/array_property/array_property_recognizer.h (100%) rename src/{ => ast}/macros/macro_finder.cpp (100%) rename src/{ => ast}/macros/macro_finder.h (100%) rename src/{ => ast}/macros/macro_manager.cpp (100%) rename src/{ => ast}/macros/macro_manager.h (100%) rename src/{ => ast}/macros/macro_substitution.cpp (100%) rename src/{ => ast}/macros/macro_substitution.h (100%) rename src/{ => ast}/macros/macro_util.cpp (100%) rename src/{ => ast}/macros/macro_util.h (100%) rename src/{ => ast}/macros/quasi_macros.cpp (100%) rename src/{ => ast}/macros/quasi_macros.h (100%) rename src/{ => ast}/pattern/pattern_inference.cpp (100%) rename src/{ => ast}/pattern/pattern_inference.h (100%) rename src/{ => ast}/proof_checker/proof_checker.cpp (100%) rename src/{ => ast}/proof_checker/proof_checker.h (100%) rename src/{ => ast}/rewriter/arith_rewriter.cpp (100%) rename src/{ => ast}/rewriter/arith_rewriter.h (100%) rename src/{ => ast}/rewriter/array_rewriter.cpp (100%) rename src/{ => ast}/rewriter/array_rewriter.h (100%) rename src/{ => ast}/rewriter/bool_rewriter.cpp (100%) rename src/{ => ast}/rewriter/bool_rewriter.h (100%) rename src/{ => ast}/rewriter/bv_rewriter.cpp (100%) rename src/{ => ast}/rewriter/bv_rewriter.h (100%) rename src/{ => ast}/rewriter/datatype_rewriter.cpp (100%) rename src/{ => ast}/rewriter/datatype_rewriter.h (100%) rename src/{ => ast}/rewriter/der.cpp (100%) rename src/{ => ast}/rewriter/der.h (100%) rename src/{ => ast}/rewriter/dl_rewriter.cpp (100%) rename src/{ => ast}/rewriter/dl_rewriter.h (100%) rename src/{ => ast}/rewriter/expr_replacer.cpp (100%) rename src/{ => ast}/rewriter/expr_replacer.h (100%) rename src/{ => ast}/rewriter/factor_rewriter.cpp (100%) rename src/{ => ast}/rewriter/factor_rewriter.h (100%) rename src/{ => ast}/rewriter/float_rewriter.cpp (100%) rename src/{ => ast}/rewriter/float_rewriter.h (100%) rename src/{ => ast}/rewriter/mk_simplified_app.cpp (100%) rename src/{ => ast}/rewriter/mk_simplified_app.h (100%) rename src/{ => ast}/rewriter/poly_rewriter.h (100%) rename src/{ => ast}/rewriter/poly_rewriter_def.h (100%) rename src/{ => ast}/rewriter/quant_hoist.cpp (100%) rename src/{ => ast}/rewriter/quant_hoist.h (100%) rename src/{ => ast}/rewriter/rewriter.cpp (100%) rename src/{ => ast}/rewriter/rewriter.h (100%) rename src/{ => ast}/rewriter/rewriter.txt (100%) rename src/{ => ast}/rewriter/rewriter_def.h (100%) rename src/{ => ast}/rewriter/rewriter_types.h (100%) rename src/{ => ast}/rewriter/th_rewriter.cpp (100%) rename src/{ => ast}/rewriter/th_rewriter.h (100%) rename src/{ => ast}/rewriter/var_subst.cpp (100%) rename src/{ => ast}/rewriter/var_subst.h (100%) rename src/{ => ast}/simplifier/README (100%) rename src/{ => ast}/simplifier/arith_simplifier_params.cpp (100%) rename src/{ => ast}/simplifier/arith_simplifier_params.h (100%) rename src/{ => ast}/simplifier/arith_simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/arith_simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/array_simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/array_simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/base_simplifier.h (100%) rename src/{ => ast}/simplifier/basic_simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/basic_simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/bit2int.cpp (100%) rename src/{ => ast}/simplifier/bit2int.h (100%) rename src/{ => ast}/simplifier/bv_elim.cpp (100%) rename src/{ => ast}/simplifier/bv_elim.h (100%) rename src/{ => ast}/simplifier/bv_simplifier_params.h (100%) rename src/{ => ast}/simplifier/bv_simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/bv_simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/datatype_simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/datatype_simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/distribute_forall.cpp (100%) rename src/{ => ast}/simplifier/distribute_forall.h (100%) rename src/{ => ast}/simplifier/elim_bounds.cpp (100%) rename src/{ => ast}/simplifier/elim_bounds.h (100%) rename src/{ => ast}/simplifier/inj_axiom.cpp (100%) rename src/{ => ast}/simplifier/inj_axiom.h (100%) rename src/{ => ast}/simplifier/maximise_ac_sharing.cpp (100%) rename src/{ => ast}/simplifier/maximise_ac_sharing.h (100%) rename src/{ => ast}/simplifier/poly_simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/poly_simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/pull_ite_tree.cpp (100%) rename src/{ => ast}/simplifier/pull_ite_tree.h (100%) rename src/{ => ast}/simplifier/push_app_ite.cpp (100%) rename src/{ => ast}/simplifier/push_app_ite.h (100%) rename src/{ => ast}/simplifier/simplifier.cpp (100%) rename src/{ => ast}/simplifier/simplifier.h (100%) rename src/{ => ast}/simplifier/simplifier_plugin.cpp (100%) rename src/{ => ast}/simplifier/simplifier_plugin.h (100%) rename src/{ => ast}/simplifier/theory_array_params.h (100%) rename src/{ => ast}/substitution/expr_offset.h (100%) rename src/{ => ast}/substitution/expr_offset_map.h (100%) rename src/{ => ast}/substitution/matcher.cpp (100%) rename src/{ => ast}/substitution/matcher.h (100%) rename src/{ => ast}/substitution/substitution.cpp (100%) rename src/{ => ast}/substitution/substitution.h (100%) rename src/{ => ast}/substitution/substitution_tree.cpp (100%) rename src/{ => ast}/substitution/substitution_tree.h (100%) rename src/{ => ast}/substitution/unifier.cpp (100%) rename src/{ => ast}/substitution/unifier.h (100%) rename src/{ => ast}/substitution/var_offset_map.h (100%) rename src/{ => tactic}/aig/aig.cpp (100%) rename src/{ => tactic}/aig/aig.h (100%) rename src/{ => tactic}/aig/aig_tactic.cpp (100%) rename src/{ => tactic}/aig/aig_tactic.h (100%) rename src/{ => tactic}/arith_tactics/add_bounds.cpp (100%) rename src/{ => tactic}/arith_tactics/add_bounds.h (100%) rename src/{ => tactic}/arith_tactics/add_bounds_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/add_bounds_tactic.h (100%) rename src/{ => tactic}/arith_tactics/bound_manager.cpp (100%) rename src/{ => tactic}/arith_tactics/bound_manager.h (100%) rename src/{ => tactic}/arith_tactics/bound_propagator.cpp (100%) rename src/{ => tactic}/arith_tactics/bound_propagator.h (100%) rename src/{ => tactic}/arith_tactics/bv2int_rewriter.cpp (100%) rename src/{ => tactic}/arith_tactics/bv2int_rewriter.h (100%) rename src/{ => tactic}/arith_tactics/bv2real_rewriter.cpp (100%) rename src/{ => tactic}/arith_tactics/bv2real_rewriter.h (100%) rename src/{ => tactic}/arith_tactics/degree_shift_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/degree_shift_tactic.h (100%) rename src/{ => tactic}/arith_tactics/diff_neq_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/diff_neq_tactic.h (100%) rename src/{ => tactic}/arith_tactics/elim_term_ite_strategy.cpp (100%) rename src/{ => tactic}/arith_tactics/elim_term_ite_strategy.h (100%) rename src/{ => tactic}/arith_tactics/factor_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/factor_tactic.h (100%) rename src/{ => tactic}/arith_tactics/fix_dl_var_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/fix_dl_var_tactic.h (100%) rename src/{ => tactic}/arith_tactics/fm_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/fm_tactic.h (100%) rename src/{ => tactic}/arith_tactics/lia2pb_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/lia2pb_tactic.h (100%) rename src/{ => tactic}/arith_tactics/linear_equation.cpp (100%) rename src/{ => tactic}/arith_tactics/linear_equation.h (100%) rename src/{ => tactic}/arith_tactics/lu.cpp (100%) rename src/{ => tactic}/arith_tactics/lu.h (100%) rename src/{ => tactic}/arith_tactics/mip_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/mip_tactic.h (100%) rename src/{ => tactic}/arith_tactics/nla2bv_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/nla2bv_tactic.h (100%) rename src/{ => tactic}/arith_tactics/normalize_bounds_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/normalize_bounds_tactic.h (100%) rename src/{ => tactic}/arith_tactics/pb2bv_model_converter.cpp (100%) rename src/{ => tactic}/arith_tactics/pb2bv_model_converter.h (100%) rename src/{ => tactic}/arith_tactics/pb2bv_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/pb2bv_tactic.h (100%) rename src/{ => tactic}/arith_tactics/probe_arith.cpp (100%) rename src/{ => tactic}/arith_tactics/probe_arith.h (100%) rename src/{ => tactic}/arith_tactics/propagate_ineqs_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/propagate_ineqs_tactic.h (100%) rename src/{ => tactic}/arith_tactics/purify_arith_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/purify_arith_tactic.h (100%) rename src/{ => tactic}/arith_tactics/recover_01_tactic.cpp (100%) rename src/{ => tactic}/arith_tactics/recover_01_tactic.h (100%) rename src/{ => tactic}/arith_tactics/smt_arith.cpp (100%) rename src/{ => tactic}/arith_tactics/smt_arith.h (100%) rename src/{ => tactic}/arith_tactics/smt_formula_compiler.cpp (100%) rename src/{ => tactic}/arith_tactics/smt_formula_compiler.h (100%) rename src/{ => tactic}/arith_tactics/smt_solver_exp.cpp (100%) rename src/{ => tactic}/arith_tactics/smt_solver_exp.h (100%) rename src/{ => tactic}/arith_tactics/smt_solver_strategy.cpp (100%) rename src/{ => tactic}/arith_tactics/smt_solver_strategy.h (100%) rename src/{ => tactic}/arith_tactics/smt_solver_types.h (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster.cpp (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster.h (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster_model_converter.cpp (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster_model_converter.h (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster_rewriter.cpp (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster_rewriter.h (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster_tpl.h (100%) rename src/{bv => tactic}/bit_blaster/bit_blaster_tpl_def.h (100%) rename src/{bv => tactic}/bit_blaster/bv1_blaster_tactic.cpp (100%) rename src/{bv => tactic}/bit_blaster/bv1_blaster_tactic.h (100%) rename src/{bv => tactic}/bit_blaster/eager_bit_blaster.cpp (100%) rename src/{bv => tactic}/bit_blaster/eager_bit_blaster.h (100%) rename src/{bv/tactics => tactic/bv_tactics}/bit_blaster_tactic.cpp (100%) rename src/{bv/tactics => tactic/bv_tactics}/bit_blaster_tactic.h (100%) rename src/{bv/tactics => tactic/bv_tactics}/bv_size_reduction_tactic.cpp (100%) rename src/{bv/tactics => tactic/bv_tactics}/bv_size_reduction_tactic.h (100%) rename src/{bv/tactics => tactic/bv_tactics}/max_bv_sharing_tactic.cpp (100%) rename src/{bv/tactics => tactic/bv_tactics}/max_bv_sharing_tactic.h (100%) rename src/{ => tactic}/core_tactics/cofactor_elim_term_ite.cpp (100%) rename src/{ => tactic}/core_tactics/cofactor_elim_term_ite.h (100%) rename src/{ => tactic}/core_tactics/cofactor_term_ite_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/cofactor_term_ite_tactic.h (100%) rename src/{ => tactic}/core_tactics/ctx_simplify_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/ctx_simplify_tactic.h (100%) rename src/{ => tactic}/core_tactics/der_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/der_tactic.h (100%) rename src/{ => tactic}/core_tactics/distribute_forall_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/distribute_forall_tactic.h (100%) rename src/{ => tactic}/core_tactics/elim_term_ite_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/elim_term_ite_tactic.h (100%) rename src/{ => tactic}/core_tactics/elim_uncnstr_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/elim_uncnstr_tactic.h (100%) rename src/{ => tactic}/core_tactics/nnf_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/nnf_tactic.h (100%) rename src/{ => tactic}/core_tactics/occf_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/occf_tactic.h (100%) rename src/{ => tactic}/core_tactics/propagate_values_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/propagate_values_tactic.h (100%) rename src/{ => tactic}/core_tactics/reduce_args_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/reduce_args_tactic.h (100%) rename src/{ => tactic}/core_tactics/simplify_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/simplify_tactic.h (100%) rename src/{ => tactic}/core_tactics/solve_eqs_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/solve_eqs_tactic.h (100%) rename src/{ => tactic}/core_tactics/split_clause_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/split_clause_tactic.h (100%) rename src/{ => tactic}/core_tactics/symmetry_reduce_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/symmetry_reduce_tactic.h (100%) rename src/{ => tactic}/core_tactics/tseitin_cnf_tactic.cpp (100%) rename src/{ => tactic}/core_tactics/tseitin_cnf_tactic.h (100%) rename src/{ => tactic}/fpa/fpa2bv_converter.cpp (100%) rename src/{ => tactic}/fpa/fpa2bv_converter.h (100%) rename src/{ => tactic}/fpa/fpa2bv_tactic.cpp (100%) rename src/{ => tactic}/fpa/fpa2bv_tactic.h (100%) rename src/{ => tactic}/fpa/qffpa_tactic.cpp (100%) rename src/{ => tactic}/fpa/qffpa_tactic.h (100%) rename src/{ => tactic}/portfolio/default_tactic.cpp (100%) rename src/{ => tactic}/portfolio/default_tactic.h (100%) rename src/{ => tactic}/portfolio/install_tactics.cpp (100%) rename src/{ => tactic}/portfolio/install_tactics.h (100%) rename src/{ => tactic}/portfolio/smt_strategic_solver.cpp (100%) rename src/{ => tactic}/portfolio/smt_strategic_solver.h (100%) rename src/{bv => tactic}/sls_tactic/sls_strategy.h (100%) rename src/{bv => tactic}/sls_tactic/sls_tactic.cpp (100%) rename src/{bv => tactic}/sls_tactic/sls_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/nra_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/nra_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfaufbv_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfaufbv_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfauflia_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfauflia_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfbv_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfbv_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfidl_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfidl_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qflia_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qflia_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qflra_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qflra_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfnia_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfnia_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfnra_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfnra_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfuf_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfuf_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/qfufbv_tactic.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/qfufbv_tactic.h (100%) rename src/{ => tactic}/smtlogic_tactics/quant_tactics.cpp (100%) rename src/{ => tactic}/smtlogic_tactics/quant_tactics.h (100%) diff --git a/scripts/mk_make.py b/scripts/mk_make.py index e260d99c7..81f4d848f 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -25,10 +25,10 @@ add_lib('sat', ['util']) add_lib('nlsat', ['polynomial', 'sat']) add_lib('subpaving', ['util'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) -add_lib('rewriter', ['ast', 'polynomial']) +add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter') # Simplifier module will be deleted in the future. # It has been replaced with rewriter module. -add_lib('simplifier', ['rewriter']) +add_lib('simplifier', ['rewriter'], 'ast/simplifier') # Model module should not depend on simplifier module. # We must replace all occurrences of simplifier with rewriter. add_lib('model', ['rewriter', 'simplifier']) @@ -40,42 +40,42 @@ add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier # Assertion set is the old tactic framework used in Z3 3.x. It will be deleted as soon as we finish the porting old # code to the new tactic framework. add_lib('assertion_set', ['cmd_context']) -add_lib('substitution', ['ast']) +add_lib('substitution', ['ast'], 'ast/substitution') add_lib('normal_forms', ['tactic', 'assertion_set']) -add_lib('pattern', ['normal_forms']) +add_lib('pattern', ['normal_forms'], 'ast/pattern') add_lib('spc', ['simplifier', 'substitution', 'old_params', 'pattern']) add_lib('parser_util', ['ast']) add_lib('smt2parser', ['cmd_context', 'parser_util']) -add_lib('macros', ['simplifier', 'old_params']) +add_lib('macros', ['simplifier', 'old_params'], 'ast/macros') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') -add_lib('proof_checker', ['rewriter', 'spc']) -add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic', 'assertion_set'], 'bv/bit_blaster') +add_lib('proof_checker', ['rewriter', 'spc'], 'ast/proof_checker') +add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic', 'assertion_set'], 'tactic/bit_blaster') add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) add_lib('user_plugin', ['smt'], 'smt/user_plugin') -add_lib('core_tactics', ['tactic', 'normal_forms']) +add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core_tactics') add_lib('sat_tactic', ['tactic', 'sat'], 'sat/tactic') add_lib('sat_strategy', ['assertion_set', 'sat_tactic'], 'sat/strategy') -add_lib('arith_tactics', ['core_tactics', 'assertion_set', 'sat', 'sat_strategy']) +add_lib('arith_tactics', ['core_tactics', 'assertion_set', 'sat', 'sat_strategy'], 'tactic/arith_tactics') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') -add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'bv/tactics') +add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv_tactics') add_lib('fuzzing', ['ast'], 'test/fuzzing') -add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic']) +add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') -add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'bv/sls_tactic') -add_lib('aig', ['cmd_context', 'assertion_set']) +add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls_tactic') +add_lib('aig', ['cmd_context', 'assertion_set'], 'tactic/aig') # TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr. add_lib('muz_qe', ['smt', 'sat', 'smt2parser']) -add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe']) +add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogic_tactics') # TODO: rewrite ufbv_strategy as a tactic and move to smtlogic_tactics. -add_lib('ufbv_strategy', ['assertion_set', 'normal_forms', 'macros', 'smt_tactic', 'rewriter'], 'bv/ufbv_strategy') -add_lib('portfolio', ['smtlogic_tactics', 'ufbv_strategy', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic']) +add_lib('ufbv_strategy', ['assertion_set', 'normal_forms', 'macros', 'smt_tactic', 'rewriter'], 'assertion_set/ufbv_strategy') +add_lib('portfolio', ['smtlogic_tactics', 'ufbv_strategy', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') # TODO: delete SMT 1.0 frontend add_lib('api', ['portfolio', 'user_plugin']) -add_lib('array_property', ['ast', 'rewriter']) +add_lib('array_property', ['ast', 'rewriter'], 'ast/array_property') add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'array_property'], exe_name='test-z3') diff --git a/src/bv/ufbv_strategy/ufbv_strategy.cpp b/src/assertion_set/ufbv_strategy/ufbv_strategy.cpp similarity index 100% rename from src/bv/ufbv_strategy/ufbv_strategy.cpp rename to src/assertion_set/ufbv_strategy/ufbv_strategy.cpp diff --git a/src/bv/ufbv_strategy/ufbv_strategy.h b/src/assertion_set/ufbv_strategy/ufbv_strategy.h similarity index 100% rename from src/bv/ufbv_strategy/ufbv_strategy.h rename to src/assertion_set/ufbv_strategy/ufbv_strategy.h diff --git a/src/array_property/array_property_expander.cpp b/src/ast/array_property/array_property_expander.cpp similarity index 100% rename from src/array_property/array_property_expander.cpp rename to src/ast/array_property/array_property_expander.cpp diff --git a/src/array_property/array_property_expander.h b/src/ast/array_property/array_property_expander.h similarity index 100% rename from src/array_property/array_property_expander.h rename to src/ast/array_property/array_property_expander.h diff --git a/src/array_property/array_property_recognizer.cpp b/src/ast/array_property/array_property_recognizer.cpp similarity index 100% rename from src/array_property/array_property_recognizer.cpp rename to src/ast/array_property/array_property_recognizer.cpp diff --git a/src/array_property/array_property_recognizer.h b/src/ast/array_property/array_property_recognizer.h similarity index 100% rename from src/array_property/array_property_recognizer.h rename to src/ast/array_property/array_property_recognizer.h diff --git a/src/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp similarity index 100% rename from src/macros/macro_finder.cpp rename to src/ast/macros/macro_finder.cpp diff --git a/src/macros/macro_finder.h b/src/ast/macros/macro_finder.h similarity index 100% rename from src/macros/macro_finder.h rename to src/ast/macros/macro_finder.h diff --git a/src/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp similarity index 100% rename from src/macros/macro_manager.cpp rename to src/ast/macros/macro_manager.cpp diff --git a/src/macros/macro_manager.h b/src/ast/macros/macro_manager.h similarity index 100% rename from src/macros/macro_manager.h rename to src/ast/macros/macro_manager.h diff --git a/src/macros/macro_substitution.cpp b/src/ast/macros/macro_substitution.cpp similarity index 100% rename from src/macros/macro_substitution.cpp rename to src/ast/macros/macro_substitution.cpp diff --git a/src/macros/macro_substitution.h b/src/ast/macros/macro_substitution.h similarity index 100% rename from src/macros/macro_substitution.h rename to src/ast/macros/macro_substitution.h diff --git a/src/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp similarity index 100% rename from src/macros/macro_util.cpp rename to src/ast/macros/macro_util.cpp diff --git a/src/macros/macro_util.h b/src/ast/macros/macro_util.h similarity index 100% rename from src/macros/macro_util.h rename to src/ast/macros/macro_util.h diff --git a/src/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp similarity index 100% rename from src/macros/quasi_macros.cpp rename to src/ast/macros/quasi_macros.cpp diff --git a/src/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h similarity index 100% rename from src/macros/quasi_macros.h rename to src/ast/macros/quasi_macros.h diff --git a/src/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp similarity index 100% rename from src/pattern/pattern_inference.cpp rename to src/ast/pattern/pattern_inference.cpp diff --git a/src/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h similarity index 100% rename from src/pattern/pattern_inference.h rename to src/ast/pattern/pattern_inference.h diff --git a/src/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp similarity index 100% rename from src/proof_checker/proof_checker.cpp rename to src/ast/proof_checker/proof_checker.cpp diff --git a/src/proof_checker/proof_checker.h b/src/ast/proof_checker/proof_checker.h similarity index 100% rename from src/proof_checker/proof_checker.h rename to src/ast/proof_checker/proof_checker.h diff --git a/src/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp similarity index 100% rename from src/rewriter/arith_rewriter.cpp rename to src/ast/rewriter/arith_rewriter.cpp diff --git a/src/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h similarity index 100% rename from src/rewriter/arith_rewriter.h rename to src/ast/rewriter/arith_rewriter.h diff --git a/src/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp similarity index 100% rename from src/rewriter/array_rewriter.cpp rename to src/ast/rewriter/array_rewriter.cpp diff --git a/src/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h similarity index 100% rename from src/rewriter/array_rewriter.h rename to src/ast/rewriter/array_rewriter.h diff --git a/src/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp similarity index 100% rename from src/rewriter/bool_rewriter.cpp rename to src/ast/rewriter/bool_rewriter.cpp diff --git a/src/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h similarity index 100% rename from src/rewriter/bool_rewriter.h rename to src/ast/rewriter/bool_rewriter.h diff --git a/src/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp similarity index 100% rename from src/rewriter/bv_rewriter.cpp rename to src/ast/rewriter/bv_rewriter.cpp diff --git a/src/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h similarity index 100% rename from src/rewriter/bv_rewriter.h rename to src/ast/rewriter/bv_rewriter.h diff --git a/src/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp similarity index 100% rename from src/rewriter/datatype_rewriter.cpp rename to src/ast/rewriter/datatype_rewriter.cpp diff --git a/src/rewriter/datatype_rewriter.h b/src/ast/rewriter/datatype_rewriter.h similarity index 100% rename from src/rewriter/datatype_rewriter.h rename to src/ast/rewriter/datatype_rewriter.h diff --git a/src/rewriter/der.cpp b/src/ast/rewriter/der.cpp similarity index 100% rename from src/rewriter/der.cpp rename to src/ast/rewriter/der.cpp diff --git a/src/rewriter/der.h b/src/ast/rewriter/der.h similarity index 100% rename from src/rewriter/der.h rename to src/ast/rewriter/der.h diff --git a/src/rewriter/dl_rewriter.cpp b/src/ast/rewriter/dl_rewriter.cpp similarity index 100% rename from src/rewriter/dl_rewriter.cpp rename to src/ast/rewriter/dl_rewriter.cpp diff --git a/src/rewriter/dl_rewriter.h b/src/ast/rewriter/dl_rewriter.h similarity index 100% rename from src/rewriter/dl_rewriter.h rename to src/ast/rewriter/dl_rewriter.h diff --git a/src/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp similarity index 100% rename from src/rewriter/expr_replacer.cpp rename to src/ast/rewriter/expr_replacer.cpp diff --git a/src/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h similarity index 100% rename from src/rewriter/expr_replacer.h rename to src/ast/rewriter/expr_replacer.h diff --git a/src/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp similarity index 100% rename from src/rewriter/factor_rewriter.cpp rename to src/ast/rewriter/factor_rewriter.cpp diff --git a/src/rewriter/factor_rewriter.h b/src/ast/rewriter/factor_rewriter.h similarity index 100% rename from src/rewriter/factor_rewriter.h rename to src/ast/rewriter/factor_rewriter.h diff --git a/src/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp similarity index 100% rename from src/rewriter/float_rewriter.cpp rename to src/ast/rewriter/float_rewriter.cpp diff --git a/src/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h similarity index 100% rename from src/rewriter/float_rewriter.h rename to src/ast/rewriter/float_rewriter.h diff --git a/src/rewriter/mk_simplified_app.cpp b/src/ast/rewriter/mk_simplified_app.cpp similarity index 100% rename from src/rewriter/mk_simplified_app.cpp rename to src/ast/rewriter/mk_simplified_app.cpp diff --git a/src/rewriter/mk_simplified_app.h b/src/ast/rewriter/mk_simplified_app.h similarity index 100% rename from src/rewriter/mk_simplified_app.h rename to src/ast/rewriter/mk_simplified_app.h diff --git a/src/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h similarity index 100% rename from src/rewriter/poly_rewriter.h rename to src/ast/rewriter/poly_rewriter.h diff --git a/src/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h similarity index 100% rename from src/rewriter/poly_rewriter_def.h rename to src/ast/rewriter/poly_rewriter_def.h diff --git a/src/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp similarity index 100% rename from src/rewriter/quant_hoist.cpp rename to src/ast/rewriter/quant_hoist.cpp diff --git a/src/rewriter/quant_hoist.h b/src/ast/rewriter/quant_hoist.h similarity index 100% rename from src/rewriter/quant_hoist.h rename to src/ast/rewriter/quant_hoist.h diff --git a/src/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp similarity index 100% rename from src/rewriter/rewriter.cpp rename to src/ast/rewriter/rewriter.cpp diff --git a/src/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h similarity index 100% rename from src/rewriter/rewriter.h rename to src/ast/rewriter/rewriter.h diff --git a/src/rewriter/rewriter.txt b/src/ast/rewriter/rewriter.txt similarity index 100% rename from src/rewriter/rewriter.txt rename to src/ast/rewriter/rewriter.txt diff --git a/src/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h similarity index 100% rename from src/rewriter/rewriter_def.h rename to src/ast/rewriter/rewriter_def.h diff --git a/src/rewriter/rewriter_types.h b/src/ast/rewriter/rewriter_types.h similarity index 100% rename from src/rewriter/rewriter_types.h rename to src/ast/rewriter/rewriter_types.h diff --git a/src/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp similarity index 100% rename from src/rewriter/th_rewriter.cpp rename to src/ast/rewriter/th_rewriter.cpp diff --git a/src/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h similarity index 100% rename from src/rewriter/th_rewriter.h rename to src/ast/rewriter/th_rewriter.h diff --git a/src/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp similarity index 100% rename from src/rewriter/var_subst.cpp rename to src/ast/rewriter/var_subst.cpp diff --git a/src/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h similarity index 100% rename from src/rewriter/var_subst.h rename to src/ast/rewriter/var_subst.h diff --git a/src/simplifier/README b/src/ast/simplifier/README similarity index 100% rename from src/simplifier/README rename to src/ast/simplifier/README diff --git a/src/simplifier/arith_simplifier_params.cpp b/src/ast/simplifier/arith_simplifier_params.cpp similarity index 100% rename from src/simplifier/arith_simplifier_params.cpp rename to src/ast/simplifier/arith_simplifier_params.cpp diff --git a/src/simplifier/arith_simplifier_params.h b/src/ast/simplifier/arith_simplifier_params.h similarity index 100% rename from src/simplifier/arith_simplifier_params.h rename to src/ast/simplifier/arith_simplifier_params.h diff --git a/src/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp similarity index 100% rename from src/simplifier/arith_simplifier_plugin.cpp rename to src/ast/simplifier/arith_simplifier_plugin.cpp diff --git a/src/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h similarity index 100% rename from src/simplifier/arith_simplifier_plugin.h rename to src/ast/simplifier/arith_simplifier_plugin.h diff --git a/src/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp similarity index 100% rename from src/simplifier/array_simplifier_plugin.cpp rename to src/ast/simplifier/array_simplifier_plugin.cpp diff --git a/src/simplifier/array_simplifier_plugin.h b/src/ast/simplifier/array_simplifier_plugin.h similarity index 100% rename from src/simplifier/array_simplifier_plugin.h rename to src/ast/simplifier/array_simplifier_plugin.h diff --git a/src/simplifier/base_simplifier.h b/src/ast/simplifier/base_simplifier.h similarity index 100% rename from src/simplifier/base_simplifier.h rename to src/ast/simplifier/base_simplifier.h diff --git a/src/simplifier/basic_simplifier_plugin.cpp b/src/ast/simplifier/basic_simplifier_plugin.cpp similarity index 100% rename from src/simplifier/basic_simplifier_plugin.cpp rename to src/ast/simplifier/basic_simplifier_plugin.cpp diff --git a/src/simplifier/basic_simplifier_plugin.h b/src/ast/simplifier/basic_simplifier_plugin.h similarity index 100% rename from src/simplifier/basic_simplifier_plugin.h rename to src/ast/simplifier/basic_simplifier_plugin.h diff --git a/src/simplifier/bit2int.cpp b/src/ast/simplifier/bit2int.cpp similarity index 100% rename from src/simplifier/bit2int.cpp rename to src/ast/simplifier/bit2int.cpp diff --git a/src/simplifier/bit2int.h b/src/ast/simplifier/bit2int.h similarity index 100% rename from src/simplifier/bit2int.h rename to src/ast/simplifier/bit2int.h diff --git a/src/simplifier/bv_elim.cpp b/src/ast/simplifier/bv_elim.cpp similarity index 100% rename from src/simplifier/bv_elim.cpp rename to src/ast/simplifier/bv_elim.cpp diff --git a/src/simplifier/bv_elim.h b/src/ast/simplifier/bv_elim.h similarity index 100% rename from src/simplifier/bv_elim.h rename to src/ast/simplifier/bv_elim.h diff --git a/src/simplifier/bv_simplifier_params.h b/src/ast/simplifier/bv_simplifier_params.h similarity index 100% rename from src/simplifier/bv_simplifier_params.h rename to src/ast/simplifier/bv_simplifier_params.h diff --git a/src/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp similarity index 100% rename from src/simplifier/bv_simplifier_plugin.cpp rename to src/ast/simplifier/bv_simplifier_plugin.cpp diff --git a/src/simplifier/bv_simplifier_plugin.h b/src/ast/simplifier/bv_simplifier_plugin.h similarity index 100% rename from src/simplifier/bv_simplifier_plugin.h rename to src/ast/simplifier/bv_simplifier_plugin.h diff --git a/src/simplifier/datatype_simplifier_plugin.cpp b/src/ast/simplifier/datatype_simplifier_plugin.cpp similarity index 100% rename from src/simplifier/datatype_simplifier_plugin.cpp rename to src/ast/simplifier/datatype_simplifier_plugin.cpp diff --git a/src/simplifier/datatype_simplifier_plugin.h b/src/ast/simplifier/datatype_simplifier_plugin.h similarity index 100% rename from src/simplifier/datatype_simplifier_plugin.h rename to src/ast/simplifier/datatype_simplifier_plugin.h diff --git a/src/simplifier/distribute_forall.cpp b/src/ast/simplifier/distribute_forall.cpp similarity index 100% rename from src/simplifier/distribute_forall.cpp rename to src/ast/simplifier/distribute_forall.cpp diff --git a/src/simplifier/distribute_forall.h b/src/ast/simplifier/distribute_forall.h similarity index 100% rename from src/simplifier/distribute_forall.h rename to src/ast/simplifier/distribute_forall.h diff --git a/src/simplifier/elim_bounds.cpp b/src/ast/simplifier/elim_bounds.cpp similarity index 100% rename from src/simplifier/elim_bounds.cpp rename to src/ast/simplifier/elim_bounds.cpp diff --git a/src/simplifier/elim_bounds.h b/src/ast/simplifier/elim_bounds.h similarity index 100% rename from src/simplifier/elim_bounds.h rename to src/ast/simplifier/elim_bounds.h diff --git a/src/simplifier/inj_axiom.cpp b/src/ast/simplifier/inj_axiom.cpp similarity index 100% rename from src/simplifier/inj_axiom.cpp rename to src/ast/simplifier/inj_axiom.cpp diff --git a/src/simplifier/inj_axiom.h b/src/ast/simplifier/inj_axiom.h similarity index 100% rename from src/simplifier/inj_axiom.h rename to src/ast/simplifier/inj_axiom.h diff --git a/src/simplifier/maximise_ac_sharing.cpp b/src/ast/simplifier/maximise_ac_sharing.cpp similarity index 100% rename from src/simplifier/maximise_ac_sharing.cpp rename to src/ast/simplifier/maximise_ac_sharing.cpp diff --git a/src/simplifier/maximise_ac_sharing.h b/src/ast/simplifier/maximise_ac_sharing.h similarity index 100% rename from src/simplifier/maximise_ac_sharing.h rename to src/ast/simplifier/maximise_ac_sharing.h diff --git a/src/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp similarity index 100% rename from src/simplifier/poly_simplifier_plugin.cpp rename to src/ast/simplifier/poly_simplifier_plugin.cpp diff --git a/src/simplifier/poly_simplifier_plugin.h b/src/ast/simplifier/poly_simplifier_plugin.h similarity index 100% rename from src/simplifier/poly_simplifier_plugin.h rename to src/ast/simplifier/poly_simplifier_plugin.h diff --git a/src/simplifier/pull_ite_tree.cpp b/src/ast/simplifier/pull_ite_tree.cpp similarity index 100% rename from src/simplifier/pull_ite_tree.cpp rename to src/ast/simplifier/pull_ite_tree.cpp diff --git a/src/simplifier/pull_ite_tree.h b/src/ast/simplifier/pull_ite_tree.h similarity index 100% rename from src/simplifier/pull_ite_tree.h rename to src/ast/simplifier/pull_ite_tree.h diff --git a/src/simplifier/push_app_ite.cpp b/src/ast/simplifier/push_app_ite.cpp similarity index 100% rename from src/simplifier/push_app_ite.cpp rename to src/ast/simplifier/push_app_ite.cpp diff --git a/src/simplifier/push_app_ite.h b/src/ast/simplifier/push_app_ite.h similarity index 100% rename from src/simplifier/push_app_ite.h rename to src/ast/simplifier/push_app_ite.h diff --git a/src/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp similarity index 100% rename from src/simplifier/simplifier.cpp rename to src/ast/simplifier/simplifier.cpp diff --git a/src/simplifier/simplifier.h b/src/ast/simplifier/simplifier.h similarity index 100% rename from src/simplifier/simplifier.h rename to src/ast/simplifier/simplifier.h diff --git a/src/simplifier/simplifier_plugin.cpp b/src/ast/simplifier/simplifier_plugin.cpp similarity index 100% rename from src/simplifier/simplifier_plugin.cpp rename to src/ast/simplifier/simplifier_plugin.cpp diff --git a/src/simplifier/simplifier_plugin.h b/src/ast/simplifier/simplifier_plugin.h similarity index 100% rename from src/simplifier/simplifier_plugin.h rename to src/ast/simplifier/simplifier_plugin.h diff --git a/src/simplifier/theory_array_params.h b/src/ast/simplifier/theory_array_params.h similarity index 100% rename from src/simplifier/theory_array_params.h rename to src/ast/simplifier/theory_array_params.h diff --git a/src/substitution/expr_offset.h b/src/ast/substitution/expr_offset.h similarity index 100% rename from src/substitution/expr_offset.h rename to src/ast/substitution/expr_offset.h diff --git a/src/substitution/expr_offset_map.h b/src/ast/substitution/expr_offset_map.h similarity index 100% rename from src/substitution/expr_offset_map.h rename to src/ast/substitution/expr_offset_map.h diff --git a/src/substitution/matcher.cpp b/src/ast/substitution/matcher.cpp similarity index 100% rename from src/substitution/matcher.cpp rename to src/ast/substitution/matcher.cpp diff --git a/src/substitution/matcher.h b/src/ast/substitution/matcher.h similarity index 100% rename from src/substitution/matcher.h rename to src/ast/substitution/matcher.h diff --git a/src/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp similarity index 100% rename from src/substitution/substitution.cpp rename to src/ast/substitution/substitution.cpp diff --git a/src/substitution/substitution.h b/src/ast/substitution/substitution.h similarity index 100% rename from src/substitution/substitution.h rename to src/ast/substitution/substitution.h diff --git a/src/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp similarity index 100% rename from src/substitution/substitution_tree.cpp rename to src/ast/substitution/substitution_tree.cpp diff --git a/src/substitution/substitution_tree.h b/src/ast/substitution/substitution_tree.h similarity index 100% rename from src/substitution/substitution_tree.h rename to src/ast/substitution/substitution_tree.h diff --git a/src/substitution/unifier.cpp b/src/ast/substitution/unifier.cpp similarity index 100% rename from src/substitution/unifier.cpp rename to src/ast/substitution/unifier.cpp diff --git a/src/substitution/unifier.h b/src/ast/substitution/unifier.h similarity index 100% rename from src/substitution/unifier.h rename to src/ast/substitution/unifier.h diff --git a/src/substitution/var_offset_map.h b/src/ast/substitution/var_offset_map.h similarity index 100% rename from src/substitution/var_offset_map.h rename to src/ast/substitution/var_offset_map.h diff --git a/src/aig/aig.cpp b/src/tactic/aig/aig.cpp similarity index 100% rename from src/aig/aig.cpp rename to src/tactic/aig/aig.cpp diff --git a/src/aig/aig.h b/src/tactic/aig/aig.h similarity index 100% rename from src/aig/aig.h rename to src/tactic/aig/aig.h diff --git a/src/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp similarity index 100% rename from src/aig/aig_tactic.cpp rename to src/tactic/aig/aig_tactic.cpp diff --git a/src/aig/aig_tactic.h b/src/tactic/aig/aig_tactic.h similarity index 100% rename from src/aig/aig_tactic.h rename to src/tactic/aig/aig_tactic.h diff --git a/src/arith_tactics/add_bounds.cpp b/src/tactic/arith_tactics/add_bounds.cpp similarity index 100% rename from src/arith_tactics/add_bounds.cpp rename to src/tactic/arith_tactics/add_bounds.cpp diff --git a/src/arith_tactics/add_bounds.h b/src/tactic/arith_tactics/add_bounds.h similarity index 100% rename from src/arith_tactics/add_bounds.h rename to src/tactic/arith_tactics/add_bounds.h diff --git a/src/arith_tactics/add_bounds_tactic.cpp b/src/tactic/arith_tactics/add_bounds_tactic.cpp similarity index 100% rename from src/arith_tactics/add_bounds_tactic.cpp rename to src/tactic/arith_tactics/add_bounds_tactic.cpp diff --git a/src/arith_tactics/add_bounds_tactic.h b/src/tactic/arith_tactics/add_bounds_tactic.h similarity index 100% rename from src/arith_tactics/add_bounds_tactic.h rename to src/tactic/arith_tactics/add_bounds_tactic.h diff --git a/src/arith_tactics/bound_manager.cpp b/src/tactic/arith_tactics/bound_manager.cpp similarity index 100% rename from src/arith_tactics/bound_manager.cpp rename to src/tactic/arith_tactics/bound_manager.cpp diff --git a/src/arith_tactics/bound_manager.h b/src/tactic/arith_tactics/bound_manager.h similarity index 100% rename from src/arith_tactics/bound_manager.h rename to src/tactic/arith_tactics/bound_manager.h diff --git a/src/arith_tactics/bound_propagator.cpp b/src/tactic/arith_tactics/bound_propagator.cpp similarity index 100% rename from src/arith_tactics/bound_propagator.cpp rename to src/tactic/arith_tactics/bound_propagator.cpp diff --git a/src/arith_tactics/bound_propagator.h b/src/tactic/arith_tactics/bound_propagator.h similarity index 100% rename from src/arith_tactics/bound_propagator.h rename to src/tactic/arith_tactics/bound_propagator.h diff --git a/src/arith_tactics/bv2int_rewriter.cpp b/src/tactic/arith_tactics/bv2int_rewriter.cpp similarity index 100% rename from src/arith_tactics/bv2int_rewriter.cpp rename to src/tactic/arith_tactics/bv2int_rewriter.cpp diff --git a/src/arith_tactics/bv2int_rewriter.h b/src/tactic/arith_tactics/bv2int_rewriter.h similarity index 100% rename from src/arith_tactics/bv2int_rewriter.h rename to src/tactic/arith_tactics/bv2int_rewriter.h diff --git a/src/arith_tactics/bv2real_rewriter.cpp b/src/tactic/arith_tactics/bv2real_rewriter.cpp similarity index 100% rename from src/arith_tactics/bv2real_rewriter.cpp rename to src/tactic/arith_tactics/bv2real_rewriter.cpp diff --git a/src/arith_tactics/bv2real_rewriter.h b/src/tactic/arith_tactics/bv2real_rewriter.h similarity index 100% rename from src/arith_tactics/bv2real_rewriter.h rename to src/tactic/arith_tactics/bv2real_rewriter.h diff --git a/src/arith_tactics/degree_shift_tactic.cpp b/src/tactic/arith_tactics/degree_shift_tactic.cpp similarity index 100% rename from src/arith_tactics/degree_shift_tactic.cpp rename to src/tactic/arith_tactics/degree_shift_tactic.cpp diff --git a/src/arith_tactics/degree_shift_tactic.h b/src/tactic/arith_tactics/degree_shift_tactic.h similarity index 100% rename from src/arith_tactics/degree_shift_tactic.h rename to src/tactic/arith_tactics/degree_shift_tactic.h diff --git a/src/arith_tactics/diff_neq_tactic.cpp b/src/tactic/arith_tactics/diff_neq_tactic.cpp similarity index 100% rename from src/arith_tactics/diff_neq_tactic.cpp rename to src/tactic/arith_tactics/diff_neq_tactic.cpp diff --git a/src/arith_tactics/diff_neq_tactic.h b/src/tactic/arith_tactics/diff_neq_tactic.h similarity index 100% rename from src/arith_tactics/diff_neq_tactic.h rename to src/tactic/arith_tactics/diff_neq_tactic.h diff --git a/src/arith_tactics/elim_term_ite_strategy.cpp b/src/tactic/arith_tactics/elim_term_ite_strategy.cpp similarity index 100% rename from src/arith_tactics/elim_term_ite_strategy.cpp rename to src/tactic/arith_tactics/elim_term_ite_strategy.cpp diff --git a/src/arith_tactics/elim_term_ite_strategy.h b/src/tactic/arith_tactics/elim_term_ite_strategy.h similarity index 100% rename from src/arith_tactics/elim_term_ite_strategy.h rename to src/tactic/arith_tactics/elim_term_ite_strategy.h diff --git a/src/arith_tactics/factor_tactic.cpp b/src/tactic/arith_tactics/factor_tactic.cpp similarity index 100% rename from src/arith_tactics/factor_tactic.cpp rename to src/tactic/arith_tactics/factor_tactic.cpp diff --git a/src/arith_tactics/factor_tactic.h b/src/tactic/arith_tactics/factor_tactic.h similarity index 100% rename from src/arith_tactics/factor_tactic.h rename to src/tactic/arith_tactics/factor_tactic.h diff --git a/src/arith_tactics/fix_dl_var_tactic.cpp b/src/tactic/arith_tactics/fix_dl_var_tactic.cpp similarity index 100% rename from src/arith_tactics/fix_dl_var_tactic.cpp rename to src/tactic/arith_tactics/fix_dl_var_tactic.cpp diff --git a/src/arith_tactics/fix_dl_var_tactic.h b/src/tactic/arith_tactics/fix_dl_var_tactic.h similarity index 100% rename from src/arith_tactics/fix_dl_var_tactic.h rename to src/tactic/arith_tactics/fix_dl_var_tactic.h diff --git a/src/arith_tactics/fm_tactic.cpp b/src/tactic/arith_tactics/fm_tactic.cpp similarity index 100% rename from src/arith_tactics/fm_tactic.cpp rename to src/tactic/arith_tactics/fm_tactic.cpp diff --git a/src/arith_tactics/fm_tactic.h b/src/tactic/arith_tactics/fm_tactic.h similarity index 100% rename from src/arith_tactics/fm_tactic.h rename to src/tactic/arith_tactics/fm_tactic.h diff --git a/src/arith_tactics/lia2pb_tactic.cpp b/src/tactic/arith_tactics/lia2pb_tactic.cpp similarity index 100% rename from src/arith_tactics/lia2pb_tactic.cpp rename to src/tactic/arith_tactics/lia2pb_tactic.cpp diff --git a/src/arith_tactics/lia2pb_tactic.h b/src/tactic/arith_tactics/lia2pb_tactic.h similarity index 100% rename from src/arith_tactics/lia2pb_tactic.h rename to src/tactic/arith_tactics/lia2pb_tactic.h diff --git a/src/arith_tactics/linear_equation.cpp b/src/tactic/arith_tactics/linear_equation.cpp similarity index 100% rename from src/arith_tactics/linear_equation.cpp rename to src/tactic/arith_tactics/linear_equation.cpp diff --git a/src/arith_tactics/linear_equation.h b/src/tactic/arith_tactics/linear_equation.h similarity index 100% rename from src/arith_tactics/linear_equation.h rename to src/tactic/arith_tactics/linear_equation.h diff --git a/src/arith_tactics/lu.cpp b/src/tactic/arith_tactics/lu.cpp similarity index 100% rename from src/arith_tactics/lu.cpp rename to src/tactic/arith_tactics/lu.cpp diff --git a/src/arith_tactics/lu.h b/src/tactic/arith_tactics/lu.h similarity index 100% rename from src/arith_tactics/lu.h rename to src/tactic/arith_tactics/lu.h diff --git a/src/arith_tactics/mip_tactic.cpp b/src/tactic/arith_tactics/mip_tactic.cpp similarity index 100% rename from src/arith_tactics/mip_tactic.cpp rename to src/tactic/arith_tactics/mip_tactic.cpp diff --git a/src/arith_tactics/mip_tactic.h b/src/tactic/arith_tactics/mip_tactic.h similarity index 100% rename from src/arith_tactics/mip_tactic.h rename to src/tactic/arith_tactics/mip_tactic.h diff --git a/src/arith_tactics/nla2bv_tactic.cpp b/src/tactic/arith_tactics/nla2bv_tactic.cpp similarity index 100% rename from src/arith_tactics/nla2bv_tactic.cpp rename to src/tactic/arith_tactics/nla2bv_tactic.cpp diff --git a/src/arith_tactics/nla2bv_tactic.h b/src/tactic/arith_tactics/nla2bv_tactic.h similarity index 100% rename from src/arith_tactics/nla2bv_tactic.h rename to src/tactic/arith_tactics/nla2bv_tactic.h diff --git a/src/arith_tactics/normalize_bounds_tactic.cpp b/src/tactic/arith_tactics/normalize_bounds_tactic.cpp similarity index 100% rename from src/arith_tactics/normalize_bounds_tactic.cpp rename to src/tactic/arith_tactics/normalize_bounds_tactic.cpp diff --git a/src/arith_tactics/normalize_bounds_tactic.h b/src/tactic/arith_tactics/normalize_bounds_tactic.h similarity index 100% rename from src/arith_tactics/normalize_bounds_tactic.h rename to src/tactic/arith_tactics/normalize_bounds_tactic.h diff --git a/src/arith_tactics/pb2bv_model_converter.cpp b/src/tactic/arith_tactics/pb2bv_model_converter.cpp similarity index 100% rename from src/arith_tactics/pb2bv_model_converter.cpp rename to src/tactic/arith_tactics/pb2bv_model_converter.cpp diff --git a/src/arith_tactics/pb2bv_model_converter.h b/src/tactic/arith_tactics/pb2bv_model_converter.h similarity index 100% rename from src/arith_tactics/pb2bv_model_converter.h rename to src/tactic/arith_tactics/pb2bv_model_converter.h diff --git a/src/arith_tactics/pb2bv_tactic.cpp b/src/tactic/arith_tactics/pb2bv_tactic.cpp similarity index 100% rename from src/arith_tactics/pb2bv_tactic.cpp rename to src/tactic/arith_tactics/pb2bv_tactic.cpp diff --git a/src/arith_tactics/pb2bv_tactic.h b/src/tactic/arith_tactics/pb2bv_tactic.h similarity index 100% rename from src/arith_tactics/pb2bv_tactic.h rename to src/tactic/arith_tactics/pb2bv_tactic.h diff --git a/src/arith_tactics/probe_arith.cpp b/src/tactic/arith_tactics/probe_arith.cpp similarity index 100% rename from src/arith_tactics/probe_arith.cpp rename to src/tactic/arith_tactics/probe_arith.cpp diff --git a/src/arith_tactics/probe_arith.h b/src/tactic/arith_tactics/probe_arith.h similarity index 100% rename from src/arith_tactics/probe_arith.h rename to src/tactic/arith_tactics/probe_arith.h diff --git a/src/arith_tactics/propagate_ineqs_tactic.cpp b/src/tactic/arith_tactics/propagate_ineqs_tactic.cpp similarity index 100% rename from src/arith_tactics/propagate_ineqs_tactic.cpp rename to src/tactic/arith_tactics/propagate_ineqs_tactic.cpp diff --git a/src/arith_tactics/propagate_ineqs_tactic.h b/src/tactic/arith_tactics/propagate_ineqs_tactic.h similarity index 100% rename from src/arith_tactics/propagate_ineqs_tactic.h rename to src/tactic/arith_tactics/propagate_ineqs_tactic.h diff --git a/src/arith_tactics/purify_arith_tactic.cpp b/src/tactic/arith_tactics/purify_arith_tactic.cpp similarity index 100% rename from src/arith_tactics/purify_arith_tactic.cpp rename to src/tactic/arith_tactics/purify_arith_tactic.cpp diff --git a/src/arith_tactics/purify_arith_tactic.h b/src/tactic/arith_tactics/purify_arith_tactic.h similarity index 100% rename from src/arith_tactics/purify_arith_tactic.h rename to src/tactic/arith_tactics/purify_arith_tactic.h diff --git a/src/arith_tactics/recover_01_tactic.cpp b/src/tactic/arith_tactics/recover_01_tactic.cpp similarity index 100% rename from src/arith_tactics/recover_01_tactic.cpp rename to src/tactic/arith_tactics/recover_01_tactic.cpp diff --git a/src/arith_tactics/recover_01_tactic.h b/src/tactic/arith_tactics/recover_01_tactic.h similarity index 100% rename from src/arith_tactics/recover_01_tactic.h rename to src/tactic/arith_tactics/recover_01_tactic.h diff --git a/src/arith_tactics/smt_arith.cpp b/src/tactic/arith_tactics/smt_arith.cpp similarity index 100% rename from src/arith_tactics/smt_arith.cpp rename to src/tactic/arith_tactics/smt_arith.cpp diff --git a/src/arith_tactics/smt_arith.h b/src/tactic/arith_tactics/smt_arith.h similarity index 100% rename from src/arith_tactics/smt_arith.h rename to src/tactic/arith_tactics/smt_arith.h diff --git a/src/arith_tactics/smt_formula_compiler.cpp b/src/tactic/arith_tactics/smt_formula_compiler.cpp similarity index 100% rename from src/arith_tactics/smt_formula_compiler.cpp rename to src/tactic/arith_tactics/smt_formula_compiler.cpp diff --git a/src/arith_tactics/smt_formula_compiler.h b/src/tactic/arith_tactics/smt_formula_compiler.h similarity index 100% rename from src/arith_tactics/smt_formula_compiler.h rename to src/tactic/arith_tactics/smt_formula_compiler.h diff --git a/src/arith_tactics/smt_solver_exp.cpp b/src/tactic/arith_tactics/smt_solver_exp.cpp similarity index 100% rename from src/arith_tactics/smt_solver_exp.cpp rename to src/tactic/arith_tactics/smt_solver_exp.cpp diff --git a/src/arith_tactics/smt_solver_exp.h b/src/tactic/arith_tactics/smt_solver_exp.h similarity index 100% rename from src/arith_tactics/smt_solver_exp.h rename to src/tactic/arith_tactics/smt_solver_exp.h diff --git a/src/arith_tactics/smt_solver_strategy.cpp b/src/tactic/arith_tactics/smt_solver_strategy.cpp similarity index 100% rename from src/arith_tactics/smt_solver_strategy.cpp rename to src/tactic/arith_tactics/smt_solver_strategy.cpp diff --git a/src/arith_tactics/smt_solver_strategy.h b/src/tactic/arith_tactics/smt_solver_strategy.h similarity index 100% rename from src/arith_tactics/smt_solver_strategy.h rename to src/tactic/arith_tactics/smt_solver_strategy.h diff --git a/src/arith_tactics/smt_solver_types.h b/src/tactic/arith_tactics/smt_solver_types.h similarity index 100% rename from src/arith_tactics/smt_solver_types.h rename to src/tactic/arith_tactics/smt_solver_types.h diff --git a/src/bv/bit_blaster/bit_blaster.cpp b/src/tactic/bit_blaster/bit_blaster.cpp similarity index 100% rename from src/bv/bit_blaster/bit_blaster.cpp rename to src/tactic/bit_blaster/bit_blaster.cpp diff --git a/src/bv/bit_blaster/bit_blaster.h b/src/tactic/bit_blaster/bit_blaster.h similarity index 100% rename from src/bv/bit_blaster/bit_blaster.h rename to src/tactic/bit_blaster/bit_blaster.h diff --git a/src/bv/bit_blaster/bit_blaster_model_converter.cpp b/src/tactic/bit_blaster/bit_blaster_model_converter.cpp similarity index 100% rename from src/bv/bit_blaster/bit_blaster_model_converter.cpp rename to src/tactic/bit_blaster/bit_blaster_model_converter.cpp diff --git a/src/bv/bit_blaster/bit_blaster_model_converter.h b/src/tactic/bit_blaster/bit_blaster_model_converter.h similarity index 100% rename from src/bv/bit_blaster/bit_blaster_model_converter.h rename to src/tactic/bit_blaster/bit_blaster_model_converter.h diff --git a/src/bv/bit_blaster/bit_blaster_rewriter.cpp b/src/tactic/bit_blaster/bit_blaster_rewriter.cpp similarity index 100% rename from src/bv/bit_blaster/bit_blaster_rewriter.cpp rename to src/tactic/bit_blaster/bit_blaster_rewriter.cpp diff --git a/src/bv/bit_blaster/bit_blaster_rewriter.h b/src/tactic/bit_blaster/bit_blaster_rewriter.h similarity index 100% rename from src/bv/bit_blaster/bit_blaster_rewriter.h rename to src/tactic/bit_blaster/bit_blaster_rewriter.h diff --git a/src/bv/bit_blaster/bit_blaster_tpl.h b/src/tactic/bit_blaster/bit_blaster_tpl.h similarity index 100% rename from src/bv/bit_blaster/bit_blaster_tpl.h rename to src/tactic/bit_blaster/bit_blaster_tpl.h diff --git a/src/bv/bit_blaster/bit_blaster_tpl_def.h b/src/tactic/bit_blaster/bit_blaster_tpl_def.h similarity index 100% rename from src/bv/bit_blaster/bit_blaster_tpl_def.h rename to src/tactic/bit_blaster/bit_blaster_tpl_def.h diff --git a/src/bv/bit_blaster/bv1_blaster_tactic.cpp b/src/tactic/bit_blaster/bv1_blaster_tactic.cpp similarity index 100% rename from src/bv/bit_blaster/bv1_blaster_tactic.cpp rename to src/tactic/bit_blaster/bv1_blaster_tactic.cpp diff --git a/src/bv/bit_blaster/bv1_blaster_tactic.h b/src/tactic/bit_blaster/bv1_blaster_tactic.h similarity index 100% rename from src/bv/bit_blaster/bv1_blaster_tactic.h rename to src/tactic/bit_blaster/bv1_blaster_tactic.h diff --git a/src/bv/bit_blaster/eager_bit_blaster.cpp b/src/tactic/bit_blaster/eager_bit_blaster.cpp similarity index 100% rename from src/bv/bit_blaster/eager_bit_blaster.cpp rename to src/tactic/bit_blaster/eager_bit_blaster.cpp diff --git a/src/bv/bit_blaster/eager_bit_blaster.h b/src/tactic/bit_blaster/eager_bit_blaster.h similarity index 100% rename from src/bv/bit_blaster/eager_bit_blaster.h rename to src/tactic/bit_blaster/eager_bit_blaster.h diff --git a/src/bv/tactics/bit_blaster_tactic.cpp b/src/tactic/bv_tactics/bit_blaster_tactic.cpp similarity index 100% rename from src/bv/tactics/bit_blaster_tactic.cpp rename to src/tactic/bv_tactics/bit_blaster_tactic.cpp diff --git a/src/bv/tactics/bit_blaster_tactic.h b/src/tactic/bv_tactics/bit_blaster_tactic.h similarity index 100% rename from src/bv/tactics/bit_blaster_tactic.h rename to src/tactic/bv_tactics/bit_blaster_tactic.h diff --git a/src/bv/tactics/bv_size_reduction_tactic.cpp b/src/tactic/bv_tactics/bv_size_reduction_tactic.cpp similarity index 100% rename from src/bv/tactics/bv_size_reduction_tactic.cpp rename to src/tactic/bv_tactics/bv_size_reduction_tactic.cpp diff --git a/src/bv/tactics/bv_size_reduction_tactic.h b/src/tactic/bv_tactics/bv_size_reduction_tactic.h similarity index 100% rename from src/bv/tactics/bv_size_reduction_tactic.h rename to src/tactic/bv_tactics/bv_size_reduction_tactic.h diff --git a/src/bv/tactics/max_bv_sharing_tactic.cpp b/src/tactic/bv_tactics/max_bv_sharing_tactic.cpp similarity index 100% rename from src/bv/tactics/max_bv_sharing_tactic.cpp rename to src/tactic/bv_tactics/max_bv_sharing_tactic.cpp diff --git a/src/bv/tactics/max_bv_sharing_tactic.h b/src/tactic/bv_tactics/max_bv_sharing_tactic.h similarity index 100% rename from src/bv/tactics/max_bv_sharing_tactic.h rename to src/tactic/bv_tactics/max_bv_sharing_tactic.h diff --git a/src/core_tactics/cofactor_elim_term_ite.cpp b/src/tactic/core_tactics/cofactor_elim_term_ite.cpp similarity index 100% rename from src/core_tactics/cofactor_elim_term_ite.cpp rename to src/tactic/core_tactics/cofactor_elim_term_ite.cpp diff --git a/src/core_tactics/cofactor_elim_term_ite.h b/src/tactic/core_tactics/cofactor_elim_term_ite.h similarity index 100% rename from src/core_tactics/cofactor_elim_term_ite.h rename to src/tactic/core_tactics/cofactor_elim_term_ite.h diff --git a/src/core_tactics/cofactor_term_ite_tactic.cpp b/src/tactic/core_tactics/cofactor_term_ite_tactic.cpp similarity index 100% rename from src/core_tactics/cofactor_term_ite_tactic.cpp rename to src/tactic/core_tactics/cofactor_term_ite_tactic.cpp diff --git a/src/core_tactics/cofactor_term_ite_tactic.h b/src/tactic/core_tactics/cofactor_term_ite_tactic.h similarity index 100% rename from src/core_tactics/cofactor_term_ite_tactic.h rename to src/tactic/core_tactics/cofactor_term_ite_tactic.h diff --git a/src/core_tactics/ctx_simplify_tactic.cpp b/src/tactic/core_tactics/ctx_simplify_tactic.cpp similarity index 100% rename from src/core_tactics/ctx_simplify_tactic.cpp rename to src/tactic/core_tactics/ctx_simplify_tactic.cpp diff --git a/src/core_tactics/ctx_simplify_tactic.h b/src/tactic/core_tactics/ctx_simplify_tactic.h similarity index 100% rename from src/core_tactics/ctx_simplify_tactic.h rename to src/tactic/core_tactics/ctx_simplify_tactic.h diff --git a/src/core_tactics/der_tactic.cpp b/src/tactic/core_tactics/der_tactic.cpp similarity index 100% rename from src/core_tactics/der_tactic.cpp rename to src/tactic/core_tactics/der_tactic.cpp diff --git a/src/core_tactics/der_tactic.h b/src/tactic/core_tactics/der_tactic.h similarity index 100% rename from src/core_tactics/der_tactic.h rename to src/tactic/core_tactics/der_tactic.h diff --git a/src/core_tactics/distribute_forall_tactic.cpp b/src/tactic/core_tactics/distribute_forall_tactic.cpp similarity index 100% rename from src/core_tactics/distribute_forall_tactic.cpp rename to src/tactic/core_tactics/distribute_forall_tactic.cpp diff --git a/src/core_tactics/distribute_forall_tactic.h b/src/tactic/core_tactics/distribute_forall_tactic.h similarity index 100% rename from src/core_tactics/distribute_forall_tactic.h rename to src/tactic/core_tactics/distribute_forall_tactic.h diff --git a/src/core_tactics/elim_term_ite_tactic.cpp b/src/tactic/core_tactics/elim_term_ite_tactic.cpp similarity index 100% rename from src/core_tactics/elim_term_ite_tactic.cpp rename to src/tactic/core_tactics/elim_term_ite_tactic.cpp diff --git a/src/core_tactics/elim_term_ite_tactic.h b/src/tactic/core_tactics/elim_term_ite_tactic.h similarity index 100% rename from src/core_tactics/elim_term_ite_tactic.h rename to src/tactic/core_tactics/elim_term_ite_tactic.h diff --git a/src/core_tactics/elim_uncnstr_tactic.cpp b/src/tactic/core_tactics/elim_uncnstr_tactic.cpp similarity index 100% rename from src/core_tactics/elim_uncnstr_tactic.cpp rename to src/tactic/core_tactics/elim_uncnstr_tactic.cpp diff --git a/src/core_tactics/elim_uncnstr_tactic.h b/src/tactic/core_tactics/elim_uncnstr_tactic.h similarity index 100% rename from src/core_tactics/elim_uncnstr_tactic.h rename to src/tactic/core_tactics/elim_uncnstr_tactic.h diff --git a/src/core_tactics/nnf_tactic.cpp b/src/tactic/core_tactics/nnf_tactic.cpp similarity index 100% rename from src/core_tactics/nnf_tactic.cpp rename to src/tactic/core_tactics/nnf_tactic.cpp diff --git a/src/core_tactics/nnf_tactic.h b/src/tactic/core_tactics/nnf_tactic.h similarity index 100% rename from src/core_tactics/nnf_tactic.h rename to src/tactic/core_tactics/nnf_tactic.h diff --git a/src/core_tactics/occf_tactic.cpp b/src/tactic/core_tactics/occf_tactic.cpp similarity index 100% rename from src/core_tactics/occf_tactic.cpp rename to src/tactic/core_tactics/occf_tactic.cpp diff --git a/src/core_tactics/occf_tactic.h b/src/tactic/core_tactics/occf_tactic.h similarity index 100% rename from src/core_tactics/occf_tactic.h rename to src/tactic/core_tactics/occf_tactic.h diff --git a/src/core_tactics/propagate_values_tactic.cpp b/src/tactic/core_tactics/propagate_values_tactic.cpp similarity index 100% rename from src/core_tactics/propagate_values_tactic.cpp rename to src/tactic/core_tactics/propagate_values_tactic.cpp diff --git a/src/core_tactics/propagate_values_tactic.h b/src/tactic/core_tactics/propagate_values_tactic.h similarity index 100% rename from src/core_tactics/propagate_values_tactic.h rename to src/tactic/core_tactics/propagate_values_tactic.h diff --git a/src/core_tactics/reduce_args_tactic.cpp b/src/tactic/core_tactics/reduce_args_tactic.cpp similarity index 100% rename from src/core_tactics/reduce_args_tactic.cpp rename to src/tactic/core_tactics/reduce_args_tactic.cpp diff --git a/src/core_tactics/reduce_args_tactic.h b/src/tactic/core_tactics/reduce_args_tactic.h similarity index 100% rename from src/core_tactics/reduce_args_tactic.h rename to src/tactic/core_tactics/reduce_args_tactic.h diff --git a/src/core_tactics/simplify_tactic.cpp b/src/tactic/core_tactics/simplify_tactic.cpp similarity index 100% rename from src/core_tactics/simplify_tactic.cpp rename to src/tactic/core_tactics/simplify_tactic.cpp diff --git a/src/core_tactics/simplify_tactic.h b/src/tactic/core_tactics/simplify_tactic.h similarity index 100% rename from src/core_tactics/simplify_tactic.h rename to src/tactic/core_tactics/simplify_tactic.h diff --git a/src/core_tactics/solve_eqs_tactic.cpp b/src/tactic/core_tactics/solve_eqs_tactic.cpp similarity index 100% rename from src/core_tactics/solve_eqs_tactic.cpp rename to src/tactic/core_tactics/solve_eqs_tactic.cpp diff --git a/src/core_tactics/solve_eqs_tactic.h b/src/tactic/core_tactics/solve_eqs_tactic.h similarity index 100% rename from src/core_tactics/solve_eqs_tactic.h rename to src/tactic/core_tactics/solve_eqs_tactic.h diff --git a/src/core_tactics/split_clause_tactic.cpp b/src/tactic/core_tactics/split_clause_tactic.cpp similarity index 100% rename from src/core_tactics/split_clause_tactic.cpp rename to src/tactic/core_tactics/split_clause_tactic.cpp diff --git a/src/core_tactics/split_clause_tactic.h b/src/tactic/core_tactics/split_clause_tactic.h similarity index 100% rename from src/core_tactics/split_clause_tactic.h rename to src/tactic/core_tactics/split_clause_tactic.h diff --git a/src/core_tactics/symmetry_reduce_tactic.cpp b/src/tactic/core_tactics/symmetry_reduce_tactic.cpp similarity index 100% rename from src/core_tactics/symmetry_reduce_tactic.cpp rename to src/tactic/core_tactics/symmetry_reduce_tactic.cpp diff --git a/src/core_tactics/symmetry_reduce_tactic.h b/src/tactic/core_tactics/symmetry_reduce_tactic.h similarity index 100% rename from src/core_tactics/symmetry_reduce_tactic.h rename to src/tactic/core_tactics/symmetry_reduce_tactic.h diff --git a/src/core_tactics/tseitin_cnf_tactic.cpp b/src/tactic/core_tactics/tseitin_cnf_tactic.cpp similarity index 100% rename from src/core_tactics/tseitin_cnf_tactic.cpp rename to src/tactic/core_tactics/tseitin_cnf_tactic.cpp diff --git a/src/core_tactics/tseitin_cnf_tactic.h b/src/tactic/core_tactics/tseitin_cnf_tactic.h similarity index 100% rename from src/core_tactics/tseitin_cnf_tactic.h rename to src/tactic/core_tactics/tseitin_cnf_tactic.h diff --git a/src/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp similarity index 100% rename from src/fpa/fpa2bv_converter.cpp rename to src/tactic/fpa/fpa2bv_converter.cpp diff --git a/src/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h similarity index 100% rename from src/fpa/fpa2bv_converter.h rename to src/tactic/fpa/fpa2bv_converter.h diff --git a/src/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp similarity index 100% rename from src/fpa/fpa2bv_tactic.cpp rename to src/tactic/fpa/fpa2bv_tactic.cpp diff --git a/src/fpa/fpa2bv_tactic.h b/src/tactic/fpa/fpa2bv_tactic.h similarity index 100% rename from src/fpa/fpa2bv_tactic.h rename to src/tactic/fpa/fpa2bv_tactic.h diff --git a/src/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp similarity index 100% rename from src/fpa/qffpa_tactic.cpp rename to src/tactic/fpa/qffpa_tactic.cpp diff --git a/src/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h similarity index 100% rename from src/fpa/qffpa_tactic.h rename to src/tactic/fpa/qffpa_tactic.h diff --git a/src/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp similarity index 100% rename from src/portfolio/default_tactic.cpp rename to src/tactic/portfolio/default_tactic.cpp diff --git a/src/portfolio/default_tactic.h b/src/tactic/portfolio/default_tactic.h similarity index 100% rename from src/portfolio/default_tactic.h rename to src/tactic/portfolio/default_tactic.h diff --git a/src/portfolio/install_tactics.cpp b/src/tactic/portfolio/install_tactics.cpp similarity index 100% rename from src/portfolio/install_tactics.cpp rename to src/tactic/portfolio/install_tactics.cpp diff --git a/src/portfolio/install_tactics.h b/src/tactic/portfolio/install_tactics.h similarity index 100% rename from src/portfolio/install_tactics.h rename to src/tactic/portfolio/install_tactics.h diff --git a/src/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp similarity index 100% rename from src/portfolio/smt_strategic_solver.cpp rename to src/tactic/portfolio/smt_strategic_solver.cpp diff --git a/src/portfolio/smt_strategic_solver.h b/src/tactic/portfolio/smt_strategic_solver.h similarity index 100% rename from src/portfolio/smt_strategic_solver.h rename to src/tactic/portfolio/smt_strategic_solver.h diff --git a/src/bv/sls_tactic/sls_strategy.h b/src/tactic/sls_tactic/sls_strategy.h similarity index 100% rename from src/bv/sls_tactic/sls_strategy.h rename to src/tactic/sls_tactic/sls_strategy.h diff --git a/src/bv/sls_tactic/sls_tactic.cpp b/src/tactic/sls_tactic/sls_tactic.cpp similarity index 100% rename from src/bv/sls_tactic/sls_tactic.cpp rename to src/tactic/sls_tactic/sls_tactic.cpp diff --git a/src/bv/sls_tactic/sls_tactic.h b/src/tactic/sls_tactic/sls_tactic.h similarity index 100% rename from src/bv/sls_tactic/sls_tactic.h rename to src/tactic/sls_tactic/sls_tactic.h diff --git a/src/smtlogic_tactics/nra_tactic.cpp b/src/tactic/smtlogic_tactics/nra_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/nra_tactic.cpp rename to src/tactic/smtlogic_tactics/nra_tactic.cpp diff --git a/src/smtlogic_tactics/nra_tactic.h b/src/tactic/smtlogic_tactics/nra_tactic.h similarity index 100% rename from src/smtlogic_tactics/nra_tactic.h rename to src/tactic/smtlogic_tactics/nra_tactic.h diff --git a/src/smtlogic_tactics/qfaufbv_tactic.cpp b/src/tactic/smtlogic_tactics/qfaufbv_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfaufbv_tactic.cpp rename to src/tactic/smtlogic_tactics/qfaufbv_tactic.cpp diff --git a/src/smtlogic_tactics/qfaufbv_tactic.h b/src/tactic/smtlogic_tactics/qfaufbv_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfaufbv_tactic.h rename to src/tactic/smtlogic_tactics/qfaufbv_tactic.h diff --git a/src/smtlogic_tactics/qfauflia_tactic.cpp b/src/tactic/smtlogic_tactics/qfauflia_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfauflia_tactic.cpp rename to src/tactic/smtlogic_tactics/qfauflia_tactic.cpp diff --git a/src/smtlogic_tactics/qfauflia_tactic.h b/src/tactic/smtlogic_tactics/qfauflia_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfauflia_tactic.h rename to src/tactic/smtlogic_tactics/qfauflia_tactic.h diff --git a/src/smtlogic_tactics/qfbv_tactic.cpp b/src/tactic/smtlogic_tactics/qfbv_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfbv_tactic.cpp rename to src/tactic/smtlogic_tactics/qfbv_tactic.cpp diff --git a/src/smtlogic_tactics/qfbv_tactic.h b/src/tactic/smtlogic_tactics/qfbv_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfbv_tactic.h rename to src/tactic/smtlogic_tactics/qfbv_tactic.h diff --git a/src/smtlogic_tactics/qfidl_tactic.cpp b/src/tactic/smtlogic_tactics/qfidl_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfidl_tactic.cpp rename to src/tactic/smtlogic_tactics/qfidl_tactic.cpp diff --git a/src/smtlogic_tactics/qfidl_tactic.h b/src/tactic/smtlogic_tactics/qfidl_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfidl_tactic.h rename to src/tactic/smtlogic_tactics/qfidl_tactic.h diff --git a/src/smtlogic_tactics/qflia_tactic.cpp b/src/tactic/smtlogic_tactics/qflia_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qflia_tactic.cpp rename to src/tactic/smtlogic_tactics/qflia_tactic.cpp diff --git a/src/smtlogic_tactics/qflia_tactic.h b/src/tactic/smtlogic_tactics/qflia_tactic.h similarity index 100% rename from src/smtlogic_tactics/qflia_tactic.h rename to src/tactic/smtlogic_tactics/qflia_tactic.h diff --git a/src/smtlogic_tactics/qflra_tactic.cpp b/src/tactic/smtlogic_tactics/qflra_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qflra_tactic.cpp rename to src/tactic/smtlogic_tactics/qflra_tactic.cpp diff --git a/src/smtlogic_tactics/qflra_tactic.h b/src/tactic/smtlogic_tactics/qflra_tactic.h similarity index 100% rename from src/smtlogic_tactics/qflra_tactic.h rename to src/tactic/smtlogic_tactics/qflra_tactic.h diff --git a/src/smtlogic_tactics/qfnia_tactic.cpp b/src/tactic/smtlogic_tactics/qfnia_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfnia_tactic.cpp rename to src/tactic/smtlogic_tactics/qfnia_tactic.cpp diff --git a/src/smtlogic_tactics/qfnia_tactic.h b/src/tactic/smtlogic_tactics/qfnia_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfnia_tactic.h rename to src/tactic/smtlogic_tactics/qfnia_tactic.h diff --git a/src/smtlogic_tactics/qfnra_tactic.cpp b/src/tactic/smtlogic_tactics/qfnra_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfnra_tactic.cpp rename to src/tactic/smtlogic_tactics/qfnra_tactic.cpp diff --git a/src/smtlogic_tactics/qfnra_tactic.h b/src/tactic/smtlogic_tactics/qfnra_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfnra_tactic.h rename to src/tactic/smtlogic_tactics/qfnra_tactic.h diff --git a/src/smtlogic_tactics/qfuf_tactic.cpp b/src/tactic/smtlogic_tactics/qfuf_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfuf_tactic.cpp rename to src/tactic/smtlogic_tactics/qfuf_tactic.cpp diff --git a/src/smtlogic_tactics/qfuf_tactic.h b/src/tactic/smtlogic_tactics/qfuf_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfuf_tactic.h rename to src/tactic/smtlogic_tactics/qfuf_tactic.h diff --git a/src/smtlogic_tactics/qfufbv_tactic.cpp b/src/tactic/smtlogic_tactics/qfufbv_tactic.cpp similarity index 100% rename from src/smtlogic_tactics/qfufbv_tactic.cpp rename to src/tactic/smtlogic_tactics/qfufbv_tactic.cpp diff --git a/src/smtlogic_tactics/qfufbv_tactic.h b/src/tactic/smtlogic_tactics/qfufbv_tactic.h similarity index 100% rename from src/smtlogic_tactics/qfufbv_tactic.h rename to src/tactic/smtlogic_tactics/qfufbv_tactic.h diff --git a/src/smtlogic_tactics/quant_tactics.cpp b/src/tactic/smtlogic_tactics/quant_tactics.cpp similarity index 100% rename from src/smtlogic_tactics/quant_tactics.cpp rename to src/tactic/smtlogic_tactics/quant_tactics.cpp diff --git a/src/smtlogic_tactics/quant_tactics.h b/src/tactic/smtlogic_tactics/quant_tactics.h similarity index 100% rename from src/smtlogic_tactics/quant_tactics.h rename to src/tactic/smtlogic_tactics/quant_tactics.h