From 5f755a5bd8c2e88f4635b77cec352c1dcd114662 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Jul 2015 13:07:16 -0700 Subject: [PATCH] Adjusted return types of set functions to ArrayExprs in Java and .NET Fixes #137 --- src/api/dotnet/Context.cs | 36 +++++++++++++++--------------- src/api/java/Context.java | 47 +++++++++++++++++---------------------- 2 files changed, 38 insertions(+), 45 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index eaf4e4777..0aee3f7d8 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2134,31 +2134,31 @@ namespace Microsoft.Z3 /// /// Create an empty set. /// - public Expr MkEmptySet(Sort domain) + public ArrayExpr MkEmptySet(Sort domain) { Contract.Requires(domain != null); Contract.Ensures(Contract.Result() != 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)); } /// /// Create the full set. /// - public Expr MkFullSet(Sort domain) + public ArrayExpr MkFullSet(Sort domain) { Contract.Requires(domain != null); Contract.Ensures(Contract.Result() != 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)); } /// /// Add an element to the set. /// - 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)); } /// /// Remove an element from a set. /// - 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)); } /// /// Take the union of a list of sets. /// - 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))); } /// /// Take the intersection of a list of sets. /// - 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() != 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))); } /// /// Take the difference between two sets. /// - 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)); } /// /// Take the complement of a set. /// - public Expr MkSetComplement(Expr arg) + public ArrayExpr MkSetComplement(ArrayExpr arg) { Contract.Requires(arg != null); Contract.Ensures(Contract.Result() != 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)); } /// /// Check for set membership. /// - 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 /// /// Check for subsetness of sets. /// - public BoolExpr MkSetSubset(Expr arg1, Expr arg2) + public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2) { Contract.Requires(arg1 != null); Contract.Requires(arg2 != null); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index b2d77e792..bec5da024 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -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())); }