From fad1e611aa53d4134139b656a123f823906e290c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 12:34:55 -0700 Subject: [PATCH 1/6] build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type Signed-off-by: Nikolaj Bjorner --- src/api/api_arith.cpp | 6 ++-- src/api/dotnet/Expr.cs | 4 +-- src/api/java/Expr.java | 4 +-- src/api/z3_api.h | 4 +-- src/smt/theory_seq.cpp | 6 ++-- src/smt/theory_seq.h | 2 +- src/tactic/core/reduce_invertible_tactic.cpp | 29 ++++++++++++++++++-- src/test/bdd.cpp | 4 +-- 8 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index cc1ccf59e..524d9393d 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -119,10 +119,10 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { + int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { LOG_Z3_is_algebraic_number(c, a); - Z3_bool r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? Z3_TRUE : Z3_FALSE; - IF_VERBOSE(10, verbose_stream() << r << "\n"); + int r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? 1 : 0; + //IF_VERBOSE(10, verbose_stream() << r << "\n"); return r; } diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 1e0f495f5..942baffab 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -239,7 +239,7 @@ namespace Microsoft.Z3 /// public bool IsAlgebraicNumber { - get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); } + get { return 0 != Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); } } #endregion @@ -1823,7 +1823,7 @@ namespace Microsoft.Z3 Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); if ( // Z3_sort_kind.Z3_REAL_SORT == sk && - Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? + 0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); if (Native.Z3_is_numeral_ast(ctx.nCtx, obj)) diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index db5c33e79..75ec9aa75 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -275,7 +275,7 @@ public class Expr extends AST **/ public boolean isAlgebraicNumber() { - return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); + return 0 != Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); } /** @@ -2108,7 +2108,7 @@ public class Expr extends AST Z3_sort_kind sk = Z3_sort_kind .fromInt(Native.getSortKind(ctx.nCtx(), s)); - if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast? + if (Native.isAlgebraicNumber(ctx.nCtx(), obj) != 0) // is this a numeral ast? return new AlgebraicNum(ctx, obj); if (Native.isNumeralAst(ctx.nCtx(), obj)) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7e12f2fa7..74f0fd254 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4397,9 +4397,9 @@ extern "C" { /** \brief Return true if the given AST is a real algebraic number. - def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) + def_API('Z3_is_algebraic_number', INT, (_in(CONTEXT), _in(AST))) */ - Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); + int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); /** \brief Convert an \c ast into an \c APP_AST. This is just type casting. diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 40aae8043..c2c3b1cfb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -199,6 +199,9 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_reset_cache(false), m_eq_id(0), m_find(*this), + m_overlap(m), + m_overlap2(m), + m_len_prop_lvl(-1), m_factory(nullptr), m_exclude(m), m_axioms(m), @@ -216,9 +219,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_atoms_qhead(0), m_new_solution(false), m_new_propagation(false), - m_len_prop_lvl(-1), - m_overlap(m), - m_overlap2(m), m_mk_aut(m) { m_prefix = "seq.p.suffix"; m_suffix = "seq.s.prefix"; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index f32b6254b..f03bdeb60 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -50,7 +50,6 @@ namespace smt { class seq_value_proc; - theory_seq_params const & m_params; // cache to track evaluations under equalities class eval_cache { @@ -295,6 +294,7 @@ namespace smt { typedef hashtable rational_set; ast_manager& m; + theory_seq_params const& m_params; dependency_manager m_dm; solution_map m_rep; // unification representative. bool m_reset_cache; // invalidate cache. diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 13af1f376..75b8cae0c 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -258,17 +258,37 @@ private: rest = arg; } if (!rest) return false; - expr_ref zero(m_arith.mk_numeral(rational::zero(), false), m); + expr_ref zero(m_arith.mk_real(0), m); new_v = m.mk_ite(m.mk_eq(zero, rest), zero, v); if (mc) { ensure_mc(mc); expr_ref def(m_arith.mk_div(v, rest), m); (*mc)->add(v, def); } - return true; + return true; } + expr* e1 = nullptr, *e2 = nullptr; + + // t / v -> if t = 0 then 0 else v + // inverse: t = 0 then 1 else v / t + if (m_arith.is_div(p, e1, e2) && e2 == v) { + expr_ref zero(m_arith.mk_real(0), m); + new_v = m.mk_ite(m.mk_eq(zero, e1), zero, v); + if (mc) { + ensure_mc(mc); + expr_ref def(m.mk_ite(m.mk_eq(zero, e1), m_arith.mk_real(1), m_arith.mk_div(e1, v)), m); + (*mc)->add(v, def); + } + return true; + } + + // v / t unless t != 0 + if (m_arith.is_div(p, e1, e2) && e1 == v) { + return false; + } + if (m.is_eq(p, e1, e2)) { if (mc && has_diagonal(e1)) { ensure_mc(mc); @@ -294,12 +314,15 @@ private: bool has_diagonal(expr* e) { return m_bv.is_bv(e) || - m.is_bool(e); + m.is_bool(e) || + m_arith.is_int_real(e); } expr * mk_diagonal(expr* e) { if (m_bv.is_bv(e)) return m_bv.mk_bv_neg(e); if (m.is_bool(e)) return m.mk_not(e); + if (m_arith.is_int(e)) return m_arith.mk_add(m_arith.mk_int(1), e); + if (m_arith.is_real(e)) return m_arith.mk_add(m_arith.mk_real(1), e); UNREACHABLE(); return e; } diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index ea5a0bc34..423142557 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -30,8 +30,8 @@ namespace sat { SASSERT(m.mk_ite(v1,v0,v0) == v0); SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); - SASSERT(!(v0 && v1) == (!v0 || !v1)); - SASSERT(!(v0 || v1) == (!v0 && !v1)); + SASSERT((!(v0 && v1)) == (!v0 || !v1)); + SASSERT((!(v0 || v1)) == (!v0 && !v1)); } static void test3() { From 13413d052954fde2f009873995081b1d16606d25 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 15:08:16 -0700 Subject: [PATCH 2/6] update for int return value Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- src/tactic/core/reduce_invertible_tactic.cpp | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 10198fcc5..f6a5b1950 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2455,7 +2455,7 @@ def _is_numeral(ctx, a): return Z3_is_numeral_ast(ctx.ref(), a) def _is_algebraic(ctx, a): - return Z3_is_algebraic_number(ctx.ref(), a) + return 0 != Z3_is_algebraic_number(ctx.ref(), a) def is_int_value(a): """Return `True` if `a` is an integer value of sort Int. diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 75b8cae0c..5fe6e9d76 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -178,11 +178,12 @@ private: if (m_bv.is_bv_mul(p)) { expr_ref rest(m); for (expr* arg : *to_app(p)) { - if (arg != v) + if (arg != v) { if (rest) rest = m_bv.mk_bv_mul(rest, arg); else rest = arg; + } } if (!rest) return false; @@ -251,11 +252,12 @@ private: if (m_arith.is_mul(p) && m_arith.is_real(p)) { expr_ref rest(m); for (expr* arg : *to_app(p)) { - if (arg != v) + if (arg != v) { if (rest) rest = m_arith.mk_mul(rest, arg); else rest = arg; + } } if (!rest) return false; expr_ref zero(m_arith.mk_real(0), m); From b38abf64d73016385685689a34608758ca0f780d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 19:30:46 -0700 Subject: [PATCH 3/6] use expr_ref on mk_concat Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 71 +++++++++++++++++++++--------------------- src/smt/theory_seq.h | 2 +- 2 files changed, 37 insertions(+), 36 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c2c3b1cfb..ef50cf3b6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -415,9 +415,9 @@ bool theory_seq::branch_binary_variable(eq const& e) { expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m); expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m); ys.push_back(Y1); - expr_ref ysY1(mk_concat(ys)); - expr_ref xsE(mk_concat(xs)); - expr_ref Y1Y2(mk_concat(Y1, Y2)); + expr_ref ysY1 = mk_concat(ys); + expr_ref xsE = mk_concat(xs); + expr_ref Y1Y2 = mk_concat(Y1, Y2); dependency* dep = e.dep(); propagate_eq(dep, ~lit, x, ysY1); propagate_eq(dep, ~lit, y, Y1Y2); @@ -524,9 +524,9 @@ bool theory_seq::eq_unit(expr* const& l, expr* const &r) const { unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) { SASSERT(!ls.empty() && !rs.empty()); unsigned_vector res; - expr* l = mk_concat(ls); - expr* r = mk_concat(rs); - expr* pair = m.mk_eq(l,r); + expr_ref l = mk_concat(ls); + expr_ref r = mk_concat(rs); + expr_ref pair(m.mk_eq(l,r), m); if (m_overlap.find(pair, res)) { return res; } @@ -535,7 +535,7 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c if (eq_unit(ls[i], rs.back())) { bool same = true; if (i >= 1) { - for (unsigned j = i-1; j>=0 && rs.size()+j-i>=1; --j) { + for (unsigned j = i - 1; rs.size() + j >= 1 + i; --j) { if (!eq_unit(ls[j], rs[rs.size()+j-i-1])) { same = false; break; @@ -556,9 +556,9 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs) { SASSERT(!ls.empty() && !rs.empty()); unsigned_vector res; - expr* l = mk_concat(ls); - expr* r = mk_concat(rs); - expr* pair = m.mk_eq(l,r); + expr_ref l = mk_concat(ls); + expr_ref r = mk_concat(rs); + expr_ref pair(m.mk_eq(l,r), m); if (m_overlap2.find(pair, res)) { return res; } @@ -567,7 +567,7 @@ unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector if (eq_unit(ls[i],rs[0])) { bool same = true; unsigned j = i+1; - while (j ys.size()) { expr_ref xs1E(m_util.str.mk_concat(ind-ys.size(), xs.c_ptr()), m); - expr_ref xxs1E(mk_concat(x, xs1E), m); + expr_ref xxs1E = mk_concat(x, xs1E); propagate_eq(dep, lits, xxs1E, y1, true); } else if (ind == ys.size()) { @@ -618,7 +619,7 @@ bool theory_seq::branch_ternary_variable_base(dependency* dep, unsigned_vector i } else { expr_ref ys1E(m_util.str.mk_concat(ys.size()-ind, ys.c_ptr()), m); - expr_ref y1ys1E(mk_concat(y1, ys1E), m); + expr_ref y1ys1E = mk_concat(y1, ys1E); propagate_eq(dep, lits, x, y1ys1E, true); } return true; @@ -661,12 +662,12 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) { return true; // x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2 - expr_ref xsE(mk_concat(xs), m); - expr_ref ysE(mk_concat(ys), m); - expr_ref y1ys(mk_concat(y1, ysE)); + expr_ref xsE = mk_concat(xs); + expr_ref ysE = mk_concat(ys); + expr_ref y1ys = mk_concat(y1, ysE); expr_ref Z(mk_skolem(m_seq_align, y2, xsE, x, y1ys), m); - expr_ref ZxsE(mk_concat(Z, xsE), m); - expr_ref y1ysZ(mk_concat(y1ys, Z), m); + expr_ref ZxsE = mk_concat(Z, xsE); + expr_ref y1ysZ = mk_concat(y1ys, Z); if (indexes.empty()) { TRACE("seq", tout << "one case\n";); TRACE("seq", display_equation(tout, e);); @@ -726,7 +727,7 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector propagate_eq(dep, lits, y1, xs1E, true); if (xs.size() - ind > ys.size()) { expr_ref xs2E(m_util.str.mk_concat(xs.size()-ind-ys.size(), xs.c_ptr()+ind+ys.size()), m); - expr_ref xs2x(mk_concat(xs2E, x), m); + expr_ref xs2x = mk_concat(xs2E, x); propagate_eq(dep, lits, xs2x, y2, true); } else if (xs.size() - ind == ys.size()) { @@ -734,7 +735,7 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector } else { expr_ref ys1E(m_util.str.mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind), m); - expr_ref ys1y2(mk_concat(ys1E, y2), m); + expr_ref ys1y2 = mk_concat(ys1E, y2); propagate_eq(dep, lits, x, ys1y2, true); } return true; @@ -776,12 +777,12 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) { return true; // xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2 - expr_ref xsE(mk_concat(xs), m); - expr_ref ysE(mk_concat(ys), m); - expr_ref ysy2(mk_concat(ysE, y2), m); + expr_ref xsE = mk_concat(xs); + expr_ref ysE = mk_concat(ys); + expr_ref ysy2 = mk_concat(ysE, y2); expr_ref Z(mk_skolem(m_seq_align, x, ysy2, y1, xsE), m); - expr_ref xsZ(mk_concat(xsE, Z), m); - expr_ref Zysy2(mk_concat(Z, ysy2), m); + expr_ref xsZ = mk_concat(xsE, Z); + expr_ref Zysy2 = mk_concat(Z, ysy2); if (indexes.empty()) { TRACE("seq", tout << "one case\n";); TRACE("seq", display_equation(tout, e);); @@ -850,9 +851,9 @@ bool theory_seq::branch_quat_variable(eq const& e) { SASSERT(!xs.empty() && !ys.empty()); xs.push_back(x2); - expr_ref xsx2(mk_concat(xs), m); + expr_ref xsx2 = mk_concat(xs); ys.push_back(y2); - expr_ref ysy2(mk_concat(ys), m); + expr_ref ysy2 = mk_concat(ys); expr_ref x1(x1_l, m); expr_ref y1(y1_l, m); expr_ref sub(mk_sub(m_util.str.mk_length(x1_l), m_util.str.mk_length(y1_l)), m); @@ -869,8 +870,8 @@ bool theory_seq::branch_quat_variable(eq const& e) { TRACE("seq", tout << "false branch\n";); TRACE("seq", display_equation(tout, e);); expr_ref Z1(mk_skolem(m_seq_align, ysy2, xsx2, x1, y1), m); - expr_ref y1Z1(mk_concat(y1, Z1), m); - expr_ref Z1xsx2(mk_concat(Z1, xsx2), m); + expr_ref y1Z1 = mk_concat(y1, Z1); + expr_ref Z1xsx2 = mk_concat(Z1, xsx2); literal_vector lits; lits.push_back(~lit2); dependency* dep = e.dep(); @@ -882,8 +883,8 @@ bool theory_seq::branch_quat_variable(eq const& e) { TRACE("seq", tout << "true branch\n";); TRACE("seq", display_equation(tout, e);); expr_ref Z2(mk_skolem(m_seq_align, xsx2, ysy2, y1, x1), m); - expr_ref x1Z2(mk_concat(x1, Z2), m); - expr_ref Z2ysy2(mk_concat(Z2, ysy2), m); + expr_ref x1Z2 = mk_concat(x1, Z2); + expr_ref Z2ysy2 = mk_concat(Z2, ysy2); literal_vector lits; lits.push_back(lit2); dependency* dep = e.dep(); @@ -1384,8 +1385,8 @@ bool theory_seq::branch_variable_mb() { for (auto elem : len2) l2 += elem; if (l1 != l2) { TRACE("seq", tout << "lengths are not compatible\n";); - expr_ref l(mk_concat(e.ls()), m); - expr_ref r(mk_concat(e.rs()), m); + expr_ref l = mk_concat(e.ls()); + expr_ref r = mk_concat(e.rs()); expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m); propagate_eq(e.dep(), lnl, lnr, false); change = true; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index f03bdeb60..3bd6baba9 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -443,7 +443,7 @@ namespace smt { expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); } expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); } expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); } - expr* mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return m_util.str.mk_concat(es.size(), es.c_ptr()); } + expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr()), m); } expr_ref mk_concat(ptr_vector const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr()); } expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); } expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); } From 0d4b4b30b1622cc732bdcfff5c1ead64928bbdbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 02:58:06 -0700 Subject: [PATCH 4/6] change storage layout of .Net binding Z3_bool to byte to deal with uninitialized memory reads on larger allocation sizes. Bug introduced when switching from defining Z3_bool as int to the bool type from stdbool Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/api/api_arith.cpp | 6 ++---- src/api/dotnet/AST.cs | 2 +- src/api/dotnet/ASTMap.cs | 2 +- src/api/dotnet/BitVecNum.cs | 8 ++++---- src/api/dotnet/Context.cs | 20 +++++++++++--------- src/api/dotnet/Expr.cs | 21 ++++++++++----------- src/api/dotnet/FPNum.cs | 24 ++++++++++++------------ src/api/dotnet/FiniteDomainNum.cs | 8 ++++---- src/api/dotnet/FuncDecl.cs | 2 +- src/api/dotnet/Global.cs | 4 ++-- src/api/dotnet/Goal.cs | 8 ++++---- src/api/dotnet/IntNum.cs | 8 ++++---- src/api/dotnet/Model.cs | 4 ++-- src/api/dotnet/Params.cs | 4 ++-- src/api/dotnet/Quantifier.cs | 12 ++++++------ src/api/dotnet/Sort.cs | 2 +- src/api/dotnet/Statistics.cs | 4 ++-- src/api/java/Expr.java | 4 ++-- src/api/python/z3/z3.py | 2 +- src/api/z3_api.h | 4 ++-- 21 files changed, 75 insertions(+), 76 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 4452ae613..b082c96e1 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr', PRINT_MODE : 'uint', ERROR_CODE : 'uint' } # Mapping to Java types diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 524d9393d..f245dfd18 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -119,11 +119,9 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { + Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { LOG_Z3_is_algebraic_number(c, a); - int r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? 1 : 0; - //IF_VERBOSE(10, verbose_stream() << r << "\n"); - return r; + return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? Z3_TRUE : Z3_FALSE; } Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index 64ec88d09..2460c50f0 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -43,7 +43,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject)); + 0 != Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 9dcb3ef82..f7c1c5914 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -37,7 +37,7 @@ namespace Microsoft.Z3 { Contract.Requires(k != null); - return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); + return 0 != Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); } /// diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs index c6055db14..66054761a 100644 --- a/src/api/dotnet/BitVecNum.cs +++ b/src/api/dotnet/BitVecNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ba76ae7eb..325758263 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -1963,7 +1963,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(t); - return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed))); + return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0))); } /// @@ -1980,7 +1980,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); + return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0))); } /// @@ -2031,7 +2031,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); + return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0))); } /// @@ -2080,7 +2080,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); + return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0))); } /// @@ -3135,7 +3135,9 @@ namespace Microsoft.Z3 public BitVecNum MkBV(bool[] bits) { Contract.Ensures(Contract.Result() != null); - return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits)); + byte[] _bits = new byte[bits.Length]; + for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0); + return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits)); } @@ -4184,7 +4186,7 @@ namespace Microsoft.Z3 public FPNum MkFPInf(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative)); + return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } /// @@ -4195,7 +4197,7 @@ namespace Microsoft.Z3 public FPNum MkFPZero(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative)); + return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } /// @@ -4241,7 +4243,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } /// @@ -4254,7 +4256,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } /// diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 942baffab..849d1af79 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -179,7 +179,7 @@ namespace Microsoft.Z3 /// public bool IsNumeral { - get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; } + get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; } } /// @@ -188,7 +188,7 @@ namespace Microsoft.Z3 /// True if the term is well-sorted, false otherwise. public bool IsWellSorted { - get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; } + get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; } } /// @@ -256,7 +256,7 @@ namespace Microsoft.Z3 return (IsExpr && Native.Z3_is_eq_sort(Context.nCtx, Native.Z3_mk_bool_sort(Context.nCtx), - Native.Z3_get_sort(Context.nCtx, NativeObject)) ); + Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0); } } @@ -423,7 +423,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) && + return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT); } @@ -789,7 +789,7 @@ namespace Microsoft.Z3 /// Check whether expression is a string constant. /// /// a Boolean - public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } } + public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject) != 0; } } /// /// Retrieve string corresponding to string constant. @@ -1336,7 +1336,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) && + return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_RELATION_SORT); } @@ -1458,7 +1458,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) && + return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); } } @@ -1789,7 +1789,7 @@ namespace Microsoft.Z3 [Pure] internal override void CheckNativeObject(IntPtr obj) { - if (Native.Z3_is_app(Context.nCtx, obj) == false && + if (Native.Z3_is_app(Context.nCtx, obj) == 0 && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a term"); @@ -1822,11 +1822,10 @@ namespace Microsoft.Z3 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); - if ( // Z3_sort_kind.Z3_REAL_SORT == sk && - 0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? + if (0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); - if (Native.Z3_is_numeral_ast(ctx.nCtx, obj)) + if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0) { switch (sk) diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index 4a2575fe4..b6d349149 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -52,7 +52,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Sign is not a Boolean value"); return res != 0; } @@ -86,7 +86,7 @@ namespace Microsoft.Z3 get { UInt64 result = 0; - if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false) + if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return result; } @@ -111,7 +111,7 @@ namespace Microsoft.Z3 /// public string Exponent(bool biased = true) { - return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased); + return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0)); } /// @@ -120,7 +120,7 @@ namespace Microsoft.Z3 public Int64 ExponentInt64(bool biased = true) { Int64 result = 0; - if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false) + if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, (byte)(biased? 1 : 0)) == 0) throw new Z3Exception("Exponent is not a 64 bit integer"); return result; } @@ -133,43 +133,43 @@ namespace Microsoft.Z3 /// public BitVecExpr ExponentBV(bool biased = true) { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased)); + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, (byte)(biased ? 1 : 0))); } /// /// Indicates whether the numeral is a NaN. /// - public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } } + public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is a +oo or -oo. /// - public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } } + public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is +zero or -zero. /// - public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } } + public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is normal. /// - public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } } + public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is subnormal. /// - public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } } + public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is positive. /// - public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } } + public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } /// /// Indicates whether the numeral is negative. /// - public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } } + public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } } #region Internal internal FPNum(Context ctx, IntPtr obj) diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs index fb51e1014..52c0af8bd 100644 --- a/src/api/dotnet/FiniteDomainNum.cs +++ b/src/api/dotnet/FiniteDomainNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 39ddfad83..0587a2276 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -38,7 +38,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject)); + Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); } /// diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs index f242003a8..17963b33d 100644 --- a/src/api/dotnet/Global.cs +++ b/src/api/dotnet/Global.cs @@ -65,7 +65,7 @@ namespace Microsoft.Z3 public static string GetParameter(string id) { IntPtr t; - if (Native.Z3_global_param_get(id, out t) == false) + if (Native.Z3_global_param_get(id, out t) == 0) return null; else return Marshal.PtrToStringAnsi(t); @@ -91,7 +91,7 @@ namespace Microsoft.Z3 /// all contexts globally. public static void ToggleWarningMessages(bool enabled) { - Native.Z3_toggle_warning_messages(enabled); + Native.Z3_toggle_warning_messages((byte)(enabled ? 1 : 0)); } /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index a5e35fcd5..ef2e9a5da 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -103,7 +103,7 @@ namespace Microsoft.Z3 /// public bool Inconsistent { - get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; } + get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } } /// @@ -163,7 +163,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedSat { - get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; } + get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } } /// @@ -171,7 +171,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedUnsat { - get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; } + get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } } /// @@ -251,7 +251,7 @@ namespace Microsoft.Z3 internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal Goal(Context ctx, bool models, bool unsatCores, bool proofs) - : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs))) + : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0))) { Contract.Requires(ctx != null); } diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs index 78fee44f4..64fd78ad2 100644 --- a/src/api/dotnet/IntNum.cs +++ b/src/api/dotnet/IntNum.cs @@ -49,7 +49,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -63,7 +63,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int"); return res; } @@ -77,7 +77,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -91,7 +91,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index 2c6d12dc0..96f62c9fb 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -86,7 +86,7 @@ namespace Microsoft.Z3 return null; else { - if (Native.Z3_is_as_array(Context.nCtx, n) == false) + if (Native.Z3_is_as_array(Context.nCtx, n) == 0) throw new Z3Exception("Argument was not an array constant"); IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); return FuncInterp(new FuncDecl(Context, fd)); @@ -227,7 +227,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); IntPtr v = IntPtr.Zero; - if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false) + if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0) throw new ModelEvaluationFailedException(); else return Expr.Create(Context, v); diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index eeda55755..f0f28d8d3 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -35,7 +35,7 @@ namespace Microsoft.Z3 { Contract.Requires(name != null); - Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value)); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (byte)(value ? 1 : 0)); return this; } @@ -90,7 +90,7 @@ namespace Microsoft.Z3 /// public Params Add(string name, bool value) { - Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value)); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (byte)(value ? 1 : 0)); return this; } diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index d729f7424..d13ca4003 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// public bool IsUniversal { - get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } + get { return 0 != Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } } /// @@ -41,7 +41,7 @@ namespace Microsoft.Z3 /// public bool IsExistential { - get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } + get { return 0 != Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } } /// @@ -193,7 +193,7 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight, + NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight, AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), @@ -201,7 +201,7 @@ namespace Microsoft.Z3 } else { - NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight, + NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (byte)(isForall ? 1 : 0), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), @@ -229,14 +229,14 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight, + NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (byte)(isForall ? 1 : 0) , weight, AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), body.NativeObject); } else { - NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight, + NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (byte)(isForall ? 1 : 0), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index 66acc5c0f..e32fd1eb3 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -41,7 +41,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context == b.Context && - Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject)); + 0 != Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index 6708035bc..c94af625c 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -134,9 +134,9 @@ namespace Microsoft.Z3 { Entry e; string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i); - if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) ) + if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0) e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i)); - else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) ) + else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0) e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i)); else throw new Z3Exception("Unknown data entry value"); diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 75ec9aa75..db5c33e79 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -275,7 +275,7 @@ public class Expr extends AST **/ public boolean isAlgebraicNumber() { - return 0 != Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); + return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); } /** @@ -2108,7 +2108,7 @@ public class Expr extends AST Z3_sort_kind sk = Z3_sort_kind .fromInt(Native.getSortKind(ctx.nCtx(), s)); - if (Native.isAlgebraicNumber(ctx.nCtx(), obj) != 0) // is this a numeral ast? + if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); if (Native.isNumeralAst(ctx.nCtx(), obj)) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f6a5b1950..10198fcc5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2455,7 +2455,7 @@ def _is_numeral(ctx, a): return Z3_is_numeral_ast(ctx.ref(), a) def _is_algebraic(ctx, a): - return 0 != Z3_is_algebraic_number(ctx.ref(), a) + return Z3_is_algebraic_number(ctx.ref(), a) def is_int_value(a): """Return `True` if `a` is an integer value of sort Int. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 74f0fd254..7e12f2fa7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4397,9 +4397,9 @@ extern "C" { /** \brief Return true if the given AST is a real algebraic number. - def_API('Z3_is_algebraic_number', INT, (_in(CONTEXT), _in(AST))) + def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) */ - int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); + Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); /** \brief Convert an \c ast into an \c APP_AST. This is just type casting. From fc8193828d58600b03ecb0109a1446c0524ef99d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 2 Jul 2018 11:43:00 +0100 Subject: [PATCH 5/6] minor simplifications to symbol class --- src/util/symbol.cpp | 29 +++++------------------------ src/util/symbol.h | 5 ++--- 2 files changed, 7 insertions(+), 27 deletions(-) diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 220711003..90b245e6c 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -21,6 +21,7 @@ Revision History: #include "util/region.h" #include "util/string_buffer.h" #include "util/z3_omp.h" +#include symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -60,7 +61,7 @@ public: } }; -internal_symbol_table* g_symbol_table = nullptr; +static internal_symbol_table* g_symbol_table = nullptr; void initialize_symbols() { if (!g_symbol_table) { @@ -140,27 +141,7 @@ bool lt(symbol const & s1, symbol const & s2) { return false; } SASSERT(!s1.is_numerical() && !s2.is_numerical()); - char const * str1 = s1.bare_str(); - char const * str2 = s2.bare_str(); - while (true) { - if (*str1 < *str2) { - return true; - } - else if (*str1 == *str2) { - str1++; - str2++; - if (!*str1) { - SASSERT(*str2); // the strings can't be equal. - return true; - } - if (!*str2) { - SASSERT(*str1); // the strings can't be equal. - return false; - } - } - else { - SASSERT(*str1 > *str2); - return false; - } - } + auto cmp = strcmp(s1.bare_str(), s2.bare_str()); + SASSERT(cmp != 0); + return cmp < 0; } diff --git a/src/util/symbol.h b/src/util/symbol.h index 6a6e93747..88e825551 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -83,8 +83,7 @@ public: // It is the inverse of c_ptr(). // It was made public to simplify the implementation of the C API. static symbol mk_symbol_from_c_ptr(void const * ptr) { - symbol s(ptr); - return s; + return symbol(ptr); } unsigned hash() const { if (m_data == nullptr) return 0x9e3779d9; @@ -93,7 +92,7 @@ public: } bool contains(char c) const; unsigned size() const; - char const * bare_str() const { SASSERT(!is_numerical()); return is_numerical() ? "" : m_data; } + char const * bare_str() const { SASSERT(!is_numerical()); return m_data; } friend std::ostream & operator<<(std::ostream & target, symbol s) { SASSERT(!s.is_marked()); if (GET_TAG(s.m_data) == 0) { From 8791f61aa75e6af444884c13dc004cae454769a6 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 2 Jul 2018 13:41:44 +0100 Subject: [PATCH 6/6] reduce mem allocation in tactic API --- scripts/mk_genfile_common.py | 10 ++-------- src/cmd_context/tactic_cmds.cpp | 8 -------- src/cmd_context/tactic_cmds.h | 20 +++++++++----------- src/nlsat/tactic/qfnra_nlsat_tactic.h | 2 -- src/solver/tactic2solver.cpp | 14 +++++++++----- src/solver/tactic2solver.h | 6 ++++-- src/tactic/tactic.h | 15 --------------- 7 files changed, 24 insertions(+), 51 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 2e0bbe2ca..7fa6d4041 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -718,17 +718,11 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path): fullname, line)) raise e # First pass will just generate the tactic factories - idx = 0 - for data in ADD_TACTIC_DATA: - fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2])) - idx = idx + 1 - fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n') + fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n') fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n') fout.write('void install_tactics(tactic_manager & ctx) {\n') - idx = 0 for data in ADD_TACTIC_DATA: - fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) - idx = idx + 1 + fout.write(' ADD_TACTIC_CMD("%s", "%s", %s);\n' % data) for data in ADD_PROBE_DATA: fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) fout.write('}\n') diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index cbe44da2d..cf0fd5111 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -32,14 +32,6 @@ Notes: #include "cmd_context/cmd_context_to_goal.h" #include "cmd_context/echo_tactic.h" -tactic_cmd::~tactic_cmd() { - dealloc(m_factory); -} - -tactic * tactic_cmd::mk(ast_manager & m) { - return (*m_factory)(m, params_ref()); -} - probe_info::probe_info(symbol const & n, char const * d, probe * p): m_name(n), m_descr(d), diff --git a/src/cmd_context/tactic_cmds.h b/src/cmd_context/tactic_cmds.h index fc15c795b..691771509 100644 --- a/src/cmd_context/tactic_cmds.h +++ b/src/cmd_context/tactic_cmds.h @@ -19,30 +19,28 @@ Notes: #define TACTIC_CMDS_H_ #include "ast/ast.h" +#include "util/params.h" #include "util/cmd_context_types.h" #include "util/ref.h" class tactic; class probe; -class tactic_factory; + +typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&); class tactic_cmd { - symbol m_name; - char const * m_descr; - tactic_factory * m_factory; + symbol m_name; + char const * m_descr; + tactic_factory m_factory; public: - tactic_cmd(symbol const & n, char const * d, tactic_factory * f): - m_name(n), m_descr(d), m_factory(f) { - SASSERT(m_factory); - } - - ~tactic_cmd(); + tactic_cmd(symbol const & n, char const * d, tactic_factory f): + m_name(n), m_descr(d), m_factory(f) {} symbol get_name() const { return m_name; } char const * get_descr() const { return m_descr; } - tactic * mk(ast_manager & m); + tactic * mk(ast_manager & m) { return m_factory(m, params_ref()); } }; void install_core_tactic_cmds(cmd_context & ctx); diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.h b/src/nlsat/tactic/qfnra_nlsat_tactic.h index b1a4d8392..29dbadb9e 100644 --- a/src/nlsat/tactic/qfnra_nlsat_tactic.h +++ b/src/nlsat/tactic/qfnra_nlsat_tactic.h @@ -25,8 +25,6 @@ class tactic; tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref()); -MK_SIMPLE_TACTIC_FACTORY(qfnra_nlsat_fct, mk_qfnra_nlsat_tactic(m, p)); - /* ADD_TACTIC("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", "mk_qfnra_nlsat_tactic(m, p)") */ diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 94509e3f6..135d402e6 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -19,6 +19,7 @@ Author: Notes: --*/ +#include "solver/tactic2solver.h" #include "solver/solver_na2as.h" #include "tactic/tactic.h" #include "ast/ast_translation.h" @@ -31,6 +32,8 @@ Notes: option for applications trying to solve many easy queries that a similar to each other. */ + +namespace { class tactic2solver : public solver_na2as { expr_ref_vector m_assertions; unsigned_vector m_scopes; @@ -258,6 +261,7 @@ unsigned tactic2solver::get_num_assertions() const { expr * tactic2solver::get_assertion(unsigned idx) const { return m_assertions.get(idx); } +} solver * mk_tactic2solver(ast_manager & m, @@ -270,6 +274,7 @@ solver * mk_tactic2solver(ast_manager & m, return alloc(tactic2solver, m, t, p, produce_proofs, produce_models, produce_unsat_cores, logic); } +namespace { class tactic2solver_factory : public solver_factory { ref m_tactic; public: @@ -284,24 +289,23 @@ public: }; class tactic_factory2solver_factory : public solver_factory { - scoped_ptr m_factory; + tactic_factory m_factory; public: - tactic_factory2solver_factory(tactic_factory * f):m_factory(f) { + tactic_factory2solver_factory(tactic_factory f):m_factory(f) { } - ~tactic_factory2solver_factory() override {} - solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override { tactic * t = (*m_factory)(m, p); return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); } }; +} solver_factory * mk_tactic2solver_factory(tactic * t) { return alloc(tactic2solver_factory, t); } -solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f) { +solver_factory * mk_tactic_factory2solver_factory(tactic_factory f) { return alloc(tactic_factory2solver_factory, f); } diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h index ddab66dc5..d9fffba24 100644 --- a/src/solver/tactic2solver.h +++ b/src/solver/tactic2solver.h @@ -23,12 +23,14 @@ Notes: #define TACTIC2SOLVER_H_ #include "util/params.h" + class ast_manager; class tactic; -class tactic_factory; class solver; class solver_factory; +typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&); + solver * mk_tactic2solver(ast_manager & m, tactic * t = nullptr, params_ref const & p = params_ref(), @@ -39,6 +41,6 @@ solver * mk_tactic2solver(ast_manager & m, solver_factory * mk_tactic2solver_factory(tactic * t); -solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f); +solver_factory * mk_tactic_factory2solver_factory(tactic_factory f); #endif diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index c9b5a23fd..92cc7315f 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -119,21 +119,6 @@ tactic * mk_fail_if_undecided_tactic(); tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl); tactic * mk_trace_tactic(char const * tag); -class tactic_factory { -public: - virtual ~tactic_factory() {} - virtual tactic * operator()(ast_manager & m, params_ref const & p) = 0; -}; - -#define MK_TACTIC_FACTORY(NAME, CODE) \ -class NAME : public tactic_factory { \ -public: \ - virtual ~NAME() {} \ - virtual tactic * operator()(ast_manager & m, params_ref const & p) { CODE } \ -}; - -#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) - void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result); lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);