auto generation of parameter helper

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

.gitignore

@@ -1,5 +1,7 @@
 *~
 *.pyc
+# .hpp files are automatically generated
+*.hpp
 .z3-trace
 # OCaml generated files
 *.a

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')

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.")))
+                

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) {
+        void updt_params(params_ref const & _p) {
-            m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+            nlsat_params p(_p);
-            m_lazy           = p.get_uint("lazy", 0);
+            m_max_memory     = p.max_memory();
-            m_simplify_cores = p.get_bool("simplify_conflicts", true);
+            m_lazy           = p.lazy();
-            bool min_cores   = p.get_bool("minimize_conflicts", false);
+            m_simplify_cores = p.simplify_conflicts();
-            m_reorder        = p.get_bool("reorder", true);
+            bool min_cores   = p.minimize_conflicts();
-            m_randomize      = p.get_bool("randomize", true);
+            m_reorder        = p.reorder();
-            m_max_conflicts  = p.get_uint("max_conflicts", UINT_MAX);
+            m_randomize      = p.randomize();
-            m_random_order   = p.get_bool("shuffle_vars", false);
+            m_max_conflicts  = p.max_conflicts();
-            m_random_seed    = p.get_uint("seed", 0);
+            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.");
+        nlsat_params::collect_param_descrs(d);
-        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.");
     }
 
     unsynch_mpq_manager & solver::qm() {