mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Adjusted return types of set functions to ArrayExprs in Java and .NET

Browse source 
Fixes #137
This commit is contained in:
Christoph M. Wintersteiger 2015-07-14 13:07:16 -07:00
parent 31eb738db5
commit 5f755a5bd8
2 changed files with 38 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2134,31 +2134,31 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create an empty set. /// Create an empty set.
/// </summary> /// </summary>
public Expr MkEmptySet(Sort domain) public ArrayExpr MkEmptySet(Sort domain)
{ {
Contract.Requires(domain != null); Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain); 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> /// <summary>
/// Create the full set. /// Create the full set.
/// </summary> /// </summary>
public Expr MkFullSet(Sort domain) public ArrayExpr MkFullSet(Sort domain)
{ {
Contract.Requires(domain != null); Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain); 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> /// <summary>
/// Add an element to the set. /// Add an element to the set.
/// </summary> /// </summary>
public Expr MkSetAdd(Expr set, Expr element) public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
{ {
Contract.Requires(set != null); Contract.Requires(set != null);
Contract.Requires(element != null); Contract.Requires(element != null);
@ -2166,14 +2166,14 @@ namespace Microsoft.Z3
CheckContextMatch(set); CheckContextMatch(set);
CheckContextMatch(element); 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> /// <summary>
/// Remove an element from a set. /// Remove an element from a set.
/// </summary> /// </summary>
public Expr MkSetDel(Expr set, Expr element) public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
{ {
Contract.Requires(set != null); Contract.Requires(set != null);
Contract.Requires(element != null); Contract.Requires(element != null);
@ -2181,38 +2181,38 @@ namespace Microsoft.Z3
CheckContextMatch(set); CheckContextMatch(set);
CheckContextMatch(element); 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> /// <summary>
/// Take the union of a list of sets. /// Take the union of a list of sets.
/// </summary> /// </summary>
public Expr MkSetUnion(params Expr[] args) public ArrayExpr MkSetUnion(params ArrayExpr[] args)
{ {
Contract.Requires(args != null); Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Requires(Contract.ForAll(args, a => a != null));
CheckContextMatch(args); 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> /// <summary>
/// Take the intersection of a list of sets. /// Take the intersection of a list of sets.
/// </summary> /// </summary>
public Expr MkSetIntersection(params Expr[] args) public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
{ {
Contract.Requires(args != null); Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Requires(Contract.ForAll(args, a => a != null));
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(args); 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> /// <summary>
/// Take the difference between two sets. /// Take the difference between two sets.
/// </summary> /// </summary>
public Expr MkSetDifference(Expr arg1, Expr arg2) public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
{ {
Contract.Requires(arg1 != null); Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null); Contract.Requires(arg2 != null);
@ -2220,25 +2220,25 @@ namespace Microsoft.Z3
CheckContextMatch(arg1); CheckContextMatch(arg1);
CheckContextMatch(arg2); 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> /// <summary>
/// Take the complement of a set. /// Take the complement of a set.
/// </summary> /// </summary>
public Expr MkSetComplement(Expr arg) public ArrayExpr MkSetComplement(ArrayExpr arg)
{ {
Contract.Requires(arg != null); Contract.Requires(arg != null);
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(arg); 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> /// <summary>
/// Check for set membership. /// Check for set membership.
/// </summary> /// </summary>
public BoolExpr MkSetMembership(Expr elem, Expr set) public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
{ {
Contract.Requires(elem != null); Contract.Requires(elem != null);
Contract.Requires(set != null); Contract.Requires(set != null);
@ -2252,7 +2252,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Check for subsetness of sets. /// Check for subsetness of sets.
/// </summary> /// </summary>
public BoolExpr MkSetSubset(Expr arg1, Expr arg2) public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
{ {
Contract.Requires(arg1 != null); Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null); Contract.Requires(arg2 != null);

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

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