From fe7c577d9964589ed351c3dc6770ca5982560d34 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jun 2015 01:54:52 -0700 Subject: [PATCH] isolate inc_sat_solver Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 7 ++----- src/{opt => sat/sat_solver}/inc_sat_solver.cpp | 1 - src/{opt => sat/sat_solver}/inc_sat_solver.h | 0 3 files changed, 2 insertions(+), 6 deletions(-) rename src/{opt => sat/sat_solver}/inc_sat_solver.cpp (99%) rename src/{opt => sat/sat_solver}/inc_sat_solver.h (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b9641c869..719ffc703 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -74,11 +74,8 @@ def init_project_def(): add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') - add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic'], 'opt') -# add_dll('foci2', ['util'], 'interp/foci2stub', -# dll_name='foci2', -# export_files=['foci2stub.cpp']) -# add_lib('interp', ['solver','foci2']) + add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') + add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp', 'opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) diff --git a/src/opt/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp similarity index 99% rename from src/opt/inc_sat_solver.cpp rename to src/sat/sat_solver/inc_sat_solver.cpp index fb8172373..5111a6cc2 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -21,7 +21,6 @@ Notes: #include "tactical.h" #include "sat_solver.h" #include "tactic2solver.h" -#include "nnf_tactic.h" #include "aig_tactic.h" #include "propagate_values_tactic.h" #include "max_bv_sharing_tactic.h" diff --git a/src/opt/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h similarity index 100% rename from src/opt/inc_sat_solver.h rename to src/sat/sat_solver/inc_sat_solver.h