mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

adjusting examples

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-03 15:19:47 -08:00
parent 6d7d205e13
commit 0ec6e2f218
3 changed files with 22 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
examples/c++/example.cpp
View file

@ -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") &

4
src/api/c++/z3++.h
View file

@ -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.
*/

13
src/api/python/z3.py
View file

@ -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)()