diff --git a/lib/lib.vcxproj b/lib/lib.vcxproj deleted file mode 100644 index 92193faba..000000000 --- a/lib/lib.vcxproj +++ /dev/null @@ -1,1326 +0,0 @@ - - - - - commercial - Win32 - - - commercial - x64 - - - Debug - Win32 - - - Debug - x64 - - - external - Win32 - - - external - x64 - - - release_mt - Win32 - - - release_mt - x64 - - - Release - Win32 - - - Release - x64 - - - Trace - Win32 - - - Trace - x64 - - - - {4A7E5A93-19D8-4382-8950-FB2EDEC7A76E} - lib - Win32Proj - - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - true - - - Application - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - true - - - StaticLibrary - Unicode - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - <_ProjectFileVersion>10.0.30319.1 - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - $(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - AllRules.ruleset - - - - - AllRules.ruleset - AllRules.ruleset - - - - - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - - - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - z3lib - - - - Disabled - WIN32;_DEBUG;Z3DEBUG;_LIB;_TRACE;_WINDOWS;ASYNC_COMMANDS;%(PreprocessorDefinitions) - true - EnableFastChecks - MultiThreadedDebugDLL - true - - - Level3 - ProgramDatabase - StreamingSIMDExtensions2 - - - $(OutDir)z3lib.lib - %(AdditionalLibraryDirectories) - MachineX86 - - - - - X64 - - - Disabled - WIN32;Z3DEBUG;_DEBUG;_LIB;_TRACE;_WINDOWS;ASYNC_COMMANDS;_AMD64_;%(PreprocessorDefinitions) - true - EnableFastChecks - MultiThreadedDebugDLL - - - Level3 - ProgramDatabase - - - $(OutDir)z3lib.lib - %(AdditionalLibraryDirectories) - MachineX64 - - - - - Full - false - WIN32;NDEBUG;_LIB;_WINDOWS;ASYNC_COMMANDS;%(PreprocessorDefinitions) - MultiThreadedDLL - true - - - Level3 - ProgramDatabase - StreamingSIMDExtensions2 - - - $(OutDir)z3lib.lib - MachineX86 - - - - - X64 - - - MaxSpeed - false - WIN32;NDEBUG;_LIB;_WINDOWS;_AMD64_;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - MachineX64 - - - - - false - WIN32;NDEBUG;_LIB;_WINDOWS;_TRACE;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - StreamingSIMDExtensions2 - - - - - X64 - - - WIN32;NDEBUG;_LIB;_WINDOWS;_TRACE;_AMD64_;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - - - Full - false - _NO_OMP_;WIN32;NDEBUG;_LIB;_WINDOWS;%(PreprocessorDefinitions) - MultiThreaded - - - Level3 - ProgramDatabase - false - StreamingSIMDExtensions2 - - - $(OutDir)z3lib.lib - false - - - - - Full - false - WIN32;NDEBUG;_LIB;_WINDOWS;_EXTERNAL_RELEASE;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - StreamingSIMDExtensions2 - - - $(OutDir)z3lib.lib - - - - - Full - false - WIN32;NDEBUG;_LIB;_WINDOWS;_Z3_COMMERCIAL;_EXTERNAL_RELEASE;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - StreamingSIMDExtensions2 - - - $(OutDir)z3lib.lib - - - - - X64 - - - MaxSpeed - false - _AMD64_;WIN32;NDEBUG;_LIB;_WINDOWS;_EXTERNAL_RELEASE;_AMD64_;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - - - X64 - - - MaxSpeed - false - WIN32;NDEBUG;_LIB;_WINDOWS;_Z3_COMMERCIAL;_EXTERNAL_RELEASE;_AMD64_;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - - - false - MultiThreaded - Level3 - Full - _NO_OMP_;_AMD64_;WIN32;NDEBUG;_LIB;_WINDOWS;%(PreprocessorDefinitions) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 3e9f673cf..1f4e4942e 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -65,10 +65,14 @@ add_lib('fpa', ['core_tactics', 'bit_blaster', 'sat_tactic']) add_lib('smt_tactic', ['smt']) 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']) # 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('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']) +add_lib('smtparser', ['api_headers', 'smt', 'spc', 'portfolio']) +add_lib('api', ['portfolio', 'user_plugin', 'smtparser']) mk_vs_solution() diff --git a/src/api_headers/z3.h b/src/api/z3.h similarity index 100% rename from src/api_headers/z3.h rename to src/api/z3.h diff --git a/src/api_headers/z3_api.h b/src/api/z3_api.h similarity index 100% rename from src/api_headers/z3_api.h rename to src/api/z3_api.h diff --git a/lib/z3_internal.h b/src/api/z3_internal.h similarity index 100% rename from lib/z3_internal.h rename to src/api/z3_internal.h diff --git a/src/api_headers/z3_internal_types.h b/src/api/z3_internal_types.h similarity index 100% rename from src/api_headers/z3_internal_types.h rename to src/api/z3_internal_types.h diff --git a/lib/z3_logger.h b/src/api/z3_logger.h similarity index 100% rename from lib/z3_logger.h rename to src/api/z3_logger.h diff --git a/src/api_headers/z3_macros.h b/src/api/z3_macros.h similarity index 100% rename from src/api_headers/z3_macros.h rename to src/api/z3_macros.h diff --git a/lib/z3_poly.h b/src/api/z3_poly.h similarity index 100% rename from lib/z3_poly.h rename to src/api/z3_poly.h diff --git a/lib/z3_private.h b/src/api/z3_private.h similarity index 100% rename from lib/z3_private.h rename to src/api/z3_private.h diff --git a/lib/z3_replayer.cpp b/src/api/z3_replayer.cpp similarity index 100% rename from lib/z3_replayer.cpp rename to src/api/z3_replayer.cpp diff --git a/lib/z3_replayer.h b/src/api/z3_replayer.h similarity index 100% rename from lib/z3_replayer.h rename to src/api/z3_replayer.h diff --git a/lib/z3_solver.cpp b/src/api/z3_solver.cpp similarity index 100% rename from lib/z3_solver.cpp rename to src/api/z3_solver.cpp diff --git a/lib/z3_solver.h b/src/api/z3_solver.h similarity index 100% rename from lib/z3_solver.h rename to src/api/z3_solver.h diff --git a/src/api_headers/z3_v1.h b/src/api/z3_v1.h similarity index 100% rename from src/api_headers/z3_v1.h rename to src/api/z3_v1.h diff --git a/lib/value_compiler_extension.h b/src/dead/value_compiler_extension.h similarity index 100% rename from lib/value_compiler_extension.h rename to src/dead/value_compiler_extension.h diff --git a/lib/default_tactic.cpp b/src/portfolio/default_tactic.cpp similarity index 100% rename from lib/default_tactic.cpp rename to src/portfolio/default_tactic.cpp diff --git a/lib/default_tactic.h b/src/portfolio/default_tactic.h similarity index 100% rename from lib/default_tactic.h rename to src/portfolio/default_tactic.h diff --git a/lib/install_tactics.cpp b/src/portfolio/install_tactics.cpp similarity index 99% rename from lib/install_tactics.cpp rename to src/portfolio/install_tactics.cpp index 36de7be76..1d3a37961 100644 --- a/lib/install_tactics.cpp +++ b/src/portfolio/install_tactics.cpp @@ -27,7 +27,7 @@ Notes: #include"bit_blaster_tactic.h" #include"bv1_blaster_tactic.h" -#include"der.h" +#include"der_tactic.h" #include"aig_tactic.h" #include"smt_tactic.h" #include"sat_tactic.h" diff --git a/lib/install_tactics.h b/src/portfolio/install_tactics.h similarity index 100% rename from lib/install_tactics.h rename to src/portfolio/install_tactics.h diff --git a/lib/smt_strategic_solver.cpp b/src/portfolio/smt_strategic_solver.cpp similarity index 100% rename from lib/smt_strategic_solver.cpp rename to src/portfolio/smt_strategic_solver.cpp diff --git a/lib/smt_strategic_solver.h b/src/portfolio/smt_strategic_solver.h similarity index 100% rename from lib/smt_strategic_solver.h rename to src/portfolio/smt_strategic_solver.h diff --git a/lib/ctx_solver_simplify_tactic.cpp b/src/smt/ctx_solver_simplify_tactic.cpp similarity index 100% rename from lib/ctx_solver_simplify_tactic.cpp rename to src/smt/ctx_solver_simplify_tactic.cpp diff --git a/lib/ctx_solver_simplify_tactic.h b/src/smt/ctx_solver_simplify_tactic.h similarity index 100% rename from lib/ctx_solver_simplify_tactic.h rename to src/smt/ctx_solver_simplify_tactic.h diff --git a/lib/mk_database.sh b/src/smt/mk_database.sh similarity index 100% rename from lib/mk_database.sh rename to src/smt/mk_database.sh diff --git a/lib/ni_solver.cpp b/src/smt/ni_solver.cpp similarity index 100% rename from lib/ni_solver.cpp rename to src/smt/ni_solver.cpp diff --git a/lib/ni_solver.h b/src/smt/ni_solver.h similarity index 100% rename from lib/ni_solver.h rename to src/smt/ni_solver.h diff --git a/lib/ufbv_strategy.cpp b/src/ufbv_strategy/ufbv_strategy.cpp similarity index 99% rename from lib/ufbv_strategy.cpp rename to src/ufbv_strategy/ufbv_strategy.cpp index 9b6b41704..37b36c020 100644 --- a/lib/ufbv_strategy.cpp +++ b/src/ufbv_strategy/ufbv_strategy.cpp @@ -17,8 +17,9 @@ Notes: --*/ #include"assertion_set_rewriter.h" +#include"smt_solver_strategy.h" #include"nnf.h" -#include"der.h" +#include"der_strategy.h" #include"distribute_forall.h" #include"macro_finder.h" #include"arith_simplifier_plugin.h" diff --git a/lib/ufbv_strategy.h b/src/ufbv_strategy/ufbv_strategy.h similarity index 100% rename from lib/ufbv_strategy.h rename to src/ufbv_strategy/ufbv_strategy.h