mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-11-17 04:26:36 +02:00
parent e9db934f1a 9053e6eba6
commit 123b50ed3c
20 changed files with 962 additions and 323 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
scripts/mk_win_dist.py
View file

@ -236,23 +236,9 @@ def mk_zip():
VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'),
re.compile('msvcp.*\.dll'),
re.compile('msvcr.*\.dll')]
VS_RUNTIME_FILES = []
def cp_vs_runtime_visitor(pattern, dir, files):
global VS_RUNTIME_FILES
for filename in files:
for pat in VS_RUNTIME_PATS:
if pat.match(filename):
if fnmatch(filename, pattern):
fname = os.path.join(dir, filename)
if not os.path.isdir(fname):
VS_RUNTIME_FILES.append(fname)
break
# Copy Visual Studio Runtime libraries
def cp_vs_runtime_core(x64):
global VS_RUNTIME_FILES
def cp_vs_runtime_core(x64):
if x64:
platform = "x64"
@ -261,7 +247,15 @@ def cp_vs_runtime_core(x64):
vcdir = os.environ['VCINSTALLDIR']
path = '%sredist\\%s' % (vcdir, platform)
VS_RUNTIME_FILES = []
os.walk(path, cp_vs_runtime_visitor, '*.dll')
for root, dirs, files in os.walk(path):
for filename in files:
if fnmatch(filename, '*.dll'):
for pat in VS_RUNTIME_PATS:
if pat.match(filename):
fname = os.path.join(root, filename)
if not os.path.isdir(fname):
VS_RUNTIME_FILES.append(fname)
bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin')
for f in VS_RUNTIME_FILES:
shutil.copy(f, bin_dist_path)

264
src/api/api_fpa.cpp
View file

