mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

merge with unstable

Browse source
This commit is contained in:
Ken McMillan 2015-07-27 11:24:17 -07:00
commit 52de96fcfc
40 changed files with 1398 additions and 1071 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_arith.cpp
View file

@ -47,7 +47,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_real(__in Z3_context c, int num, int den) {
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) {
Z3_TRY;
LOG_Z3_mk_real(c, num, den);
RESET_ERROR_CODE();

20
src/api/api_array.cpp
View file

@ -83,7 +83,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_map(__in Z3_context c, __in Z3_func_decl f, unsigned n, __in Z3_ast const* args) {
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
Z3_TRY;
LOG_Z3_mk_map(c, f, n, args);
RESET_ERROR_CODE();
@ -108,7 +108,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v) {
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v) {
Z3_TRY;
LOG_Z3_mk_const_array(c, domain, v);
RESET_ERROR_CODE();
@ -127,7 +127,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_array_default(__in Z3_context c, __in Z3_ast array) {
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array) {
Z3_TRY;
LOG_Z3_mk_array_default(c, array);
RESET_ERROR_CODE();
@ -142,7 +142,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast mk_app_array_core(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v) {
Z3_ast mk_app_array_core(Z3_context c, Z3_sort domain, Z3_ast v) {
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
expr * _v = to_expr(v);
@ -158,13 +158,13 @@ extern "C" {
return of_ast(r);
}
Z3_sort Z3_API Z3_mk_set_sort(__in Z3_context c, __in Z3_sort ty) {
Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty) {
Z3_TRY;
return Z3_mk_array_sort(c, ty, Z3_mk_bool_sort(c));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_empty_set(__in Z3_context c, __in Z3_sort domain) {
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain) {
Z3_TRY;
LOG_Z3_mk_empty_set(c, domain);
RESET_ERROR_CODE();
@ -173,7 +173,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_full_set(__in Z3_context c, __in Z3_sort domain) {
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain) {
Z3_TRY;
LOG_Z3_mk_full_set(c, domain);
RESET_ERROR_CODE();
@ -188,15 +188,15 @@ extern "C" {
MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
Z3_ast Z3_mk_set_member(__in Z3_context c, __in Z3_ast elem, __in Z3_ast set) {
Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
return Z3_mk_select(c, set, elem);
}
Z3_ast Z3_mk_set_add(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem) {
Z3_ast Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem) {
return Z3_mk_store(c, set, elem, Z3_mk_true(c));
}
Z3_ast Z3_mk_set_del(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem) {
Z3_ast Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem) {
return Z3_mk_store(c, set, elem, Z3_mk_false(c));
}

24
src/api/api_bv.cpp
View file

@ -159,7 +159,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
This function is a shorthand for <tt>shl(1, N-1)</tt>
where <tt>N</tt> are the number of bits of \c s.
*/
Z3_ast Z3_API Z3_mk_bvmsb(__in Z3_context c, __in Z3_sort s) {
Z3_ast Z3_API Z3_mk_bvmsb(Z3_context c, Z3_sort s) {
Z3_TRY;
RESET_ERROR_CODE();
// Not logging this one, since it is just syntax sugar.
@ -179,19 +179,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_mk_bvsmin(__in Z3_context c, __in Z3_sort s) {
Z3_ast Z3_mk_bvsmin(Z3_context c, Z3_sort s) {
return Z3_mk_bvmsb(c, s);
}
Z3_ast Z3_mk_bvsmax(__in Z3_context c, __in Z3_sort s) {
Z3_ast Z3_mk_bvsmax(Z3_context c, Z3_sort s) {
return Z3_mk_bvnot(c, Z3_mk_bvmsb(c, s));
}
Z3_ast Z3_mk_bvumax(__in Z3_context c, __in Z3_sort s) {
Z3_ast Z3_mk_bvumax(Z3_context c, Z3_sort s) {
return Z3_mk_int(c, -1, s);
}
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed) {
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
Z3_TRY;
RESET_ERROR_CODE();
if (is_signed) {
@ -235,7 +235,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
}
// only for signed machine integers
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
@ -263,7 +263,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
}
// only for signed machine integers
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
@ -291,7 +291,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed) {
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
Z3_TRY;
RESET_ERROR_CODE();
if (is_signed) {
@ -316,7 +316,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(__in Z3_context c, __in Z3_ast n1, __in Z3_ast n2, Z3_bool is_signed) {
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_bool is_signed) {
LOG_Z3_mk_bvmul_no_overflow(c, n1, n2, is_signed);
RESET_ERROR_CODE();
if (is_signed) {
@ -328,13 +328,13 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
}
// only for signed machine integers
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(__in Z3_context c, __in Z3_ast n1, __in Z3_ast n2) {
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast n1, Z3_ast n2) {
LOG_Z3_mk_bvmul_no_underflow(c, n1, n2);
MK_BINARY_BODY(Z3_mk_bvmul_no_underflow, mk_c(c)->get_bv_fid(), OP_BSMUL_NO_UDFL, SKIP);
}
// only for signed machine integers
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(__in Z3_context c, __in Z3_ast t) {
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_ast min = Z3_mk_bvsmin(c, Z3_get_sort(c, t));
@ -346,7 +346,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
}
// only for signed machine integers
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_sort s = Z3_get_sort(c, t1);

4
src/api/api_context.cpp
View file

@ -532,7 +532,7 @@ extern "C" {
// [Leo]: using exception handling, we don't need global error handlers anymore
}
void Z3_API Z3_set_error(__in Z3_context c, __in Z3_error_code e) {
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e) {
SET_ERROR_CODE(e);
}
@ -584,7 +584,7 @@ extern "C" {
};
Z3_API ast_manager& Z3_get_manager(__in Z3_context c) {
Z3_API ast_manager& Z3_get_manager(Z3_context c) {
return mk_c(c)->m();
}

4
src/api/api_datalog.cpp
View file

@ -304,8 +304,8 @@ extern "C" {
}
Z3_lbool Z3_API Z3_fixedpoint_query_relations(
__in Z3_context c,__in Z3_fixedpoint d,
__in unsigned num_relations, Z3_func_decl const relations[]) {
Z3_context c,Z3_fixedpoint d,
unsigned num_relations, Z3_func_decl const relations[]) {
Z3_TRY;
LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations);
RESET_ERROR_CODE();

2
src/api/api_datatype.cpp
View file

@ -619,7 +619,7 @@ extern "C" {
}
Z3_ast Z3_datatype_update_field(
__in Z3_context c, __in Z3_func_decl f, __in Z3_ast t, __in Z3_ast v) {
Z3_context c, Z3_func_decl f, Z3_ast t, Z3_ast v) {
Z3_TRY;
LOG_Z3_datatype_update_field(c, f, t, v);
RESET_ERROR_CODE();

8
src/api/api_fpa.cpp
View file

@ -737,7 +737,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) {
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);
RESET_ERROR_CODE();
@ -767,7 +767,7 @@ extern "C" {
Z3_CATCH_RETURN("");
}
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
RESET_ERROR_CODE();
@ -791,7 +791,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
RESET_ERROR_CODE();
@ -815,7 +815,7 @@ extern "C" {
Z3_CATCH_RETURN("");
}
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
RESET_ERROR_CODE();

26
src/api/api_interp.cpp
View file

@ -207,7 +207,7 @@ extern "C" {
opts->map[name] = value;
}
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p){
Z3_TRY;
LOG_Z3_get_interpolant(c, pf, pat, p);
RESET_ERROR_CODE();
@ -240,7 +240,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *out_interp, Z3_model *model){
Z3_TRY;
LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
RESET_ERROR_CODE();
@ -708,15 +708,15 @@ extern "C" {
def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
*/
Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast *cnsts,
__in_ecount(num) unsigned *parents,
__in Z3_params options,
__out_ecount(num - 1) Z3_ast *interps,
__out Z3_model *model,
__out Z3_literals *labels,
__in unsigned incremental,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast *theory);
Z3_lbool Z3_API Z3_interpolate(Z3_context ctx,
unsigned num,
Z3_ast *cnsts,
unsigned *parents,
Z3_params options,
Z3_ast *interps,
Z3_model *model,
Z3_literals *labels,
unsigned incremental,
unsigned num_theory,
Z3_ast *theory);
#endif

36
src/api/dotnet/Context.cs
View file

@ -2134,31 +2134,31 @@ namespace Microsoft.Z3
/// <summary>
/// Create an empty set.
/// </summary>
public Expr MkEmptySet(Sort domain)
public ArrayExpr MkEmptySet(Sort domain)
{
Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain);
return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
}
/// <summary>
/// Create the full set.
/// </summary>
public Expr MkFullSet(Sort domain)
public ArrayExpr MkFullSet(Sort domain)
{
Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain);
return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
}
/// <summary>
/// Add an element to the set.
/// </summary>
public Expr MkSetAdd(Expr set, Expr element)
public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
{
Contract.Requires(set != null);
Contract.Requires(element != null);
@ -2166,14 +2166,14 @@ namespace Microsoft.Z3
CheckContextMatch(set);
CheckContextMatch(element);
return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
}
/// <summary>
/// Remove an element from a set.
/// </summary>
public Expr MkSetDel(Expr set, Expr element)
public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
{
Contract.Requires(set != null);
Contract.Requires(element != null);
@ -2181,38 +2181,38 @@ namespace Microsoft.Z3
CheckContextMatch(set);
CheckContextMatch(element);
return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
}
/// <summary>
/// Take the union of a list of sets.
/// </summary>
public Expr MkSetUnion(params Expr[] args)
public ArrayExpr MkSetUnion(params ArrayExpr[] args)
{
Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null));
CheckContextMatch(args);
return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
}
/// <summary>
/// Take the intersection of a list of sets.
/// </summary>
public Expr MkSetIntersection(params Expr[] args)
public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
{
Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null));
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(args);
return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
}
/// <summary>
/// Take the difference between two sets.
/// </summary>
public Expr MkSetDifference(Expr arg1, Expr arg2)
public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
{
Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null);
@ -2220,25 +2220,25 @@ namespace Microsoft.Z3
CheckContextMatch(arg1);
CheckContextMatch(arg2);
return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
}
/// <summary>
/// Take the complement of a set.
/// </summary>
public Expr MkSetComplement(Expr arg)
public ArrayExpr MkSetComplement(ArrayExpr arg)
{
Contract.Requires(arg != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(arg);
return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
}
/// <summary>
/// Check for set membership.
/// </summary>
public BoolExpr MkSetMembership(Expr elem, Expr set)
public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
{
Contract.Requires(elem != null);
Contract.Requires(set != null);
@ -2252,7 +2252,7 @@ namespace Microsoft.Z3
/// <summary>
/// Check for subsetness of sets.
/// </summary>
public BoolExpr MkSetSubset(Expr arg1, Expr arg2)
public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
{
Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null);

41
src/api/dotnet/Symbol.cs
View file

@ -66,6 +66,47 @@ namespace Microsoft.Z3
throw new Z3Exception("Unknown symbol kind encountered");
}
/// <summary>
/// Equality overloading.
/// </summary>
public static bool operator ==(Symbol s1, Symbol s2)
{
return Object.ReferenceEquals(s1, s2) ||
(!Object.ReferenceEquals(s1, null) &&
!Object.ReferenceEquals(s2, null) &&
s1.NativeObject == s2.NativeObject);
}
/// <summary>
/// Equality overloading.
/// </summary>
public static bool operator !=(Symbol s1, Symbol s2)
{
return !(s1.NativeObject == s2.NativeObject);
}
/// <summary>
/// Object comparison.
/// </summary>
public override bool Equals(object o)
{
Symbol casted = o as Symbol;
if (casted == null) return false;
return this == casted;
}
/// <summary>
/// The Symbols's hash code.
/// </summary>
/// <returns>A hash code</returns>
public override int GetHashCode()
{
return (int)NativeObject;
}
#region Internal
/// <summary>
/// Symbol constructor

15
src/api/java/AST.java
View file

@ -22,10 +22,8 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
/**
* The abstract syntax tree (AST) class.
**/
public class AST extends Z3Object
public class AST extends Z3Object implements Comparable
{
/* Overloaded operators are not translated. */
/**
* Object comparison.
*
@ -35,7 +33,7 @@ public class AST extends Z3Object
{
AST casted = null;
try
try
{
casted = AST.class.cast(o);
} catch (ClassCastException e)
@ -43,8 +41,13 @@ public class AST extends Z3Object
return false;
}
return this.getNativeObject() == casted.getNativeObject();
}
return
(this == casted) ||
(this != null) &&
(casted != null) &&
(getContext().nCtx() == casted.getContext().nCtx()) &&
(Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
}
/**
* Object Comparison.

53
src/api/java/Context.java
View file

@ -1725,32 +1725,31 @@ public class Context extends IDisposable
/**
* Create an empty set.
**/
public Expr mkEmptySet(Sort domain)
public ArrayExpr mkEmptySet(Sort domain)
{
checkContextMatch(domain);
return Expr.create(this,
return (ArrayExpr)Expr.create(this,
Native.mkEmptySet(nCtx(), domain.getNativeObject()));
}
/**
* Create the full set.
**/
public Expr mkFullSet(Sort domain)
public ArrayExpr mkFullSet(Sort domain)
{
checkContextMatch(domain);
return Expr.create(this,
return (ArrayExpr)Expr.create(this,
Native.mkFullSet(nCtx(), domain.getNativeObject()));
}
/**
* Add an element to the set.
**/
public Expr mkSetAdd(Expr set, Expr element)
public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
{
checkContextMatch(set);
checkContextMatch(element);
return Expr.create(
this,
return (ArrayExpr)Expr.create(this,
Native.mkSetAdd(nCtx(), set.getNativeObject(),
element.getNativeObject()));
}
@ -1758,12 +1757,11 @@ public class Context extends IDisposable
/**
* Remove an element from a set.
**/
public Expr mkSetDel(Expr set, Expr element)
public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
{
checkContextMatch(set);
checkContextMatch(element);
return Expr.create(
this,
return (ArrayExpr)Expr.create(this,
Native.mkSetDel(nCtx(), set.getNativeObject(),
element.getNativeObject()));
}
@ -1771,11 +1769,10 @@ public class Context extends IDisposable
/**
* Take the union of a list of sets.
**/
public Expr mkSetUnion(Expr... args)
public ArrayExpr mkSetUnion(ArrayExpr... args)
{
checkContextMatch(args);
return Expr.create(
this,
return (ArrayExpr)Expr.create(this,
Native.mkSetUnion(nCtx(), (int) args.length,
AST.arrayToNative(args)));
}
@ -1783,11 +1780,10 @@ public class Context extends IDisposable
/**
* Take the intersection of a list of sets.
**/
public Expr mkSetIntersection(Expr... args)
public ArrayExpr mkSetIntersection(ArrayExpr... args)
{
checkContextMatch(args);
return Expr.create(
this,
return (ArrayExpr)Expr.create(this,
Native.mkSetIntersect(nCtx(), (int) args.length,
AST.arrayToNative(args)));
}
@ -1795,12 +1791,11 @@ public class Context extends IDisposable
/**
* Take the difference between two sets.
**/
public Expr mkSetDifference(Expr arg1, Expr arg2)
public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
{
checkContextMatch(arg1);
checkContextMatch(arg2);
return Expr.create(
this,
return (ArrayExpr)Expr.create(this,
Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
arg2.getNativeObject()));
}
@ -1808,22 +1803,21 @@ public class Context extends IDisposable
/**
* Take the complement of a set.
**/
public Expr mkSetComplement(Expr arg)
public ArrayExpr mkSetComplement(ArrayExpr arg)
{
checkContextMatch(arg);
return Expr.create(this,
return (ArrayExpr)Expr.create(this,
Native.mkSetComplement(nCtx(), arg.getNativeObject()));
}
/**
* Check for set membership.
**/
public BoolExpr mkSetMembership(Expr elem, Expr set)
public BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
{
checkContextMatch(elem);
checkContextMatch(set);
return (BoolExpr) Expr.create(
this,
return (BoolExpr) Expr.create(this,
Native.mkSetMember(nCtx(), elem.getNativeObject(),
set.getNativeObject()));
}
@ -1831,12 +1825,11 @@ public class Context extends IDisposable
/**
* Check for subsetness of sets.
**/
public BoolExpr mkSetSubset(Expr arg1, Expr arg2)
public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
{
checkContextMatch(arg1);
checkContextMatch(arg2);
return (BoolExpr) Expr.create(
this,
return (BoolExpr) Expr.create(this,
Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
arg2.getNativeObject()));
}
@ -3678,6 +3671,7 @@ public class Context extends IDisposable
private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10);
public IDecRefQueue getASTDRQ()
{
@ -3754,6 +3748,11 @@ public class Context extends IDisposable
return m_Fixedpoint_DRQ;
}
public IDecRefQueue getOptimizeDRQ()
{
return m_Optimize_DRQ;
}
protected long m_refCount = 0;
/**

23
src/api/java/FuncDecl.java
View file

@ -26,22 +26,6 @@ import com.microsoft.z3.enumerations.Z3_parameter_kind;
**/
public class FuncDecl extends AST
{
/**
* Comparison operator.
*
* @return True if {@code a"/> and <paramref name="b} share the
* same context and are equal, false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Comparison operator.
*
* @return True if {@code a"/> and <paramref name="b} do not
* share the same context or are not equal, false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Object comparison.
**/
@ -55,7 +39,12 @@ public class FuncDecl extends AST
return false;
}
return this.getNativeObject() == casted.getNativeObject();
return
(this == casted) ||
(this != null) &&
(casted != null) &&
(getContext().nCtx() == casted.getContext().nCtx()) &&
(Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
}
/**

261
src/api/java/Optimize.java Normal file
View file

@ -0,0 +1,261 @@
/**
Copyright (c) 2015 Microsoft Corporation
Module Name:
Optimize.java
Abstract:
Z3 Java API: Optimizes
Author:
Nikolaj Bjorner (nbjorner) 2015-07-16
Notes:
**/
package com.microsoft.z3;
import com.microsoft.z3.enumerations.Z3_lbool;
/**
* Object for managing optimizization context
**/
public class Optimize extends Z3Object
{
/**
* A string that describes all available optimize solver parameters.
**/
public String getHelp()
{
return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
}
/**
* Sets the optimize solver parameters.
*
* @throws Z3Exception
**/
public void setParameters(Params value)
{
Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
}
/**
* Retrieves parameter descriptions for Optimize solver.
**/
public ParamDescrs getParameterDescriptions()
{
return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
}
/**
* Assert a constraint (or multiple) into the optimize solver.
**/
public void Assert(BoolExpr ... constraints)
{
getContext().checkContextMatch(constraints);
for (BoolExpr a : constraints)
{
Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
}
}
/**
* Alias for Assert.
**/
public void Add(BoolExpr ... constraints)
{
Assert(constraints);
}
/**
* Handle to objectives returned by objective functions.
**/
public class Handle
{
Optimize opt;
int handle;
Handle(Optimize opt, int h)
{
this.opt = opt;
this.handle = h;
}
/**
* Retrieve a lower bound for the objective handle.
**/
public ArithExpr getLower()
{
return opt.GetLower(handle);
}
/**
* Retrieve an upper bound for the objective handle.
**/
public ArithExpr getUpper()
{
return opt.GetUpper(handle);
}
/**
* Retrieve the value of an objective.
**/
public ArithExpr getValue()
{
return getLower();
}
}
/**
* Assert soft constraint
*
* Return an objective which associates with the group of constraints.
*
**/
public Handle AssertSoft(BoolExpr constraint, int weight, String group)
{
getContext().checkContextMatch(constraint);
Symbol s = getContext().mkSymbol(group);
return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
}
/**
* Check satisfiability of asserted constraints.
* Produce a model that (when the objectives are bounded and
* don't use strict inequalities) meets the objectives.
**/
public Status Check()
{
Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
switch (r) {
case Z3_L_TRUE:
return Status.SATISFIABLE;
case Z3_L_FALSE:
return Status.UNSATISFIABLE;
default:
return Status.UNKNOWN;
}
}
/**
* Creates a backtracking point.
**/
public void Push()
{
Native.optimizePush(getContext().nCtx(), getNativeObject());
}
/**
* Backtrack one backtracking point.
*
* Note that an exception is thrown if Pop is called without a corresponding Push.
**/
public void Pop()
{
Native.optimizePop(getContext().nCtx(), getNativeObject());
}
/**
* The model of the last Check.
*
* The result is null if Check was not invoked before,
* if its results was not SATISFIABLE, or if model production is not enabled.
**/
public Model getModel()
{
long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
if (x == 0)
return null;
else
return new Model(getContext(), x);
}
/**
* Declare an arithmetical maximization objective.
* Return a handle to the objective. The handle is used as
* to retrieve the values of objectives after calling Check.
**/
public Handle MkMaximize(ArithExpr e)
{
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
}
/**
* Declare an arithmetical minimization objective.
* Similar to MkMaximize.
**/
public Handle MkMinimize(ArithExpr e)
{
return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
}
/**
* Retrieve a lower bound for the objective handle.
**/
private ArithExpr GetLower(int index)
{
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
}
/**
* Retrieve an upper bound for the objective handle.
**/
private ArithExpr GetUpper(int index)
{
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
}
/**
* Print the context to a String (SMT-LIB parseable benchmark).
**/
public String toString()
{
return Native.optimizeToString(getContext().nCtx(), getNativeObject());
}
/**
* Optimize statistics.
**/
public Statistics getStatistics()
{
return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
}
Optimize(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);
}
Optimize(Context ctx) throws Z3Exception
{
super(ctx, Native.mkOptimize(ctx.nCtx()));
}
void incRef(long o)
{
getContext().getOptimizeDRQ().incAndClear(getContext(), o);
super.incRef(o);
}
void decRef(long o)
{
getContext().getOptimizeDRQ().add(o);
super.decRef(o);
}
}

53
src/api/java/OptimizeDecRefQueue.java Normal file
View file

@ -0,0 +1,53 @@
/**
Copyright (c) 2012-2015 Microsoft Corporation
Module Name:
OptimizeDecRefQueue.java
Abstract:
Author:
@author Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
**/
package com.microsoft.z3;
class OptimizeDecRefQueue extends IDecRefQueue
{
public OptimizeDecRefQueue()
{
super();
}
public OptimizeDecRefQueue(int move_limit)
{
super(move_limit);
}
protected void incRef(Context ctx, long obj)
{
try
{
Native.fixedpointIncRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
}
protected void decRef(Context ctx, long obj)
{
try
{
Native.fixedpointDecRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
}
};

9
src/api/java/Sort.java
View file

@ -25,8 +25,6 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
**/
public class Sort extends AST
{
/* Overloaded operators are not translated. */
/**
* Equality operator for objects of type Sort.
* @param o
@ -42,7 +40,12 @@ public class Sort extends AST
return false;
}
return this.getNativeObject() == casted.getNativeObject();
return
(this == casted) ||
(this != null) &&
(casted != null) &&
(getContext().nCtx() == casted.getContext().nCtx()) &&
(Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
}
/**

10
src/api/z3.h
View file

@ -30,15 +30,5 @@ Notes:
#include"z3_interp.h"
#include"z3_fpa.h"
#undef __in
#undef __out
#undef __inout
#undef __in_z
#undef __out_z
#undef __ecount
#undef __in_ecount
#undef __out_ecount
#undef __inout_ecount
#endif

38
src/api/z3_algebraic.h
View file

@ -43,7 +43,7 @@ extern "C" {
def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
/**
\brief Return the Z3_TRUE if \c a is positive, and Z3_FALSE otherwise.
@ -52,7 +52,7 @@ extern "C" {
def_API('Z3_algebraic_is_pos', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
/**
\brief Return the Z3_TRUE if \c a is negative, and Z3_FALSE otherwise.
@ -61,7 +61,7 @@ extern "C" {
def_API('Z3_algebraic_is_neg', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
/**
\brief Return the Z3_TRUE if \c a is zero, and Z3_FALSE otherwise.
@ -70,7 +70,7 @@ extern "C" {
def_API('Z3_algebraic_is_zero', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a);
/**
\brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative.
@ -79,7 +79,7 @@ extern "C" {
def_API('Z3_algebraic_sign', INT, (_in(CONTEXT), _in(AST)))
*/
int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a);
/**
\brief Return the value a + b.
@ -90,7 +90,7 @@ extern "C" {
def_API('Z3_algebraic_add', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the value a - b.
@ -101,7 +101,7 @@ extern "C" {
def_API('Z3_algebraic_sub', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the value a * b.
@ -112,7 +112,7 @@ extern "C" {
def_API('Z3_algebraic_mul', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the value a / b.
@ -124,7 +124,7 @@ extern "C" {
def_API('Z3_algebraic_div', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return the a^(1/k)
@ -135,7 +135,7 @@ extern "C" {
def_API('Z3_algebraic_root', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
*/
Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k);
/**
\brief Return the a^k
@ -145,7 +145,7 @@ extern "C" {
def_API('Z3_algebraic_power', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
*/
Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k);
/**
\brief Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
@ -155,7 +155,7 @@ extern "C" {
def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
@ -165,7 +165,7 @@ extern "C" {
def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
@ -175,7 +175,7 @@ extern "C" {
def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
@ -185,7 +185,7 @@ extern "C" {
def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
@ -195,7 +195,7 @@ extern "C" {
def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
@ -205,7 +205,7 @@ extern "C" {
def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
/**
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
@ -217,7 +217,7 @@ extern "C" {
def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/
Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
/**
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the
@ -228,7 +228,7 @@ extern "C" {
def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/
int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
/*@}*/
/*@}*/

1442
src/api/z3_api.h
View file

File diff suppressed because it is too large Load diff

140
src/api/z3_fpa.h
View file

@ -42,7 +42,7 @@ extern "C" {
def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
@ -51,7 +51,7 @@ extern "C" {
def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
@ -60,7 +60,7 @@ extern "C" {
def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_rne(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
@ -69,7 +69,7 @@ extern "C" {
def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
@ -78,7 +78,7 @@ extern "C" {
def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_rna(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
@ -87,7 +87,7 @@ extern "C" {
def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
@ -96,7 +96,7 @@ extern "C" {
def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_rtp(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
@ -105,7 +105,7 @@ extern "C" {
def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
@ -114,7 +114,7 @@ extern "C" {
def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_rtn(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
@ -123,7 +123,7 @@ extern "C" {
def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);
/**
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
@ -132,7 +132,7 @@ extern "C" {
def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
*/
Z3_ast Z3_API Z3_mk_fpa_rtz(__in Z3_context c);
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c);
/**
\brief Create a FloatingPoint sort.
@ -145,7 +145,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
*/
Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits);
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);
/**
\brief Create the half-precision (16-bit) FloatingPoint sort.
@ -154,7 +154,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c);
/**
\brief Create the half-precision (16-bit) FloatingPoint sort.
@ -163,7 +163,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);
/**
\brief Create the single-precision (32-bit) FloatingPoint sort.
@ -172,7 +172,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c);
/**
\brief Create the single-precision (32-bit) FloatingPoint sort.
@ -181,7 +181,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);
/**
\brief Create the double-precision (64-bit) FloatingPoint sort.
@ -190,7 +190,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c);
/**
\brief Create the double-precision (64-bit) FloatingPoint sort.
@ -199,7 +199,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);
/**
\brief Create the quadruple-precision (128-bit) FloatingPoint sort.
@ -208,7 +208,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c);
/**
\brief Create the quadruple-precision (128-bit) FloatingPoint sort.
@ -217,7 +217,7 @@ extern "C" {
def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
*/
Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c);
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
/**
\brief Create a floating-point NaN of sort s.
@ -227,7 +227,7 @@ extern "C" {
def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
/**
\brief Create a floating-point infinity of sort s.
@ -240,7 +240,7 @@ extern "C" {
def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
*/
Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative);
/**
\brief Create a floating-point zero of sort s.
@ -253,7 +253,7 @@ extern "C" {
def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
*/
Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative);
/**
\brief Create an expression of FloatingPoint sort from three bit-vector expressions.
@ -271,7 +271,7 @@ extern "C" {
def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig);
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);
/**
\brief Create a numeral of FloatingPoint sort from a float.
@ -289,7 +289,7 @@ extern "C" {
def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_numeral_float(__in Z3_context c, __in float v, __in Z3_sort ty);
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty);
/**
\brief Create a numeral of FloatingPoint sort from a double.
@ -307,7 +307,7 @@ extern "C" {
def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty);
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty);
/**
\brief Create a numeral of FloatingPoint sort from a signed integer.
@ -322,7 +322,7 @@ extern "C" {
def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_numeral_int(__in Z3_context c, __in signed v, Z3_sort ty);
Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty);
/**
\brief Create a numeral of FloatingPoint sort from a sign bit and two integers.
@ -339,7 +339,7 @@ extern "C" {
def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(__in Z3_context c, __in Z3_bool sgn, __in signed exp, __in unsigned sig, Z3_sort ty);
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, Z3_bool sgn, signed exp, unsigned sig, Z3_sort ty);
/**
\brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
@ -356,7 +356,7 @@ extern "C" {
def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(__in Z3_context c, __in Z3_bool sgn, __in __int64 exp, __in __uint64 sig, Z3_sort ty);
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, __int64 exp, __uint64 sig, Z3_sort ty);
/**
\brief Floating-point absolute value
@ -366,7 +366,7 @@ extern "C" {
def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);
/**
\brief Floating-point negation
@ -376,7 +376,7 @@ extern "C" {
def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_neg(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);
/**
\brief Floating-point addition
@ -390,7 +390,7 @@ extern "C" {
def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_add(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point subtraction
@ -404,7 +404,7 @@ extern "C" {
def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_sub(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point multiplication
@ -418,7 +418,7 @@ extern "C" {
def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_mul(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point division
@ -432,7 +432,7 @@ extern "C" {
def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_div(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point fused multiply-add.
@ -449,7 +449,7 @@ extern "C" {
def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_fma(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3);
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3);
/**
\brief Floating-point square root
@ -462,7 +462,7 @@ extern "C" {
def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_sqrt(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t);
/**
\brief Floating-point remainder
@ -475,7 +475,7 @@ extern "C" {
def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point roundToIntegral. Rounds a floating-point number to
@ -489,7 +489,7 @@ extern "C" {
def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t);
/**
\brief Minimum of floating-point numbers.
@ -502,7 +502,7 @@ extern "C" {
def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Maximum of floating-point numbers.
@ -515,7 +515,7 @@ extern "C" {
def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point less than or equal.
@ -528,7 +528,7 @@ extern "C" {
def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_leq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point less than.
@ -541,7 +541,7 @@ extern "C" {
def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point greater than or equal.
@ -554,7 +554,7 @@ extern "C" {
def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_geq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point greater than.
@ -567,7 +567,7 @@ extern "C" {
def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Floating-point equality.
@ -582,7 +582,7 @@ extern "C" {
def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Predicate indicating whether t is a normal floating-point number.
@ -594,7 +594,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_normal(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a subnormal floating-point number.
@ -606,7 +606,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
@ -618,7 +618,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_zero(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a floating-point number representing +oo or -oo.
@ -630,7 +630,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_infinite(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a NaN.
@ -642,7 +642,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a negative floating-point number.
@ -654,7 +654,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_negative(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a positive floating-point number.
@ -666,7 +666,7 @@ extern "C" {
def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_positive(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);
/**
\brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
@ -684,7 +684,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(__in Z3_context c, __in Z3_ast bv, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s);
/**
\brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
@ -702,7 +702,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
/**
\brief Conversion of a term of real sort into a term of FloatingPoint sort.
@ -720,7 +720,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
/**
\brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
@ -739,7 +739,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
/**
\brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
@ -758,7 +758,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
/**
\brief Conversion of a floating-point term into an unsigned bit-vector.
@ -774,7 +774,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_ubv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);
/**
\brief Conversion of a floating-point term into a signed bit-vector.
@ -790,7 +790,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_sbv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);
/**
\brief Conversion of a floating-point term into a real-numbered term.
@ -804,7 +804,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_real(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t);
/**
@ -820,7 +820,7 @@ extern "C" {
def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
*/
unsigned Z3_API Z3_fpa_get_ebits(__in Z3_context c, __in Z3_sort s);
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s);
/**
\brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
@ -830,7 +830,7 @@ extern "C" {
def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
*/
unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
/**
\brief Retrieves the sign of a floating-point literal.
@ -843,7 +843,7 @@ extern "C" {
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
*/
Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
/**
\brief Return the significand value of a floating-point numeral as a string.
@ -856,7 +856,7 @@ extern "C" {
def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
*/
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t);
/**
\brief Return the significand value of a floating-point numeral as a uint64.
@ -870,7 +870,7 @@ extern "C" {
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(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
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
@ -880,7 +880,7 @@ extern "C" {
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
*/
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t);
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t);
/**
\brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
@ -891,7 +891,7 @@ extern "C" {
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
*/
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n);
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n);
/**
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
@ -908,7 +908,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t);
/**
\brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
@ -927,7 +927,7 @@ extern "C" {
def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast exp, __in Z3_ast sig, __in Z3_sort s);
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s);
/*@}*/

64
src/api/z3_interp.h
View file

@ -43,7 +43,7 @@ extern "C" {
def_API('Z3_mk_interpolant', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a);
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a);
/** \brief This function generates a Z3 context suitable for generation of
@ -62,7 +62,7 @@ extern "C" {
*/
Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg);
/** Compute an interpolant from a refutation. This takes a proof of
"false" from a set of formulas C, and an interpolation
@ -130,7 +130,7 @@ extern "C" {
def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
*/
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p);
/* Compute an interpolant for an unsatisfiable conjunction of formulas.
@ -164,11 +164,11 @@ extern "C" {
def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
*/
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c,
__in Z3_ast pat,
__in Z3_params p,
__out Z3_ast_vector *interp,
__out Z3_model *model);
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
Z3_ast pat,
Z3_params p,
Z3_ast_vector *interp,
Z3_model *model);
/** Return a string summarizing cumulative time used for
interpolation. This string is purely for entertainment purposes
@ -180,7 +180,7 @@ extern "C" {
def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
*/
Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx);
/**
\brief Read an interpolation problem from file.
@ -219,14 +219,14 @@ extern "C" {
*/
int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
__out unsigned *num,
__out Z3_ast *cnsts[],
__out unsigned *parents[],
__in Z3_string filename,
__out_opt Z3_string_ptr error,
__out unsigned *num_theory,
__out Z3_ast *theory[]);
int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
unsigned *num,
Z3_ast *cnsts[],
unsigned *parents[],
Z3_string filename,
Z3_string_ptr error,
unsigned *num_theory,
Z3_ast *theory[]);
@ -250,14 +250,14 @@ extern "C" {
def_API('Z3_check_interpolant', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in_array(1, AST), _out(STRING), _in(UINT), _in_array(6, AST)))
*/
int Z3_API Z3_check_interpolant(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast cnsts[],
__in_ecount(num) unsigned parents[],
__in_ecount(num - 1) Z3_ast *interps,
__out_opt Z3_string_ptr error,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast theory[]);
int Z3_API Z3_check_interpolant(Z3_context ctx,
unsigned num,
Z3_ast cnsts[],
unsigned parents[],
Z3_ast *interps,
Z3_string_ptr error,
unsigned num_theory,
Z3_ast theory[]);
/** Write an interpolation problem to file suitable for reading with
Z3_read_interpolation_problem. The output file is a sequence
@ -275,13 +275,13 @@ extern "C" {
def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST)))
*/
void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx,
__in unsigned num,
__in_ecount(num) Z3_ast cnsts[],
__in_ecount(num) unsigned parents[],
__in Z3_string filename,
__in unsigned num_theory,
__in_ecount(num_theory) Z3_ast theory[]);
void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
unsigned num,
Z3_ast cnsts[],
unsigned parents[],
Z3_string filename,
unsigned num_theory,
Z3_ast theory[]);
/*@}*/
/*@}*/

32
src/api/z3_macros.h
View file

@ -4,38 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
--*/
#ifndef __in
#define __in
#endif
#ifndef __out
#define __out
#endif
#ifndef __out_opt
#define __out_opt __out
#endif
#ifndef __ecount
#define __ecount(num_args)
#endif
#ifndef __in_ecount
#define __in_ecount(num_args) __in __ecount(num_args)
#endif
#ifndef __out_ecount
#define __out_ecount(num_args) __out __ecount(num_args)
#endif
#ifndef __inout_ecount
#define __inout_ecount(num_args) __in __out __ecount(num_args)
#endif
#ifndef __inout
#define __inout __in __out
#endif
#ifndef Z3_bool_opt
#define Z3_bool_opt Z3_bool
#endif

2
src/api/z3_polynomial.h
View file

@ -48,7 +48,7 @@ extern "C" {
def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x);
Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x);
/*@}*/

2
src/api/z3_private.h
View file

@ -34,7 +34,7 @@ extern "C" {
[pointer_default(ref)] interface Z3 {
#endif // CAMLIDL
Z3_bool Z3_API Z3_get_numeral_rational(__in Z3_context c, __in Z3_ast a, rational& r);
Z3_bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r);
#ifndef CAMLIDL
#ifdef __cplusplus

46
src/api/z3_rcf.h
View file

@ -43,42 +43,42 @@ extern "C" {
def_API('Z3_rcf_del', VOID, (_in(CONTEXT), _in(RCF_NUM)))
*/
void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a);
void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a);
/**
\brief Return a RCF rational using the given string.
def_API('Z3_rcf_mk_rational', RCF_NUM, (_in(CONTEXT), _in(STRING)))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val);
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val);
/**
\brief Return a RCF small integer.
def_API('Z3_rcf_mk_small_int', RCF_NUM, (_in(CONTEXT), _in(INT)))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val);
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val);
/**
\brief Return Pi
def_API('Z3_rcf_mk_pi', RCF_NUM, (_in(CONTEXT),))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c);
Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c);
/**
\brief Return e (Euler's constant)
def_API('Z3_rcf_mk_e', RCF_NUM, (_in(CONTEXT),))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c);
Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c);
/**
\brief Return a new infinitesimal that is smaller than all elements in the Z3 field.
def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT),))
*/
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c);
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
/**
\brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
@ -89,112 +89,112 @@ extern "C" {
def_API('Z3_rcf_mk_roots', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, RCF_NUM), _out_array(1, RCF_NUM)))
*/
unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[]);
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
/**
\brief Return the value a + b.
def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a - b.
def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a * b.
def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a / b.
def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value -a
def_API('Z3_rcf_neg', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a);
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a);
/**
\brief Return the value 1/a
def_API('Z3_rcf_inv', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a);
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
/**
\brief Return the value a^k
def_API('Z3_rcf_power', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k);
Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
/**
\brief Return Z3_TRUE if a < b
def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_bool Z3_API Z3_rcf_lt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return Z3_TRUE if a > b
def_API('Z3_rcf_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_bool Z3_API Z3_rcf_gt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return Z3_TRUE if a <= b
def_API('Z3_rcf_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_bool Z3_API Z3_rcf_le(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return Z3_TRUE if a >= b
def_API('Z3_rcf_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return Z3_TRUE if a == b
def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return Z3_TRUE if a != b
def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
Z3_bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Convert the RCF numeral into a string.
def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL)))
*/
Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html);
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact, Z3_bool html);
/**
\brief Convert the RCF numeral into a string in decimal notation.
def_API('Z3_rcf_num_to_decimal_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec);
Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec);
/**
\brief Extract the "numerator" and "denominator" of the given RCF numeral.
@ -202,7 +202,7 @@ extern "C" {
def_API('Z3_rcf_get_numerator_denominator', VOID, (_in(CONTEXT), _in(RCF_NUM), _out(RCF_NUM), _out(RCF_NUM)))
*/
void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d);
void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
/*@}*/
/*@}*/

10
src/ast/ast.cpp
View file

@ -2046,8 +2046,14 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
}
app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
if (decl->get_arity() != num_args && !decl->is_right_associative() &&
!decl->is_left_associative() && !decl->is_chainable()) {
bool type_error =
decl->get_arity() != num_args && !decl->is_right_associative() &&
!decl->is_left_associative() && !decl->is_chainable();
type_error |= (decl->get_arity() != num_args && num_args < 2 &&
decl->get_family_id() == m_basic_family_id && !decl->is_associative());
if (type_error) {
std::ostringstream buffer;
buffer << "Wrong number of arguments (" << num_args
<< ") passed to function " << mk_pp(decl, *this);

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

@ -2975,7 +2975,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz));
shift = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
m_bv_util.mk_numeral(bv_sz, ebits + 2));
shift_neg = m_bv_util.mk_bv_neg(shift);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
@ -2987,8 +2987,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
// sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...]
// [ ... ubv ... ][r][g][ ... s ... ]
expr_ref max_shift(m);
max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
// expr_ref max_shift(m);
// max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
@ -3440,7 +3440,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef Z3DEBUG
return;
// return;
// CMW: This works only for quantifier-free formulas.
expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e));

