From 0ec6e2f218a65a2f1c029773aee072459d1c47d7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Dec 2012 15:19:47 -0800
Subject: [PATCH] adjusting examples

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/c++/example.cpp | 17 +++++++++--------
 src/api/c++/z3++.h       |  4 ++++
 src/api/python/z3.py     | 13 +++++++++----
 3 files changed, 22 insertions(+), 12 deletions(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 180117a96..ab6e67ab9 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -143,7 +143,7 @@ void prove_example2() {
 void nonlinear_example1() {
     std::cout << "nonlinear example 1\n";
     config cfg;
-    cfg.set(":auto-config", true);
+    cfg.set("auto_config", true);
     context c(cfg);
 
     expr x = c.real_const("x");
@@ -158,12 +158,13 @@ void nonlinear_example1() {
     std::cout << s.check() << "\n";
     model m = s.get_model();
     std::cout << m << "\n";
-    c.set(":pp-decimal", true); // set decimal notation
+    set_param("pp.decimal", true); // set decimal notation
     std::cout << "model in decimal notation\n";
     std::cout << m << "\n";
-    c.set(":pp-decimal-precision", 50); // increase number of decimal places to 50.
+    set_param("pp.decimal-precision", 50); // increase number of decimal places to 50.
     std::cout << "model using 50 decimal places\n";
     std::cout << m << "\n";
+    set_param("pp.decimal", false); // disable decimal notation
 }
 
 /**
@@ -352,7 +353,7 @@ void quantifier_example() {
     
     // making sure model based quantifier instantiation is enabled.
     params p(c);
-    p.set(":mbqi", true);
+    p.set("mbqi", true);
     s.set(p);
 
     s.add(forall(x, y, f(x, y) >= 0));
@@ -468,7 +469,7 @@ void unsat_core_example3() {
 
     // enabling unsat core tracking
     params p(c);
-    p.set(":unsat-core", true);
+    p.set("unsat_core", true);
     s.set(p);
 
     // The following assertion will not be tracked.
@@ -585,7 +586,7 @@ void tactic_example4() {
     std::cout << "tactic example 4\n";
     context c;
     params p(c);
-    p.set(":mul2concat", true);
+    p.set("mul2concat", true);
     tactic t = 
         with(tactic(c, "simplify"), p) &
         tactic(c, "solve-eqs") &
@@ -628,8 +629,8 @@ void tactic_example6() {
     std::cout << "tactic example 6\n";
     context c;
     params p(c);
-    p.set(":arith-lhs", true);
-    p.set(":som", true); // sum-of-monomials normal form
+    p.set("arith_lhs", true);
+    p.set("som", true); // sum-of-monomials normal form
     solver s = 
         (with(tactic(c, "simplify"), p) &
          tactic(c, "normalize-bounds") &
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 7fc36575a..bdb462df0 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -64,6 +64,10 @@ namespace z3 {
     class apply_result;
     class fixedpoint;
 
+    inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
+    inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
+    inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
+
     /**
        \brief Exception used to sign API usage errors.
     */
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 71fd9a732..301267ce1 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -198,10 +198,10 @@ def _get_ctx(ctx):
     else:
         return ctx
 
-def set_option(*args, **kws):
+def set_param(*args, **kws):
     """Set Z3 global (or module) parameters.
 
-    >>> set_option(precision=10)
+    >>> set_param(precision=10)
     """
     if __debug__:
         _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
@@ -219,10 +219,15 @@ def set_option(*args, **kws):
             Z3_global_param_set(str(prev), _to_param_value(a))
             prev = None
 
-def get_option(name):
+def set_option(*args, **kws):
+    """Alias for 'set_param' for backward compatibility.
+    """
+    return set_param(*args, **kws)
+
+def get_param(name):
     """Return the value of a Z3 global (or module) parameter
 
-    >>> get_option('nlsat.reorder')
+    >>> get_param('nlsat.reorder')
     'true'
     """
     ptr = (ctypes.c_char_p * 1)()