From b37a5b16794670c8cbfd03f6f338d6d18219d485 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 May 2018 10:27:12 -0700 Subject: [PATCH] clean up python build files Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b03ced763..f2720c893 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -40,8 +40,7 @@ def init_project_def(): add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') add_lib('aig_tactic', ['tactic'], 'tactic/aig') add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization') - add_lib('interp', ['solver']) - add_lib('cmd_context', ['solver', 'rewriter', 'interp']) + add_lib('cmd_context', ['solver', 'rewriter']) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa') @@ -56,7 +55,6 @@ def init_project_def(): 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('duality', ['smt', 'interp', 'qe']) add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') add_lib('dataflow', ['muz'], 'muz/dataflow') add_lib('transforms', ['muz', 'hilbert', 'dataflow'], 'muz/transforms') @@ -67,16 +65,15 @@ def init_project_def(): add_lib('tab', ['muz', 'transforms'], 'muz/tab') add_lib('bmc', ['muz', 'transforms'], 'muz/bmc') add_lib('ddnf', ['muz', 'transforms', 'rel'], 'muz/ddnf') - add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality') - add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf', 'spacer'], 'muz/fp') + add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'ddnf', 'spacer'], 'muz/fp') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') 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', '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_interp.h', 'z3_fpa.h', 'z3_spacer.h'] - add_lib('api', ['portfolio', 'realclosure', 'interp', '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_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)