From 8fc0ba0ab544a92e93033626c9744ce9e6c101a4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 12:33:53 +0100 Subject: [PATCH 01/17] Moved auxiliary fp.isNaN lemma injection to the right place. Fixes #102 --- src/ast/fpa/fpa2bv_converter.cpp | 7 ------- src/tactic/fpa/fpa2bv_tactic.cpp | 16 ++++++++++++++++ 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index cc0fef3c3..1d794c898 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3044,13 +3044,6 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { m_simp.mk_not(sig_is_zero, sig_is_not_zero); m_simp.mk_eq(exp, top_exp, exp_is_top); m_simp.mk_and(exp_is_top, sig_is_not_zero, result); - - // Inject auxiliary lemmas that fix e to the one and only NaN value, - // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation - // has a value to propagate. - m_extra_assertions.push_back(m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1))); - m_extra_assertions.push_back(m.mk_eq(exp, top_exp)); - m_extra_assertions.push_back(m.mk_eq(sig, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(sig)))); } void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 5fb35d972..9149f1b9a 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -88,6 +88,22 @@ class fpa2bv_tactic : public tactic { new_pr = m.mk_modus_ponens(pr, new_pr); } g->update(idx, new_curr, new_pr, g->dep(idx)); + + if (is_app(new_curr)) { + const app * a = to_app(new_curr.get()); + if (a->get_family_id() == m_conv.fu().get_family_id() && + a->get_decl_kind() == OP_FPA_IS_NAN) { + // Inject auxiliary lemmas that fix e to the one and only NaN value, + // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation + // has a value to propagate. + expr * sgn, *sig, *exp; + expr_ref top_exp(m); + m_conv.split_fp(new_curr, sgn, exp, sig); + m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)); + m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))); + m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))); + } + } } if (g->models_enabled()) From 279ef05713462237e427dc96192d911a9cb18dbc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:57:05 -0700 Subject: [PATCH 02/17] expose BoolExpr[] for ASTVector and merge common functionality Signed-off-by: Nikolaj Bjorner --- src/api/java/ASTVector.java | 8 ++++++++ src/api/java/Fixedpoint.java | 12 ++---------- src/api/java/InterpolationContext.java | 8 +++++--- src/api/java/Solver.java | 6 +----- 4 files changed, 16 insertions(+), 18 deletions(-) diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 9c6504493..e08a75e7f 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -119,4 +119,12 @@ public class ASTVector extends Z3Object getContext().getASTVectorDRQ().add(o); super.decRef(o); } + + BoolExpr[] ToBoolArray() { + int n = size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(getContext(), get(i).getNativeObject()); + return res; + } } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index c9d14288b..daa0f4e3f 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -298,11 +298,7 @@ public class Fixedpoint extends Z3Object ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( getContext().nCtx(), getNativeObject())); - int n = v.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); - return res; + return v.ToBoolArray(); } /** @@ -315,11 +311,7 @@ public class Fixedpoint extends Z3Object ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( getContext().nCtx(), getNativeObject())); - int n = v.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); - return res; + return v.ToBoolArray(); } /** diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 667c91a53..50c6a223a 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public ASTVector interp = null; + public BoolExpr[] interp = null; public Model model = null; }; @@ -109,8 +109,10 @@ public class InterpolationContext extends Context ComputeInterpolantResult res = new ComputeInterpolantResult(); Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); - res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); + res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); + if (res.status == Z3_lbool.Z3_L_FALSE) { + res.interp = (new ASTVector(this, n_i.value)).ToBoolArray(); + } if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index e4ba9de42..7c4c1f4b9 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -190,11 +190,7 @@ public class Solver extends Z3Object { ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); - int n = assrts.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject()); - return res; + return assrts.ToBoolArray(); } /** From 13a3bdd7a3589c0a7e8b622acfba20e542c2f2b8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 22 May 2015 10:28:19 -0700 Subject: [PATCH 03/17] fix proof for extended GCD rule --- src/smt/theory_arith_int.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index b600dd3c0..7c9e67da6 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -777,8 +777,8 @@ namespace smt { // u += ncoeff * lower_bound(v).get_rational(); u.addmul(ncoeff, lower_bound(v).get_rational()); } - lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); - upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); + lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled()); + upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled()); } else if (gcds.is_zero()) { gcds = abs_ncoeff; From e438143abce11f3217b275c916307a9cb14ca51e Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 22 May 2015 11:02:26 -0700 Subject: [PATCH 04/17] fix for github issue #105 --- src/interp/iz3translate.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index f510f4070..2debdaf42 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -966,7 +966,7 @@ public: get_linear_coefficients(t,coeffs); if(coeffs.size() == 0) return make_int("1"); // arbitrary - rational d = coeffs[0]; + rational d = abs(coeffs[0]); for(unsigned i = 1; i < coeffs.size(); i++){ d = gcd(d,coeffs[i]); } From 6f6cd61817a1f5767be5f84a625c12ff14332a79 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 20:30:12 +0100 Subject: [PATCH 05/17] Bugfix for float-to-float conversion. Fixes #77 --- src/ast/fpa/fpa2bv_converter.cpp | 116 ++++++++++++++++++++----------- src/util/mpf.cpp | 2 +- 2 files changed, 78 insertions(+), 40 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1d794c898..2c32e7f1a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -48,19 +48,31 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); - expr_ref sgn(m), s(m), e(m); - m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), sgn); - m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), e); - m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), s); + TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl; + tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;); + + expr_ref eq_sgn(m), eq_exp(m), eq_sig(m); + m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn); + m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp); + m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig); + + dbg_decouple("fpa2bv_eq_sgn", eq_sgn); + dbg_decouple("fpa2bv_eq_exp", eq_exp); + dbg_decouple("fpa2bv_eq_sig", eq_sig); + + expr_ref both_the_same(m); + m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same); + dbg_decouple("fpa2bv_eq_both_the_same", both_the_same); // The SMT FPA theory asks for _one_ NaN value, but the bit-blasting // has many, like IEEE754. This encoding of equality makes it look like // a single NaN again. - expr_ref both_the_same(m), a_is_nan(m), b_is_nan(m), both_are_nan(m); - m_simp.mk_and(sgn, s, e, both_the_same); + expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m); mk_is_nan(a, a_is_nan); mk_is_nan(b, b_is_nan); m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan); + dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan); + m_simp.mk_or(both_are_nan, both_the_same, result); } @@ -2051,6 +2063,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); + dbg_decouple("fpa2bv_to_float_x_sgn", sgn); dbg_decouple("fpa2bv_to_float_x_sig", sig); dbg_decouple("fpa2bv_to_float_x_exp", exp); dbg_decouple("fpa2bv_to_float_lz", lz); @@ -2068,13 +2081,17 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * // make sure that sig has at least to_sbits + 3 res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits + 3 - from_sbits)); } - else if (from_sbits >(to_sbits + 3)) { + else if (from_sbits > (to_sbits + 3)) { // collapse the extra bits into a sticky bit. expr_ref sticky(m), low(m), high(m); - low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); + SASSERT(m_bv_util.get_bv_size(high) == to_sbits + 2); + low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); - res_sig = m_bv_util.mk_concat(high, sticky); + SASSERT(m_bv_util.get_bv_size(sticky) == 1); + dbg_decouple("fpa2bv_to_float_sticky", sticky); + res_sig = m_bv_util.mk_concat(high, sticky); + SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 3); } else res_sig = sig; @@ -2083,8 +2100,9 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * unsigned sig_sz = m_bv_util.get_bv_size(res_sig); SASSERT(sig_sz == to_sbits + 4); - expr_ref exponent_overflow(m); + expr_ref exponent_overflow(m), exponent_underflow(m); exponent_overflow = m.mk_false(); + exponent_underflow = m.mk_false(); if (from_ebits < (to_ebits + 2)) { res_exp = m_bv_util.mk_sign_extend(to_ebits - from_ebits + 2, exp); @@ -2094,37 +2112,58 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz); res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); } - else if (from_ebits >(to_ebits + 2)) { - expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); - expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m); - high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp); - low = m_bv_util.mk_extract(to_ebits + 1, 0, exp); - lows = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low); - - high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get()); - high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); - - zero1 = m_bv_util.mk_numeral(0, 1); - m_simp.mk_eq(high_red_and, one1, h_and_eq); - m_simp.mk_eq(high_red_or, zero1, h_or_eq); - m_simp.mk_eq(lows, zero1, s_is_zero); - m_simp.mk_eq(lows, one1, s_is_one); - - expr_ref c2(m); - m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2); - m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow); - - // Note: Upon overflow, we _could_ try to shift the significand around... - - // subtract lz for subnormal numbers. - expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m); - lz_ext = m_bv_util.mk_extract(to_ebits + 1, 0, lz); + else if (from_ebits > (to_ebits + 2)) { + expr_ref lz_rest(m), lz_redor(m), lz_redor_bool(m); lz_rest = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, lz); lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get()); m_simp.mk_eq(lz_redor, one1, lz_redor_bool); - m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow); + dbg_decouple("fpa2bv_to_float_exp_lz_redor", lz_redor); - res_exp = m_bv_util.mk_bv_sub(low, lz_ext); + // subtract lz for subnormal numbers. + expr_ref exp_sub_lz(m); + exp_sub_lz = m_bv_util.mk_bv_sub(exp, lz); + dbg_decouple("fpa2bv_to_float_exp_sub_lz", exp_sub_lz); + + expr_ref high(m), low(m), low_msb(m); + expr_ref no_ovf(m), zero1(m); + high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp_sub_lz); + low = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz); + low_msb = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low); + dbg_decouple("fpa2bv_to_float_exp_high", high); + dbg_decouple("fpa2bv_to_float_exp_low", low); + dbg_decouple("fpa2bv_to_float_exp_low_msb", low_msb); + + res_exp = low; + + expr_ref high_red_or(m), high_red_and(m); + high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get()); + high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); + + expr_ref h_or_eq_0(m), h_and_eq_1(m), low_msb_is_one(m), low_msb_is_zero(m); + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(high_red_and, one1, h_and_eq_1); + m_simp.mk_eq(high_red_or, zero1, h_or_eq_0); + m_simp.mk_eq(low_msb, zero1, low_msb_is_zero); + m_simp.mk_eq(low_msb, one1, low_msb_is_one); + dbg_decouple("fpa2bv_to_float_exp_h_and_eq_1", h_and_eq_1); + dbg_decouple("fpa2bv_to_float_exp_h_or_eq_0", h_or_eq_0); + dbg_decouple("fpa2bv_to_float_exp_s_is_zero", low_msb_is_zero); + dbg_decouple("fpa2bv_to_float_exp_s_is_one", low_msb_is_one); + + m_simp.mk_and(h_or_eq_0, low_msb_is_one, exponent_underflow); + m_simp.mk_and(h_and_eq_1, low_msb_is_zero, exponent_overflow); + m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow); + dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); + dbg_decouple("fpa2bv_to_float_exp_udf", exponent_underflow); + + // exponent underflow means that the result is the smallest + // representable float, rounded according to rm. + m_simp.mk_ite(exponent_underflow, + m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1), + m_bv_util.mk_numeral(1, to_ebits+1)), + res_exp, + res_exp); + m_simp.mk_ite(exponent_underflow, m_bv_util.mk_numeral(1, to_sbits+4), res_sig, res_sig); } else // from_ebits == (to_ebits + 2) res_exp = m_bv_util.mk_bv_sub(exp, lz); @@ -2143,8 +2182,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * m_simp.mk_eq(sgn, one1, is_neg); mk_ite(is_neg, ninf, pinf, sig_inf); - dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); - mk_ite(exponent_overflow, sig_inf, rounded, v6); + mk_ite(exponent_overflow, sig_inf, rounded, v6); // And finally, we tie them together. mk_ite(c5, v5, v6, result); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index e66f6d270..1521a8f87 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -348,7 +348,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode bool sticky = false; while (ds < 0) { - if (!m_mpz_manager.is_even(o.significand)) sticky = true; + sticky |= m_mpz_manager.is_odd(o.significand); m_mpz_manager.machine_div2k(o.significand, 1); ds++; } From c577ab361b0b668434726316b86afe961013b82b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 23 May 2015 11:45:12 +0100 Subject: [PATCH 06/17] fix assorted undefined behaviors caught by clang Signed-off-by: Nuno Lopes --- src/ast/ast.cpp | 9 ++++++--- src/math/polynomial/polynomial.cpp | 1 + src/smt/smt_justification.cpp | 3 ++- src/util/hash.cpp | 2 +- src/util/inf_int_rational.cpp | 25 ++++++++++++++++++++++--- src/util/inf_int_rational.h | 6 ++++-- src/util/inf_rational.cpp | 30 +++++++++++++++++++++++++----- src/util/inf_rational.h | 10 ++++++---- src/util/rational.cpp | 16 ++++++++++++++-- 9 files changed, 81 insertions(+), 21 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d56bb73ff..59efb2a89 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -316,7 +316,8 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain, decl(AST_FUNC_DECL, name, info), m_arity(arity), m_range(range) { - memcpy(const_cast(get_domain()), domain, sizeof(sort *) * arity); + if (arity != 0) + memcpy(const_cast(get_domain()), domain, sizeof(sort *) * arity); } // ----------------------------------- @@ -378,8 +379,10 @@ quantifier::quantifier(bool forall, unsigned num_decls, sort * const * decl_sort memcpy(const_cast(get_decl_sorts()), decl_sorts, sizeof(sort *) * num_decls); memcpy(const_cast(get_decl_names()), decl_names, sizeof(symbol) * num_decls); - memcpy(const_cast(get_patterns()), patterns, sizeof(expr *) * num_patterns); - memcpy(const_cast(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns); + if (num_patterns != 0) + memcpy(const_cast(get_patterns()), patterns, sizeof(expr *) * num_patterns); + if (num_no_patterns != 0) + memcpy(const_cast(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns); } // ----------------------------------- diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 8f4c55392..638c83642 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -542,6 +542,7 @@ namespace polynomial { increase_capacity(sz * 2); SASSERT(sz < m_capacity); m_ptr->m_size = sz; + if (sz == 0) return; memcpy(m_ptr->m_powers, pws, sizeof(power) * sz); } diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 81f496187..de3594fcc 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -308,7 +308,8 @@ namespace smt { simple_justification(r, num_lits, lits), m_num_eqs(num_eqs) { m_eqs = new (r) enode_pair[num_eqs]; - memcpy(m_eqs, eqs, sizeof(enode_pair) * num_eqs); + if (num_eqs != 0) + memcpy(m_eqs, eqs, sizeof(enode_pair) * num_eqs); DEBUG_CODE({ for (unsigned i = 0; i < num_eqs; i++) { SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root()); diff --git a/src/util/hash.cpp b/src/util/hash.cpp index 8b7530376..41c4db584 100644 --- a/src/util/hash.cpp +++ b/src/util/hash.cpp @@ -23,7 +23,7 @@ Revision History: // I'm using Bob Jenkin's hash function. // http://burtleburtle.net/bob/hash/doobs.html unsigned string_hash(const char * str, unsigned length, unsigned init_value) { - register unsigned a, b, c, len; + unsigned a, b, c, len; /* Set up the internal state */ len = length; diff --git a/src/util/inf_int_rational.cpp b/src/util/inf_int_rational.cpp index 54a838a75..7bc68e641 100644 --- a/src/util/inf_int_rational.cpp +++ b/src/util/inf_int_rational.cpp @@ -19,9 +19,9 @@ Revision History: #include #include"inf_int_rational.h" -inf_int_rational inf_int_rational::m_zero(0); -inf_int_rational inf_int_rational::m_one(1); -inf_int_rational inf_int_rational::m_minus_one(-1); +inf_int_rational inf_int_rational::m_zero; +inf_int_rational inf_int_rational::m_one; +inf_int_rational inf_int_rational::m_minus_one; std::string inf_int_rational::to_string() const { if (m_second == 0) { @@ -39,3 +39,22 @@ std::string inf_int_rational::to_string() const { return s.str(); } +void initialize_inf_int_rational() { + inf_int_rational::init(); +} + +void inf_int_rational::init() { + m_zero.m_first = rational::zero(); + m_one.m_first = rational::one(); + m_minus_one.m_first = rational::minus_one(); +} + +void finalize_inf_int_rational() { + inf_int_rational::finalize(); +} + +void inf_int_rational::finalize() { + m_zero.~inf_int_rational(); + m_one.~inf_int_rational(); + m_minus_one.~inf_int_rational(); +} diff --git a/src/util/inf_int_rational.h b/src/util/inf_int_rational.h index b1b1fb89f..06cbc1267 100644 --- a/src/util/inf_int_rational.h +++ b/src/util/inf_int_rational.h @@ -33,6 +33,8 @@ class inf_int_rational { rational m_first; int m_second; public: + static void init(); // called from rational::initialize() only + static void finalize(); // called from rational::finalize() only unsigned hash() const { return m_first.hash() ^ (static_cast(m_second) + 1); @@ -272,7 +274,7 @@ class inf_int_rational { if (r.m_second >= 0) { return r.m_first; } - return r.m_first - rational(1); + return r.m_first - rational::one(); } return floor(r.m_first); @@ -283,7 +285,7 @@ class inf_int_rational { if (r.m_second <= 0) { return r.m_first; } - return r.m_first + rational(1); + return r.m_first + rational::one(); } return ceil(r.m_first); diff --git a/src/util/inf_rational.cpp b/src/util/inf_rational.cpp index 3837d2c15..0b043e94d 100644 --- a/src/util/inf_rational.cpp +++ b/src/util/inf_rational.cpp @@ -18,9 +18,9 @@ Revision History: --*/ #include"inf_rational.h" -inf_rational inf_rational::m_zero(0); -inf_rational inf_rational::m_one(1); -inf_rational inf_rational::m_minus_one(-1); +inf_rational inf_rational::m_zero; +inf_rational inf_rational::m_one; +inf_rational inf_rational::m_minus_one; inf_rational inf_mult(inf_rational const& r1, inf_rational const& r2) { @@ -128,7 +128,7 @@ inf_rational inf_power(inf_rational const& r, unsigned n) // 0 will work. } else if (r.m_first.is_zero()) { - result.m_first = rational(-1); + result.m_first = rational::minus_one(); } else if (r.m_first.is_pos()) { result.m_first = rational(r.m_first - r.m_first/rational(2)).expt(n); @@ -152,7 +152,7 @@ inf_rational sup_power(inf_rational const& r, unsigned n) result.m_first = r.m_first.expt(n); } else if (r.m_first.is_zero() || (n == 0)) { - result.m_first = rational(1); + result.m_first = rational::one(); } else if (r.m_first.is_pos() || is_even) { result.m_first = rational(r.m_first + r.m_first/rational(2)).expt(n); @@ -177,3 +177,23 @@ inf_rational sup_root(inf_rational const& r, unsigned n) // use r. return r; } + +void initialize_inf_rational() { + inf_rational::init(); +} + +void inf_rational::init() { + m_zero.m_first = rational::zero(); + m_one.m_first = rational::one(); + m_minus_one.m_first = rational::minus_one(); +} + +void finalize_inf_rational() { + inf_rational::finalize(); +} + +void inf_rational::finalize() { + m_zero.~inf_rational(); + m_one.~inf_rational(); + m_minus_one.~inf_rational(); +} diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index e1060a7b0..b832b8793 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -33,6 +33,8 @@ class inf_rational { rational m_first; rational m_second; public: + static void init(); // called from rational::initialize() only + static void finalize(); // called from rational::finalize() only unsigned hash() const { return m_first.hash() ^ (m_second.hash()+1); @@ -40,7 +42,7 @@ class inf_rational { struct hash_proc { unsigned operator()(inf_rational const& r) const { return r.hash(); } }; - struct eq_proc { bool operator()(inf_rational const& r1, inf_rational const& r2) const { return r1 == r2; } }; + struct eq_proc { bool operator()(inf_rational const& r1, inf_rational const& r2) const { return r1 == r2; } }; void swap(inf_rational & n) { m_first.swap(n.m_first); @@ -82,7 +84,7 @@ class inf_rational { explicit inf_rational(rational const& r, bool pos_inf): m_first(r), - m_second(pos_inf?rational(1):rational(-1)) + m_second(pos_inf ? rational::one() : rational::minus_one()) {} inf_rational(rational const& r): @@ -313,7 +315,7 @@ class inf_rational { if (r.m_second.is_nonneg()) { return r.m_first; } - return r.m_first - rational(1); + return r.m_first - rational::one(); } return floor(r.m_first); @@ -324,7 +326,7 @@ class inf_rational { if (r.m_second.is_nonpos()) { return r.m_first; } - return r.m_first + rational(1); + return r.m_first + rational::one(); } return ceil(r.m_first); diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 743038972..43dc9110a 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -29,9 +29,9 @@ rational rational::m_one; rational rational::m_minus_one; vector rational::m_powers_of_two; -void mk_power_up_to(vector & pws, unsigned n) { +static void mk_power_up_to(vector & pws, unsigned n) { if (pws.empty()) { - pws.push_back(rational(1)); + pws.push_back(rational::one()); } unsigned sz = pws.size(); rational curr = pws[sz - 1]; @@ -53,16 +53,28 @@ rational rational::power_of_two(unsigned k) { return result; } +// in inf_rational.cpp +void initialize_inf_rational(); +void finalize_inf_rational(); + +// in inf_int_rational.cpp +void initialize_inf_int_rational(); +void finalize_inf_int_rational(); + void rational::initialize() { if (!g_mpq_manager) { g_mpq_manager = alloc(synch_mpq_manager); m().set(m_zero.m_val, 0); m().set(m_one.m_val, 1); m().set(m_minus_one.m_val, -1); + initialize_inf_rational(); + initialize_inf_int_rational(); } } void rational::finalize() { + finalize_inf_rational(); + finalize_inf_int_rational(); m_powers_of_two.finalize(); m_zero.~rational(); m_one.~rational(); From d5c39798ea455262bf31b86d87d00ca08af61895 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 12:02:53 +0100 Subject: [PATCH 07/17] Bugfix for hwf --- src/util/hwf.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 5a41ac86c..94255bb84 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -17,16 +17,15 @@ Revision History: --*/ #include +#include #ifdef _WINDOWS #pragma float_control( except, on ) // exception semantics; this does _not_ mean that exceptions are enabled (we want them off!) #pragma float_control( precise, on ) // precise semantics (no guessing!) #pragma fp_contract(off) // contractions off (`contraction' means x*y+z is turned into a fused-mul-add). #pragma fenv_access(on) // fpu environment sensitivity (needed to be allowed to make FPU mode changes). +#include #else -#ifdef _WINDOWS -#pragma STDC FENV_ACCESS ON -#endif #include #include #endif @@ -35,8 +34,6 @@ Revision History: #define USE_INTRINSICS #endif -#include - #include"hwf.h" // Note: From 08b563532788bef18c70ec5980eabf45c8eaa6b2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 23 May 2015 12:13:39 +0100 Subject: [PATCH 08/17] fix unaligned load in hash_string() Signed-off-by: Nuno Lopes --- src/test/polynomial_factorization.cpp | 3 ++- src/util/hash.cpp | 14 +++++++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/test/polynomial_factorization.cpp b/src/test/polynomial_factorization.cpp index 06c67b9c2..7af0742ef 100644 --- a/src/test/polynomial_factorization.cpp +++ b/src/test/polynomial_factorization.cpp @@ -24,7 +24,8 @@ Notes: #include"polynomial_factorization.h" #endif -using namespace std; +using std::cout; +using std::endl; // some prime numbers unsigned primes[] = { diff --git a/src/util/hash.cpp b/src/util/hash.cpp index 41c4db584..bb5ca0a41 100644 --- a/src/util/hash.cpp +++ b/src/util/hash.cpp @@ -19,6 +19,13 @@ Revision History: #include"debug.h" #include"hash.h" +#include + +static unsigned read_unsigned(const char *s) { + unsigned n; + memcpy(&n, s, sizeof(unsigned)); + return n; +} // I'm using Bob Jenkin's hash function. // http://burtleburtle.net/bob/hash/doobs.html @@ -31,10 +38,11 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) { c = init_value; /* the previous hash value */ /*---------------------------------------- handle most of the key */ + SASSERT(sizeof(unsigned) == 4); while (len >= 12) { - a += reinterpret_cast(str)[0]; - b += reinterpret_cast(str)[1]; - c += reinterpret_cast(str)[2]; + a += read_unsigned(str); + b += read_unsigned(str+4); + c += read_unsigned(str+8); mix(a,b,c); str += 12; len -= 12; } From 98f33c3f8b8c5fc64679656dad99798afa21c38c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 13:10:07 +0100 Subject: [PATCH 09/17] Bug/build fix for hwf::fma --- src/util/hwf.cpp | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 94255bb84..21f1c281f 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -16,6 +16,7 @@ Author: Revision History: --*/ +#include #include #include @@ -24,10 +25,8 @@ Revision History: #pragma float_control( precise, on ) // precise semantics (no guessing!) #pragma fp_contract(off) // contractions off (`contraction' means x*y+z is turned into a fused-mul-add). #pragma fenv_access(on) // fpu environment sensitivity (needed to be allowed to make FPU mode changes). -#include #else -#include -#include +#include #endif #ifndef _M_IA64 @@ -54,7 +53,7 @@ Revision History: hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) -{ +{ #ifdef _WINDOWS #if defined(_AMD64_) || defined(_M_IA64) // Precision control is not supported on x64. @@ -307,14 +306,28 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co // CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium, // Intel Sandybridge and AMD Bulldozers support that (via AVX). -#ifdef _M_IA64 - // IA64 (Itanium) will do it, if contractions are on. set_rounding_mode(rm); + +#ifdef _M_IA64 + // IA64 (Itanium) will do it, if contractions are on. o.value = x.value * y.value + z.value; #else - set_rounding_mode(rm); +#if defined(_WINDOWS) +#if _MSC_VER >= 1800 + o.value = ::fma(x.value, y.value, z.value); +#else // Windows, older than VS 2013 + #ifdef USE_INTRINSICS + _mm_store_sd(&o.value, _mm_fmadd_sd(_mm_set_sd(x.value), _mm_set_sd(y.value), _mm_set_sd(z.value))); + #else + // If all else fails, we are imprecise. + o.value = (x.value * y.value) + z; + #endif +#endif +#else + // Linux, OSX o.value = ::fma(x.value, y.value, z.value); #endif +#endif } #ifdef _M_IA64 From a361e4dcefc9e63f5164c4bc09fea4419c7f3b54 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 16:40:43 +0100 Subject: [PATCH 10/17] typo --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index da24f4caf..ec321b66d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6022,7 +6022,7 @@ END_MLAPI_EXCLUDE /** \brief Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. - Return the set of queries in the file. + Return the set of queries in the string. \param c - context. \param f - fixedpoint context. From e33ff427664f161f9960bddce964f0e760f3f146 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 16:49:41 +0100 Subject: [PATCH 11/17] Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality. Fixes #103 --- src/api/dotnet/ASTMap.cs | 5 +++-- src/api/dotnet/ASTVector.cs | 24 ++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 6f296147e..596b2943f 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -98,11 +98,12 @@ namespace Microsoft.Z3 /// /// The keys stored in the map. /// - public ASTVector Keys + public AST[] Keys { get { - return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject)); + ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject)); + return res.ToArray(); } } diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index b70ff13b6..f858c7862 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -99,6 +99,30 @@ namespace Microsoft.Z3 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject); } + /// + /// Translates an AST vector into an AST[] + /// + public AST[] ToArray() + { + uint n = Size; + AST[] res = new AST[n]; + for (uint i = 0; i < n; i++) + res[i] = AST.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an AST vector into an Expr[] + /// + public Expr[] ToExprArray() + { + uint n = Size; + Expr[] res = new Expr[n]; + for (uint i = 0; i < n; i++) + res[i] = Expr.Create(this.Context, this[i].NativeObject); + return res; + } + #region Internal internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); } From d8f6d84217a6999fd70eccae9c7656bc86bd7654 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 16:53:47 +0100 Subject: [PATCH 12/17] Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality. Fixes #103 --- src/api/dotnet/Fixedpoint.cs | 31 +- src/api/dotnet/InterpolationContext.cs | 10 +- src/api/dotnet/Model.cs | 8 +- src/api/dotnet/Solver.cs | 22 +- src/api/java/ASTMap.java | 6 +- src/api/java/ASTVector.java | 23 +- src/api/java/Fixedpoint.java | 36 +- src/api/java/InterpolationContext.java | 11 +- src/api/java/Model.java | 6 +- src/api/java/Solver.java | 19 +- src/api/ml/z3.ml | 661 ++++++++++++++----------- src/api/ml/z3.mli | 134 ++--- 12 files changed, 529 insertions(+), 438 deletions(-) diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 925e741c7..54dbcd3c1 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -269,14 +269,6 @@ namespace Microsoft.Z3 AST.ArrayLength(queries), AST.ArrayToNative(queries)); } - BoolExpr[] ToBoolExprs(ASTVector v) { - uint n = v.Size; - BoolExpr[] res = new BoolExpr[n]; - for (uint i = 0; i < n; i++) - res[i] = new BoolExpr(Context, v[i].NativeObject); - return res; - } - /// /// Retrieve set of rules added to fixedpoint context. /// @@ -286,7 +278,8 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != null); - return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject))); + ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)); + return (BoolExpr[])av.ToExprArray(); } } @@ -299,7 +292,8 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != null); - return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject))); + ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)); + return (BoolExpr[])av.ToExprArray(); } } @@ -316,21 +310,24 @@ namespace Microsoft.Z3 } } - /// + /// /// Parse an SMT-LIB2 file with fixedpoint rules. /// Add the rules to the current fixedpoint context. /// Return the set of queries in the file. /// - public BoolExpr[] ParseFile(string file) { - return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file))); + public BoolExpr[] ParseFile(string file) + { + ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)); + return (BoolExpr[])av.ToExprArray(); } /// /// Similar to ParseFile. Instead it takes as argument a string. - /// - - public BoolExpr[] ParseString(string s) { - return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s))); + /// + public BoolExpr[] ParseString(string s) + { + ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)); + return (BoolExpr[])av.ToExprArray(); } diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index d54c8f634..9fbdf456e 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -59,11 +59,7 @@ namespace Microsoft.Z3 CheckContextMatch(p); ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject)); - uint n = seq.Size; - Expr[] res = new Expr[n]; - for (uint i = 0; i < n; i++) - res[i] = Expr.Create(this, seq[i].NativeObject); - return res; + return seq.ToExprArray(); } /// @@ -72,7 +68,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_compute_interpolant in the C/C++ API, which is /// well documented. - public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model) + public Z3_lbool ComputeInterpolant(Expr pat, Params p, out Expr[] interp, out Model model) { Contract.Requires(pat != null); Contract.Requires(p != null); @@ -84,7 +80,7 @@ namespace Microsoft.Z3 IntPtr i = IntPtr.Zero, m = IntPtr.Zero; int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m); - interp = new ASTVector(this, i); + interp = new ASTVector(this, i).ToExprArray(); model = new Model(this, m); return (Z3_lbool)r; } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index adf233a98..a7f62e6e8 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -265,12 +265,8 @@ namespace Microsoft.Z3 Contract.Requires(s != null); Contract.Ensures(Contract.Result() != null); - ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject)); - uint n = nUniv.Size; - Expr[] res = new Expr[n]; - for (uint i = 0; i < n; i++) - res[i] = Expr.Create(Context, nUniv[i].NativeObject); - return res; + ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject)); + return av.ToExprArray(); } /// diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 012a283f5..c5227d18f 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -178,8 +178,8 @@ namespace Microsoft.Z3 { get { - ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); - return ass.Size; + ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); + return assertions.Size; } } @@ -192,12 +192,8 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != null); - ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); - uint n = ass.Size; - BoolExpr[] res = new BoolExpr[n]; - for (uint i = 0; i < n; i++) - res[i] = new BoolExpr(Context, ass[i].NativeObject); - return res; + ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); + return (BoolExpr[])assertions.ToExprArray(); } } @@ -270,18 +266,14 @@ namespace Microsoft.Z3 /// The result is empty if Check was not invoked before, /// if its results was not UNSATISFIABLE, or if core production is disabled. /// - public Expr[] UnsatCore + public BoolExpr[] UnsatCore { get { Contract.Ensures(Contract.Result() != null); - ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject)); - uint n = core.Size; - Expr[] res = new Expr[n]; - for (uint i = 0; i < n; i++) - res[i] = Expr.Create(Context, core[i].NativeObject); - return res; + ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject)); + return (BoolExpr[])core.ToExprArray(); } } diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index 398aac77f..afeb868ca 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -92,10 +92,10 @@ class ASTMap extends Z3Object * * @throws Z3Exception **/ - public ASTVector getKeys() + public AST[] getKeys() { - return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(), - getNativeObject())); + ASTVector av = new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(), getNativeObject())); + return av.ToArray(); } /** diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index e08a75e7f..7011eeb50 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -119,12 +119,27 @@ public class ASTVector extends Z3Object getContext().getASTVectorDRQ().add(o); super.decRef(o); } - - BoolExpr[] ToBoolArray() { + + /** + * Translates the AST vector into an AST[] + * */ + public AST[] ToArray() + { int n = size(); - BoolExpr[] res = new BoolExpr[n]; + AST[] res = new AST[n]; for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), get(i).getNativeObject()); + res[i] = AST.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an Expr[] + * */ + public Expr[] ToExprArray() { + int n = size(); + Expr[] res = new Expr[n]; + for (int i = 0; i < n; i++) + res[i] = Expr.create(getContext(), get(i).getNativeObject()); return res; } } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index daa0f4e3f..b59a9700a 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -295,10 +295,8 @@ public class Fixedpoint extends Z3Object **/ public BoolExpr[] getRules() { - - ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( - getContext().nCtx(), getNativeObject())); - return v.ToBoolArray(); + ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject())); + return (BoolExpr[]) v.ToExprArray(); } /** @@ -308,10 +306,8 @@ public class Fixedpoint extends Z3Object **/ public BoolExpr[] getAssertions() { - - ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( - getContext().nCtx(), getNativeObject())); - return v.ToBoolArray(); + ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject())); + return (BoolExpr[]) v.ToExprArray(); } /** @@ -319,12 +315,34 @@ public class Fixedpoint extends Z3Object * * @throws Z3Exception **/ - public Statistics getStatistics() throws Z3Exception + public Statistics getStatistics() { return new Statistics(getContext(), Native.fixedpointGetStatistics( getContext().nCtx(), getNativeObject())); } + /** + * Parse an SMT-LIB2 file with fixedpoint rules. + * Add the rules to the current fixedpoint context. + * Return the set of queries in the file. + **/ + public BoolExpr[] ParseFile(String file) + { + ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file)); + return (BoolExpr[])av.ToExprArray(); + } + + /** + * Parse an SMT-LIB2 string with fixedpoint rules. + * Add the rules to the current fixedpoint context. + * Return the set of queries in the file. + **/ + public BoolExpr[] ParseString(String s) + { + ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s)); + return (BoolExpr[])av.ToExprArray(); + } + Fixedpoint(Context ctx, long obj) throws Z3Exception { diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 50c6a223a..5af2a6af8 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -80,11 +80,7 @@ public class InterpolationContext extends Context checkContextMatch(p); ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); - int n = seq.size(); - Expr[] res = new Expr[n]; - for (int i = 0; i < n; i++) - res[i] = Expr.create(this, seq.get(i).getNativeObject()); - return res; + return seq.ToExprArray(); } public class ComputeInterpolantResult @@ -110,9 +106,8 @@ public class InterpolationContext extends Context Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) { - res.interp = (new ASTVector(this, n_i.value)).ToBoolArray(); - } + if (res.status == Z3_lbool.Z3_L_FALSE) + res.interp = (BoolExpr[]) (new ASTVector(this, n_i.value)).ToExprArray(); if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 22d232006..e9922ac58 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -273,11 +273,7 @@ public class Model extends Z3Object ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse( getContext().nCtx(), getNativeObject(), s.getNativeObject())); - int n = nUniv.size(); - Expr[] res = new Expr[n]; - for (int i = 0; i < n; i++) - res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject()); - return res; + return nUniv.ToExprArray(); } /** diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 7c4c1f4b9..eb8e81aa5 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -176,8 +176,7 @@ public class Solver extends Z3Object **/ public int getNumAssertions() { - ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( - getContext().nCtx(), getNativeObject())); + ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject())); return assrts.size(); } @@ -188,9 +187,8 @@ public class Solver extends Z3Object **/ public BoolExpr[] getAssertions() { - ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( - getContext().nCtx(), getNativeObject())); - return assrts.ToBoolArray(); + ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject())); + return (BoolExpr[]) assrts.ToExprArray(); } /** @@ -278,16 +276,11 @@ public class Solver extends Z3Object * * @throws Z3Exception **/ - public Expr[] getUnsatCore() + public BoolExpr[] getUnsatCore() { - ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore( - getContext().nCtx(), getNativeObject())); - int n = core.size(); - Expr[] res = new Expr[n]; - for (int i = 0; i < n; i++) - res[i] = Expr.create(getContext(), core.get(i).getNativeObject()); - return res; + ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject())); + return (BoolExpr[])core.ToExprArray(); } /** diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d03c5bba9..fa6ce6c81 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -192,8 +192,59 @@ struct end -module AST = -struct +module rec AST : +sig + type ast = z3_native_object + val context_of_ast : ast -> context + val nc_of_ast : ast -> Z3native.z3_context + val ptr_of_ast : ast -> Z3native.ptr + val ast_of_ptr : context -> Z3native.ptr -> ast + module ASTVector : + sig + type ast_vector = z3_native_object + val create : context -> Z3native.ptr -> ast_vector + val mk_ast_vector : context -> ast_vector + val get_size : ast_vector -> int + val get : ast_vector -> int -> ast + val set : ast_vector -> int -> ast -> unit + val resize : ast_vector -> int -> unit + val push : ast_vector -> ast -> unit + val translate : ast_vector -> context -> ast_vector + val to_list : ast_vector -> ast list + val to_expr_list : ast_vector -> Expr.expr list + val to_string : ast_vector -> string + end + module ASTMap : + sig + type ast_map = z3_native_object + val create : context -> Z3native.ptr -> ast_map + val mk_ast_map : context -> ast_map + val contains : ast_map -> ast -> bool + val find : ast_map -> ast -> ast + val insert : ast_map -> ast -> ast -> unit + val erase : ast_map -> ast -> unit + val reset : ast_map -> unit + val get_size : ast_map -> int + val get_keys : ast_map -> Expr.expr list + val to_string : ast_map -> string + end + val hash : ast -> int + val get_id : ast -> int + val get_ast_kind : ast -> Z3enums.ast_kind + val is_expr : ast -> bool + val is_app : ast -> bool + val is_var : ast -> bool + val is_quantifier : ast -> bool + val is_sort : ast -> bool + val is_func_decl : ast -> bool + val to_string : ast -> string + val to_sexpr : ast -> string + val equal : ast -> ast -> bool + val compare : ast -> ast -> int + val translate : ast -> context -> ast + val unwrap_ast : ast -> Z3native.ptr + val wrap_ast : context -> Z3native.z3_ast -> ast +end = struct type ast = z3_native_object let context_of_ast ( x : ast ) = (z3obj_gc x) @@ -216,13 +267,13 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_vector = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.ast_vector_inc_ref ; - dec_ref = Z3native.ast_vector_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.ast_vector_inc_ref ; + dec_ref = Z3native.ast_vector_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res - + let mk_ast_vector ( ctx : context ) = (create ctx (Z3native.mk_ast_vector (context_gno ctx))) let get_size ( x : ast_vector ) = @@ -242,6 +293,16 @@ struct let translate ( x : ast_vector ) ( to_ctx : context ) = create to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) + + let to_list ( x : ast_vector ) = + let xs = (get_size x) in + let f i = (get x i) in + mk_list f xs + + let to_expr_list ( x : ast_vector ) = + let xs = (get_size x) in + let f i = (Expr.expr_of_ptr (z3obj_gc x) (z3obj_gno (get x i))) in + mk_list f xs let to_string ( x : ast_vector ) = Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x) @@ -253,9 +314,9 @@ struct let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_map = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.ast_map_inc_ref ; - dec_ref = Z3native.ast_map_dec_ref } in + m_n_obj = null ; + inc_ref = Z3native.ast_map_inc_ref ; + dec_ref = Z3native.ast_map_dec_ref } in (z3obj_sno res ctx no) ; (z3obj_create res) ; res @@ -291,8 +352,7 @@ struct let get_keys ( x : ast_map ) = let av = ASTVector.create (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) in - let f i = (ASTVector.get av i) in - mk_list f (ASTVector.get_size av) + (ASTVector.to_expr_list av) let to_string ( x : ast_map ) = Z3native.ast_map_to_string (z3obj_gnc x) (z3obj_gno x) @@ -341,31 +401,43 @@ struct let wrap_ast ( ctx : context ) ( ptr : Z3native.ptr ) = ast_of_ptr ctx ptr end -open AST - - -module Sort = -struct +and Sort : +sig + type sort = Sort of AST.ast + val ast_of_sort : Sort.sort -> AST.ast + val sort_of_ptr : context -> Z3native.ptr -> sort + val gc : sort -> context + val gnc : sort -> Z3native.ptr + val gno : sort -> Z3native.ptr + val sort_lton : sort list -> Z3native.ptr array + val sort_option_lton : sort option list -> Z3native.ptr array + val equal : sort -> sort -> bool + val get_id : sort -> int + val get_sort_kind : sort -> Z3enums.sort_kind + val get_name : sort -> Symbol.symbol + val to_string : sort -> string + val mk_uninterpreted : context -> Symbol.symbol -> sort + val mk_uninterpreted_s : context -> string -> sort +end = struct type sort = Sort of AST.ast let sort_of_ptr : context -> Z3native.ptr -> sort = fun ctx no -> - let q = (z3_native_object_of_ast_ptr ctx no) in if ((Z3enums.ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) != Z3enums.SORT_AST) then raise (Z3native.Exception "Invalid coercion") else match (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) no)) with - | ARRAY_SORT - | BOOL_SORT - | BV_SORT - | DATATYPE_SORT - | INT_SORT - | REAL_SORT - | UNINTERPRETED_SORT - | FINITE_DOMAIN_SORT - | RELATION_SORT - | FLOATING_POINT_SORT - | ROUNDING_MODE_SORT -> Sort(q) - | UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered") + | ARRAY_SORT + | BOOL_SORT + | BV_SORT + | DATATYPE_SORT + | INT_SORT + | REAL_SORT + | UNINTERPRETED_SORT + | FINITE_DOMAIN_SORT + | RELATION_SORT + | FLOATING_POINT_SORT + | ROUNDING_MODE_SORT -> Sort(z3_native_object_of_ast_ptr ctx no) + | UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered") let ast_of_sort s = match s with Sort(x) -> x @@ -387,7 +459,7 @@ struct false else (Z3native.is_eq_sort (gnc a) (gno a) (gno b)) - + let get_id ( x : sort ) = Z3native.get_sort_id (gnc x) (gno x) let get_sort_kind ( x : sort ) = (sort_kind_of_int (Z3native.get_sort_kind (gnc x) (gno x))) @@ -407,10 +479,7 @@ struct mk_uninterpreted ctx (Symbol.mk_string ( ctx : context ) s) end -open Sort - - -module rec FuncDecl : +and FuncDecl : sig type func_decl = FuncDecl of AST.ast val ast_of_func_decl : FuncDecl.func_decl -> AST.ast @@ -467,21 +536,21 @@ end = struct let ast_of_func_decl f = match f with FuncDecl(x) -> x - let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort list ) ( range : sort ) = + let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) = let res = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.inc_ref ; dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (sort_lton domain) (Sort.gno range))) ; + (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; (z3obj_create res) ; FuncDecl(res) - let create_pdr ( ctx : context) ( prefix : string ) ( domain : sort list ) ( range : sort ) = + let create_pdr ( ctx : context) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = let res = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.inc_ref ; dec_ref = Z3native.dec_ref } in - (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (sort_lton domain) (Sort.gno range))) ; + (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ; (z3obj_create res) ; FuncDecl(res) @@ -546,22 +615,22 @@ end = struct | _ -> raise (Z3native.Exception "parameter is not a rational string") end - let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort list ) ( range : sort ) = + let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) = create_ndr ctx name domain range - let mk_func_decl_s ( ctx : context ) ( name : string ) ( domain : sort list ) ( range : sort ) = + let mk_func_decl_s ( ctx : context ) ( name : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = mk_func_decl ctx (Symbol.mk_string ctx name) domain range - let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : sort list ) ( range : sort ) = + let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = create_pdr ctx prefix domain range - let mk_const_decl ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) = + let mk_const_decl ( ctx : context ) ( name : Symbol.symbol ) ( range : Sort.sort ) = create_ndr ctx name [] range - let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : sort ) = + let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : Sort.sort ) = create_ndr ctx (Symbol.mk_string ctx name) [] range - let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : sort ) = + let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) = create_pdr ctx prefix [] range @@ -581,11 +650,11 @@ end = struct let get_domain ( x : func_decl ) = let n = (get_domain_size x) in - let f i = sort_of_ptr (gc x) (Z3native.get_domain (gnc x) (gno x) i) in + let f i = Sort.sort_of_ptr (gc x) (Z3native.get_domain (gnc x) (gno x) i) in mk_list f n let get_range ( x : func_decl ) = - sort_of_ptr (gc x) (Z3native.get_range (gnc x) (gno x)) + Sort.sort_of_ptr (gc x) (Z3native.get_range (gnc x) (gno x)) let get_decl_kind ( x : func_decl ) = (decl_kind_of_int (Z3native.get_decl_kind (gnc x) (gno x))) @@ -599,7 +668,7 @@ end = struct | PARAMETER_INT -> Parameter.P_Int (Z3native.get_decl_int_parameter (gnc x) (gno x) i) | PARAMETER_DOUBLE -> Parameter.P_Dbl (Z3native.get_decl_double_parameter (gnc x) (gno x) i) | PARAMETER_SYMBOL-> Parameter.P_Sym (Symbol.create (gc x) (Z3native.get_decl_symbol_parameter (gnc x) (gno x) i)) - | PARAMETER_SORT -> Parameter.P_Srt (sort_of_ptr (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i)) + | PARAMETER_SORT -> Parameter.P_Srt (Sort.sort_of_ptr (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i)) | PARAMETER_AST -> Parameter.P_Ast (AST.ast_of_ptr (gc x) (Z3native.get_decl_ast_parameter (gnc x) (gno x) i)) | PARAMETER_FUNC_DECL -> Parameter.P_Fdl (func_decl_of_ptr (gc x) (Z3native.get_decl_func_decl_parameter (gnc x) (gno x) i)) | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gnc x) (gno x) i) @@ -820,29 +889,29 @@ end = struct let is_well_sorted ( x : expr ) = Z3native.is_well_sorted (gnc x) (gno x) - let get_sort ( x : expr ) = sort_of_ptr (Expr.gc x) (Z3native.get_sort (gnc x) (gno x)) + let get_sort ( x : expr ) = Sort.sort_of_ptr (Expr.gc x) (Z3native.get_sort (gnc x) (gno x)) let is_const ( x : expr ) = (match x with Expr(a) -> (AST.is_app a)) && (get_num_args x) == 0 && (FuncDecl.get_domain_size (get_func_decl x)) == 0 - let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_const (context_gno ctx) (Symbol.gno name) (Sort.gno range)) - let mk_const_s ( ctx : context ) ( name : string ) ( range : sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( range : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) range let mk_const_f ( ctx : context ) ( f : FuncDecl.func_decl ) = Expr.expr_of_func_app ctx f [] - let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : sort ) = + let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fresh_const (context_gno ctx) prefix (Sort.gno range)) let mk_app ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr list ) = expr_of_func_app ctx f args - let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : sort ) = + let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno ty)) - let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) = + let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty)) let equal ( a : expr ) ( b : expr ) = AST.equal (ast_of_expr a) (ast_of_expr b) @@ -856,7 +925,7 @@ open Expr module Boolean = struct let mk_sort ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx))) let mk_const ( ctx : context ) ( name : Symbol.symbol ) = (Expr.mk_const ctx name (mk_sort ctx)) @@ -943,7 +1012,7 @@ struct module Pattern = struct - type pattern = Pattern of ast + type pattern = Pattern of AST.ast let ast_of_pattern e = match e with Pattern(x) -> x @@ -1002,13 +1071,13 @@ struct let get_bound_variable_sorts ( x : quantifier ) = let n = (get_num_bound x) in - let f i = (sort_of_ptr (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in + let f i = (Sort.sort_of_ptr (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in mk_list f n let get_body ( x : quantifier ) = expr_of_ptr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x)) - let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) = + let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) let mk_pattern ( ctx : context ) ( terms : expr list ) = @@ -1017,14 +1086,14 @@ struct else Pattern.Pattern(z3_native_object_of_ast_ptr ctx (Z3native.mk_pattern (context_gno ctx) (List.length terms) (expr_lton terms))) - let mk_forall ( ctx : context ) ( sorts : sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_forall ( ctx : context ) ( sorts : Sort.sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (List.length sorts) != (List.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) true (match weight with | None -> 1 | Some(x) -> x) (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length sorts) (sort_lton sorts) + (List.length sorts) (Sort.sort_lton sorts) (Symbol.symbol_lton names) (Expr.gno body))) else @@ -1034,7 +1103,7 @@ struct (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) (List.length nopatterns) (expr_lton nopatterns) - (List.length sorts) (sort_lton sorts) + (List.length sorts) (Sort.sort_lton sorts) (Symbol.symbol_lton names) (Expr.gno body))) @@ -1055,14 +1124,14 @@ struct (List.length nopatterns) (expr_lton nopatterns) (Expr.gno body))) - let mk_exists ( ctx : context ) ( sorts : sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_exists ( ctx : context ) ( sorts : Sort.sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (List.length sorts) != (List.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) false (match weight with | None -> 1 | Some(x) -> x) (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) - (List.length sorts) (sort_lton sorts) + (List.length sorts) (Sort.sort_lton sorts) (Symbol.symbol_lton names) (Expr.gno body))) else @@ -1072,7 +1141,7 @@ struct (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns))) (List.length nopatterns) (expr_lton nopatterns) - (List.length sorts) (sort_lton sorts) + (List.length sorts) (Sort.sort_lton sorts) (Symbol.symbol_lton names) (Expr.gno body))) @@ -1093,7 +1162,7 @@ struct (List.length nopatterns) (expr_lton nopatterns) (Expr.gno body))) - let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : Sort.sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (universal) then (mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id) else @@ -1111,8 +1180,8 @@ end module Z3Array = struct - let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) = - sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range)) + let mk_sort ( ctx : context ) ( domain : Sort.sort ) ( range : Sort.sort ) = + Sort.sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range)) let is_store ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) let is_select ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT) @@ -1124,13 +1193,13 @@ struct (Z3native.is_app (Expr.gnc x) (Expr.gno x)) && ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == ARRAY_SORT) - let get_domain ( x : sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_domain (Sort.gnc x) (Sort.gno x)) - let get_range ( x : sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_range (Sort.gnc x) (Sort.gno x)) + let get_domain ( x : Sort.sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_domain (Sort.gnc x) (Sort.gno x)) + let get_range ( x : Sort.sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_range (Sort.gnc x) (Sort.gno x)) - let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort ) ( range : sort ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort ) ( range : Sort.sort ) = (Expr.mk_const ctx name (mk_sort ctx domain range)) - let mk_const_s ( ctx : context ) ( name : string ) ( domain : sort ) ( range : sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( domain : Sort.sort ) ( range : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) domain range let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) = @@ -1139,7 +1208,7 @@ struct let mk_store ( ctx : context ) ( a : expr ) ( i : expr ) ( v : expr ) = expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (Expr.gno a) (Expr.gno i) (Expr.gno v)) - let mk_const_array ( ctx : context ) ( domain : sort ) ( v : expr ) = + let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : expr ) = expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v)) let mk_map ( ctx : context ) ( f : func_decl ) ( args : expr list ) = @@ -1153,8 +1222,8 @@ end module Set = struct - let mk_sort ( ctx : context ) ( ty : sort ) = - sort_of_ptr ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty)) + let mk_sort ( ctx : context ) ( ty : Sort.sort ) = + Sort.sort_of_ptr ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty)) let is_union ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) let is_intersect ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) @@ -1163,10 +1232,10 @@ struct let is_subset ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) - let mk_empty ( ctx : context ) ( domain : sort ) = + let mk_empty ( ctx : context ) ( domain : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_empty_set (context_gno ctx) (Sort.gno domain))) - let mk_full ( ctx : context ) ( domain : sort ) = + let mk_full ( ctx : context ) ( domain : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain)) let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) = @@ -1199,7 +1268,7 @@ end module FiniteDomain = struct let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) = - (sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size)) + Sort.sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size) let mk_sort_s ( ctx : context ) ( name : string ) ( size : int ) = mk_sort ctx (Symbol.mk_string ctx name) size @@ -1211,7 +1280,7 @@ struct let is_lt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) - let get_size ( x : sort ) = + let get_size ( x : Sort.sort ) = let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gnc x) (Sort.gno x)) in if r then v else raise (Z3native.Exception "Conversion failed.") @@ -1239,11 +1308,11 @@ struct let is_select ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) let is_clone ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE) - let get_arity ( x : sort ) = Z3native.get_relation_arity (Sort.gnc x) (Sort.gno x) + let get_arity ( x : Sort.sort ) = Z3native.get_relation_arity (Sort.gnc x) (Sort.gno x) - let get_column_sorts ( x : sort ) = + let get_column_sorts ( x : Sort.sort ) = let n = get_arity x in - let f i = (sort_of_ptr (Sort.gc x) (Z3native.get_relation_column (Sort.gnc x) (Sort.gno x) i)) in + let f i = (Sort.sort_of_ptr (Sort.gc x) (Z3native.get_relation_column (Sort.gnc x) (Sort.gno x) i)) in mk_list f n end @@ -1262,7 +1331,7 @@ struct let _field_nums = FieldNumTable.create 0 - let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) = + let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) = let n = (List.length field_names) in if n != (List.length sorts) then raise (Z3native.Exception "Number of field names does not match number of sorts") @@ -1274,7 +1343,7 @@ struct (Symbol.gno recognizer) n (Symbol.symbol_lton field_names) - (sort_option_lton sorts) + (Sort.sort_option_lton sorts) (Array.of_list sort_refs)) in let no : constructor = { m_ctx = ctx ; m_n_obj = null ; @@ -1321,17 +1390,17 @@ struct res end - let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) = + let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) = Constructor.create ctx name recognizer field_names sorts sort_refs - let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) = + let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) = mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor list ) = let f x = (z3obj_gno x) in let (x,_) = (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (List.length constructors) (Array.of_list (List.map f constructors))) in - sort_of_ptr ctx x + Sort.sort_of_ptr ctx x let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : Constructor.constructor list ) = mk_sort ctx (Symbol.mk_string ctx name) constructors @@ -1341,7 +1410,7 @@ struct let f e = (AST.ptr_of_ast (ConstructorList.create ctx e)) in let cla = (Array.of_list (List.map f c)) in let (r, a) = (Z3native.mk_datatypes (context_gno ctx) n (Symbol.symbol_lton names) cla) in - let g i = (sort_of_ptr ctx (Array.get r i)) in + let g i = (Sort.sort_of_ptr ctx (Array.get r i)) in mk_list g (Array.length r) let mk_sorts_s ( ctx : context ) ( names : string list ) ( c : Constructor.constructor list list ) = @@ -1352,19 +1421,19 @@ struct ) c - let get_num_constructors ( x : sort ) = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) + let get_num_constructors ( x : Sort.sort ) = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) - let get_constructors ( x : sort ) = + let get_constructors ( x : Sort.sort ) = let n = (get_num_constructors x) in let f i = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) i) in mk_list f n - let get_recognizers ( x : sort ) = + let get_recognizers ( x : Sort.sort ) = let n = (get_num_constructors x) in let f i = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i) in mk_list f n - let get_accessors ( x : sort ) = + let get_accessors ( x : Sort.sort ) = let n = (get_num_constructors x) in let f i = ( let fd = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) i) in @@ -1380,80 +1449,80 @@ module Enumeration = struct let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( enum_names : Symbol.symbol list ) = let (a, _, _) = (Z3native.mk_enumeration_sort (context_gno ctx) (Symbol.gno name) (List.length enum_names) (Symbol.symbol_lton enum_names)) in - sort_of_ptr ctx a + Sort.sort_of_ptr ctx a let mk_sort_s ( ctx : context ) ( name : string ) ( enum_names : string list ) = mk_sort ctx (Symbol.mk_string ctx name) (Symbol.mk_strings ctx enum_names) - let get_const_decls ( x : sort ) = + let get_const_decls ( x : Sort.sort ) = let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) in let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) i)) in mk_list f n - let get_const_decl ( x : sort ) ( inx : int ) = + let get_const_decl ( x : Sort.sort ) ( inx : int ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) inx) - let get_consts ( x : sort ) = + let get_consts ( x : Sort.sort ) = let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) in let f i = (Expr.mk_const_f (Sort.gc x) (get_const_decl x i)) in mk_list f n - let get_const ( x : sort ) ( inx : int ) = + let get_const ( x : Sort.sort ) ( inx : int ) = Expr.mk_const_f (Sort.gc x) (get_const_decl x inx) - let get_tester_decls ( x : sort ) = + let get_tester_decls ( x : Sort.sort ) = let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) in let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i)) in mk_list f n - let get_tester_decl ( x : sort ) ( inx : int ) = + let get_tester_decl ( x : Sort.sort ) ( inx : int ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) inx) end module Z3List = struct - let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : sort ) = + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : Sort.sort ) = let (r, _, _, _, _, _, _) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in - sort_of_ptr ctx r + Sort.sort_of_ptr ctx r - let mk_list_s ( ctx : context ) (name : string) elem_sort = + let mk_list_s ( ctx : context ) ( name : string ) elem_sort = mk_sort ctx (Symbol.mk_string ctx name) elem_sort - let get_nil_decl ( x : sort ) = + let get_nil_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) 0) - let get_is_nil_decl ( x : sort ) = + let get_is_nil_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) 0) - let get_cons_decl ( x : sort ) = + let get_cons_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) 1) - let get_is_cons_decl ( x : sort ) = + let get_is_cons_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) 1) - let get_head_decl ( x : sort ) = + let get_head_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor_accessor (Sort.gnc x) (Sort.gno x) 1 0) - let get_tail_decl ( x : sort ) = + let get_tail_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor_accessor (Sort.gnc x) (Sort.gno x) 1 1) - let nil ( x : sort ) = expr_of_func_app (Sort.gc x) (get_nil_decl x) [] + let nil ( x : Sort.sort ) = expr_of_func_app (Sort.gc x) (get_nil_decl x) [] end module Tuple = struct - let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( field_sorts : sort list ) = - let (r, _, _) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (List.length field_names) (Symbol.symbol_lton field_names) (sort_lton field_sorts)) in - sort_of_ptr ctx r + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( field_sorts : Sort.sort list ) = + let (r, _, _) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (List.length field_names) (Symbol.symbol_lton field_names) (Sort.sort_lton field_sorts)) in + Sort.sort_of_ptr ctx r - let get_mk_decl ( x : sort ) = + let get_mk_decl ( x : Sort.sort ) = func_decl_of_ptr (Sort.gc x) (Z3native.get_tuple_sort_mk_decl (Sort.gnc x) (Sort.gno x)) - let get_num_fields ( x : sort ) = Z3native.get_tuple_sort_num_fields (Sort.gnc x) (Sort.gno x) + let get_num_fields ( x : Sort.sort ) = Z3native.get_tuple_sort_num_fields (Sort.gnc x) (Sort.gno x) - let get_field_decls ( x : sort ) = + let get_field_decls ( x : Sort.sort ) = let n = get_num_fields x in let f i = func_decl_of_ptr (Sort.gc x) (Z3native.get_tuple_sort_field_decl (Sort.gnc x) (Sort.gno x) i) in mk_list f n @@ -1510,7 +1579,7 @@ struct module Integer = struct let mk_sort ( ctx : context ) = - sort_of_ptr ctx (Z3native.mk_int_sort (context_gno ctx)) + Sort.sort_of_ptr ctx (Z3native.mk_int_sort (context_gno ctx)) let get_int ( x : expr ) = let (r, v) = Z3native.get_numeral_int (Expr.gnc x) (Expr.gno x) in @@ -1553,7 +1622,7 @@ struct module Real = struct let mk_sort ( ctx : context ) = - sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) + Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) let get_numerator ( x : expr ) = expr_of_ptr (Expr.gc x) (Z3native.get_numerator (Expr.gnc x) (Expr.gno x)) @@ -1599,14 +1668,14 @@ struct module AlgebraicNumber = struct let to_upper ( x : expr ) ( precision : int ) = - expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision) - + expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision) + let to_lower ( x : expr ) precision = - expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision) - + expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision) + let to_decimal_string ( x : expr ) ( precision : int ) = - Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision - + Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision + let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) end end @@ -1649,7 +1718,7 @@ end module BitVector = struct let mk_sort ( ctx : context ) size = - sort_of_ptr ctx (Z3native.mk_bv_sort (context_gno ctx) size) + Sort.sort_of_ptr ctx (Z3native.mk_bv_sort (context_gno ctx) size) let is_bv ( x : expr ) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == BV_SORT) let is_bv_numeral ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM) @@ -1703,7 +1772,7 @@ struct let is_bv2int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) let is_bv_carry ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) let is_bv_xor3 ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) - let get_size (x : sort ) = Z3native.get_bv_sort_size (Sort.gnc x) (Sort.gno x) + let get_size (x : Sort.sort ) = Z3native.get_bv_sort_size (Sort.gnc x) (Sort.gno x) let get_int ( x : expr ) = let (r, v) = Z3native.get_numeral_int (Expr.gnc x) (Expr.gno x) in if r then v @@ -1817,7 +1886,7 @@ struct module RoundingMode = struct let mk_sort ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx))) let is_fprm ( x : expr ) = (Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT let mk_round_nearest_ties_to_even ( ctx : context ) = @@ -1843,40 +1912,40 @@ struct end let mk_sort ( ctx : context ) ( ebits : int ) ( sbits : int ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits)) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits)) let mk_sort_half ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx))) let mk_sort_16 ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx))) let mk_sort_single ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx))) let mk_sort_32 ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx))) let mk_sort_double ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx))) let mk_sort_64 ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx))) let mk_sort_quadruple ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx))) let mk_sort_128 ( ctx : context ) = - (sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx))) + (Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx))) - let mk_nan ( ctx : context ) ( s : sort ) = + let mk_nan ( ctx : context ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_nan (context_gno ctx) (Sort.gno s))) - let mk_inf ( ctx : context ) ( s : sort ) ( negative : bool ) = + let mk_inf ( ctx : context ) ( s : Sort.sort ) ( negative : bool ) = (expr_of_ptr ctx (Z3native.mk_fpa_inf (context_gno ctx) (Sort.gno s) negative)) - let mk_zero ( ctx : context ) ( s : sort ) ( negative : bool ) = + let mk_zero ( ctx : context ) ( s : Sort.sort ) ( negative : bool ) = (expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative)) let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) = (expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand))) - let mk_numeral_f ( ctx : context ) ( value : float ) ( s : sort ) = + let mk_numeral_f ( ctx : context ) ( value : float ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s))) - let mk_numeral_i ( ctx : context ) ( value : int ) ( s : sort ) = + let mk_numeral_i ( ctx : context ) ( value : int ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_numeral_int (context_gno ctx) value (Sort.gno s))) - let mk_numeral_i_u ( ctx : context ) ( sign : bool ) ( exponent : int ) ( significand : int ) ( s : sort ) = + let mk_numeral_i_u ( ctx : context ) ( sign : bool ) ( exponent : int ) ( significand : int ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_numeral_int64_uint64 (context_gno ctx) sign exponent significand (Sort.gno s))) - let mk_numeral_s ( ctx : context ) ( v : string ) ( s : sort ) = + let mk_numeral_s ( ctx : context ) ( v : string ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno s))) let is_fp ( x : expr ) = (Sort.get_sort_kind (Expr.get_sort x)) == FLOATING_POINT_SORT @@ -1912,9 +1981,9 @@ struct let is_to_ieee_bv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_IEEE_BV) let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) - let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( s : sort ) = + let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( s : Sort.sort ) = Expr.mk_const ctx name s - let mk_const_s ( ctx : context ) ( name : string ) ( s : sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( s : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) s let mk_abs ( ctx : context ) ( t : expr ) = @@ -1965,15 +2034,15 @@ struct expr_of_ptr ctx (Z3native.mk_fpa_is_negative (context_gno ctx) (Expr.gno t)) let mk_is_positive ( ctx : context ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_fpa_is_positive (context_gno ctx) (Expr.gno t)) - let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : sort ) = + let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_bv (context_gno ctx) (Expr.gno t) (Sort.gno s)) - let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) = + let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_float (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s)) - let mk_to_fp_real ( ctx : context ) ( rm : expr ) ( t : expr ) ( s : sort ) = + let mk_to_fp_real ( ctx : context ) ( rm : expr ) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_real (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s)) - let mk_to_fp_signed ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) = + let mk_to_fp_signed ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_signed (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s)) - let mk_to_fp_unsigned ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) = + let mk_to_fp_unsigned ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_unsigned (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s)) let mk_to_ubv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) = expr_of_ptr ctx (Z3native.mk_fpa_to_ubv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size) @@ -1982,9 +2051,9 @@ struct let mk_to_real ( ctx : context ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t)) - let get_ebits ( ctx : context ) ( s : sort ) = + let get_ebits ( ctx : context ) ( s : Sort.sort ) = (Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s)) - let get_sbits ( ctx : context ) ( s : sort ) = + let get_sbits ( ctx : context ) ( s : Sort.sort ) = (Z3native.fpa_get_sbits (context_gno ctx) (Sort.gno s)) let get_numeral_sign ( ctx : context ) ( t : expr ) = (Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t)) @@ -1997,7 +2066,7 @@ struct let mk_to_ieee_bv ( ctx : context ) ( t : expr ) = (expr_of_ptr ctx (Z3native.mk_fpa_to_ieee_bv (context_gno ctx) (Expr.gno t))) - let mk_to_fp_int_real ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : sort ) = + let mk_to_fp_int_real ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_to_fp_int_real (context_gno ctx) (Expr.gno rm) (Expr.gno exponent) (Expr.gno significand) (Sort.gno s))) let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) @@ -2280,14 +2349,12 @@ struct let get_sorts ( x : model ) = let n = (get_num_sorts x) in - let f i = (sort_of_ptr (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in + let f i = (Sort.sort_of_ptr (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in mk_list f n - let sort_universe ( x : model ) ( s : sort ) = - let n_univ = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in - let n = (AST.ASTVector.get_size n_univ) in - let f i = (AST.ASTVector.get n_univ i) in - mk_list f n + let sort_universe ( x : model ) ( s : Sort.sort ) = + let av = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in + (AST.ASTVector.to_expr_list av) let to_string ( x : model ) = Z3native.model_to_string (z3obj_gnc x) (z3obj_gno x) end @@ -2475,6 +2542,91 @@ struct end +module Statistics = +struct + type statistics = z3_native_object + + let create ( ctx : context ) ( no : Z3native.ptr ) = + let res : statistics = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.stats_inc_ref ; + dec_ref = Z3native.stats_dec_ref } in + (z3obj_sno res ctx no) ; + (z3obj_create res) ; + res + + + module Entry = + struct + type statistics_entry = { + mutable m_key : string; + mutable m_is_int : bool ; + mutable m_is_float : bool ; + mutable m_int : int ; + mutable m_float : float } + + let create_si k v = + let res : statistics_entry = { + m_key = k ; + m_is_int = true ; + m_is_float = false ; + m_int = v ; + m_float = 0.0 + } in + res + + let create_sd k v = + let res : statistics_entry = { + m_key = k ; + m_is_int = false ; + m_is_float = true ; + m_int = 0 ; + m_float = v + } in + res + + + let get_key (x : statistics_entry) = x.m_key + let get_int (x : statistics_entry) = x.m_int + let get_float (x : statistics_entry) = x.m_float + let is_int (x : statistics_entry) = x.m_is_int + let is_float (x : statistics_entry) = x.m_is_float + let to_string_value (x : statistics_entry) = + if (is_int x) then + string_of_int (get_int x) + else if (is_float x) then + string_of_float (get_float x) + else + raise (Z3native.Exception "Unknown statistical entry type") + let to_string ( x : statistics_entry ) = (get_key x) ^ ": " ^ (to_string_value x) + end + + let to_string ( x : statistics ) = Z3native.stats_to_string (z3obj_gnc x) (z3obj_gno x) + + let get_size ( x : statistics ) = Z3native.stats_size (z3obj_gnc x) (z3obj_gno x) + + let get_entries ( x : statistics ) = + let n = (get_size x ) in + let f i = ( + let k = Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i in + if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then + (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) + else + (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) + ) in + mk_list f n + + let get_keys ( x : statistics ) = + let n = (get_size x) in + let f i = (Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i) in + mk_list f n + + let get ( x : statistics ) ( key : string ) = + let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in + List.fold_left f None (get_entries x) +end + + module Solver = struct type solver = z3_native_object @@ -2494,90 +2646,6 @@ struct | SATISFIABLE -> "satisfiable" | _ -> "unknown" - module Statistics = - struct - type statistics = z3_native_object - - let create ( ctx : context ) ( no : Z3native.ptr ) = - let res : statistics = { m_ctx = ctx ; - m_n_obj = null ; - inc_ref = Z3native.stats_inc_ref ; - dec_ref = Z3native.stats_dec_ref } in - (z3obj_sno res ctx no) ; - (z3obj_create res) ; - res - - - module Entry = - struct - type statistics_entry = { - mutable m_key : string; - mutable m_is_int : bool ; - mutable m_is_float : bool ; - mutable m_int : int ; - mutable m_float : float } - - let create_si k v = - let res : statistics_entry = { - m_key = k ; - m_is_int = true ; - m_is_float = false ; - m_int = v ; - m_float = 0.0 - } in - res - - let create_sd k v = - let res : statistics_entry = { - m_key = k ; - m_is_int = false ; - m_is_float = true ; - m_int = 0 ; - m_float = v - } in - res - - - let get_key (x : statistics_entry) = x.m_key - let get_int (x : statistics_entry) = x.m_int - let get_float (x : statistics_entry) = x.m_float - let is_int (x : statistics_entry) = x.m_is_int - let is_float (x : statistics_entry) = x.m_is_float - let to_string_value (x : statistics_entry) = - if (is_int x) then - string_of_int (get_int x) - else if (is_float x) then - string_of_float (get_float x) - else - raise (Z3native.Exception "Unknown statistical entry type") - let to_string ( x : statistics_entry ) = (get_key x) ^ ": " ^ (to_string_value x) - end - - let to_string ( x : statistics ) = Z3native.stats_to_string (z3obj_gnc x) (z3obj_gno x) - - let get_size ( x : statistics ) = Z3native.stats_size (z3obj_gnc x) (z3obj_gno x) - - let get_entries ( x : statistics ) = - let n = (get_size x ) in - let f i = ( - let k = Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i in - if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then - (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) - else - (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) - ) in - mk_list f n - - let get_keys ( x : statistics ) = - let n = (get_size x) in - let f i = (Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i) in - mk_list f n - - let get ( x : statistics ) ( key : string ) = - let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in - List.fold_left f None (get_entries x) - end - let get_help ( x : solver ) = Z3native.solver_get_help (z3obj_gnc x) (z3obj_gno x) let set_parameters ( x : solver ) ( p : Params.params )= @@ -2613,10 +2681,8 @@ struct (AST.ASTVector.get_size a) let get_assertions ( x : solver ) = - let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in - let n = (AST.ASTVector.get_size a) in - let f i = (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in - mk_list f n + let av = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in + (AST.ASTVector.to_expr_list av) let check ( x : solver ) ( assumptions : expr list ) = let r = @@ -2646,10 +2712,8 @@ struct Some (expr_of_ptr (z3obj_gc x) q) let get_unsat_core ( x : solver ) = - let cn = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in - let n = (AST.ASTVector.get_size cn) in - let f i = (AST.ASTVector.get cn i) in - mk_list f n + let av = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in + (AST.ASTVector.to_expr_list av) let get_reason_unknown ( x : solver ) = Z3native.solver_get_reason_unknown (z3obj_gnc x) (z3obj_gno x) @@ -2720,7 +2784,7 @@ struct | _ -> Solver.UNKNOWN let query_r ( x : fixedpoint ) ( relations : func_decl list ) = - let f x = ptr_of_ast (ast_of_func_decl x) in + let f x = AST.ptr_of_ast (ast_of_func_decl x) in match (lbool_of_int (Z3native.fixedpoint_query_relations (z3obj_gnc x) (z3obj_gno x) (List.length relations) (Array.of_list (List.map f relations)))) with | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE @@ -2768,18 +2832,26 @@ struct Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (List.length queries) (Array.of_list (List.map f queries)) let get_rules ( x : fixedpoint ) = - let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in - let n = (AST.ASTVector.get_size v) in - let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in - mk_list f n + let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in + (AST.ASTVector.to_expr_list av) let get_assertions ( x : fixedpoint ) = - let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in - let n = (AST.ASTVector.get_size v) in - let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in - mk_list f n + let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in + (AST.ASTVector.to_expr_list av) let mk_fixedpoint ( ctx : context ) = create ctx + + let get_statistics ( x : fixedpoint ) = + let s = Z3native.fixedpoint_get_statistics (z3obj_gnc x) (z3obj_gno x) in + (Statistics.create (z3obj_gc x) s) + + let parse_string ( x : fixedpoint ) ( s : string ) = + let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_from_string (z3obj_gnc x) (z3obj_gno x) s)) in + (AST.ASTVector.to_expr_list av) + + let parse_file ( x : fixedpoint ) ( filename : string ) = + let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_from_file (z3obj_gnc x) (z3obj_gno x) filename)) in + (AST.ASTVector.to_expr_list av) end @@ -2790,7 +2862,7 @@ struct (List.length assumptions) (let f x = Expr.gno (x) in (Array.of_list (List.map f assumptions))) (Expr.gno formula) - let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = + let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in @@ -2799,14 +2871,14 @@ struct raise (Z3native.Exception "Argument size mismatch") else Z3native.parse_smtlib_string (context_gno ctx) str - cs - (Symbol.symbol_lton sort_names) - (sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) - let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = + let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in @@ -2815,13 +2887,13 @@ struct raise (Z3native.Exception "Argument size mismatch") else Z3native.parse_smtlib_file (context_gno ctx) file_name - cs - (Symbol.symbol_lton sort_names) - (sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) - + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))) + let get_num_smtlib_formulas ( ctx : context ) = Z3native.get_smtlib_num_formulas (context_gno ctx) let get_smtlib_formulas ( ctx : context ) = @@ -2847,10 +2919,10 @@ struct let get_smtlib_sorts ( ctx : context ) = let n = (get_num_smtlib_sorts ctx) in - let f i = (sort_of_ptr ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in + let f i = (Sort.sort_of_ptr ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in mk_list f n - let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = + let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in @@ -2859,14 +2931,14 @@ struct raise (Z3native.Exception "Argument size mismatch") else (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) str - cs - (Symbol.symbol_lton sort_names) - (sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) - - let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) + + let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) = let csn = (List.length sort_names) in let cs = (List.length sorts) in let cdn = (List.length decl_names) in @@ -2875,12 +2947,12 @@ struct raise (Z3native.Exception "Argument size mismatch") else (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) file_name - cs - (Symbol.symbol_lton sort_names) - (sort_lton sorts) - cd - (Symbol.symbol_lton decl_names) - (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) + cs + (Symbol.symbol_lton sort_names) + (Sort.sort_lton sorts) + cd + (Symbol.symbol_lton decl_names) + (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls))))) end module Interpolation = @@ -2902,14 +2974,17 @@ struct res let get_interpolant ( ctx : context ) ( pf : expr ) ( pat: expr ) ( p : Params.params ) = - (ASTVector.create ctx (Z3native.get_interpolant (context_gno ctx) (Expr.gno pf) (Expr.gno pat) (z3obj_gno p))) + let av = (AST.ASTVector.create ctx (Z3native.get_interpolant (context_gno ctx) (Expr.gno pf) (Expr.gno pat) (z3obj_gno p))) in + AST.ASTVector.to_expr_list av let compute_interpolant ( ctx : context ) ( pat : expr ) ( p : Params.params ) = let (r, interp, model) = (Z3native.compute_interpolant (context_gno ctx) (Expr.gno pat) (z3obj_gno p)) in - match (lbool_of_int r) with - | L_TRUE -> ((ASTVector.create ctx interp), (Model.create ctx model)) - | _ -> raise (Z3native.Exception "Error computing interpolant.") - + let res = (lbool_of_int r) in + match res with + | L_TRUE -> (res, None, Some(Model.create ctx model)) + | L_FALSE -> (res, Some((AST.ASTVector.to_expr_list (AST.ASTVector.create ctx interp))), None) + | _ -> (res, None, None) + let get_interpolation_profile ( ctx : context ) = (Z3native.interpolation_profile (context_gno ctx)) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 3c3b65f56..2099359fa 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -123,7 +123,7 @@ sig end (** The abstract syntax tree (AST) module *) -module AST : +module rec AST : sig type ast @@ -156,6 +156,12 @@ sig @return A new ASTVector *) val translate : ast_vector -> context -> ast_vector + (** Translates the ASTVector into an (Ast.ast list) *) + val to_list : ast_vector -> ast list + + (** Translates the ASTVector into an (Expr.expr list) *) + val to_expr_list : ast_vector -> Expr.expr list + (** Retrieves a string representation of the vector. *) val to_string : ast_vector -> string end @@ -189,7 +195,7 @@ sig val get_size : ast_map -> int (** The keys stored in the map. *) - val get_keys : ast_map -> ast list + val get_keys : ast_map -> Expr.expr list (** Retrieves a string representation of the map.*) val to_string : ast_map -> string @@ -260,7 +266,7 @@ sig end (** The Sort module implements type information for ASTs *) -module Sort : +and Sort : sig type sort = Sort of AST.ast @@ -291,7 +297,7 @@ sig end (** Function declarations *) -module rec FuncDecl : +and FuncDecl : sig type func_decl = FuncDecl of AST.ast @@ -2751,7 +2757,7 @@ sig (** The finite set of distinct values that represent the interpretation of a sort. {!get_sorts} @return A list of expressions, where each is an element of the universe of the sort *) - val sort_universe : model -> Sort.sort -> AST.ast list + val sort_universe : model -> Sort.sort -> Expr.expr list (** Conversion of models to strings. @return A string representation of the model. *) @@ -2938,6 +2944,55 @@ sig val interrupt : context -> unit end +(** Objects that track statistical information. *) +module Statistics : +sig + type statistics + + (** Statistical data is organized into pairs of \[Key, Entry\], where every + Entry is either a floating point or integer value. *) + module Entry : + sig + type statistics_entry + + (** The key of the entry. *) + val get_key : statistics_entry -> string + + (** The int-value of the entry. *) + val get_int : statistics_entry -> int + + (** The float-value of the entry. *) + val get_float : statistics_entry -> float + + (** True if the entry is uint-valued. *) + val is_int : statistics_entry -> bool + + (** True if the entry is float-valued. *) + val is_float : statistics_entry -> bool + + (** The string representation of the the entry's value. *) + val to_string_value : statistics_entry -> string + + (** The string representation of the entry (key and value) *) + val to_string : statistics_entry -> string + end + + (** A string representation of the statistical data. *) + val to_string : statistics -> string + + (** The number of statistical data. *) + val get_size : statistics -> int + + (** The data entries. *) + val get_entries : statistics -> Entry.statistics_entry list + + (** The statistical counters. *) + val get_keys : statistics -> string list + + (** The value of a particular statistical counter. *) + val get : statistics -> string -> Entry.statistics_entry option +end + (** Solvers *) module Solver : sig @@ -2946,56 +3001,6 @@ sig val string_of_status : status -> string - (** Objects that track statistical information about solvers. *) - module Statistics : - sig - type statistics - - (** Statistical data is organized into pairs of \[Key, Entry\], where every - Entry is either a floating point or integer value. - *) - module Entry : - sig - type statistics_entry - - (** The key of the entry. *) - val get_key : statistics_entry -> string - - (** The int-value of the entry. *) - val get_int : statistics_entry -> int - - (** The float-value of the entry. *) - val get_float : statistics_entry -> float - - (** True if the entry is uint-valued. *) - val is_int : statistics_entry -> bool - - (** True if the entry is float-valued. *) - val is_float : statistics_entry -> bool - - (** The string representation of the the entry's value. *) - val to_string_value : statistics_entry -> string - - (** The string representation of the entry (key and value) *) - val to_string : statistics_entry -> string - end - - (** A string representation of the statistical data. *) - val to_string : statistics -> string - - (** The number of statistical data. *) - val get_size : statistics -> int - - (** The data entries. *) - val get_entries : statistics -> Entry.statistics_entry list - - (** The statistical counters. *) - val get_keys : statistics -> string list - - (** The value of a particular statistical counter. *) - val get : statistics -> string -> Entry.statistics_entry option - end - (** A string that describes all available solver parameters. *) val get_help : solver -> string @@ -3081,7 +3086,7 @@ sig The unsat core is a subset of [Assertions] The result is empty if [Check] was not invoked before, if its results was not [UNSATISFIABLE], or if core production is disabled. *) - val get_unsat_core : solver -> AST.ast list + val get_unsat_core : solver -> Expr.expr list (** A brief justification of why the last call to [Check] returned [UNKNOWN]. *) val get_reason_unknown : solver -> string @@ -3198,6 +3203,19 @@ sig (** Create a Fixedpoint context. *) val mk_fixedpoint : context -> fixedpoint + + (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *) + val get_statistics : fixedpoint -> Statistics.statistics + + (** Parse an SMT-LIB2 string with fixedpoint rules. + Add the rules to the current fixedpoint context. + Return the set of queries in the string. *) + val parse_string : fixedpoint -> string -> Expr.expr list + + (** Parse an SMT-LIB2 file with fixedpoint rules. + Add the rules to the current fixedpoint context. + Return the set of queries in the file. *) + val parse_file : fixedpoint -> string -> Expr.expr list end (** Functions for handling SMT and SMT2 expressions and files *) @@ -3272,12 +3290,12 @@ sig (** Gets an interpolant. For more information on interpolation please refer too the C/C++ API, which is well documented. *) - val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> AST.ASTVector.ast_vector + val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> Expr.expr list (** Computes an interpolant. For more information on interpolation please refer too the C/C++ API, which is well documented. *) - val compute_interpolant : context -> Expr.expr -> Params.params -> (AST.ASTVector.ast_vector * Model.model) + val compute_interpolant : context -> Expr.expr -> Params.params -> (Z3enums.lbool * Expr.expr list option * Model.model option) (** Retrieves an interpolation profile. For more information on interpolation please refer From 4da7286a7b09b6c94fca5be167b72c31cbd9a1cd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 17:30:19 +0100 Subject: [PATCH 13/17] Fixed various signed/unsigned conversion warnings. --- src/math/simplex/sparse_matrix.h | 2 +- src/math/simplex/sparse_matrix_def.h | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index c02375e7e..8c0357691 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -79,7 +79,7 @@ namespace simplex { }; col_entry(int r, int i): m_row_id(r), m_row_idx(i) {} col_entry(): m_row_id(0), m_row_idx(0) {} - bool is_dead() const { return m_row_id == dead_id; } + bool is_dead() const { return (unsigned) m_row_id == dead_id; } }; struct column; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index 9fa3ceda7..64dcd8d84 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -79,7 +79,7 @@ namespace simplex { void sparse_matrix::_row::del_row_entry(unsigned idx) { _row_entry & t = m_entries[idx]; SASSERT(!t.is_dead()); - t.m_next_free_row_entry_idx = m_first_free_idx; + t.m_next_free_row_entry_idx = (unsigned)m_first_free_idx; t.m_var = dead_id; m_size--; m_first_free_idx = idx; @@ -513,8 +513,8 @@ namespace simplex { SASSERT(!m.is_zero(e.m_coeff)); SASSERT(e.m_var != dead_id); col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx]; - SASSERT(c.m_row_id == row_id); - SASSERT(c.m_row_idx == i); + SASSERT((unsigned)c.m_row_id == row_id); + SASSERT((unsigned)c.m_row_idx == i); vars.insert(e.m_var); } int idx = r.m_first_free_idx; @@ -544,7 +544,7 @@ namespace simplex { _row const& row = m_rows[c.m_row_id]; _row_entry const& r = row.m_entries[c.m_row_idx]; SASSERT(r.m_var == v); - SASSERT(r.m_col_idx == i); + SASSERT((unsigned)r.m_col_idx == i); rows.insert(c.m_row_id); } int idx = col.m_first_free_idx; From 9912b2cd67def9fab10a81dcd9e5bc6490b69d1a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 May 2015 18:01:00 +0100 Subject: [PATCH 14/17] Re-enabled the smt.arith.greatest_error_pivot parameter. --- src/smt/params/smt_params_helper.pyg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 240d45f15..8be6110d5 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -44,7 +44,8 @@ def_module_params(module_name='smt', ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), - ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'), + ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'), + ('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'), From 91352369a979d90abb7143c327329cc3c8d433cc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 26 May 2015 11:20:19 +0100 Subject: [PATCH 15/17] Added conversion functions to ASTVectors in .NET and Java. Fixes #108 --- src/api/dotnet/ASTVector.cs | 110 ++++++++++++++++++++++++- src/api/dotnet/Fixedpoint.cs | 8 +- src/api/dotnet/InterpolationContext.cs | 10 +-- src/api/dotnet/Solver.cs | 4 +- src/api/java/ASTVector.java | 110 ++++++++++++++++++++++++- src/api/java/Fixedpoint.java | 8 +- src/api/java/InterpolationContext.java | 8 +- src/api/java/Solver.java | 4 +- 8 files changed, 239 insertions(+), 23 deletions(-) diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index f858c7862..8b599ca48 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -112,7 +112,7 @@ namespace Microsoft.Z3 } /// - /// Translates an AST vector into an Expr[] + /// Translates an ASTVector into an Expr[] /// public Expr[] ToExprArray() { @@ -123,6 +123,114 @@ namespace Microsoft.Z3 return res; } + /// + /// Translates an ASTVector into a BoolExpr[] + /// + public BoolExpr[] ToBoolExprArray() + { + uint n = Size; + BoolExpr[] res = new BoolExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a BitVecExpr[] + /// + public BitVecExpr[] ToBitVecExprArray() + { + uint n = Size; + BitVecExpr[] res = new BitVecExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a ArithExpr[] + /// + public ArithExpr[] ToArithExprArray() + { + uint n = Size; + ArithExpr[] res = new ArithExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a ArrayExpr[] + /// + public ArrayExpr[] ToArrayExprArray() + { + uint n = Size; + ArrayExpr[] res = new ArrayExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a DatatypeExpr[] + /// + public DatatypeExpr[] ToDatatypeExprArray() + { + uint n = Size; + DatatypeExpr[] res = new DatatypeExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a FPExpr[] + /// + public FPExpr[] ToFPExprArray() + { + uint n = Size; + FPExpr[] res = new FPExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a FPRMExpr[] + /// + public FPRMExpr[] ToFPRMExprArray() + { + uint n = Size; + FPRMExpr[] res = new FPRMExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a IntExpr[] + /// + public IntExpr[] ToIntExprArray() + { + uint n = Size; + IntExpr[] res = new IntExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + + /// + /// Translates an ASTVector into a RealExpr[] + /// + public RealExpr[] ToRealExprArray() + { + uint n = Size; + RealExpr[] res = new RealExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject); + return res; + } + #region Internal internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 54dbcd3c1..66449ddbb 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -279,7 +279,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)); - return (BoolExpr[])av.ToExprArray(); + return av.ToBoolExprArray(); } } @@ -293,7 +293,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)); - return (BoolExpr[])av.ToExprArray(); + return av.ToBoolExprArray(); } } @@ -318,7 +318,7 @@ namespace Microsoft.Z3 public BoolExpr[] ParseFile(string file) { ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)); - return (BoolExpr[])av.ToExprArray(); + return av.ToBoolExprArray(); } /// @@ -327,7 +327,7 @@ namespace Microsoft.Z3 public BoolExpr[] ParseString(string s) { ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)); - return (BoolExpr[])av.ToExprArray(); + return av.ToBoolExprArray(); } diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 9fbdf456e..e6e258b9a 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -47,7 +47,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_get_interpolant in the C/C++ API, which is /// well documented. - public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) + public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p) { Contract.Requires(pf != null); Contract.Requires(pat != null); @@ -59,7 +59,7 @@ namespace Microsoft.Z3 CheckContextMatch(p); ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject)); - return seq.ToExprArray(); + return seq.ToBoolExprArray(); } /// @@ -68,7 +68,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_compute_interpolant in the C/C++ API, which is /// well documented. - public Z3_lbool ComputeInterpolant(Expr pat, Params p, out Expr[] interp, out Model model) + public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model) { Contract.Requires(pat != null); Contract.Requires(p != null); @@ -80,7 +80,7 @@ namespace Microsoft.Z3 IntPtr i = IntPtr.Zero, m = IntPtr.Zero; int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m); - interp = new ASTVector(this, i).ToExprArray(); + interp = new ASTVector(this, i).ToBoolExprArray(); model = new Model(this, m); return (Z3_lbool)r; } @@ -102,7 +102,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_check_interpolant in the C/C++ API, which is /// well documented. - public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory) + public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory) { Contract.Requires(cnsts.Length == parents.Length); Contract.Requires(cnsts.Length == interps.Length + 1); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index c5227d18f..80ca7a0cd 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -193,7 +193,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); - return (BoolExpr[])assertions.ToExprArray(); + return assertions.ToBoolExprArray(); } } @@ -273,7 +273,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject)); - return (BoolExpr[])core.ToExprArray(); + return core.ToBoolExprArray(); } } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 7011eeb50..5b57db9d9 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -142,4 +142,112 @@ public class ASTVector extends Z3Object res[i] = Expr.create(getContext(), get(i).getNativeObject()); return res; } -} + + /** + * Translates the AST vector into an BoolExpr[] + * */ + public BoolExpr[] ToBoolExprArray() + { + int n = size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an BitVecExpr[] + * */ + public BitVecExpr[] ToBitVecExprArray() + { + int n = size(); + BitVecExpr[] res = new BitVecExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an ArithExpr[] + * */ + public ArithExpr[] ToArithExprExprArray() + { + int n = size(); + ArithExpr[] res = new ArithExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an ArrayExpr[] + * */ + public ArrayExpr[] ToArrayExprArray() + { + int n = size(); + ArrayExpr[] res = new ArrayExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an DatatypeExpr[] + * */ + public DatatypeExpr[] ToDatatypeExprArray() + { + int n = size(); + DatatypeExpr[] res = new DatatypeExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an FPExpr[] + * */ + public FPExpr[] ToFPExprArray() + { + int n = size(); + FPExpr[] res = new FPExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an FPRMExpr[] + * */ + public FPRMExpr[] ToFPRMExprArray() + { + int n = size(); + FPRMExpr[] res = new FPRMExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an IntExpr[] + * */ + public IntExpr[] ToIntExprArray() + { + int n = size(); + IntExpr[] res = new IntExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } + + /** + * Translates the AST vector into an RealExpr[] + * */ + public RealExpr[] ToRealExprArray() + { + int n = size(); + RealExpr[] res = new RealExpr[n]; + for (int i = 0; i < n; i++) + res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject()); + return res; + } +} \ No newline at end of file diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index b59a9700a..e1fccdf4f 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -296,7 +296,7 @@ public class Fixedpoint extends Z3Object public BoolExpr[] getRules() { ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject())); - return (BoolExpr[]) v.ToExprArray(); + return v.ToBoolExprArray(); } /** @@ -307,7 +307,7 @@ public class Fixedpoint extends Z3Object public BoolExpr[] getAssertions() { ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject())); - return (BoolExpr[]) v.ToExprArray(); + return v.ToBoolExprArray(); } /** @@ -329,7 +329,7 @@ public class Fixedpoint extends Z3Object public BoolExpr[] ParseFile(String file) { ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file)); - return (BoolExpr[])av.ToExprArray(); + return av.ToBoolExprArray(); } /** @@ -340,7 +340,7 @@ public class Fixedpoint extends Z3Object public BoolExpr[] ParseString(String s) { ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s)); - return (BoolExpr[])av.ToExprArray(); + return av.ToBoolExprArray(); } diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 5af2a6af8..ddce9ee33 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -73,14 +73,14 @@ public class InterpolationContext extends Context * well documented. * @throws Z3Exception **/ - public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) + public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p) { checkContextMatch(pf); checkContextMatch(pat); checkContextMatch(p); ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject())); - return seq.ToExprArray(); + return seq.ToBoolExprArray(); } public class ComputeInterpolantResult @@ -107,7 +107,7 @@ public class InterpolationContext extends Context Native.LongPtr n_m = new Native.LongPtr(); res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); if (res.status == Z3_lbool.Z3_L_FALSE) - res.interp = (BoolExpr[]) (new ASTVector(this, n_i.value)).ToExprArray(); + res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray(); if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } @@ -135,7 +135,7 @@ public class InterpolationContext extends Context /// Remarks: For more information on interpolation please refer /// too the function Z3_check_interpolant in the C/C++ API, which is /// well documented. - public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) + public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory) { CheckInterpolantResult res = new CheckInterpolantResult(); Native.StringPtr n_err_str = new Native.StringPtr(); diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index eb8e81aa5..4d2d9b641 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -188,7 +188,7 @@ public class Solver extends Z3Object public BoolExpr[] getAssertions() { ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject())); - return (BoolExpr[]) assrts.ToExprArray(); + return assrts.ToBoolExprArray(); } /** @@ -280,7 +280,7 @@ public class Solver extends Z3Object { ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject())); - return (BoolExpr[])core.ToExprArray(); + return core.ToBoolExprArray(); } /** From 98975e518715b60722df294487df6e105935ef9f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 27 May 2015 14:47:24 +0100 Subject: [PATCH 16/17] Reordered the default qflia probe to be checked before the more permissive qfauflia. --- src/tactic/portfolio/default_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index ad811cc70..72c486c24 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -35,9 +35,9 @@ Notes: tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), - cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), - cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), + cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), + cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), From b10f79a941c0114e37d8daa9a30b1b84d1cf5e08 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 27 May 2015 17:07:18 +0100 Subject: [PATCH 17/17] dl_compiler: minor simplifications Signed-off-by: Nuno Lopes --- src/muz/rel/dl_compiler.cpp | 14 ++++++++------ src/muz/rel/dl_compiler.h | 8 ++++---- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 9e8ead241..59ba260a4 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -85,7 +85,7 @@ namespace datalog { removed_cols.size(), removed_cols.c_ptr(), result)); } - void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, + void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col, reg_idx & result, bool reuse, instruction_block & acc) { relation_signature res_sig; relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig); @@ -139,7 +139,7 @@ namespace datalog { return r; } - compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) { + compiler::reg_idx compiler::get_single_column_register(const relation_sort s) { relation_signature singl_sig; singl_sig.push_back(s); return get_fresh_register(singl_sig); @@ -165,7 +165,7 @@ namespace datalog { } } - void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val, + void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val, reg_idx & result, bool & dealloc, instruction_block & acc) { reg_idx singleton_table; if(!m_constant_registers.find(s, val, singleton_table)) { @@ -185,7 +185,7 @@ namespace datalog { } } - void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, + void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result, bool & dealloc, instruction_block & acc) { TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); @@ -862,9 +862,11 @@ namespace datalog { ast_manager& m = m_context.get_manager(); unsigned pt_len = r->get_positive_tail_size(); unsigned ut_len = r->get_uninterpreted_tail_size(); - if (pt_len == ut_len) { + + // no negated predicates + if (pt_len == ut_len) return; - } + // populate negative variables: for (unsigned i = pt_len; i < ut_len; ++i) { app * neg_tail = r->get_tail(i); diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 8c33f987c..4902b9387 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -135,7 +135,7 @@ namespace datalog { reg_idx get_fresh_register(const relation_signature & sig); reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r); - reg_idx get_single_column_register(const relation_sort & s); + reg_idx get_single_column_register(const relation_sort s); /** \brief Allocate registers for predicates in \c pred and add them into the \c regs map. @@ -150,7 +150,7 @@ namespace datalog { const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc); void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc); - void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, + void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col, reg_idx & result, bool reuse, instruction_block & acc); /** \brief Create add an union or widen operation and put it into \c acc. @@ -174,10 +174,10 @@ namespace datalog { void make_dealloc_non_void(reg_idx r, instruction_block & acc); - void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val, + void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val, reg_idx & result, bool & dealloc, instruction_block & acc); - void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, + void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result, bool & dealloc, instruction_block & acc); void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, instruction_block & acc);