mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-10-07 12:42:13 -07:00
commit 37f7c30e23
7 changed files with 124 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -363,7 +363,7 @@ def mk_dotnet(dotnet):
dotnet.write(' {\n\n')
dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n')
dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
dotnet.write(' public unsafe class LIB\n')
dotnet.write(' public class LIB\n')
dotnet.write(' {\n')
dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n'
' \n')

59
src/api/dotnet/core/DummyContracts.cs Normal file
View file

@ -0,0 +1,59 @@
/*++
Copyright (<c>) 2016 Microsoft Corporation
Module Name:
Contracts.cs
Abstract:
Z3 Managed API: Dummy Code Contracts class for .NET
frameworks that don't support them (e.g., CoreCLR).
Author:
Christoph Wintersteiger (cwinter) 2016-10-06
Notes:
--*/
namespace System.Diagnostics.Contracts
{
public class ContractClass : Attribute
{
public ContractClass(Type t) { }
}
public class ContractClassFor : Attribute
{
public ContractClassFor(Type t) { }
}
public class ContractInvariantMethod : Attribute
{
public ContractInvariantMethod() { }
}
public class ContractVerification : Attribute
{
public ContractVerification(bool b) { }
}
public class Pure : Attribute { }
public static class Contract
{
public static void Ensures(bool b) { }
public static void Requires(bool b) { }
public static void Assume(bool b, string msg) { }
public static void Assert(bool b) { }
public static bool ForAll(bool b) { return true; }
public static bool ForAll(Object c, Func<Object, bool> p) { return true; }
public static bool ForAll(int from, int to, Predicate<int> p) { return true; }
public static void Invariant(bool b) { }
public static T[] Result<T>() { return new T[1]; }
public static void EndContractBlock() { }
public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
}
}

21
src/api/dotnet/core/project.json Normal file
View file

@ -0,0 +1,21 @@
{
"version": "1.0.0-*",
"buildOptions": {
"debugType": "portable",
"emitEntryPoint": false,
"outputName": "Microsoft.Z3",
"compile": [ "../*.cs", "*.cs" ]
},
"dependencies": { },
"frameworks": {
"netcoreapp1.0": {
"dependencies": {
"Microsoft.NETCore.App": {
"type": "platform",
"version": "1.0.1"
}
},
"imports": "dnxcore50"
}
}
}

4
src/api/python/z3/z3num.py
View file

@ -10,6 +10,8 @@ from .z3core import *
from .z3printer import *
from fractions import Fraction
from .z3 import _get_ctx
def _to_numeral(num, ctx=None):
if isinstance(num, Numeral):
return num
@ -86,7 +88,7 @@ class Numeral:
def __init__(self, num, ctx=None):
if isinstance(num, Ast):
self.ast = num
self.ctx = z3._get_ctx(ctx)
self.ctx = _get_ctx(ctx)
elif isinstance(num, RatNumRef) or isinstance(num, AlgebraicNumRef):
self.ast = num.ast
self.ctx = num.ctx

6
src/api/z3_api.h
View file

