exposed old simplifier parameters

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

scripts/mk_util.py

@@ -1461,6 +1461,9 @@ def pyg_default_as_c_literal(p):
         return 'symbol("%s")' % p[2]
     return p[2]
 
+def to_c_method(s):
+    return s.replace('.', '_')
+
 def def_module_params(module_name, export, params, class_name=None):
     pyg = get_curr_pyg()
     dirname = os.path.split(get_curr_pyg())[0]
@@ -1493,10 +1496,10 @@ def def_module_params(module_name, export, params, class_name=None):
     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)))
+                      (TYPE2CTYPE[param[1]], to_c_method(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)))
+                      (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
     out.write('};\n')
     if is_verbose():
         print "Generated '%s'" % hpp

src/ast/simplifier/arith_simplifier_params.h

@@ -19,13 +19,20 @@ Revision History:
 #ifndef _ARITH_SIMPLIFIER_PARAMS_H_
 #define _ARITH_SIMPLIFIER_PARAMS_H_
 
-struct arith_simplifier_params {
+#include"arith_simplifier_params_helper.hpp"
+
+struct arith_simplifier_params { 
     bool    m_arith_expand_eqs;
     bool    m_arith_process_all_eqs;
 
-    arith_simplifier_params():
-        m_arith_expand_eqs(false),
-        m_arith_process_all_eqs(false) {
+    arith_simplifier_params(params_ref const & p = params_ref()) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & _p) {
+        arith_simplifier_params_helper p(_p);
+        m_arith_expand_eqs      = p.arith_expand_eqs();
+        m_arith_process_all_eqs = p.arith_process_all_eqs();
     }
 };
     

src/ast/simplifier/arith_simplifier_params_helper.pyg

@@ -0,0 +1,6 @@
+def_module_params(class_name='arith_simplifier_params_helper',
+                  module_name="old_simplify", # Parameters will be in the old_simplify module
+                  export=True,
+                  params=(
+                          ('arith.expand_eqs', BOOL, False, 'expand equalities into two inequalities'),
+                          ('arith.process_all_eqs', BOOL, False, 'put all equations in the form (= t c), where c is a numeral')))

src/ast/simplifier/array_simplifier_params.h

@@ -19,13 +19,20 @@ Revision History:
 #ifndef _ARRAY_SIMPLIFIER_PARAMS_H_
 #define _ARRAY_SIMPLIFIER_PARAMS_H_
 
+#include"array_simplifier_params_helper.hpp"
+
 struct array_simplifier_params {
     bool            m_array_canonize_simplify;
     bool            m_array_simplify; // temporary hack for disabling array simplifier plugin.
 
-    array_simplifier_params():
-        m_array_canonize_simplify(false),
-        m_array_simplify(true) {
+    array_simplifier_params(params_ref const & p = params_ref()) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & _p) {
+        array_simplifier_params_helper p(_p);
+        m_array_canonize_simplify = p.array_canonize();
+        m_array_simplify          = p.array_simplify();
     }
 };
     

src/ast/simplifier/array_simplifier_params_helper.pyg

@@ -0,0 +1,6 @@
+def_module_params(class_name='array_simplifier_params_helper',
+                  module_name="old_simplify", # Parameters will be in the old_simplify module
+                  export=True,
+                  params=(
+                          ('array.canonize', BOOL, False, 'normalize array terms into normal form during simplification'),
+                          ('array.simplify', BOOL, True, 'enable/disable array simplifications')))

src/ast/simplifier/bv_simplifier_params.h

@@ -19,13 +19,20 @@ Revision History:
 #ifndef _BV_SIMPLIFIER_PARAMS_H_
 #define _BV_SIMPLIFIER_PARAMS_H_
 
+#include"bv_simplifier_params_helper.hpp"
+
 struct bv_simplifier_params {
     bool  m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
     bool  m_bv2int_distribute; //!< if true allows downward propagation of bv2int.
 
-    bv_simplifier_params():
-        m_hi_div0(true),
-        m_bv2int_distribute(true) {
+    bv_simplifier_params(params_ref const & p = params_ref()) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & _p) {
+        bv_simplifier_params_helper p(_p);
+        m_hi_div0 = p.bv_hi_div0();
+        m_bv2int_distribute = p.bv_bv2int_distribute();
     }
 };
 

src/ast/simplifier/bv_simplifier_params_helper.pyg

@@ -0,0 +1,6 @@
+def_module_params(class_name='bv_simplifier_params_helper',
+                  module_name="old_simplify", # Parameters will be in the old_simplify module
+                  export=True,
+                  params=(
+                          ('bv.hi_div0', BOOL, True, 'if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero; otherwise, these operations are considered uninterpreted'),
+                          ('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators')))