From 2b82fd5d0cc6c275e54979a1a135a196ad782f6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Aug 2017 10:51:47 -0700 Subject: [PATCH] updated include directives Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 6 +- scripts/update_include.py | 8 +- .../ackermannize_bv_tactic.cpp | 2 +- src/ackermannization/lackr.cpp | 2 +- src/api/api_ast.cpp | 2 +- src/api/api_model.cpp | 4 +- src/api/api_qe.cpp | 20 +- src/ast/ast_smt2_pp.cpp | 2 +- src/ast/fpa/fpa2bv_rewriter.cpp | 2 +- src/ast/normal_forms/nnf.cpp | 2 +- src/ast/pattern/pattern_inference.cpp | 2 +- src/ast/pattern/pattern_inference_params.cpp | 2 +- src/ast/pp.cpp | 2 +- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/ast/rewriter/array_rewriter.cpp | 2 +- src/ast/rewriter/bool_rewriter.cpp | 2 +- src/ast/rewriter/bv_rewriter.cpp | 2 +- src/ast/rewriter/fpa_rewriter.cpp | 2 +- src/ast/rewriter/poly_rewriter_def.h | 2 +- src/ast/rewriter/th_rewriter.cpp | 2 +- .../simplifier/arith_simplifier_params.cpp | 2 +- .../simplifier/array_simplifier_params.cpp | 2 +- src/ast/simplifier/bv_simplifier_params.cpp | 4 +- src/cmd_context/basic_cmds.cpp | 2 +- src/cmd_context/cmd_context.cpp | 2 +- .../extra_cmds/polynomial_cmds.cpp | 2 +- src/cmd_context/interpolant_cmds.cpp | 2 +- src/math/polynomial/algebraic_numbers.cpp | 2 +- src/math/realclosure/realclosure.cpp | 2 +- src/model/model_evaluator.cpp | 2 +- src/muz/base/dl_context.cpp | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 2 +- src/muz/duality/duality_dl_interface.cpp | 2 +- src/muz/fp/dl_cmds.cpp | 2 +- src/muz/fp/horn_tactic.cpp | 2 +- src/muz/pdr/pdr_context.h | 2 +- src/muz/spacer/spacer_context.h | 4 +- src/muz/spacer/spacer_legacy_frames.cpp | 2 +- src/muz/spacer/spacer_legacy_mev.cpp | 2 +- src/muz/spacer/spacer_mev_array.cpp | 2 +- src/muz/spacer/spacer_prop_solver.cpp | 2 +- src/muz/tab/tab_context.cpp | 2 +- src/muz/transforms/dl_mk_array_eq_rewrite.cpp | 187 ++++++++---------- src/muz/transforms/dl_mk_array_eq_rewrite.h | 12 +- .../transforms/dl_mk_array_instantiation.cpp | 14 +- .../transforms/dl_mk_array_instantiation.h | 2 +- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- .../dl_mk_interp_tail_simplifier.cpp | 2 +- .../dl_mk_quantifier_abstraction.cpp | 2 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 2 +- src/muz/transforms/dl_mk_scale.cpp | 2 +- .../transforms/dl_mk_subsumption_checker.cpp | 2 +- src/muz/transforms/dl_transforms.cpp | 2 +- src/nlsat/nlsat_solver.cpp | 2 +- src/opt/maxres.cpp | 2 +- src/opt/opt_cmds.cpp | 2 +- src/opt/opt_context.cpp | 2 +- src/opt/opt_solver.cpp | 4 +- src/opt/optsmt.cpp | 2 +- src/parsers/smt/smtlib_solver.cpp | 4 +- src/parsers/smt2/smt2parser.cpp | 2 +- src/parsers/smt2/smt2scanner.cpp | 2 +- src/sat/sat_asymm_branch.cpp | 2 +- src/sat/sat_config.cpp | 2 +- src/sat/sat_scc.cpp | 2 +- src/sat/sat_simplifier.cpp | 2 +- src/shell/lp_frontend.cpp | 2 +- src/smt/params/dyn_ack_params.cpp | 2 +- src/smt/params/preprocessor_params.cpp | 2 +- src/smt/params/qi_params.cpp | 2 +- src/smt/params/smt_params.cpp | 4 +- src/smt/params/theory_arith_params.cpp | 2 +- src/smt/params/theory_array_params.cpp | 2 +- src/smt/params/theory_bv_params.cpp | 2 +- src/smt/params/theory_pb_params.cpp | 2 +- src/smt/params/theory_str_params.cpp | 2 +- src/smt/proto_model/proto_model.cpp | 2 +- src/smt/smt_kernel.cpp | 2 +- src/smt/smt_solver.cpp | 2 +- src/smt/tactic/smt_tactic.cpp | 4 +- src/smt/theory_lra.cpp | 2 +- src/solver/combined_solver.cpp | 2 +- src/tactic/bv/bv_bound_chk_tactic.cpp | 2 +- src/tactic/sls/sls_engine.cpp | 2 +- src/tactic/sls/sls_tactic.cpp | 2 +- src/tactic/sls/sls_tracker.h | 2 +- src/tactic/smtlogics/qfufbv_tactic.cpp | 4 +- 87 files changed, 209 insertions(+), 216 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a3bba73ba..8845786f9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -257,8 +257,10 @@ else() message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised") endif() -list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS "${CMAKE_SOURCE_DIR}/src") - +list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS + "${CMAKE_BINARY_DIR}/src" + "${CMAKE_SOURCE_DIR}/src" +) ################################################################################ # GNU multiple precision library support ################################################################################ diff --git a/scripts/update_include.py b/scripts/update_include.py index 555d9f094..c7a33f73f 100644 --- a/scripts/update_include.py +++ b/scripts/update_include.py @@ -8,7 +8,6 @@ is_include2 = re.compile("#include\"(.*)\"") def fix_include(file, paths): - print(file) tmp = "%s.tmp" % file ins = open(file) ous = open(tmp,'w') @@ -36,6 +35,7 @@ def fix_include(file, paths): ins.close() ous.close() if found: + print(file) os.system("move %s %s" % (tmp, file)) else: os.system("del %s" % tmp) @@ -48,6 +48,10 @@ def find_paths(dir): if f.endswith('.h'): path = "%s/%s" % (root1, f) paths[f] = path + if f.endswith('.pyg'): + f = f.replace("pyg","hpp") + path = "%s/%s" % (root1, f) + paths[f] = path return paths paths = find_paths('src') @@ -55,6 +59,8 @@ paths = find_paths('src') def fixup(dir): for root, dirs, files in os.walk(dir): for f in files: + if f == "z3.h": + continue if f.endswith('.h') or f.endswith('.cpp'): path = "%s\\%s" % (root, f) fix_include(path, paths) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 82ac50a95..82ef19274 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -17,7 +17,7 @@ Revision History: #include "tactic/tactical.h" #include "ackermannization/lackr.h" #include "model/model_smt2_pp.h" -#include"ackermannize_bv_tactic_params.hpp" +#include "ackermannization/ackermannize_bv_tactic_params.hpp" #include "ackermannization/ackermannize_bv_model_converter.h" diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index 76fbe0617..aac98d7dc 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -16,7 +16,7 @@ --*/ #include "ackermannization/lackr.h" -#include"ackermannization_params.hpp" +#include "ackermannization/ackermannization_params.hpp" #include "tactic/tactic.h" #include "ackermannization/lackr_model_constructor.h" #include "ackermannization/ackr_info.h" diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 6ae10b8f9..c14a24df1 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -37,7 +37,7 @@ Revision History: #include "util/scoped_ctrl_c.h" #include "util/cancel_eh.h" #include "util/scoped_timer.h" -#include"pp_params.hpp" +#include "ast/pp_params.hpp" extern bool is_numeral_sort(Z3_context c, Z3_sort ty); diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index ccd70e79e..73428a3d7 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -25,8 +25,8 @@ Revision History: #include "model/model.h" #include "model/model_v2_pp.h" #include "model/model_smt2_pp.h" -#include"model_params.hpp" -#include"model_evaluator_params.hpp" +#include "model/model_params.hpp" +#include "model/model_evaluator_params.hpp" extern "C" { diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index ee49acc2a..343855a1a 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -18,19 +18,19 @@ Notes: --*/ #include -#include "z3.h" +#include "api/z3.h" #include "api_log_macros.h" -#include "api_context.h" -#include "api_util.h" -#include "api_model.h" -#include "api_ast_map.h" -#include "api_ast_vector.h" +#include "api/api_context.h" +#include "api/api_util.h" +#include "api/api_model.h" +#include "api/api_ast_map.h" +#include "api/api_ast_vector.h" -#include "qe_vartest.h" -#include "qe_lite.h" -#include "spacer_util.h" +#include "qe/qe_vartest.h" +#include "qe/qe_lite.h" +#include "muz/spacer/spacer_util.h" -#include "expr_map.h" +#include "ast/expr_map.h" extern "C" { diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 89cab9de4..5c3eb93c2 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -24,7 +24,7 @@ Revision History: #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" #include "math/polynomial/algebraic_numbers.h" -#include"pp_params.hpp" +#include "ast/pp_params.hpp" using namespace format_ns; #define ALIAS_PREFIX "a" diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 57cd9facc..0e3899c53 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -21,7 +21,7 @@ Notes: #include "ast/rewriter/rewriter_def.h" #include "ast/fpa/fpa2bv_rewriter.h" #include "util/cooperate.h" -#include"fpa2bv_rewriter_params.hpp" +#include "ast/fpa/fpa2bv_rewriter_params.hpp" fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) : diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index cca9c2c93..247e9dea1 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include "ast/normal_forms/nnf.h" -#include"nnf_params.hpp" +#include "ast/normal_forms/nnf_params.hpp" #include "util/warning.h" #include "ast/used_vars.h" #include "ast/well_sorted.h" diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index d55c20c1c..c8247e409 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -576,7 +576,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings, m_candidates.reset(); } -#include "database.h" +#include "ast/pattern/database.h" void pattern_inference::reduce1_quantifier(quantifier * q) { TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";); diff --git a/src/ast/pattern/pattern_inference_params.cpp b/src/ast/pattern/pattern_inference_params.cpp index 8d978e09c..1f1118a02 100644 --- a/src/ast/pattern/pattern_inference_params.cpp +++ b/src/ast/pattern/pattern_inference_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "ast/pattern/pattern_inference_params.h" -#include"pattern_inference_params_helper.hpp" +#include "ast/pattern/pattern_inference_params_helper.hpp" void pattern_inference_params::updt_params(params_ref const & _p) { pattern_inference_params_helper p(_p); diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp index 522d3eca6..39f1986ee 100644 --- a/src/ast/pp.cpp +++ b/src/ast/pp.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "ast/pp.h" -#include"pp_params.hpp" +#include "ast/pp_params.hpp" using namespace format_ns; static std::pair space_upto_line_break(ast_manager & m, format * f) { diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 4b91ad789..6d2e9dae1 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/arith_rewriter.h" -#include"arith_rewriter_params.hpp" +#include "ast/rewriter/arith_rewriter_params.hpp" #include "ast/rewriter/poly_rewriter_def.h" #include "math/polynomial/algebraic_numbers.h" #include "ast/ast_pp.h" diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 85f639bc9..fb7783fe9 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/array_rewriter.h" -#include"array_rewriter_params.hpp" +#include "ast/rewriter/array_rewriter_params.hpp" #include "ast/ast_lt.h" #include "ast/ast_pp.h" diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 511e7607d..44fccb49e 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/bool_rewriter.h" -#include"bool_rewriter_params.hpp" +#include "ast/rewriter/bool_rewriter_params.hpp" #include "ast/rewriter/rewriter_def.h" void bool_rewriter::updt_params(params_ref const & _p) { diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index d176c8008..edd601c9c 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/bv_rewriter.h" -#include"bv_rewriter_params.hpp" +#include "ast/rewriter/bv_rewriter_params.hpp" #include "ast/rewriter/poly_rewriter_def.h" #include "ast/ast_smt2_pp.h" diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index f82d6df3e..563437b99 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/fpa_rewriter.h" -#include"fpa_rewriter_params.hpp" +#include "ast/rewriter/fpa_rewriter_params.hpp" #include "ast/ast_smt2_pp.h" fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) : diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 81d3aec9f..5e2e39722 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/poly_rewriter.h" -#include"poly_rewriter_params.hpp" +#include "ast/rewriter/poly_rewriter_params.hpp" #include "ast/ast_lt.h" #include "ast/ast_ll_pp.h" #include "ast/ast_smt2_pp.h" diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 240b43b30..764fa8eef 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "ast/rewriter/th_rewriter.h" -#include"rewriter_params.hpp" +#include "ast/rewriter/rewriter_params.hpp" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/arith_rewriter.h" #include "ast/rewriter/bv_rewriter.h" diff --git a/src/ast/simplifier/arith_simplifier_params.cpp b/src/ast/simplifier/arith_simplifier_params.cpp index efe21c43d..73bbbaa1a 100644 --- a/src/ast/simplifier/arith_simplifier_params.cpp +++ b/src/ast/simplifier/arith_simplifier_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "ast/simplifier/arith_simplifier_params.h" -#include"arith_simplifier_params_helper.hpp" +#include "ast/simplifier/arith_simplifier_params_helper.hpp" void arith_simplifier_params::updt_params(params_ref const & _p) { arith_simplifier_params_helper p(_p); diff --git a/src/ast/simplifier/array_simplifier_params.cpp b/src/ast/simplifier/array_simplifier_params.cpp index 94a858ac6..ff7dba25f 100644 --- a/src/ast/simplifier/array_simplifier_params.cpp +++ b/src/ast/simplifier/array_simplifier_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "ast/simplifier/array_simplifier_params.h" -#include"array_simplifier_params_helper.hpp" +#include "ast/simplifier/array_simplifier_params_helper.hpp" void array_simplifier_params::updt_params(params_ref const & _p) { array_simplifier_params_helper p(_p); diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp index 2639b230c..4c6b4a5fa 100644 --- a/src/ast/simplifier/bv_simplifier_params.cpp +++ b/src/ast/simplifier/bv_simplifier_params.cpp @@ -17,8 +17,8 @@ Revision History: --*/ #include "ast/simplifier/bv_simplifier_params.h" -#include"bv_simplifier_params_helper.hpp" -#include"bv_rewriter_params.hpp" +#include "ast/simplifier/bv_simplifier_params_helper.hpp" +#include "ast/rewriter/bv_rewriter_params.hpp" void bv_simplifier_params::updt_params(params_ref const & _p) { bv_simplifier_params_helper p(_p); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index ace4b6a55..8830358af 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -29,7 +29,7 @@ Notes: #include "util/gparams.h" #include "util/env_params.h" #include "ast/well_sorted.h" -#include"pp_params.hpp" +#include "ast/pp_params.hpp" class help_cmd : public cmd { svector m_cmds; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1c9372228..a893a1637 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -43,7 +43,7 @@ Notes: #include "cmd_context/interpolant_cmds.h" #include "model/model_smt2_pp.h" #include "model/model_v2_pp.h" -#include"model_params.hpp" +#include "model/model_params.hpp" #include "ast/rewriter/th_rewriter.h" #include "tactic/tactic_exception.h" #include "solver/smt_logics.h" diff --git a/src/cmd_context/extra_cmds/polynomial_cmds.cpp b/src/cmd_context/extra_cmds/polynomial_cmds.cpp index 33f252a64..7a748ac66 100644 --- a/src/cmd_context/extra_cmds/polynomial_cmds.cpp +++ b/src/cmd_context/extra_cmds/polynomial_cmds.cpp @@ -29,7 +29,7 @@ Notes: #include "math/polynomial/polynomial_var2value.h" #include "ast/expr2var.h" #include "ast/pp.h" -#include"pp_params.hpp" +#include "ast/pp_params.hpp" static void to_poly(cmd_context & ctx, expr * t) { polynomial::numeral_manager nm; diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 65e7a17d8..b5bbea18c 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -31,7 +31,7 @@ #include "interp/iz3interp.h" #include "interp/iz3checker.h" #include "interp/iz3profiling.h" -#include"interp_params.hpp" +#include "interp/interp_params.hpp" #include "ast/scoped_proof.h" static void show_interpolant_and_maybe_check(cmd_context & ctx, diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 353a8c107..22b50326b 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -25,7 +25,7 @@ Notes: #include "util/scoped_ptr_vector.h" #include "util/mpbqi.h" #include "util/timeit.h" -#include"algebraic_params.hpp" +#include "math/polynomial/algebraic_params.hpp" #include "util/common_msgs.h" namespace algebraic_numbers { diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 93cfc98f4..8f2d933e2 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -20,7 +20,7 @@ Notes: --*/ #include "math/realclosure/realclosure.h" -#include"rcf_params.hpp" +#include "math/realclosure/rcf_params.hpp" #include "util/array.h" #include "util/mpbq.h" #include "math/realclosure/mpz_matrix.h" diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 5020fb98b..2b8f8abd6 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "model/model.h" -#include"model_evaluator_params.hpp" +#include "model/model_evaluator_params.hpp" #include "ast/rewriter/rewriter_types.h" #include "model/model_evaluator.h" #include "ast/rewriter/bool_rewriter.h" diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 7be434477..97a2c841a 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -27,7 +27,7 @@ Revision History: #include "ast/ast_smt2_pp.h" #include "ast/datatype_decl_plugin.h" #include "ast/scoped_proof.h" -#include"fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" #include "ast/ast_pp_util.h" diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index fc5067355..0f7914e0c 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -33,7 +33,7 @@ Revision History: #include "muz/transforms/dl_mk_rule_inliner.h" #include "ast/scoped_proof.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 30f8a7dfa..5ce4ef957 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -34,7 +34,7 @@ #include "ast/expr_abstract.h" #include "model/model_smt2_pp.h" #include "model/model_v2_pp.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" #include "ast/used_vars.h" #include "ast/func_decl_dependencies.h" #include "muz/transforms/dl_transforms.h" diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index a82737b78..42c614912 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -30,7 +30,7 @@ Notes: #include "util/scoped_ctrl_c.h" #include "util/scoped_timer.h" #include "util/trail.h" -#include"fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" #include diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 8a9f13144..5db57a12c 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -27,7 +27,7 @@ Revision History: #include "muz/transforms/dl_mk_slice.h" #include "tactic/filter_model_converter.h" #include "muz/transforms/dl_transforms.h" -#include"fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" #include "ast/ast_util.h" #include "ast/rewriter/var_subst.h" diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 087f77f9e..f160cff6a 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -28,7 +28,7 @@ Revision History: #include "muz/pdr/pdr_manager.h" #include "muz/pdr/pdr_prop_solver.h" #include "muz/pdr/pdr_reachable_cache.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index b6cfaff0c..cb422d08f 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -32,7 +32,7 @@ Notes: #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_prop_solver.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { class rule_set; @@ -174,7 +174,7 @@ class pred_transformer { }; /// manager of the lemmas in all the frames -#include "spacer_legacy_frames.h" +#include "muz/spacer/spacer_legacy_frames.h" class frames { private: pred_transformer &m_pt; diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp index 6c732ecc0..d3e01a585 100644 --- a/src/muz/spacer/spacer_legacy_frames.cpp +++ b/src/muz/spacer/spacer_legacy_frames.cpp @@ -19,7 +19,7 @@ #include "muz/base/dl_rule_set.h" #include "smt/tactic/unit_subsumption_tactic.h" #include "model/model_smt2_pp.h" -#include "dl_mk_rule_inliner.h" +#include "muz/transforms/dl_mk_rule_inliner.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" #include "ast/ast_util.h" diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp index 8b53410b1..69f479836 100644 --- a/src/muz/spacer/spacer_legacy_mev.cpp +++ b/src/muz/spacer/spacer_legacy_mev.cpp @@ -22,7 +22,7 @@ Copyright (c) 2017 Arie Gurfinkel #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_legacy_mev.h" #include "muz/spacer/spacer_util.h" -#include "arith_decl_plugin.h" +#include "ast/arith_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" #include "model/model_smt2_pp.h" #include "ast/scoped_proof.h" diff --git a/src/muz/spacer/spacer_mev_array.cpp b/src/muz/spacer/spacer_mev_array.cpp index 9e04b457e..7a4bc321b 100644 --- a/src/muz/spacer/spacer_mev_array.cpp +++ b/src/muz/spacer/spacer_mev_array.cpp @@ -15,7 +15,7 @@ Revision History: --*/ #include"model/model.h" -#include"model_evaluator_params.hpp" +#include "model/model_evaluator_params.hpp" #include"ast/rewriter/rewriter_types.h" #include"model/model_evaluator.h" #include"muz/spacer/spacer_mev_array.h" diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 719443457..19c5c3aa3 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -35,7 +35,7 @@ Revision History: #include "muz/spacer/spacer_farkas_learner.h" #include "muz/spacer/spacer_prop_solver.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace spacer { diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 8309f812e..8809c0dc7 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -30,7 +30,7 @@ Revision History: #include "ast/for_each_expr.h" #include "ast/substitution/matcher.h" #include "ast/scoped_proof.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" #include "ast/ast_util.h" namespace tb { diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp index c9caa6148..2001cb01b 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp +++ b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp @@ -15,126 +15,111 @@ Revision History: --*/ - -#include "dl_mk_array_eq_rewrite.h" -#include "dl_context.h" -#include "pattern_inference.h" -#include "dl_context.h" -#include "expr_safe_replace.h" -#include "expr_abstract.h" -#include"fixedpoint_params.hpp" +#include "ast/pattern/pattern_inference.h" +#include "ast/rewriter/expr_safe_replace.h" +#include "ast/expr_abstract.h" +#include "muz/base/dl_context.h" +#include "muz/base/dl_context.h" +#include "muz/base/fixedpoint_params.hpp" +#include "muz/transforms/dl_mk_array_eq_rewrite.h" #include "../spacer/obj_equiv_class.h" +// NSB code review: avoid dependency on spacer inside this directory. +// The python build system will rightfully complain if you include +// "muz/spacer/obj_equiv_class.h". + namespace datalog { - mk_array_eq_rewrite::mk_array_eq_rewrite( + mk_array_eq_rewrite::mk_array_eq_rewrite( context & ctx, unsigned priority): plugin(priority), m(ctx.get_manager()), m_ctx(ctx), m_a(m) - { - } - - rule_set * mk_array_eq_rewrite::operator()(rule_set const & source) - { - src_set = &source; - rule_set * result = alloc(rule_set, m_ctx); - result->inherit_predicates(source); - dst=result; - unsigned nbrules = source.get_num_rules(); - src_manager = &source.get_rule_manager(); - for(unsigned i =0;iget_counter().get_max_rule_var(r)+1; - - - expr_ref_vector new_tail(m); - unsigned nb_predicates = r.get_uninterpreted_tail_size(); - unsigned tail_size = r.get_tail_size(); - for(unsigned i=0;iinherit_predicates(source); + m_dst = result; + m_src_manager = &source.get_rule_manager(); + for (rule * rp : source) { + instantiate_rule(*rp, *result); } - } - for(spacer::expr_equiv_class::iterator it = (*c_eq).begin(); - it!=(*c_eq).end(); ++it) - { - for(unsigned i=0;imk_rule(m.mk_implies(m.mk_and(res_conjs.size(), res_conjs.c_ptr()), r.get_head()), pr, dest, r.name()); - } - expr* mk_array_eq_rewrite::replace(expr* e, expr* new_val, expr* old_val) - { - if(e==old_val) - return new_val; - else if(!is_app(e)) + void mk_array_eq_rewrite::instantiate_rule(const rule& r, rule_set & dest) { - return e; + //Reset everything + m_cnt = m_src_manager->get_counter().get_max_rule_var(r)+1; + + + expr_ref_vector new_tail(m); + unsigned nb_predicates = r.get_uninterpreted_tail_size(); + unsigned tail_size = r.get_tail_size(); + for (unsigned i = 0; i < nb_predicates; i++) { + new_tail.push_back(r.get_tail(i)); + } + + spacer::expr_equiv_class array_eq_classes(m); + for(unsigned i = nb_predicates; i < tail_size; i++) { + expr* cond = r.get_tail(i); + expr* e1, *e2; + if (m.is_eq(cond, e1, e2) && m_a.is_array(get_sort(e1))) { + array_eq_classes.merge(e1, e2); + } + else { + new_tail.push_back(cond); + } + } + + for (auto & c_eq : array_eq_classes) { + expr* representative = *(c_eq.begin()); + for (expr * v : c_eq) { + if (!is_var(v)) { + representative = v; + break; + } + } + for (expr * v : c_eq) { + for (unsigned i = 0; i < new_tail.size(); i++) + new_tail[i] = replace(new_tail[i].get(), representative, v); + } + for (expr * v : c_eq) { + new_tail.push_back(m.mk_eq(v, representative)); + } + } + params_ref select_over_store; + select_over_store.set_bool("expand_select_store", true); + th_rewriter t(m, select_over_store); + expr_ref_vector res_conjs(m); + for (expr* e : new_tail) { + expr_ref tmp(m); + t(e, tmp); + res_conjs.push_back(tmp); + } + proof_ref pr(m); + m_src_manager->mk_rule(m.mk_implies(m.mk_and(res_conjs.size(), res_conjs.c_ptr()), r.get_head()), pr, dest, r.name()); } - app*f = to_app(e); - ptr_vector n_args; - for(unsigned i=0;iget_num_args();i++) + + // NSB Code review: use substitution facility, such as expr_safe_replace or expr_replacer. + expr* mk_array_eq_rewrite::replace(expr* e, expr* new_val, expr* old_val) { - n_args.push_back(replace(f->get_arg(i), new_val, old_val)); + if (e == old_val) + return new_val; + else if (!is_app(e)) { + return e; + } + app* f = to_app(e); + ptr_vector n_args; + for (expr * arg : *f) { + n_args.push_back(replace(arg, new_val, old_val)); + } + return m.mk_app(f->get_decl(), n_args.size(), n_args.c_ptr()); } - return m.mk_app(f->get_decl(), n_args.size(), n_args.c_ptr()); - } } diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.h b/src/muz/transforms/dl_mk_array_eq_rewrite.h index 0229ff487..cfdca990f 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.h +++ b/src/muz/transforms/dl_mk_array_eq_rewrite.h @@ -19,7 +19,7 @@ Revision History: #define DL_MK_ARRAY_EQ_REWRITE_H_ -#include "dl_rule_transformer.h" +#include "muz/base/dl_rule_transformer.h" #include "../spacer/obj_equiv_class.h" namespace datalog { @@ -29,13 +29,13 @@ namespace datalog { //Context objects ast_manager& m; context& m_ctx; - array_util m_a; + array_util m_a; //Rule set context - const rule_set*src_set; - rule_set*dst; - rule_manager* src_manager; - unsigned cnt;//Index for new variables + const rule_set* m_src_set; + rule_set* m_dst; + rule_manager* m_src_manager; + unsigned m_cnt;//Index for new variables expr* replace(expr* e, expr* new_val, expr* old_val); void instantiate_rule(const rule& r, rule_set & dest); diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp index 762884545..9d983abd2 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.cpp +++ b/src/muz/transforms/dl_mk_array_instantiation.cpp @@ -17,13 +17,13 @@ Revision History: --*/ -#include "dl_mk_array_instantiation.h" -#include "dl_context.h" -#include "pattern_inference.h" -#include "dl_context.h" -#include "expr_safe_replace.h" -#include "expr_abstract.h" -#include"fixedpoint_params.hpp" +#include "muz/transforms/dl_mk_array_instantiation.h" +#include "muz/base/dl_context.h" +#include "ast/pattern/pattern_inference.h" +#include "muz/base/dl_context.h" +#include "ast/rewriter/expr_safe_replace.h" +#include "ast/expr_abstract.h" +#include "muz/base/fixedpoint_params.hpp" #include "../spacer/obj_equiv_class.h" namespace datalog { diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h index 0af57ee84..2ef9873f4 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.h +++ b/src/muz/transforms/dl_mk_array_instantiation.h @@ -70,7 +70,7 @@ Revision History: #define DL_MK_ARRAY_INSTANTIATION_H_ -#include "dl_rule_transformer.h" +#include "muz/base/dl_rule_transformer.h" #include "../spacer/obj_equiv_class.h" namespace datalog { diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 20baf66b6..3c8045e34 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -24,7 +24,7 @@ Revision History: #include "ast/rewriter/expr_safe_replace.h" #include "tactic/filter_model_converter.h" #include "muz/transforms/dl_mk_interp_tail_simplifier.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" #include "ast/scoped_proof.h" #include "model/model_v2_pp.h" diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 1559f4f65..30505a5e8 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -27,7 +27,7 @@ Revision History: #include "muz/transforms/dl_mk_interp_tail_simplifier.h" #include "ast/ast_util.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { // ----------------------------------- diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index d2195a8d9..b171aaa7c 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -23,7 +23,7 @@ Revision History: #include "muz/base/dl_context.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/expr_abstract.h" -#include"fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 1c7a6b219..30ff330ab 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -52,7 +52,7 @@ Subsumption transformation (remove rule): #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "muz/transforms/dl_mk_rule_inliner.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index cc6321b31..5bc10b957 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -18,7 +18,7 @@ Revision History: #include "muz/transforms/dl_mk_scale.h" #include "muz/base/dl_context.h" -#include"fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index d3b959792..e26f105c6 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -25,7 +25,7 @@ Revision History: #include "ast/rewriter/rewriter_def.h" #include "muz/transforms/dl_mk_subsumption_checker.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index b684139f6..95b0f6cd6 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -35,7 +35,7 @@ Revision History: #include "muz/transforms/dl_mk_scale.h" #include "muz/transforms/dl_mk_array_eq_rewrite.h" #include "muz/transforms/dl_mk_array_instantiation.h" -#include "fixedpoint_params.hpp" +#include "muz/base/fixedpoint_params.hpp" namespace datalog { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 2e32e2fbd..c5e9babae 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -31,7 +31,7 @@ Revision History: #include "util/dependency.h" #include "math/polynomial/polynomial_cache.h" #include "util/permutation.h" -#include"nlsat_params.hpp" +#include "nlsat/nlsat_params.hpp" #define NLSAT_EXTRA_VERBOSE diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index cbde02009..e708788f6 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -61,7 +61,7 @@ Notes: #include "sat/sat_solver/inc_sat_solver.h" #include "opt/opt_context.h" #include "ast/pb_decl_plugin.h" -#include "opt_params.hpp" +#include "opt/opt_params.hpp" #include "ast/ast_util.h" #include "smt/smt_solver.h" diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index d88b0a406..7ca2be4aa 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -29,7 +29,7 @@ Notes: #include "util/scoped_ctrl_c.h" #include "util/scoped_timer.h" #include "cmd_context/parametric_cmd.h" -#include "opt_params.hpp" +#include "opt/opt_params.hpp" #include "model/model_smt2_pp.h" static opt::context& get_opt(cmd_context& cmd, opt::context* opt) { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index beba8a60b..2b31e243c 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -20,7 +20,7 @@ Notes: #include "opt/opt_context.h" #include "ast/ast_pp.h" #include "opt/opt_solver.h" -#include "opt_params.hpp" +#include "opt/opt_params.hpp" #include "ast/for_each_expr.h" #include "tactic/goal.h" #include "tactic/tactic.h" diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 0c7a14065..f453d9fe2 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -29,8 +29,8 @@ Notes: #include "smt/theory_lra.h" #include "ast/ast_pp.h" #include "ast/ast_smt_pp.h" -#include "pp_params.hpp" -#include "opt_params.hpp" +#include "ast/pp_params.hpp" +#include "opt/opt_params.hpp" #include "model/model_smt2_pp.h" #include "util/stopwatch.h" diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 3c8e31e59..f8f75fbfd 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -37,7 +37,7 @@ Notes: #include "ast/ast_util.h" #include "model/model_pp.h" #include "ast/rewriter/th_rewriter.h" -#include "opt_params.hpp" +#include "opt/opt_params.hpp" namespace opt { diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp index 128b9de88..b4487cbc5 100644 --- a/src/parsers/smt/smtlib_solver.cpp +++ b/src/parsers/smt/smtlib_solver.cpp @@ -28,8 +28,8 @@ Revision History: #include "solver/solver.h" #include "tactic/portfolio/smt_strategic_solver.h" #include "cmd_context/cmd_context.h" -#include"model_params.hpp" -#include"parser_params.hpp" +#include "model/model_params.hpp" +#include "parsers/util/parser_params.hpp" namespace smtlib { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 46c719487..b86a663a7 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -29,7 +29,7 @@ Revision History: #include "ast/rewriter/rewriter.h" #include "ast/has_free_vars.h" #include "ast/ast_smt2_pp.h" -#include"parser_params.hpp" +#include "parsers/util/parser_params.hpp" #include namespace smt2 { diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index b31440faf..c1cc40b2b 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "parsers/smt2/smt2scanner.h" -#include"parser_params.hpp" +#include "parsers/util/parser_params.hpp" namespace smt2 { diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 6d8fa05a0..8d5778f0b 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "sat/sat_asymm_branch.h" -#include"sat_asymm_branch_params.hpp" +#include "sat/sat_asymm_branch_params.hpp" #include "sat/sat_solver.h" #include "util/stopwatch.h" #include "util/trace.h" diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 00ee0f48e..9cd343bd3 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "sat/sat_config.h" #include "sat/sat_types.h" -#include"sat_params.hpp" +#include "sat/sat_params.hpp" namespace sat { diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 5ab0bbd38..9682da4e8 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -21,7 +21,7 @@ Revision History: #include "sat/sat_elim_eqs.h" #include "util/stopwatch.h" #include "util/trace.h" -#include"sat_scc_params.hpp" +#include "sat/sat_scc_params.hpp" namespace sat { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index ef74a58f4..67101b4d8 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include "sat/sat_simplifier.h" -#include"sat_simplifier_params.hpp" +#include "sat/sat_simplifier_params.hpp" #include "sat/sat_solver.h" #include "util/stopwatch.h" #include "util/trace.h" diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 950b4a628..61015c860 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -7,7 +7,7 @@ Author: --*/ -#include "lp_params.hpp" +#include "util/lp/lp_params.hpp" #include "util/lp/lp_settings.h" #include "util/lp/mps_reader.h" #include "util/timeout.h" diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index 1a51b45bd..4ba230a47 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/dyn_ack_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void dyn_ack_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 599400c0c..9267dbeba 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/preprocessor_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void preprocessor_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index 34a58c14e..a9cff6e8c 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/qi_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void qi_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8a8fac952..a8eb81a2e 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -17,8 +17,8 @@ Revision History: --*/ #include "smt/params/smt_params.h" -#include"smt_params_helper.hpp" -#include"model_params.hpp" +#include "smt/params/smt_params_helper.hpp" +#include "model/model_params.hpp" #include "util/gparams.h" void smt_params::updt_local_params(params_ref const & _p) { diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index e6ecd50b8..2b5a14493 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/theory_arith_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void theory_arith_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/theory_array_params.cpp b/src/smt/params/theory_array_params.cpp index a73411c7f..9a9e5aa7b 100644 --- a/src/smt/params/theory_array_params.cpp +++ b/src/smt/params/theory_array_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/theory_array_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void theory_array_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 48ad07047..4b4808a1f 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/theory_bv_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void theory_bv_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/theory_pb_params.cpp b/src/smt/params/theory_pb_params.cpp index be1cc681b..b285429d9 100644 --- a/src/smt/params/theory_pb_params.cpp +++ b/src/smt/params/theory_pb_params.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/params/theory_pb_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void theory_pb_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index 62dc881d8..afbfc33fc 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -16,7 +16,7 @@ Revision History: --*/ #include "smt/params/theory_str_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" void theory_str_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index c69fa6edc..f14034601 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "smt/proto_model/proto_model.h" -#include"model_params.hpp" +#include "model/model_params.hpp" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/rewriter/var_subst.h" diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index d870d9b9a..e4ce30f91 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -19,7 +19,7 @@ Revision History: #include "smt/smt_kernel.h" #include "smt/smt_context.h" #include "ast/ast_smt2_pp.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" namespace smt { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 1a4cc00d1..ba86f017a 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -20,7 +20,7 @@ Notes: #include "smt/smt_kernel.h" #include "ast/reg_decl_plugins.h" #include "smt/params/smt_params.h" -#include"smt_params_helper.hpp" +#include "smt/params/smt_params_helper.hpp" #include "solver/mus.h" #include "ast/for_each_expr.h" #include "ast/ast_smt2_pp.h" diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 3328d6030..f2dc83cfe 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -20,8 +20,8 @@ Notes: #include "tactic/tactical.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" -#include"smt_params_helper.hpp" -#include"lp_params.hpp" +#include "smt/params/smt_params_helper.hpp" +#include "util/lp/lp_params.hpp" #include "ast/rewriter/rewriter_types.h" #include "tactic/filter_model_converter.h" #include "ast/ast_util.h" diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index e55ac16e8..124fea910 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -26,7 +26,7 @@ Revision History: #include "util/lp/lar_solver.h" #include "util/nat_set.h" #include "util/optional.h" -#include "lp_params.hpp" +#include "util/lp/lp_params.hpp" #include "util/inf_rational.h" #include "smt/smt_theory.h" #include "smt/smt_context.h" diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index cbe6373c2..744ac494a 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -20,7 +20,7 @@ Notes: --*/ #include "solver/solver.h" #include "util/scoped_timer.h" -#include"combined_solver_params.hpp" +#include "solver/combined_solver_params.hpp" #include "util/common_msgs.h" #define PS_VB_LVL 15 diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index ee7cb1ded..b71b44bd0 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -19,7 +19,7 @@ #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/bv_bounds.h" -#include"rewriter_params.hpp" +#include "ast/rewriter/rewriter_params.hpp" #include "ast/rewriter/bool_rewriter.h" #include "util/cooperate.h" diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index b89a05231..4e1c6a693 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -27,7 +27,7 @@ Notes: #include "util/cooperate.h" #include "util/luby.h" -#include"sls_params.hpp" +#include "tactic/sls/sls_params.hpp" #include "tactic/sls/sls_engine.h" diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 2bbef288e..19937e8b0 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -27,7 +27,7 @@ Notes: #include "tactic/core/nnf_tactic.h" #include "util/stopwatch.h" #include "tactic/sls/sls_tactic.h" -#include"sls_params.hpp" +#include "tactic/sls/sls_params.hpp" #include "tactic/sls/sls_engine.h" class sls_tactic : public tactic { diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index d5ce8ee3c..651e4ef14 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -26,7 +26,7 @@ Notes: #include "ast/bv_decl_plugin.h" #include "model/model.h" -#include"sls_params.hpp" +#include "tactic/sls/sls_params.hpp" #include "tactic/sls/sls_powers.h" class sls_tracker { diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 2e64d1e0a..e89da3631 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -27,12 +27,12 @@ Notes: #include "tactic/bv/bv_size_reduction_tactic.h" #include "tactic/core/reduce_args_tactic.h" #include "tactic/smtlogics/qfbv_tactic.h" -#include"qfufbv_tactic_params.hpp" +#include "tactic/smtlogics/qfufbv_tactic_params.hpp" /////////////// #include "model/model_smt2_pp.h" #include "util/cooperate.h" #include "ackermannization/lackr.h" -#include"ackermannization_params.hpp" +#include "ackermannization/ackermannization_params.hpp" #include "tactic/smtlogics/qfufbv_ackr_model_converter.h" /////////////// #include "sat/sat_solver/inc_sat_solver.h"