diff --git a/scripts/mk_project.py b/scripts/mk_project.py index c34cfc4554e..548733b3f01 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -24,12 +24,12 @@ def init_project_def(): add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) add_lib('params', ['ast', 'util']) - add_lib('euf', ['ast','util'], 'ast/euf') + add_lib('euf', ['ast', 'util'], 'ast/euf') add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') - add_lib('sat', ['util','dd', 'grobner']) + add_lib('sat', ['util', 'dd', 'grobner']) add_lib('nlsat', ['polynomial', 'sat']) - add_lib('lp', ['util','nlsat','grobner', 'interval'], 'math/lp') - add_lib('rewriter', ['ast', 'polynomial', 'automata','params'], 'ast/rewriter') + add_lib('lp', ['util', 'nlsat', 'grobner', 'interval'], 'math/lp') + add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter') add_lib('macros', ['rewriter'], 'ast/macros') add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') add_lib('model', ['rewriter']) @@ -61,7 +61,7 @@ def init_project_def(): add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('qe', ['smt','sat','nlsat','tactic','nlsat_tactic'], 'qe') + add_lib('qe', ['smt', 'sat', 'nlsat', 'tactic', 'nlsat_tactic'], 'qe') add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') add_lib('fd_solver', ['core_tactics', 'arith_tactics', 'sat_solver', 'smt'], 'tactic/fd_solver') add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') @@ -75,15 +75,15 @@ def init_project_def(): add_lib('bmc', ['muz', 'transforms', 'fd_solver'], 'muz/bmc') add_lib('fp', ['muz', 'clp', 'tab', 'rel', 'bmc', 'ddnf', 'spacer'], 'muz/fp') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') - add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics') + add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz', 'qe'], 'tactic/smtlogics') add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') - add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'fd_solver', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') + add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'fd_solver', 'qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h'] add_lib('api', ['portfolio', 'realclosure', 'opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'arith_tactics'], 'cmd_context/extra_cmds') - add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') + add_exe('shell', ['api', 'sat', 'extra_cmds', 'opt'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], exe_name='test-z3', install=False) _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', reexports=['api'], diff --git a/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt index 2a6d0763cc5..7f3e1892e58 100644 --- a/src/ast/fpa/CMakeLists.txt +++ b/src/ast/fpa/CMakeLists.txt @@ -8,6 +8,4 @@ z3_add_component(fpa rewriter model util - PYG_FILES - fpa2bv_rewriter_params.pyg ) diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 6c3e70017ea..962deda65a1 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -20,7 +20,7 @@ Module Name: #include "ast/rewriter/rewriter_def.h" #include "ast/fpa/fpa2bv_rewriter.h" -#include "ast/fpa/fpa2bv_rewriter_params.hpp" +#include "params/fpa2bv_rewriter_params.hpp" fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) : diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 249b25a5d2d..93a28a32397 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -11,6 +11,7 @@ z3_add_component(params bool_rewriter_params.pyg bv_rewriter_params.pyg fpa_rewriter_params.pyg + fpa2bv_rewriter_params.pyg pattern_inference_params_helper.pyg poly_rewriter_params.pyg rewriter_params.pyg diff --git a/src/ast/fpa/fpa2bv_rewriter_params.pyg b/src/params/fpa2bv_rewriter_params.pyg similarity index 100% rename from src/ast/fpa/fpa2bv_rewriter_params.pyg rename to src/params/fpa2bv_rewriter_params.pyg