@ -909,14 +909,16 @@ extern "C" {
Z3_TRY;
LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
if (sgn == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
family_id fid = mk_c(c)->get_fpa_fid();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
@ -933,6 +935,71 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_sign_bv(c, t);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
family_id fid = mk_c(c)->get_fpa_fid();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
api::context * ctx = mk_c(c);
expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(to_expr(t), val);
if (!r || mpfm.is_nan(val)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
app * a;
if (mpfm.is_pos(val))
a = ctx->bvutil().mk_numeral(0, 1);
else
a = ctx->bvutil().mk_numeral(1, 1);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_significand_bv(c, t);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
family_id fid = mk_c(c)->get_fpa_fid();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
SASSERT(plugin != 0);
expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
unsigned sbits = val.get().get_sbits();
scoped_mpq q(mpqm);
mpqm.set(q, mpfm.sig(val));
if (mpfm.is_inf(val)) mpqm.set(q, 0);
app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits-1);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_significand_string(c, t);
@ -952,8 +1019,8 @@ extern "C" {
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG)
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
}
unsigned sbits = val.get().get_sbits();
@ -972,6 +1039,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
if (n == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
@ -992,7 +1061,7 @@ extern "C" {
bool r = plugin->is_numeral(e, val);
const mpz & z = mpfm.sig(val);
if (!r ||
!(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val)) ||
!(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val)) ||
!mpzm.is_uint64(z)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
*n = 0;
@ -1003,10 +1072,12 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t) {
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
LOG_Z3_fpa_get_numeral_exponent_string(c, t, biased);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
family_id fid = mk_c(c)->get_fpa_fid();
@ -1019,23 +1090,35 @@ extern "C" {
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) {
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
}
mpf_exp_t exp = mpfm.is_zero(val) ? 0 :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
mpfm.exp(val);
unsigned ebits = val.get().get_ebits();
mpf_exp_t exp;
if (biased) {
exp = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val));
}
else {
exp = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.exp(val);
}
std::stringstream ss;
ss << exp;
return mk_c(c)->mk_external_string(ss.str());
Z3_CATCH_RETURN("");
}
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n) {
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n, biased);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
if (n == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
@ -1053,22 +1136,73 @@ extern "C" {
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) {
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
*n = 0;
return 0;
}
*n = mpfm.is_zero(val) ? 0 :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
mpfm.exp(val);
unsigned ebits = val.get().get_ebits();
if (biased) {
*n = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val));
}
else {
*n = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.exp(val);
}
return 1;
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_bv(c, t, biased);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
family_id fid = mk_c(c)->get_fpa_fid();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
unsigned ebits = val.get().get_ebits();
mpf_exp_t exp;
if (biased) {
exp = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val));
}
else {
exp = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.exp(val);
}
app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_to_ieee_bv(c, t);
RESET_ERROR_CODE();
CHECK_NON_NULL(t, 0);
CHECK_VALID_AST(t, 0);
if (!is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
@ -1098,4 +1232,102 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_nan(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_nan(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_inf(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_inf(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_zero(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_zero(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_normal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_normal(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_subnormal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_subnormal(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_positive(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_positive(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_negative(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_negative(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
};

100
src/api/dotnet/FPNum.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
@ -27,6 +27,20 @@ namespace Microsoft.Z3
[ContractVerification(true)]
public class FPNum : FPExpr
{
/// <summary>
/// The sign of a floating-point numeral as a bit-vector expression
/// </summary>
/// <remarks>
/// NaN's do not have a bit-vector sign, so they are invalid arguments.
/// </remarks>
public BitVecExpr SignBV
{
get
{
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject));
}
}
/// <summary>
/// Retrieves the sign of a floating-point literal
/// </summary>
@ -38,7 +52,7 @@ namespace Microsoft.Z3
get
{
int res = 0;
if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Sign is not a Boolean value");
return res != 0;
}
@ -63,7 +77,7 @@ namespace Microsoft.Z3
/// The significand value of a floating-point numeral as a UInt64
/// </summary>
/// <remarks>
/// This function extracts the significand bits, without the
/// This function extracts the significand bits, without the
/// hidden bit or normalization. Throws an exception if the
/// significand does not fit into a UInt64.
/// </remarks>
@ -73,36 +87,90 @@ namespace Microsoft.Z3
{
UInt64 result = 0;
if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
return result;
}
}
/// <summary>
/// Return the exponent value of a floating-point numeral as a string
/// The significand of a floating-point numeral as a bit-vector expression
/// </summary>
public string Exponent
/// <remarks>
/// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments.
/// </remarks>
public BitVecExpr SignificandBV
{
get
{
return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject));
}
}
/// <summary>
/// Return the (biased) exponent value of a floating-point numeral as a string
/// </summary>
public string Exponent(bool biased = true)
{
return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0);
}
/// <summary>
/// Return the exponent value of a floating-point numeral as a signed 64-bit integer
/// </summary>
public Int64 ExponentInt64
public Int64 ExponentInt64(bool biased = true)
{
get
{
Int64 result = 0;
if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0)
throw new Z3Exception("Exponent is not a 64 bit integer");
return result;
}
Int64 result = 0;
if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0)
throw new Z3Exception("Exponent is not a 64 bit integer");
return result;
}
/// <summary>
/// The exponent of a floating-point numeral as a bit-vector expression
/// </summary>
/// <remarks>
/// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments.
/// </remarks>
public BitVecExpr ExponentBV(bool biased = true)
{
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0));
}
/// <summary>
/// Indicates whether the numeral is a NaN.
/// </summary>
public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is a +oo or -oo.
/// </summary>
public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is +zero or -zero.
/// </summary>
public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is normal.
/// </summary>
public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is subnormal.
/// </summary>
public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is positive.
/// </summary>
public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is negative.
/// </summary>
public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
#region Internal
internal FPNum(Context ctx, IntPtr obj)
: base(ctx, obj)
@ -113,7 +181,7 @@ namespace Microsoft.Z3
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);

114
src/api/java/FPNum.java
View file

@ -20,7 +20,7 @@ package com.microsoft.z3;
* FloatingPoint Numerals
*/
public class FPNum extends FPExpr
{
{
/**
* Retrieves the sign of a floating-point literal
* Remarks: returns true if the numeral is negative
@ -33,6 +33,15 @@ public class FPNum extends FPExpr
return res.value != 0;
}
/**
* The sign of a floating-point numeral as a bit-vector expression
* Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments.
* @throws Z3Exception
*/
public BitVecExpr getSignBV() {
return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
}
/**
* The significand value of a floating-point numeral as a string
* Remarks: The significand s is always 0 &lt; s &lt; 2.0; the resulting string is long
@ -57,25 +66,117 @@ public class FPNum extends FPExpr
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
return res.value;
}
/**
* The significand of a floating-point numeral as a bit-vector expression
* Remarks: NaN is an invalid argument.
* @throws Z3Exception
*/
public BitVecExpr getSignificandBV() {
return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
}
/**
* Return the exponent value of a floating-point numeral as a string
* Remarks: NaN is an invalid argument.
* @throws Z3Exception
*/
public String getExponent() {
return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
public String getExponent(boolean biased) {
return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
}
/**
* Return the exponent value of a floating-point numeral as a signed 64-bit integer
* Remarks: NaN is an invalid argument.
* @throws Z3Exception
*/
public long getExponentInt64() {
public long getExponentInt64(boolean biased) {
Native.LongPtr res = new Native.LongPtr();
if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res))
if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased))
throw new Z3Exception("Exponent is not a 64 bit integer");
return res.value;
}
/**
* The exponent of a floating-point numeral as a bit-vector expression
* Remarks: NaN is an invalid argument.
* @throws Z3Exception
*/
public BitVecExpr getExponentBV(boolean biased) {
return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
}
/**
* Indicates whether the numeral is a NaN.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isNaN()
{
return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the numeral is a +oo or -oo.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isInf()
{
return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the numeral is +zero or -zero.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isZero()
{
return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the numeral is normal.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isNormal()
{
return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the numeral is subnormal.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isSubnormal()
{
return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the numeral is positive.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isPositive()
{
return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the numeral is negative.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isNegative()
{
return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
}
public FPNum(Context ctx, long obj)
{
@ -88,6 +189,5 @@ public class FPNum extends FPExpr
public String toString()
{
return Native.getNumeralString(getContext().nCtx(), getNativeObject());
}
}
}

14
src/api/ml/z3.ml
View file

@ -1325,10 +1325,20 @@ struct
let get_ebits = Z3native.fpa_get_ebits
let get_sbits = Z3native.fpa_get_sbits
let get_numeral_sign = Z3native.fpa_get_numeral_sign
let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string
let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64
let get_numeral_sign_bv = Z3native.fpa_get_numeral_sign_bv
let get_numeral_exponent_string = Z3native.fpa_get_numeral_exponent_string
let get_numeral_exponent_int = Z3native.fpa_get_numeral_exponent_int64
let get_numeral_exponent_bv = Z3native.fpa_get_numeral_exponent_bv
let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string
let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64
let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv
let is_numeral_nan = Z3native.fpa_is_numeral_nan
let is_numeral_inf = Z3native.fpa_is_numeral_inf
let is_numeral_zero = Z3native.fpa_is_numeral_zero
let is_numeral_normal = Z3native.fpa_is_numeral_normal
let is_numeral_subnormal = Z3native.fpa_is_numeral_subnormal
let is_numeral_positive = Z3native.fpa_is_numeral_positive
let is_numeral_negative = Z3native.fpa_is_numeral_negative
let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv
let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real
let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x

78
src/api/ml/z3.mli
View file

@ -2141,21 +2141,54 @@ sig
(** Retrieves the sign of a floating-point literal. *)
val get_numeral_sign : context -> Expr.expr -> bool * int
(** Return the sign of a floating-point numeral as a bit-vector expression.
Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. *)
val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr
(** Return the exponent value of a floating-point numeral as a string *)
val get_numeral_exponent_string : context -> Expr.expr -> bool -> string
(** Return the exponent value of a floating-point numeral as a signed integer *)
val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int
(** Return the exponent of a floating-point numeral as a bit-vector expression.
Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *)
val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr
(** Return the significand value of a floating-point numeral as a bit-vector expression.
Remark: NaN's do not have a bit-vector significand, so they are invalid arguments. *)
val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr
(** Return the significand value of a floating-point numeral as a string. *)
val get_numeral_significand_string : context -> Expr.expr -> string
(** Return the significand value of a floating-point numeral as a uint64.
Remark: This function extracts the significand bits, without the
hidden bit or normalization. Throws an exception if the
significand does not fit into a uint64. *)
significand does not fit into an int. *)
val get_numeral_significand_uint : context -> Expr.expr -> bool * int
(** Return the exponent value of a floating-point numeral as a string *)
val get_numeral_exponent_string : context -> Expr.expr -> string
(** Indicates whether a floating-point numeral is a NaN. *)
val is_numeral_nan : context -> Expr.expr -> bool
(** Return the exponent value of a floating-point numeral as a signed integer *)
val get_numeral_exponent_int : context -> Expr.expr -> bool * int
(** Indicates whether a floating-point numeral is +oo or -oo. *)
val is_numeral_inf : context -> Expr.expr -> bool
(** Indicates whether a floating-point numeral is +zero or -zero. *)
val is_numeral_zero : context -> Expr.expr -> bool
(** Indicates whether a floating-point numeral is normal. *)
val is_numeral_normal : context -> Expr.expr -> bool
(** Indicates whether a floating-point numeral is subnormal. *)
val is_numeral_subnormal : context -> Expr.expr -> bool
(** Indicates whether a floating-point numeral is positive. *)
val is_numeral_positive : context -> Expr.expr -> bool
(** Indicates whether a floating-point numeral is negative. *)
val is_numeral_negative : context -> Expr.expr -> bool
(** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *)
val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr
@ -3023,29 +3056,22 @@ sig
(** Assert a constraint (or multiple) into the solver. *)
val add : solver -> Expr.expr list -> unit
(** * Assert multiple constraints (cs) into the solver, and track them (in the
* unsat) core
* using the Boolean constants in ps.
*
* This API is an alternative to {!check} with assumptions for
* extracting unsat cores.
* Both APIs can be used in the same solver. The unsat core will contain a
* combination
* of the Boolean variables provided using {!assert_and_track}
* and the Boolean literals
* provided using {!check} with assumptions. *)
(** Assert multiple constraints (cs) into the solver, and track them (in the
unsat) core using the Boolean constants in ps.
This API is an alternative to {!check} with assumptions for extracting unsat cores.
Both APIs can be used in the same solver. The unsat core will contain a combination
of the Boolean variables provided using {!assert_and_track} and the Boolean literals
provided using {!check} with assumptions. *)
val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit
(** * Assert a constraint (c) into the solver, and track it (in the unsat) core
* using the Boolean constant p.
*
* This API is an alternative to {!check} with assumptions for
* extracting unsat cores.
* Both APIs can be used in the same solver. The unsat core will contain a
* combination
* of the Boolean variables provided using {!assert_and_track}
* and the Boolean literals
* provided using {!check} with assumptions. *)
(** Assert a constraint (c) into the solver, and track it (in the unsat) core
using the Boolean constant p.
This API is an alternative to {!check} with assumptions for extracting unsat cores.
Both APIs can be used in the same solver. The unsat core will contain a combination
of the Boolean variables provided using {!assert_and_track} and the Boolean literals
provided using {!check} with assumptions. *)
val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit
(** The number of assertions in the solver. *)

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

@ -8452,27 +8452,13 @@ def is_fprm_value(a):
### FP Numerals
class FPNumRef(FPRef):
def isNaN(self):
return self.decl().kind() == Z3_OP_FPA_NAN
class FPNumRef(FPRef):
"""The sign of the numeral.
def isInf(self):
return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF
def isZero(self):
return self.decl().kind() == Z3_OP_FPA_PLUS_ZERO or self.decl().kind() == Z3_OP_FPA_MINUS_ZERO
def isNegative(self):
k = self.decl().kind()
return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True)
"""
The sign of the numeral.
>>> x = FPNumRef(+1.0, FPSort(8, 24))
>>> x = FPVal(+1.0, FPSort(8, 24))
>>> x.sign()
False
>>> x = FPNumRef(-1.0, FPSort(8, 24))
>>> x = FPVal(-1.0, FPSort(8, 24))
>>> x.sign()
True
"""
@ -8482,48 +8468,103 @@ class FPNumRef(FPRef):
raise Z3Exception("error retrieving the sign of a numeral.")
return l.value != 0
"""The sign of a floating-point numeral as a bit-vector expression.
Remark: NaN's are invalid arguments.
"""
The significand of the numeral.
def sign_as_bv(self):
return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
>>> x = FPNumRef(2.5, FPSort(8, 24))
"""The significand of the numeral.
>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.significand()
1.25
"""
def significand(self):
return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
"""
The exponent of the numeral.
"""The significand of the numeral as a long.
>>> x = FPNumRef(2.5, FPSort(8, 24))
>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.significand_as_long()
1.25
"""
def significand_as_long(self):
return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast())
"""The significand of the numeral as a bit-vector expression.
Remark: NaN are invalid arguments.
"""
def significand_as_bv(self):
return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
"""The exponent of the numeral.
>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.exponent()
1
"""
def exponent(self):
return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast())
def exponent(self, biased=True):
return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
"""
The exponent of the numeral as a long.
"""The exponent of the numeral as a long.
>>> x = FPNumRef(2.5, FPSort(8, 24))
>>> x = FPVal(2.5, FPSort(8, 24))
>>> x.exponent_as_long()
1
"""
def exponent_as_long(self):
def exponent_as_long(self, biased=True):
ptr = (ctypes.c_longlong * 1)()
if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr):
if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
raise Z3Exception("error retrieving the exponent of a numeral.")
return ptr[0]
"""The exponent of the numeral as a bit-vector expression.
Remark: NaNs are invalid arguments.
"""
def exponent_as_bv(self, biased=True):
return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
"""Indicates whether the numeral is a NaN."""
def isNaN(self):
return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is +oo or -oo."""
def isInf(self):
return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is +zero or -zero."""
def isZero(self):
return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is normal."""
def isNormal(self):
return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is subnormal."""
def isSubnormal(self):
return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is postitive."""
def isPositive(self):
return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is negative."""
def isNegative(self):
return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
"""
The string representation of the numeral.
>>> x = FPNumRef(20, FPSort(8, 24))
>>> x = FPVal(20, FPSort(8, 24))
>>> x.as_string()
1.25*(2**4)
"""
def as_string(self):
s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
return ("FPVal(%s, %s)" % (s, self.sort()))
def is_fp(a):
@ -8676,7 +8717,7 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
>>> v = FPVal(20.0, FPSort(8, 24))
>>> v
1.25*(2**4)
>>> print("0x%.8x" % v.exponent_as_long())
>>> print("0x%.8x" % v.exponent_as_long(False))
0x00000004
>>> v = FPVal(2.25, FPSort(8, 24))
>>> v

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

@ -620,8 +620,8 @@ class Formatter:
r = []
sgn = c_int(0)
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast)
r.append(to_format('FPVal('))
if sgnb and sgn.value != 0:
r.append(to_format('-'))
@ -650,8 +650,8 @@ class Formatter:
r = []
sgn = (ctypes.c_int)(0)
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast)
if sgnb and sgn.value != 0:
r.append(to_format('-'))
r.append(to_format(sig))

128
src/api/z3_fpa.h
View file

@ -253,9 +253,9 @@ extern "C" {
This is the operator named `fp' in the SMT FP theory definition.
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
are required to be greater than 1 and 2 respectively. The FloatingPoint sort
are required to be longer than 1 and 2 respectively. The FloatingPoint sort
of the resulting expression is automatically determined from the bit-vector sizes
of the arguments.
of the arguments. The exponent is assumed to be in IEEE-754 biased representation.
\param c logical context
\param sgn sign
@ -822,6 +822,100 @@ extern "C" {
*/
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
/**
\brief Checks whether a given floating-point numeral is a NaN.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is a +oo or -oo.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is +zero or -zero.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is normal.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is subnormal.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is positive.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is negative.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
/**
\brief Retrieves the sign of a floating-point literal as a bit-vector expression.
\param c logical context
\param t a floating-point numeral
Remarks: NaN is an invalid argument.
def_API('Z3_fpa_get_numeral_sign_bv', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t);
/**
\brief Retrieves the significand of a floating-point literal as a bit-vector expression.
\param c logical context
\param t a floating-point numeral
Remarks: NaN is an invalid argument.
def_API('Z3_fpa_get_numeral_significand_bv', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t);
/**
\brief Retrieves the sign of a floating-point literal.
@ -858,23 +952,25 @@ extern "C" {
Remarks: This function extracts the significand bits in `t`, without the
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
significand does not fit into a uint64.
significand does not fit into a uint64. NaN is an invalid argument.
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
*/
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n);
/**
\brief Return the exponent value of a floating-point numeral as a string
\brief Return the exponent value of a floating-point numeral as a string.
\param c logical context
\param t a floating-point numeral
\param biased flag to indicate whether the result is in biased representation
Remarks: This function extracts the exponent in `t`, without normalization.
NaN is an invalid argument.
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST), _in(BOOL)))
*/
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t);
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased);
/**
\brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
@ -882,12 +978,28 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
\param n exponent
\param biased flag to indicate whether the result is in biased representation
Remarks: This function extracts the exponent in `t`, without normalization.
NaN is an invalid argument.
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL)))
*/
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n);
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased);
/**
\brief Retrieves the exponent of a floating-point literal as a bit-vector expression.
\param c logical context
\param t a floating-point numeral
\param biased flag to indicate whether the result is in biased representation
Remarks: This function extracts the exponent in `t`, without normalization.
NaN is an invalid arguments.
def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST), _in(BOOL)))
*/
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased);
/**
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

5
src/ast/fpa_decl_plugin.h
View file

@ -288,11 +288,16 @@ public:
app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); }
bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); }
bool is_inf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_inf(v); }
bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); }
bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); }
bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); }
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
bool is_normal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_normal(v); }
bool is_subnormal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_denormal(v); }
bool is_positive(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pos(v); }
bool is_negative(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_neg(v); }
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);

6
src/sat/sat_clause.h
View file

@ -102,10 +102,14 @@ namespace sat {
unsigned m_val1;
unsigned m_val2;
public:
bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
bin_clause(literal l1, literal l2, bool learned) :m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
literal get_literal1() const { return to_literal(m_val1); }
literal get_literal2() const { return to_literal(m_val2 >> 1); }
bool is_learned() const { return (m_val2 & 1) == 1; }
bool operator==(const bin_clause & other) const {
return (m_val1 == other.m_val1 && m_val2 == other.m_val2) ||
(m_val1 == other.m_val2 && m_val2 == other.m_val1);
}
};
class tmp_clause {

23
src/sat/sat_probing.cpp
View file

@ -95,7 +95,7 @@ namespace sat {
if (updt_cache)
cache_bins(l, old_tr_sz);
s.pop(1);
literal_vector::iterator it = m_to_assert.begin();
literal_vector::iterator end = m_to_assert.end();
for (; it != end; ++it) {
@ -178,10 +178,10 @@ namespace sat {
m_num_assigned(p.m_num_assigned) {
m_watch.start();
}
~report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-probing :probing-assigned "
<< (m_probing.m_num_assigned - m_num_assigned)
<< " :cost " << m_probing.m_counter;
@ -189,7 +189,7 @@ namespace sat {
verbose_stream() << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
};
bool probing::operator()(bool force) {
if (!m_probing)
return true;
@ -200,8 +200,8 @@ namespace sat {
CASSERT("probing", s.check_invariant());
if (!force && m_counter > 0)
return true;
if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit)
m_cached_bins.finalize();
report rpt(*this);
@ -239,7 +239,7 @@ namespace sat {
m_counter *= 2;
}
CASSERT("probing", s.check_invariant());
free_memory();
finalize();
return r;
}
@ -255,15 +255,16 @@ namespace sat {
// TODO
}
void probing::free_memory() {
m_assigned.cleanup();
void probing::finalize() {
m_assigned.finalize();
m_to_assert.finalize();
m_cached_bins.finalize();
}
void probing::collect_statistics(statistics & st) const {
st.update("probing assigned", m_num_assigned);
}
void probing::reset_statistics() {
m_num_assigned = 0;
}

2
src/sat/sat_probing.h
View file

@ -69,7 +69,7 @@ namespace sat {
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void free_memory();
void finalize();
void collect_statistics(statistics & st) const;
void reset_statistics();

37
src/sat/sat_simplifier.cpp
View file

@ -63,6 +63,7 @@ namespace sat {
}
simplifier::~simplifier() {
finalize();
}
inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
@ -96,7 +97,7 @@ namespace sat {
inline void simplifier::remove_clause_core(clause & c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++)
insert_todo(c[i].var());
insert_elim_todo(c[i].var());
m_sub_todo.erase(c);
c.set_removed(true);
TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@ -116,6 +117,7 @@ namespace sat {
inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
s.get_wlist(~l1).erase(watched(l2, learned));
m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
}
void simplifier::init_visited() {
@ -123,21 +125,38 @@ namespace sat {
m_visited.resize(2*s.num_vars(), false);
}
void simplifier::free_memory() {
void simplifier::finalize() {
m_use_list.finalize();
m_sub_todo.finalize();
m_sub_bin_todo.finalize();
m_elim_todo.finalize();
m_visited.finalize();
m_bs_cs.finalize();
m_bs_ls.finalize();
}
void simplifier::initialize() {
m_need_cleanup = false;
s.m_cleaner(true);
m_last_sub_trail_sz = s.m_trail.size();
m_use_list.init(s.num_vars());
m_sub_todo.reset();
m_sub_bin_todo.reset();
m_elim_todo.reset();
init_visited();
TRACE("after_cleanup", s.display(tout););
CASSERT("sat_solver", s.check_invariant());
}
void simplifier::operator()(bool learned) {
if (s.inconsistent())
return;
if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
return;
initialize();
CASSERT("sat_solver", s.check_invariant());
TRACE("before_simplifier", s.display(tout););
@ -157,10 +176,10 @@ namespace sat {
}
register_clauses(s.m_clauses);
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
elim_blocked_clauses();
if (!learned)
m_num_calls++;
@ -199,7 +218,7 @@ namespace sat {
}
CASSERT("sat_solver", s.check_invariant());
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
free_memory();
finalize();
}
/**
@ -619,7 +638,7 @@ namespace sat {
TRACE("elim_lit", tout << "processing: " << c << "\n";);
m_need_cleanup = true;
m_num_elim_lits++;
insert_todo(l.var());
insert_elim_todo(l.var());
c.elim(l);
clause_use_list & occurs = m_use_list.get(l);
occurs.erase_not_removed(c);
@ -922,10 +941,10 @@ namespace sat {
void process(literal l) {
TRACE("blocked_clause", tout << "processing: " << l << "\n";);
model_converter::entry * new_entry = 0;
if (s.is_external(l.var()) || s.was_eliminated(l.var()))
if (s.is_external(l.var()) || s.was_eliminated(l.var()))
return;
{
{
m_to_remove.reset();
{
clause_use_list & occs = s.m_use_list.get(l);
@ -1237,12 +1256,14 @@ namespace sat {
for (; it2 != end2; ++it2) {
if (it2->is_binary_clause() && it2->get_literal() == l) {
TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";);
m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned()));
continue;
}
*itprev = *it2;
itprev++;
}
wlist2.set_end(itprev);
m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned()));
}
}
TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);
@ -1345,7 +1366,7 @@ namespace sat {
}
TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
// eliminate variable
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
save_clauses(mc_entry, m_pos_cls);

23
src/sat/sat_simplifier.h
View file

@ -9,7 +9,7 @@ Abstract:
SAT simplification procedures that use a "full" occurrence list:
Subsumption, Blocked Clause Removal, Variable Elimination, ...
Author:
@ -83,7 +83,7 @@ namespace sat {
bool m_subsumption;
unsigned m_subsumption_limit;
bool m_elim_vars;
// stats
unsigned m_num_blocked_clauses;
unsigned m_num_subsumed;
@ -97,6 +97,8 @@ namespace sat {
void checkpoint();
void initialize();
void init_visited();
void mark_visited(literal l) { m_visited[l.index()] = true; }
void unmark_visited(literal l) { m_visited[l.index()] = false; }
@ -135,7 +137,7 @@ namespace sat {
void mark_as_not_learned_core(watch_list & wlist, literal l2);
void mark_as_not_learned(literal l1, literal l2);
void subsume();
void cleanup_watches();
void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
@ -145,7 +147,7 @@ namespace sat {
lbool value(literal l) const;
watch_list & get_wlist(literal l);
watch_list const & get_wlist(literal l) const;
struct blocked_clause_elim;
void elim_blocked_clauses();
@ -172,15 +174,20 @@ namespace sat {
simplifier(solver & s, params_ref const & p);
~simplifier();
void insert_todo(bool_var v) { m_elim_todo.insert(v); }
void reset_todo() { m_elim_todo.reset(); }
void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); }
void reset_todos() {
m_elim_todo.reset();
m_sub_todo.reset();
m_sub_bin_todo.reset();
}
void operator()(bool learned);
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void free_memory();
void finalize();
void collect_statistics(statistics & st) const;
void reset_statistics();

132
src/sat/sat_solver.cpp
View file

@ -141,7 +141,7 @@ namespace sat {
m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
m_assigned_since_gc.push_back(false);
m_case_split_queue.mk_var_eh(v);
m_simplifier.insert_todo(v);
m_simplifier.insert_elim_todo(v);
SASSERT(!was_eliminated(v));
return v;
}
@ -151,7 +151,7 @@ namespace sat {
for (unsigned i = 0; i < num_lits; i++)
SASSERT(m_eliminated[lits[i].var()] == false);
});
if (m_user_scope_literals.empty()) {
mk_clause_core(num_lits, lits, false);
}
@ -175,8 +175,8 @@ namespace sat {
void solver::del_clause(clause& c) {
if (!c.is_learned()) m_stats.m_non_learned_generation++;
m_cls_allocator.del_clause(&c);
m_stats.m_del_clause++;
m_cls_allocator.del_clause(&c);
m_stats.m_del_clause++;
}
clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) {
@ -188,7 +188,7 @@ namespace sat {
return 0; // clause is equivalent to true.
}
++m_stats.m_non_learned_generation;
}
}
switch (num_lits) {
case 0:
@ -739,10 +739,10 @@ namespace sat {
m_restart_threshold = m_config.m_restart_initial;
}
// iff3_finder(*this)();
// iff3_finder(*this)();
simplify_problem();
if (check_inconsistent()) return l_false;
if (m_config.m_max_conflicts == 0) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
@ -763,7 +763,7 @@ namespace sat {
restart();
simplify_problem();
if (check_inconsistent()) return l_false;
if (check_inconsistent()) return l_false;
gc();
}
}
@ -891,7 +891,7 @@ namespace sat {
else {
mk_model();
return l_true;
}
}
}
@ -920,8 +920,8 @@ namespace sat {
return;
}
TRACE("sat",
for (unsigned i = 0; i < num_lits; ++i)
TRACE("sat",
for (unsigned i = 0; i < num_lits; ++i)
tout << lits[i] << " ";
tout << "\n";
if (!m_user_scope_literals.empty()) {
@ -932,7 +932,7 @@ namespace sat {
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
literal nlit = ~m_user_scope_literals[i];
assign(nlit, justification());
assign(nlit, justification());
}
if (weights && !inconsistent()) {
@ -947,9 +947,9 @@ namespace sat {
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
SASSERT(is_external(lit.var()));
add_assumption(lit);
assign(lit, justification());
SASSERT(is_external(lit.var()));
add_assumption(lit);
assign(lit, justification());
}
}
@ -962,10 +962,10 @@ namespace sat {
unsigned num_cores = 0;
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
SASSERT(is_external(lit.var()));
SASSERT(is_external(lit.var()));
TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";);
SASSERT(m_scope_lvl == 1);
add_assumption(lit);
add_assumption(lit);
switch(value(lit)) {
case l_undef:
values.push_back(l_true);
@ -973,10 +973,10 @@ namespace sat {
if (num_cores*2 >= num_lits) {
break;
}
propagate(false);
propagate(false);
if (inconsistent()) {
flet<bool> _init(m_initializing_preferred, true);
while (inconsistent()) {
while (inconsistent()) {
if (!resolve_conflict()) {
return true;
}
@ -1001,15 +1001,15 @@ namespace sat {
for (unsigned k = i; k >= j; --k) {
if (is_assumption(lits[k])) {
pop_assumption();
}
}
}
values.resize(j);
TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";);
i = j - 1;
}
break;
case l_false:
break;
case l_false:
++num_cores;
values.push_back(l_false);
SASSERT(!inconsistent());
@ -1028,14 +1028,14 @@ namespace sat {
SASSERT(m_assumptions.size() <= i+1);
if (m_core.size() <= 3) {
m_inconsistent = true;
TRACE("opt", tout << "found small core: " << m_core << "\n";);
TRACE("opt", tout << "found small core: " << m_core << "\n";);
IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";);
return true;
}
pop_assumption();
m_inconsistent = false;
m_inconsistent = false;
break;
case l_true:
case l_true:
values.push_back(l_true);
SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0);
break;
@ -1046,7 +1046,7 @@ namespace sat {
if (m_weight >= max_weight) {
// block the current correction set candidate.
++m_stats.m_blocked_corr_sets;
TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";);
TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";);
IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";);
pop_to_base_level();
mk_clause_core(m_blocker);
@ -1062,17 +1062,17 @@ namespace sat {
m_min_core.reset();
m_min_core.append(m_core);
m_min_core_valid = true;
}
}
}
void solver::reset_assumptions() {
m_assumptions.reset();
m_assumption_set.reset();
m_assumption_set.reset();
}
void solver::add_assumption(literal lit) {
m_assumption_set.insert(lit);
m_assumptions.push_back(lit);
m_assumption_set.insert(lit);
m_assumptions.push_back(lit);
}
void solver::pop_assumption() {
@ -1089,8 +1089,8 @@ namespace sat {
for (unsigned i = 0; i < m_min_core.size(); ++i) {
literal lit = m_min_core[i];
SASSERT(is_external(lit.var()));
add_assumption(lit);
assign(lit, justification());
add_assumption(lit);
assign(lit, justification());
}
propagate(false);
SASSERT(inconsistent());
@ -1132,7 +1132,7 @@ namespace sat {
m_min_core_valid = false;
m_min_core.reset();
TRACE("sat", display(tout););
if (m_config.m_bcd) {
bceq bc(*this);
bc();
@ -1149,11 +1149,11 @@ namespace sat {
}
IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";);
// Disable simplification during MUS computation.
// Disable simplification during MUS computation.
// if (m_mus.is_active()) return;
TRACE("sat", tout << "simplify\n";);
pop(scope_lvl());
pop(scope_lvl());
SASSERT(scope_lvl() == 0);
@ -1166,7 +1166,7 @@ namespace sat {
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
if (!m_learned.empty()) {
m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation());
@ -1260,7 +1260,7 @@ namespace sat {
TRACE("sat", tout << "failed: " << c << "\n";
tout << "assumptions: " << m_assumptions << "\n";
tout << "trail: " << m_trail << "\n";
tout << "model: " << m << "\n";
tout << "model: " << m << "\n";
m_mc.display(tout);
);
ok = false;
@ -1289,10 +1289,10 @@ namespace sat {
}
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
if (value_at(m_assumptions[i], m) != l_true) {
TRACE("sat",
TRACE("sat",
tout << m_assumptions[i] << " does not model check\n";
tout << "trail: " << m_trail << "\n";
tout << "model: " << m << "\n";
tout << "model: " << m << "\n";
m_mc.display(tout);
);
ok = false;
@ -1664,7 +1664,7 @@ namespace sat {
resolve_conflict_for_unsat_core();
return false;
}
if (m_conflict_lvl == 0) {
return false;
}
@ -1849,11 +1849,11 @@ namespace sat {
bool solver::resolve_conflict_for_init() {
if (m_conflict_lvl == 0) {
return false;
}
}
m_lemma.reset();
m_lemma.push_back(null_literal); // asserted literal
if (m_not_l != null_literal) {
TRACE("sat", tout << "not_l: " << m_not_l << "\n";);
TRACE("sat", tout << "not_l: " << m_not_l << "\n";);
process_antecedent_for_init(m_not_l);
}
literal consequent = m_not_l;
@ -1988,7 +1988,7 @@ namespace sat {
SASSERT(!is_marked(m_trail[i].var()));
}});
unsigned old_size = m_unmark.size();
unsigned old_size = m_unmark.size();
int idx = skip_literals_above_conflict_level();
if (m_not_l != null_literal) {
@ -2005,7 +2005,7 @@ namespace sat {
process_consequent_for_unsat_core(m_not_l, js);
}
}
literal consequent = m_not_l;
justification js = m_conflict;
@ -2031,7 +2031,7 @@ namespace sat {
SASSERT(lvl(consequent) == m_conflict_lvl);
js = m_justification[c_var];
idx--;
}
}
reset_unmark(old_size);
if (m_config.m_core_minimize) {
if (m_min_core_valid && m_min_core.size() < m_core.size()) {
@ -2039,7 +2039,7 @@ namespace sat {
m_core.reset();
m_core.append(m_min_core);
}
// TBD:
// TBD:
// apply optional clause minimization by detecting subsumed literals.
// initial experiment suggests it has no effect.
m_mus(); // ignore return value on cancelation.
@ -2511,7 +2511,7 @@ namespace sat {
void solver::pop_reinit(unsigned num_scopes) {
pop(num_scopes);
reinit_assumptions();
reinit_assumptions();
}
void solver::pop(unsigned num_scopes) {
@ -2578,13 +2578,13 @@ namespace sat {
m_clauses_to_reinit.shrink(j);
}
//
//
// All new clauses that are added to the solver
// are relative to the user-scope literals.
//
//
void solver::user_push() {
literal lit;
literal lit;
bool_var new_v = mk_var(true, false);
lit = literal(new_v, false);
m_user_scope_literals.push_back(lit);
@ -2674,7 +2674,7 @@ namespace sat {
m_phase.shrink(v);
m_prev_phase.shrink(v);
m_assigned_since_gc.shrink(v);
m_simplifier.reset_todo();
m_simplifier.reset_todos();
}
}
@ -2698,7 +2698,7 @@ namespace sat {
unassign_vars(i);
break;
}
}
}
gc_var(lit.var());
}
}
@ -3042,7 +3042,7 @@ namespace sat {
if (scope_lvl() > 0 || inconsistent())
return;
m_simplifier(learned);
m_simplifier.free_memory();
m_simplifier.finalize();
if (m_ext)
m_ext->clauses_modifed();
}
@ -3084,10 +3084,10 @@ namespace sat {
}
bool non_empty = true;
m_seen[0].reset();
while (non_empty) {
while (non_empty) {
literal_vector mutex;
bool turn = false;
m_reachable[turn] = ps;
m_reachable[turn] = ps;
while (!m_reachable[turn].empty()) {
literal p = m_reachable[turn].pop();
if (m_seen[0].contains(p)) {
@ -3104,7 +3104,7 @@ namespace sat {
turn = !turn;
}
if (mutex.size() > 1) {
mutexes.push_back(mutex);
mutexes.push_back(mutex);
}
non_empty = !mutex.empty();
}
@ -3148,7 +3148,7 @@ namespace sat {
switch (get_model()[v]) {
case l_true: lits.push_back(literal(v, false)); break;
case l_false: lits.push_back(literal(v, true)); break;
default: break;
default: break;
}
}
is_sat = get_consequences(asms, lits, conseq);
@ -3175,7 +3175,7 @@ namespace sat {
}
propagate(false);
if (check_inconsistent()) return l_false;
unsigned num_units = 0, num_iterations = 0;
extract_fixed_consequences(num_units, assumptions, vars, conseq);
while (!vars.empty()) {
@ -3192,14 +3192,14 @@ namespace sat {
push();
assign(~lit, justification());
propagate(false);
while (inconsistent()) {
while (inconsistent()) {
if (!resolve_conflict()) {
TRACE("sat", display(tout << "inconsistent\n"););
m_inconsistent = false;
is_sat = l_undef;
break;
}
propagate(false);
propagate(false);
++num_resolves;
}
if (scope_lvl() == 1) {
@ -3213,7 +3213,7 @@ namespace sat {
else {
is_sat = bounded_search();
if (is_sat == l_undef) {
restart();
restart();
}
}
}
@ -3224,7 +3224,7 @@ namespace sat {
if (is_sat == l_true) {
delete_unfixed(vars);
}
extract_fixed_consequences(num_units, assumptions, vars, conseq);
extract_fixed_consequences(num_units, assumptions, vars, conseq);
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
<< " iterations: " << num_iterations
<< " variables: " << vars.size()
@ -3244,10 +3244,10 @@ namespace sat {
if (value(lit) == l_true) {
to_keep.insert(lit);
}
}
}
unfixed = to_keep;
}
void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq) {
if (scope_lvl() > 1) {
pop(scope_lvl() - 1);
@ -3297,7 +3297,7 @@ namespace sat {
}
void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq) {
index_set s;
index_set s;
if (assumptions.contains(lit)) {
s.insert(lit.index());
}

6
src/sat/sat_solver.h
View file

@ -237,7 +237,11 @@ namespace sat {
lbool status(clause const & c) const;
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
void checkpoint() {
if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); }
if (!m_rlimit.inc()) {
m_mc.reset();
m_model_is_current = false;
throw solver_exception(Z3_CANCELED_MSG);
}
++m_num_checkpoints;
if (m_num_checkpoints < 10) return;
m_num_checkpoints = 0;

4
src/sat/sat_types.h
View file

@ -200,7 +200,7 @@ namespace sat {
iterator begin() const { return m_set.begin(); }
iterator end() const { return m_set.end(); }
void reset() { m_set.reset(); m_in_set.reset(); }
void cleanup() { m_set.finalize(); m_in_set.finalize(); }
void finalize() { m_set.finalize(); m_in_set.finalize(); }
uint_set& operator&=(uint_set const& other) {
unsigned j = 0;
for (unsigned i = 0; i < m_set.size(); ++i) {
@ -259,7 +259,7 @@ namespace sat {
bool empty() const { return m_set.empty(); }
unsigned size() const { return m_set.size(); }
void reset() { m_set.reset(); }
void cleanup() { m_set.cleanup(); }
void finalize() { m_set.finalize(); }
class iterator {
uint_set::iterator m_it;
public:

164
src/smt/smt_conflict_resolution.cpp
View file

@ -22,13 +22,13 @@ Revision History:
#include"ast_ll_pp.h"
namespace smt {
// ---------------------------
//
// Base class
//
// ---------------------------
conflict_resolution::conflict_resolution(ast_manager & m,
context & ctx,
dyn_ack_manager & dyn_ack_manager,
@ -42,7 +42,7 @@ namespace smt {
m_dyn_ack_manager(dyn_ack_manager),
m_assigned_literals(assigned_literals),
m_lemma_atoms(m),
m_todo_js_qhead(0),
m_todo_js_qhead(0),
m_antecedents(0),
m_watches(watches),
m_new_proofs(m),
@ -67,7 +67,7 @@ namespace smt {
}
/**
\brief Find a common ancestor (anc) of n1 and n2 in the 'proof' tree.
\brief Find a common ancestor (anc) of n1 and n2 in the 'proof' tree.
The common ancestor is used to produce irredundant transitivity proofs.
n1 = a1 = ... = ai = ANC = ... = root
@ -100,7 +100,7 @@ namespace smt {
*/
void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) {
SASSERT(m_antecedents);
TRACE("conflict_detail",
TRACE("conflict_detail",
ast_manager& m = get_manager();
tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
switch (js.get_kind()) {
@ -133,7 +133,7 @@ namespace smt {
mark_eq(lhs->get_arg(1), rhs->get_arg(0));
}
else {
for (unsigned i = 0; i < num_args; i++)
for (unsigned i = 0; i < num_args; i++)
mark_eq(lhs->get_arg(i), rhs->get_arg(i));
}
break;
@ -146,9 +146,9 @@ namespace smt {
/**
\brief Process the transitivity 'proof' from n1 and n2, where
n1 and n2 are in the same branch
n1 -> ... -> n2
This method may update m_antecedents, m_todo_js and m_todo_eqs.
The resultant set of literals is stored in m_antecedents.
@ -163,7 +163,7 @@ namespace smt {
/**
\brief Process the justification of n1 = n2.
This method may update m_antecedents, m_todo_js and m_todo_eqs.
The resultant set of literals is stored in m_antecedents.
@ -180,8 +180,8 @@ namespace smt {
The result is stored in result.
\remark This method does not reset the vectors m_antecedents, m_todo_js, m_todo_eqs, nor reset the
marks in the justification objects.
\remark This method does not reset the vectors m_antecedents, m_todo_js, m_todo_eqs, nor reset the
marks in the justification objects.
*/
void conflict_resolution::justification2literals_core(justification * js, literal_vector & result) {
SASSERT(m_todo_js_qhead <= m_todo_js.size());
@ -294,13 +294,13 @@ namespace smt {
if (js)
r = std::max(r, get_justification_max_lvl(js));
break;
}
}
case b_justification::BIN_CLAUSE:
r = std::max(r, m_ctx.get_assign_level(js.get_literal()));
break;
case b_justification::AXIOM:
break;
case b_justification::JUSTIFICATION:
case b_justification::JUSTIFICATION:
r = std::max(r, get_justification_max_lvl(js.get_justification()));
break;
default:
@ -313,8 +313,8 @@ namespace smt {
bool_var var = antecedent.var();
unsigned lvl = m_ctx.get_assign_level(var);
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";);
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
@ -386,17 +386,17 @@ namespace smt {
consequent = false_literal;
if (not_l != null_literal)
consequent = ~not_l;
m_conflict_lvl = get_max_lvl(consequent, js);
TRACE("conflict_bug",
tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level()
TRACE("conflict_bug",
tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level()
<< " search_lvl: " << m_ctx.get_search_level() << "\n";
tout << "js.kind: " << js.get_kind() << "\n";
tout << "consequent: " << consequent << ": ";
m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
m_ctx.display(tout, js); tout << "\n";
);
);
// m_conflict_lvl can be smaller than m_ctx.get_search_level() when:
// there are user level scopes created using the Z3 API, and
@ -413,7 +413,7 @@ namespace smt {
}
TRACE("conflict", tout << "conflict_lvl: " << m_conflict_lvl << "\n";);
SASSERT(!m_assigned_literals.empty());
SASSERT(m_todo_js.empty());
@ -425,32 +425,32 @@ namespace smt {
/**
\brief Cleanup datastructures used during resolve(), minimize lemma (when minimization is enabled),
compute m_new_scope_lvl and m_lemma_iscope_lvl, generate proof if needed.
This method assumes that the lemma is stored in m_lemma (and the associated atoms in m_lemma_atoms).
\warning This method assumes the literals in m_lemma[1] ... m_lemma[m_lemma.size() - 1] are marked.
*/
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
unmark_justifications(0);
TRACE("conflict",
tout << "before minimization:\n";
m_ctx.display_literals(tout, m_lemma);
tout << "\n";);
TRACE("conflict_verbose",
tout << "before minimization:\n";
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
if (m_params.m_minimize_lemmas)
minimize_lemma();
TRACE("conflict",
tout << "after minimization:\n";
m_ctx.display_literals(tout, m_lemma);
tout << "\n";);
TRACE("conflict_verbose",
tout << "after minimization:\n";
m_ctx.display_literals_verbose(tout, m_lemma);
@ -459,7 +459,7 @@ namespace smt {
TRACE("conflict_bug",
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
m_new_scope_lvl = m_ctx.get_search_level();
@ -478,11 +478,11 @@ namespace smt {
m_lemma_iscope_lvl = lvl;
}
}
TRACE("conflict",
tout << "new scope level: " << m_new_scope_lvl << "\n";
tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";);
if (m_manager.proofs_enabled())
mk_conflict_proof(conflict, not_l);
}
@ -505,7 +505,7 @@ namespace smt {
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal(tout, not_l); tout << "\n";);
process_antecedent(not_l, num_marks);
}
do {
if (get_manager().has_trace_stream()) {
@ -542,7 +542,7 @@ namespace smt {
process_antecedent(~l, num_marks);
}
justification * js = cls->get_justification();
if (js)
if (js)
process_justification(js, num_marks);
break;
}
@ -558,13 +558,13 @@ namespace smt {
default:
UNREACHABLE();
}
while (true) {
literal l = m_assigned_literals[idx];
if (m_ctx.is_marked(l.var()))
if (m_ctx.is_marked(l.var()))
break;
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
tout << "\n";);
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
// it may also be an (out-of-order) asserted literal
@ -580,7 +580,7 @@ namespace smt {
idx--;
num_marks--;
m_ctx.unset_mark(c_var);
}
}
while (num_marks > 0);
TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent); tout << "\n";);
@ -589,8 +589,8 @@ namespace smt {
m_lemma_atoms.set(0, m_ctx.bool_var2expr(consequent.var()));
// TODO:
//
// equality optimization should go here.
//
// equality optimization should go here.
//
finalize_resolve(conflict, not_l);
@ -600,7 +600,7 @@ namespace smt {
/**
\brief Return an approximation for the set of scope levels where the literals in m_lemma
were assigned.
were assigned.
*/
level_approx_set conflict_resolution::get_lemma_approx_level_set() {
level_approx_set result;
@ -640,7 +640,7 @@ namespace smt {
unsigned lvl = m_ctx.get_assign_level(var);
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
if (m_lvl_set.may_contain(lvl)) {
m_ctx.set_mark(var);
m_ctx.set_mark(var);
m_unmark.push_back(var);
m_lemma_min_stack.push_back(var);
}
@ -667,18 +667,18 @@ namespace smt {
}
/**
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
The idea is to stop the recursive search with a failure
as soon as we find a literal assigned in a level that is not in lvl_set.
as soon as we find a literal assigned in a level that is not in lvl_set.
*/
bool conflict_resolution::implied_by_marked(literal lit) {
m_lemma_min_stack.reset(); // avoid recursive function
m_lemma_min_stack.push_back(lit.var());
unsigned old_size = m_unmark.size();
unsigned old_js_qhead = m_todo_js_qhead;
while (!m_lemma_min_stack.empty()) {
bool_var var = m_lemma_min_stack.back();
m_lemma_min_stack.pop_back();
@ -739,7 +739,7 @@ namespace smt {
m_unmark.reset();
m_lvl_set = get_lemma_approx_level_set();
unsigned sz = m_lemma.size();
unsigned i = 1; // the first literal is the FUIP
unsigned j = 1;
@ -756,7 +756,7 @@ namespace smt {
j++;
}
}
reset_unmark_and_justifications(0, 0);
m_lemma .shrink(j);
m_lemma_atoms.shrink(j);
@ -810,7 +810,7 @@ namespace smt {
}
if (m_manager.coarse_grain_proofs())
return pr;
TRACE("norm_eq_proof",
TRACE("norm_eq_proof",
tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";
tout << mk_ll_pp(pr, m_manager, true, false););
SASSERT(m_manager.is_eq(fact) || m_manager.is_iff(fact));
@ -906,7 +906,7 @@ namespace smt {
return 0;
}
}
/**
\brief Return the proof object associated with the given literal if it already
exists. Otherwise, return 0 and add l to the todo-list.
@ -939,13 +939,13 @@ namespace smt {
// p1: is a proof of "A"
// p2: is a proof of "not A"
// [unit-resolution p1 p2]: false
//
//
// Let us assume that "A" was assigned first during propagation.
// Then, the "resolve" method will never select "not A" as a hypothesis.
// "not_A" will be the not_l argument in this method.
// "not_A" will be the not_l argument in this method.
// Since we are assuming that "A" was assigned first", m_ctx.get_justification("A") will be
// p1.
//
//
// So, the test "m_ctx.get_justification(l.var()) == js" is used to check
// if l was assigned before ~l.
if ((m_ctx.is_marked(l.var()) && m_ctx.get_justification(l.var()) == js) || (js.get_kind() == b_justification::AXIOM)) {
@ -1022,11 +1022,11 @@ namespace smt {
tout << mk_pp(m_manager.get_fact(prs[i]), m_manager) << "\n";
}
tout << "consequent:\n" << mk_pp(l_exr, m_manager) << "\n";);
TRACE("get_proof",
TRACE("get_proof",
tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " ";
m_ctx.display_literal(tout, l); tout << " --->\n";
tout << mk_ll_pp(l_exr, m_manager););
CTRACE("get_proof_bug_after",
CTRACE("get_proof_bug_after",
invocation_counter >= DUMP_AFTER_NUM_INVOCATIONS,
tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " ";
m_ctx.display_literal(tout, l); tout << " --->\n";
@ -1040,7 +1040,7 @@ namespace smt {
}
}
}
/**
\brief Return the proof object associated with the given justification
if it already exists. Otherwise, return 0 and add js to the todo-list.
@ -1094,7 +1094,7 @@ namespace smt {
i = 2;
}
}
for (; i < num_lits; i++)
for (; i < num_lits; i++)
if (get_proof(~cls->get_literal(i)) == 0)
visited = false;
return visited;
@ -1109,7 +1109,7 @@ namespace smt {
SASSERT(pr);
TRACE("proof_gen_bug", tout << "lit2pr_saved: #" << l << "\n";);
m_lit2proof.insert(l, pr);
TRACE("mk_proof",
TRACE("mk_proof",
tout << mk_bounded_pp(m_ctx.bool_var2expr(l.var()), m_manager, 10) << "\n";
tout << "storing proof for: "; m_ctx.display_literal(tout, l); tout << "\n";
tout << mk_ll_pp(pr, m_manager););
@ -1118,7 +1118,7 @@ namespace smt {
/**
\brief Given that lhs = ... = rhs, and lhs reaches rhs in the 'proof' tree branch.
Then, return true if all proof objects needed to create the proof steps are already
available. Otherwise return false and update m_todo_pr with info about the proof
available. Otherwise return false and update m_todo_pr with info about the proof
objects that need to be created.
*/
bool conflict_resolution::visit_trans_proof(enode * lhs, enode * rhs) {
@ -1174,7 +1174,7 @@ namespace smt {
/**
\brief Return true if all proof objects that are used to build the proof that lhs = rhs were
already built. If the result is false, then m_todo_pr is updated with info about the proof
already built. If the result is false, then m_todo_pr is updated with info about the proof
objects that need to be created.
*/
bool conflict_resolution::visit_eq_justications(enode * lhs, enode * rhs) {
@ -1226,7 +1226,7 @@ namespace smt {
if (prs1.size() == 1)
pr = prs1[0];
else {
TRACE("mk_transitivity",
TRACE("mk_transitivity",
unsigned sz = prs1.size();
for (unsigned i = 0; i < sz; i++) {
tout << mk_ll_pp(prs1[i], m_manager) << "\n";
@ -1288,7 +1288,7 @@ namespace smt {
}
case tp_elem::LITERAL: {
literal l = to_literal(elem.m_lidx);
if (m_lit2proof.contains(l))
if (m_lit2proof.contains(l))
m_todo_pr.pop_back();
else {
b_justification js = m_ctx.get_justification(l.var());
@ -1342,11 +1342,11 @@ namespace smt {
void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) {
bool_var var = antecedent.var();
TRACE("conflict", tout << "processing antecedent: ";
m_ctx.display_literal_info(tout << antecedent << " ", antecedent);
tout << (m_ctx.is_marked(var)?"marked":"not marked");
tout << "\n";);
TRACE("conflict", tout << "processing antecedent: ";
m_ctx.display_literal_info(tout << antecedent << " ", antecedent);
tout << (m_ctx.is_marked(var)?"marked":"not marked");
tout << "\n";);
if (!m_ctx.is_marked(var)) {
m_ctx.set_mark(var);
m_unmark.push_back(var);
@ -1355,7 +1355,7 @@ namespace smt {
m_assumptions.push_back(antecedent);
}
}
void conflict_resolution::process_justification_for_unsat_core(justification * js) {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
@ -1370,7 +1370,7 @@ namespace smt {
SASSERT(m_ctx.tracking_assumptions());
m_assumptions.reset();
m_unmark.reset();
SASSERT(m_conflict_lvl <= m_ctx.get_search_level());
unsigned search_lvl = m_ctx.get_search_level();
@ -1378,17 +1378,17 @@ namespace smt {
literal consequent = false_literal;
if (not_l != null_literal) {
consequent = ~not_l;
}
}
int idx = skip_literals_above_conflict_level();
if (not_l != null_literal)
process_antecedent_for_unsat_core(consequent);
if (m_assigned_literals.empty()) {
goto end_unsat_core;
}
while (true) {
TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
switch (js.get_kind()) {
@ -1411,7 +1411,7 @@ namespace smt {
process_antecedent_for_unsat_core(~l);
}
justification * js = cls->get_justification();
if (js)
if (js)
process_justification_for_unsat_core(js);
break;
}
@ -1430,17 +1430,17 @@ namespace smt {
if (m_ctx.is_assumption(consequent.var())) {
m_assumptions.push_back(consequent);
}
}
while (idx >= 0) {
literal l = m_assigned_literals[idx];
TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
if (m_ctx.get_assign_level(l) < search_lvl)
goto end_unsat_core;
if (m_ctx.is_marked(l.var()))
if (m_ctx.get_assign_level(l) < search_lvl)
goto end_unsat_core;
if (m_ctx.is_marked(l.var()))
break;
idx--;
}
if (idx < 0) {
if (idx < 0) {
goto end_unsat_core;
}
@ -1456,12 +1456,12 @@ namespace smt {
TRACE("unsat_core", tout << "assumptions:\n"; m_ctx.display_literals(tout, m_assumptions); tout << "\n";);
reset_unmark_and_justifications(0, 0);
}
conflict_resolution * mk_conflict_resolution(ast_manager & m,
conflict_resolution * mk_conflict_resolution(ast_manager & m,
context & ctx,
dyn_ack_manager & dack_manager,
smt_params const & params,
literal_vector const & assigned_literals,
literal_vector const & assigned_literals,
vector<watch_list> & watches) {
return alloc(conflict_resolution, m, ctx, dack_manager, params, assigned_literals, watches);
}

48
src/smt/theory_fpa.cpp
View file

@ -334,23 +334,30 @@ namespace smt {
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
try {
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
catch (rewriter_exception &)
{
m_th_rw.reset();
throw;
}
else
UNREACHABLE();
return res;
}
@ -743,8 +750,15 @@ namespace smt {
// These are the conversion functions fp.to_* */
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
}
else
UNREACHABLE();
else {
/* Theory variables can be merged when (= bv-term (bvwrap fp-term)),
in which case context::relevant_eh may call theory_fpa::relevant_eh
after theory_bv::relevant_eh, regardless of whether theory_fpa is
interested in this term. But, this can only happen because of
(bvwrap ...) terms, i.e., `n' must be a bit-vector expression,
which we can safely ignore. */
SASSERT(m_bv_util.is_bv(n));
}
}
void theory_fpa::reset_eh() {