From 4f9442864a846d5b934157a6c6b38e696fc0c04d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Nov 2012 15:31:40 -0800 Subject: [PATCH] auto generation of parameter helper Signed-off-by: Leonardo de Moura --- .gitignore | 2 + scripts/mk_util.py | 97 ++++++++++++++++++++++++++++++++++++-- src/nlsat/nlsat_params.pyg | 13 +++++ src/nlsat/nlsat_solver.cpp | 33 ++++++------- 4 files changed, 123 insertions(+), 22 deletions(-) create mode 100644 src/nlsat/nlsat_params.pyg diff --git a/.gitignore b/.gitignore index 3fe56e9f3..3d6e631f1 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,7 @@ *~ *.pyc +# .hpp files are automatically generated +*.hpp .z3-trace # OCaml generated files *.a diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e449f9c0f..782990cd7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1420,11 +1420,102 @@ def mk_makefile(): # Generate automatically generated source code def mk_auto_src(): if not ONLY_MAKEFILES: + exec_pyg_scripts() mk_pat_db() mk_all_install_tactic_cpps() mk_all_mem_initializer_cpps() mk_all_gparams_register_modules() +UINT = 0 +BOOL = 1 +DOUBLE = 2 +STRING = 3 +SYMBOL = 4 +UINT_MAX = 4294967295 +CURR_PYG = None + +def get_curr_pyg(): + return CURR_PYG + +TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' } +TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' } +TYPE2GETTER = { UINT : 'get_uint', BOOL : 'get_bool', DOUBLE : 'get_double', STRING : 'get_str', SYMBOL : 'get_sym' } + +def pyg_default(p): + if p[1] == BOOL: + if p[2]: + return "true" + else: + return "false" + return p[2] + +def pyg_default_as_c_literal(p): + if p[1] == BOOL: + if p[2]: + return "true" + else: + return "false" + elif p[1] == STRING: + return '"%s"' % p[2] + elif p[1] == SYMBOL: + return 'symbol("%s")' % p[2] + return p[2] + +def def_module_params(module_name, export, params): + pyg = get_curr_pyg() + hpp = '%shpp' % pyg[:len(pyg)-3] + out = open(hpp, 'w') + out.write('// Automatically generated file\n') + out.write('#include"params.h"\n') + if export: + out.write('#include"gparams.h"\n') + out.write('struct %s_params {\n' % module_name) + out.write(' params_ref const & p;\n') + if export: + out.write(' params_ref const & g;\n') + out.write(' %s_params(params_ref const & _p = params_ref()):\n' % module_name) + out.write(' p(_p)') + if export: + out.write(', g(gparams::get_module("%s"))' % module_name) + out.write(' {}\n') + out.write(' static void collect_param_descrs(param_descrs & d) {\n') + for param in params: + out.write(' d.insert("%s", %s, "%s", "%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param))) + out.write(' }\n') + if export: + out.write(' /*\n') + out.write(" REG_MODULE_PARAMS('%s', '%s_params::collect_param_descrs')\n" % (module_name, module_name)) + out.write(' */\n') + # Generated accessors + for param in params: + if export: + out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' % + (TYPE2CTYPE[param[1]], param[0], TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + else: + out.write(' %s %s() const { return p.%s("%s", %s); }\n' % + (TYPE2CTYPE[param[1]], param[0], TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + out.write('};\n') + if is_verbose(): + print "Generated '%s'" % hpp + +def max_memory_param(): + return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes.') + +PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL, + 'UINT_MAX' : UINT_MAX, + 'max_memory_param' : max_memory_param, + 'def_module_params' : def_module_params } + +# Execute python auxiliary scripts that generate extra code for Z3. +def exec_pyg_scripts(): + global CURR_PYG + for root, dirs, files in os.walk('src'): + for f in files: + if f.endswith('.pyg'): + script = os.path.join(root, f) + CURR_PYG = script + execfile(script, PYG_GLOBALS) + # TODO: delete after src/ast/pattern/expr_pattern_match # database.smt ==> database.h def mk_pat_db(): @@ -1548,7 +1639,7 @@ def mk_install_tactic_cpp(cnames, path): probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') for cname in cnames: c = get_component(cname) - h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir)) + h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir)) for h_file in h_files: added_include = False fin = open("%s/%s" % (c.src_dir, h_file), 'r') @@ -1613,7 +1704,7 @@ def mk_mem_initializer_cpp(cnames, path): finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') for cname in cnames: c = get_component(cname) - h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir)) + h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir)) for h_file in h_files: added_include = False fin = open("%s/%s" % (c.src_dir, h_file), 'r') @@ -1674,7 +1765,7 @@ def mk_gparams_register_modules(cnames, path): reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') for cname in cnames: c = get_component(cname) - h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir)) + h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir)) for h_file in h_files: added_include = False fin = open("%s/%s" % (c.src_dir, h_file), 'r') diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg new file mode 100644 index 000000000..2728e1180 --- /dev/null +++ b/src/nlsat/nlsat_params.pyg @@ -0,0 +1,13 @@ + +def_module_params('nlsat', + export=True, + params=(max_memory_param(), + ('lazy', UINT, 0, "how lazy the solver is."), + ('reorder', BOOL, True, "reorder variables."), + ('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."), + ('minimize_conflicts', BOOL, False, "minimize conflicts"), + ('randomize', BOOL, True, "randomize selection of a witness in nlsat."), + ('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."), + ('shuffle_vars', BOOL, False, "use a random variable order."), + ('seed', UINT, 0, "random seed."))) + diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index d76d584f7..341431556 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -31,6 +31,7 @@ Revision History: #include"dependency.h" #include"polynomial_cache.h" #include"permutation.h" +#include"nlsat_params.hpp" #define NLSAT_EXTRA_VERBOSE @@ -197,20 +198,21 @@ namespace nlsat { mk_clause(1, &true_lit, false, 0); } - void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_lazy = p.get_uint("lazy", 0); - m_simplify_cores = p.get_bool("simplify_conflicts", true); - bool min_cores = p.get_bool("minimize_conflicts", false); - m_reorder = p.get_bool("reorder", true); - m_randomize = p.get_bool("randomize", true); - m_max_conflicts = p.get_uint("max_conflicts", UINT_MAX); - m_random_order = p.get_bool("shuffle_vars", false); - m_random_seed = p.get_uint("seed", 0); + void updt_params(params_ref const & _p) { + nlsat_params p(_p); + m_max_memory = p.max_memory(); + m_lazy = p.lazy(); + m_simplify_cores = p.simplify_conflicts(); + bool min_cores = p.minimize_conflicts(); + m_reorder = p.reorder(); + m_randomize = p.randomize(); + m_max_conflicts = p.max_conflicts(); + m_random_order = p.shuffle_vars(); + m_random_seed = p.seed(); m_ism.set_seed(m_random_seed); m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_minimize_cores(min_cores); - m_am.updt_params(p); + m_am.updt_params(p.p); } void set_cancel(bool f) { @@ -2570,15 +2572,8 @@ namespace nlsat { } void solver::collect_param_descrs(param_descrs & d) { - insert_max_memory(d); algebraic_numbers::manager::collect_param_descrs(d); - d.insert("max_conflicts", CPK_UINT, "(default: inf) maximum number of conflicts."); - d.insert("shuffle_vars", CPK_BOOL, "(default: false) use a variable order."); - d.insert("seed", CPK_UINT, "(default: 0) random seed."); - d.insert("randomize", CPK_BOOL, "(default: true) randomize selection of a witness in nlsat."); - d.insert("reorder", CPK_BOOL, "(default: true) reorder variables."); - d.insert("lazy", CPK_UINT, "(default: 0) how lazy the solver is."); - d.insert("simplify_conflicts", CPK_BOOL, "(default: true) simplify conflicts using equalities before resolving them in nlsat solver."); + nlsat_params::collect_param_descrs(d); } unsynch_mpq_manager & solver::qm() {