@ -1997,9 +1997,9 @@ extern "C" {
\param c logical context.
\param constr constructor container. The container must have been passed in to a #Z3_mk_datatype call.
\param num_fields number of accessor fields in the constructor.
\param constructor constructor function declaration.
\param tester constructor test function declaration.
\param accessors array of accessor function declarations.
\param constructor constructor function declaration, allocated by user.
\param tester constructor test function declaration, allocated by user.
\param accessors array of accessor function declarations allocated by user. The array must contain num_fields elements.
def_API('Z3_query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL)))
*/

55
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -90,19 +90,28 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
}
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
SASSERT(m_util.is_fp(t) && m_util.is_fp(f));
if (m_util.is_fp(t) && m_util.is_fp(f)) {
expr *t_sgn, *t_sig, *t_exp;
expr *f_sgn, *f_sig, *f_exp;
split_fp(t, t_sgn, t_exp, t_sig);
split_fp(f, f_sgn, f_exp, f_sig);
expr *t_sgn, *t_sig, *t_exp;
expr *f_sgn, *f_sig, *f_exp;
split_fp(t, t_sgn, t_exp, t_sig);
split_fp(f, f_sgn, f_exp, f_sig);
expr_ref sgn(m), s(m), e(m);
m_simp.mk_ite(c, t_sgn, f_sgn, sgn);
m_simp.mk_ite(c, t_sig, f_sig, s);
m_simp.mk_ite(c, t_exp, f_exp, e);
expr_ref sgn(m), s(m), e(m);
m_simp.mk_ite(c, t_sgn, f_sgn, sgn);
m_simp.mk_ite(c, t_sig, f_sig, s);
m_simp.mk_ite(c, t_exp, f_exp, e);
result = m_util.mk_fp(sgn, e, s);
result = m_util.mk_fp(sgn, e, s);
}
else if (m_util.is_rm(t) && m_util.is_rm(f))
{
SASSERT(m_util.is_bv2rm(t) && m_util.is_bv2rm(f));
TRACE("fpa2bv", tout << "ite rm: t=" << mk_ismt2_pp(t, m) << " f=" << mk_ismt2_pp(f, m) << std::endl; );
m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), result);
result = m_util.mk_bv2rm(result);
}
else
UNREACHABLE();
}
void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -264,7 +273,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
rng = f->get_range();
fapp = m.mk_app(f, num, args);
if (m_util.is_float(rng)) {
sort_ref bv_rng(m);
sort_ref bv_rng(m);
expr_ref new_eq(m);
unsigned ebits = m_util.get_ebits(rng);
unsigned sbits = m_util.get_sbits(rng);
@ -290,7 +299,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a
m_extra_assertions.push_back(new_eq);
result = flt_app;
}
else
else
result = fapp;
TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
@ -1057,7 +1066,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
// (x is 0) -> x
c5 = x_is_zero;
v5 = pzero;
// exp(x) < exp(y) -> x
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
@ -1117,15 +1126,15 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
dbg_decouple("fpa2bv_rem_exp_diff", exp_diff);
// CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal,
// but calculating this via rem = x - y * nearest(x/y) creates huge
// but calculating this via rem = x - y * nearest(x/y) creates huge
// circuits, too. Lazy instantiation seems the way to go in the long run
// (using the lazy bit-blaster helps on simple instances).
// (using the lazy bit-blaster helps on simple instances).
expr_ref a_sig_ext(m), b_sig_ext(m), lshift(m), rshift(m), shifted(m), huge_rem(m);
a_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(max_exp_diff_ui, a_sig), m_bv_util.mk_numeral(0, 3));
b_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(max_exp_diff_ui, b_sig), m_bv_util.mk_numeral(0, 3));
lshift = m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - (ebits+2) + 3, exp_diff);
rshift = m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - (ebits+2) + 3, neg_exp_diff);
shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift),
shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift),
m_bv_util.mk_bv_shl(a_sig_ext, lshift));
huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext);
dbg_decouple("fpa2bv_rem_huge_rem", huge_rem);
@ -1142,7 +1151,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
expr_ref r_ge_y_half(m), r_gt_ny_half(m), r_le_y_half(m), r_lt_ny_half(m);
expr_ref r_ge_zero(m), r_le_zero(m);
expr_ref rounded_sub_y(m), rounded_add_y(m);
mpf zero, two;
mpf zero, two;
m_mpf_manager.set(two, ebits, sbits, 2);
m_mpf_manager.set(zero, ebits, sbits, 0);
mk_numeral(s, two, two_e);
@ -1151,7 +1160,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
mk_neg(s, y_half, ny_half);
mk_is_zero(y_half, y_half_is_zero);
y_half_is_nz = m.mk_not(y_half_is_zero);
mk_float_ge(s, rndd, y_half, r_ge_y_half);
mk_float_gt(s, rndd, ny_half, r_gt_ny_half);
mk_float_le(s, rndd, y_half, r_le_y_half);
@ -1161,8 +1170,8 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
mk_add(s, rne_bv, rndd, y, rounded_add_y);
expr_ref sub_cnd(m), add_cnd(m);
sub_cnd = m.mk_and(y_half_is_nz,
m.mk_or(m.mk_and(y_is_pos, r_ge_y_half),
sub_cnd = m.mk_and(y_half_is_nz,
m.mk_or(m.mk_and(y_is_pos, r_ge_y_half),
m.mk_and(y_is_neg, r_le_y_half)));
add_cnd = m.mk_and(y_half_is_nz,
m.mk_or(m.mk_and(y_is_pos, r_lt_ny_half),
@ -1170,7 +1179,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
mk_ite(add_cnd, rounded_add_y, rndd, v7);
mk_ite(sub_cnd, rounded_sub_y, v7, v7);
// And finally, we tie them together.
mk_ite(c6, v6, v7, result);
mk_ite(c5, v5, result, result);
@ -3698,7 +3707,7 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
// CMW: This works only for quantifier-free formulas.
if (m_util.is_fp(e)) {
expr_ref new_bv(m);
expr *e_sgn, *e_sig, *e_exp;
expr *e_sgn, *e_sig, *e_exp;
split_fp(e, e_sgn, e_exp, e_sig);
unsigned ebits = m_bv_util.get_bv_size(e_exp);
unsigned sbits = m_bv_util.get_bv_size(e_sig) + 1;

10
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -86,10 +86,10 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
return BR_DONE;
}
return BR_FAILED;
}
}
else if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
if (m_conv.is_float(args[1]) || m_conv.is_rm(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}
@ -103,7 +103,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
@ -157,7 +157,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BV2RM:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
@ -169,7 +169,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
NOT_IMPLEMENTED_YET();
}
}
else
else
{
SASSERT(!m_conv.is_float_family(f));
if (m_conv.fu().contains_floats(f)) {