move fpa

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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'],

src/ast/fpa/CMakeLists.txt

@@ -8,6 +8,4 @@ z3_add_component(fpa
     rewriter
     model
     util
-  PYG_FILES
-    fpa2bv_rewriter_params.pyg
 )

src/ast/fpa/fpa2bv_rewriter.cpp

@@ -20,7 +20,7 @@ Notes:
 
 #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) :

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