From 78b11ccd8eb4828adf511109e97e3e64088cfb15 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Oct 2012 21:50:58 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 13 ++-- scripts/mk_util.py | 64 +++++++++++++++---- src/{smtparser => api}/expr_pattern_match.cpp | 0 src/{smtparser => api}/expr_pattern_match.h | 0 src/{smtparser => api}/smtlib.cpp | 0 src/{smtparser => api}/smtlib.h | 0 src/{smtparser => api}/smtlib_solver.cpp | 0 src/{smtparser => api}/smtlib_solver.h | 0 src/{smtparser => api}/smtparser.cpp | 0 src/{smtparser => api}/smtparser.h | 0 {shell => src/dead}/simple_sat.cpp | 0 {shell => src/dead}/simple_sat.h | 0 {shell => src/shell}/datalog_frontend.cpp | 0 {shell => src/shell}/datalog_frontend.h | 0 {shell => src/shell}/dimacs_frontend.cpp | 0 {shell => src/shell}/dimacs_frontend.h | 0 {shell => src/shell}/main.cpp | 0 {shell => src/shell}/options.h | 0 {shell => src/shell}/resource.h | 0 {shell => src/shell}/smtlib_frontend.cpp | 0 {shell => src/shell}/smtlib_frontend.h | 0 {shell => src/shell}/z3_log_frontend.cpp | 0 {shell => src/shell}/z3_log_frontend.h | 0 23 files changed, 58 insertions(+), 19 deletions(-) rename src/{smtparser => api}/expr_pattern_match.cpp (100%) rename src/{smtparser => api}/expr_pattern_match.h (100%) rename src/{smtparser => api}/smtlib.cpp (100%) rename src/{smtparser => api}/smtlib.h (100%) rename src/{smtparser => api}/smtlib_solver.cpp (100%) rename src/{smtparser => api}/smtlib_solver.h (100%) rename src/{smtparser => api}/smtparser.cpp (100%) rename src/{smtparser => api}/smtparser.h (100%) rename {shell => src/dead}/simple_sat.cpp (100%) rename {shell => src/dead}/simple_sat.h (100%) rename {shell => src/shell}/datalog_frontend.cpp (100%) rename {shell => src/shell}/datalog_frontend.h (100%) rename {shell => src/shell}/dimacs_frontend.cpp (100%) rename {shell => src/shell}/dimacs_frontend.h (100%) rename {shell => src/shell}/main.cpp (100%) rename {shell => src/shell}/options.h (100%) rename {shell => src/shell}/resource.h (100%) rename {shell => src/shell}/smtlib_frontend.cpp (100%) rename {shell => src/shell}/smtlib_frontend.h (100%) rename {shell => src/shell}/z3_log_frontend.cpp (100%) rename {shell => src/shell}/z3_log_frontend.h (100%) diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 1f4e4942e..059382be4 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -63,16 +63,17 @@ add_lib('bv_tactics', ['tactic']) add_lib('fuzzing', ['ast']) add_lib('fpa', ['core_tactics', 'bit_blaster', 'sat_tactic']) add_lib('smt_tactic', ['smt']) +add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics']) add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics']) -add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic']) -# TODO: rewrite ufbv_strategy as a tactic and move to smtlogic_tactics. -add_lib('ufbv_strategy', ['assertion_set', 'normal_forms', 'macros', 'smt_tactic', 'rewriter']) +add_lib('aig', ['cmd_context', 'assertion_set']) # 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('aig', ['cmd_context', 'assertion_set']) +add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe']) +# TODO: rewrite ufbv_strategy as a tactic and move to smtlogic_tactics. +add_lib('ufbv_strategy', ['assertion_set', 'normal_forms', 'macros', 'smt_tactic', 'rewriter']) add_lib('portfolio', ['smtlogic_tactics', 'ufbv_strategy', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic']) # TODO: delete SMT 1.0 frontend -add_lib('smtparser', ['api_headers', 'smt', 'spc', 'portfolio']) -add_lib('api', ['portfolio', 'user_plugin', 'smtparser']) +add_lib('api', ['portfolio', 'user_plugin']) +add_exe('shell', ['api', 'sat', 'extra_cmds']) mk_vs_solution() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 658f266c2..9e6853795 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -41,8 +41,10 @@ Name2GUI = {} def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id +MODULES = [] HEADERS = [] LIBS = [] +EXES = [] DEPS = {} class MKException(Exception): @@ -73,6 +75,17 @@ def module_src_dir(name): def module_build_dir(name): return '%s%s%s' % (BUILD_DIR, os.sep, name) +LIB_KIND = 0 +EXE_KIND = 1 + +def get_extension(kind): + if kind == LIB_KIND: + return 'lib' + elif kind == EXE_KIND: + return 'exe' + else: + raise MKException('unknown kind %s' % kind) + def vs_header(f): f.write( '\n' @@ -98,11 +111,16 @@ def vs_project_configurations(f, name): Name2GUI[name] = GUI GUI = GUI + 1 -def vs_lib_configurations(f, name): +def vs_configurations(f, name, kind): for mode in MODES: for platform in PLATFORMS: f.write(' \n' % (mode, platform)) - f.write(' StaticLibrary\n') + if kind == LIB_KIND: + f.write(' StaticLibrary\n') + elif kind == EXE_KIND: + f.write(' Application\n') + else: + raise MKException("unknown kind %s" % kind) f.write(' Unicode\n') f.write(' false\n') f.write(' \n') @@ -125,10 +143,10 @@ def vs_lib_configurations(f, name): for mode in MODES: for platform in PLATFORMS: f.write(' %s\n' % (mode, platform, name)) - f.write(' .lib\n' % (mode, platform)) + f.write(' .%s\n' % (mode, platform, get_extension(kind))) f.write(' \n') -def vs_compilation_options(f, name, deps): +def vs_compilation_options(f, name, deps, kind): for mode in MODES: for platform in PLATFORMS: f.write(' \n' % (mode, platform)) @@ -163,12 +181,21 @@ def vs_compilation_options(f, name, deps): f.write('\n') f.write(' \n') f.write(' \n') - f.write(' $(OutDir)%s.lib\n' % name) + f.write(' $(OutDir)%s.%s\n' % (name, get_extension(kind))) f.write(' %(AdditionalLibraryDirectories)\n') if is_x64(platform): f.write(' MachineX64\n') else: f.write(' MachineX86\n') + if kind == EXE_KIND: + f.write('kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib') + for dep in deps: + f.write(';$(OutDir)%s.lib' % dep) + # if is_x64(platform): + # f.write(';..\%s\%s\%s\%s.lib' % (dep, platform, mode, dep)) + # else: + # f.write(';..\%s\%s\%s.lib' % (dep, mode, dep)) + f.write(';%(AdditionalDependencies)\n') f.write(' \n') f.write(' \n') @@ -187,7 +214,7 @@ def vs_footer(f): '\n') def check_new_component(name): - if (name in HEADERS) or (name in LIBS): + if (name in HEADERS) or (name in LIBS) or (name in EXES): raise MKException("Component '%s' was already defined" % name) # Add a directory containing only .h files @@ -211,9 +238,15 @@ def find_all_deps(name, deps): raise MKException("Unknown component '%s' at '%s'." % (dep, name)) return new_deps -def add_lib(name, deps): +def add_component(name, deps, kind): check_new_component(name) - LIBS.append(name) + if kind == LIB_KIND: + LIBS.append(name) + elif kind == EXE_KIND: + EXES.append(name) + else: + raise MKException("unknown kind %s" % kind) + MODULES.append(name) deps = find_all_deps(name, deps) DEPS[name] = deps print "Dependencies for '%s': %s" % (name, deps) @@ -224,11 +257,17 @@ def add_lib(name, deps): vs_proj = open('%s%s%s.vcxproj' % (module_dir, os.sep, name), 'w') vs_header(vs_proj) vs_project_configurations(vs_proj, name) - vs_lib_configurations(vs_proj, name) - vs_compilation_options(vs_proj, name, deps) + vs_configurations(vs_proj, name, kind) + vs_compilation_options(vs_proj, name, deps, kind) add_vs_cpps(vs_proj, name) vs_footer(vs_proj) +def add_lib(name, deps): + add_component(name, deps, LIB_KIND) + +def add_exe(name, deps): + add_component(name, deps, EXE_KIND) + def is_lib(name): # Add DLL dependency return name in LIBS @@ -238,8 +277,7 @@ def mk_vs_solution(): sln.write('\n') sln.write("Microsoft Visual Studio Solution File, Format Version 11.00\n") sln.write("# Visual Studio 2010\n") - modules = LIBS - for module in modules: + for module in MODULES: gui = Name2GUI[module] deps = DEPS[module] sln.write('Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "%s", "%s%s%s.vcxproj", "{%s}"\n' % @@ -259,7 +297,7 @@ def mk_vs_solution(): sln.write(' %s|%s = %s|%s\n' % (mode, platform, mode, platform)) sln.write('EndGlobalSection\n') sln.write('GlobalSection(ProjectConfigurationPlatforms) = postSolution\n') - for module in modules: + for module in MODULES: gui = Name2GUI[module] for mode in MODES: for platform in PLATFORMS: diff --git a/src/smtparser/expr_pattern_match.cpp b/src/api/expr_pattern_match.cpp similarity index 100% rename from src/smtparser/expr_pattern_match.cpp rename to src/api/expr_pattern_match.cpp diff --git a/src/smtparser/expr_pattern_match.h b/src/api/expr_pattern_match.h similarity index 100% rename from src/smtparser/expr_pattern_match.h rename to src/api/expr_pattern_match.h diff --git a/src/smtparser/smtlib.cpp b/src/api/smtlib.cpp similarity index 100% rename from src/smtparser/smtlib.cpp rename to src/api/smtlib.cpp diff --git a/src/smtparser/smtlib.h b/src/api/smtlib.h similarity index 100% rename from src/smtparser/smtlib.h rename to src/api/smtlib.h diff --git a/src/smtparser/smtlib_solver.cpp b/src/api/smtlib_solver.cpp similarity index 100% rename from src/smtparser/smtlib_solver.cpp rename to src/api/smtlib_solver.cpp diff --git a/src/smtparser/smtlib_solver.h b/src/api/smtlib_solver.h similarity index 100% rename from src/smtparser/smtlib_solver.h rename to src/api/smtlib_solver.h diff --git a/src/smtparser/smtparser.cpp b/src/api/smtparser.cpp similarity index 100% rename from src/smtparser/smtparser.cpp rename to src/api/smtparser.cpp diff --git a/src/smtparser/smtparser.h b/src/api/smtparser.h similarity index 100% rename from src/smtparser/smtparser.h rename to src/api/smtparser.h diff --git a/shell/simple_sat.cpp b/src/dead/simple_sat.cpp similarity index 100% rename from shell/simple_sat.cpp rename to src/dead/simple_sat.cpp diff --git a/shell/simple_sat.h b/src/dead/simple_sat.h similarity index 100% rename from shell/simple_sat.h rename to src/dead/simple_sat.h diff --git a/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp similarity index 100% rename from shell/datalog_frontend.cpp rename to src/shell/datalog_frontend.cpp diff --git a/shell/datalog_frontend.h b/src/shell/datalog_frontend.h similarity index 100% rename from shell/datalog_frontend.h rename to src/shell/datalog_frontend.h diff --git a/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp similarity index 100% rename from shell/dimacs_frontend.cpp rename to src/shell/dimacs_frontend.cpp diff --git a/shell/dimacs_frontend.h b/src/shell/dimacs_frontend.h similarity index 100% rename from shell/dimacs_frontend.h rename to src/shell/dimacs_frontend.h diff --git a/shell/main.cpp b/src/shell/main.cpp similarity index 100% rename from shell/main.cpp rename to src/shell/main.cpp diff --git a/shell/options.h b/src/shell/options.h similarity index 100% rename from shell/options.h rename to src/shell/options.h diff --git a/shell/resource.h b/src/shell/resource.h similarity index 100% rename from shell/resource.h rename to src/shell/resource.h diff --git a/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp similarity index 100% rename from shell/smtlib_frontend.cpp rename to src/shell/smtlib_frontend.cpp diff --git a/shell/smtlib_frontend.h b/src/shell/smtlib_frontend.h similarity index 100% rename from shell/smtlib_frontend.h rename to src/shell/smtlib_frontend.h diff --git a/shell/z3_log_frontend.cpp b/src/shell/z3_log_frontend.cpp similarity index 100% rename from shell/z3_log_frontend.cpp rename to src/shell/z3_log_frontend.cpp diff --git a/shell/z3_log_frontend.h b/src/shell/z3_log_frontend.h similarity index 100% rename from shell/z3_log_frontend.h rename to src/shell/z3_log_frontend.h