1
src/ast/fpa_decl_plugin.cpp
View file

@ -629,7 +629,6 @@ func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, par
symbol name("fp.to_sbv");
sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters);
return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,

14
src/cmd_context/basic_cmds.cpp
View file

@ -21,14 +21,12 @@ Notes:
#include"ast_smt2_pp.h"
#include"ast_pp.h"
#include"model_smt2_pp.h"
#include"model_v2_pp.h"
#include"array_decl_plugin.h"
#include"pp.h"
#include"cmd_util.h"
#include"simplify_cmd.h"
#include"eval_cmd.h"
#include"gparams.h"
#include"model_params.hpp"
#include"env_params.h"
class help_cmd : public cmd {
@ -105,17 +103,7 @@ ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat co
throw cmd_exception("model is not available");
model_ref m;
ctx.get_check_sat_result()->get_model(m);
model_params p;
if (p.v1() || p.v2()) {
std::ostringstream buffer;
model_v2_pp(buffer, *m, p.partial());
ctx.regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl;
} else {
ctx.regular_stream() << "(model " << std::endl;
model_smt2_pp(ctx.regular_stream(), ctx, *(m.get()), 2);
// m->display(ctx.regular_stream());
ctx.regular_stream() << ")" << std::endl;
}
ctx.display_model(m);
});
ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {

30
src/cmd_context/cmd_context.cpp
View file

@ -41,6 +41,8 @@ Notes:
#include"scoped_timer.h"
#include"interpolant_cmds.h"
#include"model_smt2_pp.h"
#include"model_v2_pp.h"
#include"model_params.hpp"
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
@ -1409,11 +1411,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
if (get_opt()->print_model()) {
model_ref mdl;
get_opt()->get_model(mdl);
if (mdl) {
regular_stream() << "(model " << std::endl;
model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2);
regular_stream() << ")" << std::endl;
}
display_model(mdl);
}
r = get_opt()->optimize();
}
@ -1456,9 +1454,29 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
}
display_sat_result(r);
validate_check_sat_result(r);
if (r == l_true)
if (r == l_true) {
validate_model();
if (m_params.m_dump_models) {
model_ref md;
get_check_sat_result()->get_model(md);
display_model(md);
}
}
}
void cmd_context::display_model(model_ref& mdl) {
if (mdl) {
model_params p;
if (p.v1() || p.v2()) {
std::ostringstream buffer;
model_v2_pp(buffer, *mdl, p.partial());
regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl;
} else {
regular_stream() << "(model " << std::endl;
model_smt2_pp(regular_stream(), *this, *mdl, 2);
regular_stream() << ")" << std::endl;
}
}
}
void cmd_context::display_sat_result(lbool r) {

1
src/cmd_context/cmd_context.h
View file

@ -325,6 +325,7 @@ public:
check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
check_sat_state cs_state() const;
void validate_model();
void display_model(model_ref& mdl);
void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
bool is_func_decl(symbol const & s) const;

6
src/cmd_context/context_params.cpp
View file

@ -27,6 +27,7 @@ context_params::context_params() {
m_unsat_core = false;
m_model = true;
m_model_validate = false;
m_dump_models = false;
m_auto_config = true;
m_proof = false;
m_trace = false;
@ -79,6 +80,9 @@ void context_params::set(char const * param, char const * value) {
else if (p == "model_validate") {
set_bool(m_model_validate, param, value);
}
else if (p == "dump_models") {
set_bool(m_dump_models, param, value);
}
else if (p == "trace") {
set_bool(m_trace, param, value);
}
@ -116,6 +120,7 @@ void context_params::updt_params(params_ref const & p) {
m_proof = p.get_bool("proof", m_proof);
m_model = p.get_bool("model", m_model);
m_model_validate = p.get_bool("model_validate", m_model_validate);
m_dump_models = p.get_bool("dump_models", m_dump_models);
m_trace = p.get_bool("trace", m_trace);
m_trace_file_name = p.get_str("trace_file_name", "z3.log");
m_unsat_core = p.get_bool("unsat_core", m_unsat_core);
@ -129,6 +134,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "false");
d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");

1
src/cmd_context/context_params.h
View file

@ -36,6 +36,7 @@ public:
bool m_well_sorted_check;
bool m_model;
bool m_model_validate;
bool m_dump_models;
bool m_unsat_core;
bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
unsigned m_timeout;

6
src/muz/transforms/dl_mk_filter_rules.cpp
View file

@ -79,13 +79,13 @@ namespace datalog {
filter_key * key = alloc(filter_key, m);
mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
func_decl * filter_decl = 0;
if (!m_tail2filter.find(key, filter_decl)) {
filter_cache::obj_map_entry *entry = m_tail2filter.insert_if_not_there2(key, 0);
func_decl*& filter_decl = entry->get_data().m_value;
if (!filter_decl) {
filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"),
filter_domain.size(), filter_domain.c_ptr(), pred->get_decl());
m_pinned.push_back(filter_decl);
m_tail2filter.insert(key, filter_decl);
app_ref filter_head(m);
filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
app * filter_tail = key->new_pred;

10
src/smt/smt_relevancy.cpp
View file

@ -148,8 +148,11 @@ namespace smt {
unsigned m_trail_lim;
};
svector<scope> m_scopes;
bool m_propagating;
relevancy_propagator_imp(context & ctx):relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()) {}
relevancy_propagator_imp(context & ctx):
relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()),
m_propagating(false) {}
virtual ~relevancy_propagator_imp() {
undo_trail(0);
@ -448,6 +451,11 @@ namespace smt {
relevant expressions.
*/
virtual void propagate() {
if (m_propagating) {
return;
}
flet<bool> l_prop(m_propagating, true);
ast_manager & m = get_manager();
while (m_qhead < m_relevant_exprs.size()) {
expr * n = m_relevant_exprs.get(m_qhead);

2
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -125,7 +125,7 @@ protected:
m_solver.assert_expr(fml1);
lbool is_sat = m_solver.check();
TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
if (is_sat != l_false) {
if (is_sat == l_true) {
TRACE("ctx_solver_simplify_tactic",
tout << "result is not equivalent to input\n";
tout << mk_pp(fml1, m) << "\n";);

6
src/smt/theory_arith_aux.h
View file

@ -1479,9 +1479,9 @@ namespace smt {
SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
SASSERT(min_gain.is_minus_one() || !min_gain.is_neg());
SASSERT(!is_int(x_i) || min_gain.is_pos());
SASSERT(!is_int(x_i) || min_gain.is_int());
SASSERT(!is_int(x_i) || max_gain.is_int());
//SASSERT(!is_int(x_i) || min_gain.is_pos());
//SASSERT(!is_int(x_i) || min_gain.is_int());
//SASSERT(!is_int(x_i) || max_gain.is_int());
return is_tighter;
}

4
src/smt/theory_arith_core.h
View file

@ -3065,6 +3065,10 @@ namespace smt {
SASSERT(v != null_theory_var);
inf_numeral const & val = get_value(v);
rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
if (is_int(v) && !num.is_int()) {
TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
num = floor(num);
}
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
}

12
src/util/util.h
View file

@ -273,18 +273,6 @@ bool has_duplicates(const IT & begin, const IT & end) {
return false;
}
#ifndef __out
#define __out
#endif
#ifndef __in
#define __in
#endif
#ifndef __inout
#define __inout
#endif
#ifndef __fallthrough
#define __fallthrough
#endif