Skip to content

Commit df816ca

Browse files
CopilotNikolajBjorner
Copilot
and
NikolajBjorner
authored
Add finite set API support for C# and Java bindings (#8003)
* Initial plan * Add finite set API support for Java and C# Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add documentation and examples for finite set APIs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Delete FINITE_SET_API_EXAMPLES.md * Add FiniteSetSort files to CMakeLists.txt build configurations Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
1 parent 5b92f8f commit df816ca

File tree

6 files changed

+410
-0
lines changed

6 files changed

+410
-0
lines changed

‎src/api/dotnet/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
6464
FiniteDomainExpr.cs
6565
FiniteDomainNum.cs
6666
FiniteDomainSort.cs
67+
FiniteSetSort.cs
6768
Fixedpoint.cs
6869
FPExpr.cs
6970
FPNum.cs

‎src/api/dotnet/Context.cs‎

Lines changed: 174 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2442,6 +2442,180 @@ public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
24422442

24432443
#endregion
24442444

2445+
#region Finite Sets
2446+
2447+
/// <summary>
2448+
/// Create a finite set sort over the given element sort.
2449+
/// </summary>
2450+
public FiniteSetSort MkFiniteSetSort(Sort elemSort)
2451+
{
2452+
Debug.Assert(elemSort != null);
2453+
2454+
CheckContextMatch(elemSort);
2455+
return new FiniteSetSort(this, elemSort);
2456+
}
2457+
2458+
/// <summary>
2459+
/// Check if a sort is a finite set sort.
2460+
/// </summary>
2461+
public bool IsFiniteSetSort(Sort s)
2462+
{
2463+
Debug.Assert(s != null);
2464+
2465+
CheckContextMatch(s);
2466+
return Native.Z3_is_finite_set_sort(nCtx, s.NativeObject) != 0;
2467+
}
2468+
2469+
/// <summary>
2470+
/// Get the element sort (basis) of a finite set sort.
2471+
/// </summary>
2472+
public Sort GetFiniteSetSortBasis(Sort s)
2473+
{
2474+
Debug.Assert(s != null);
2475+
2476+
CheckContextMatch(s);
2477+
return Sort.Create(this, Native.Z3_get_finite_set_sort_basis(nCtx, s.NativeObject));
2478+
}
2479+
2480+
/// <summary>
2481+
/// Create an empty finite set.
2482+
/// </summary>
2483+
public Expr MkFiniteSetEmpty(Sort setSort)
2484+
{
2485+
Debug.Assert(setSort != null);
2486+
2487+
CheckContextMatch(setSort);
2488+
return Expr.Create(this, Native.Z3_mk_finite_set_empty(nCtx, setSort.NativeObject));
2489+
}
2490+
2491+
/// <summary>
2492+
/// Create a singleton finite set.
2493+
/// </summary>
2494+
public Expr MkFiniteSetSingleton(Expr elem)
2495+
{
2496+
Debug.Assert(elem != null);
2497+
2498+
CheckContextMatch(elem);
2499+
return Expr.Create(this, Native.Z3_mk_finite_set_singleton(nCtx, elem.NativeObject));
2500+
}
2501+
2502+
/// <summary>
2503+
/// Create the union of two finite sets.
2504+
/// </summary>
2505+
public Expr MkFiniteSetUnion(Expr s1, Expr s2)
2506+
{
2507+
Debug.Assert(s1 != null);
2508+
Debug.Assert(s2 != null);
2509+
2510+
CheckContextMatch(s1);
2511+
CheckContextMatch(s2);
2512+
return Expr.Create(this, Native.Z3_mk_finite_set_union(nCtx, s1.NativeObject, s2.NativeObject));
2513+
}
2514+
2515+
/// <summary>
2516+
/// Create the intersection of two finite sets.
2517+
/// </summary>
2518+
public Expr MkFiniteSetIntersect(Expr s1, Expr s2)
2519+
{
2520+
Debug.Assert(s1 != null);
2521+
Debug.Assert(s2 != null);
2522+
2523+
CheckContextMatch(s1);
2524+
CheckContextMatch(s2);
2525+
return Expr.Create(this, Native.Z3_mk_finite_set_intersect(nCtx, s1.NativeObject, s2.NativeObject));
2526+
}
2527+
2528+
/// <summary>
2529+
/// Create the difference of two finite sets.
2530+
/// </summary>
2531+
public Expr MkFiniteSetDifference(Expr s1, Expr s2)
2532+
{
2533+
Debug.Assert(s1 != null);
2534+
Debug.Assert(s2 != null);
2535+
2536+
CheckContextMatch(s1);
2537+
CheckContextMatch(s2);
2538+
return Expr.Create(this, Native.Z3_mk_finite_set_difference(nCtx, s1.NativeObject, s2.NativeObject));
2539+
}
2540+
2541+
/// <summary>
2542+
/// Check for membership in a finite set.
2543+
/// </summary>
2544+
public BoolExpr MkFiniteSetMember(Expr elem, Expr set)
2545+
{
2546+
Debug.Assert(elem != null);
2547+
Debug.Assert(set != null);
2548+
2549+
CheckContextMatch(elem);
2550+
CheckContextMatch(set);
2551+
return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_member(nCtx, elem.NativeObject, set.NativeObject));
2552+
}
2553+
2554+
/// <summary>
2555+
/// Get the cardinality of a finite set.
2556+
/// </summary>
2557+
public Expr MkFiniteSetSize(Expr set)
2558+
{
2559+
Debug.Assert(set != null);
2560+
2561+
CheckContextMatch(set);
2562+
return Expr.Create(this, Native.Z3_mk_finite_set_size(nCtx, set.NativeObject));
2563+
}
2564+
2565+
/// <summary>
2566+
/// Check if one finite set is a subset of another.
2567+
/// </summary>
2568+
public BoolExpr MkFiniteSetSubset(Expr s1, Expr s2)
2569+
{
2570+
Debug.Assert(s1 != null);
2571+
Debug.Assert(s2 != null);
2572+
2573+
CheckContextMatch(s1);
2574+
CheckContextMatch(s2);
2575+
return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_subset(nCtx, s1.NativeObject, s2.NativeObject));
2576+
}
2577+
2578+
/// <summary>
2579+
/// Map a function over all elements in a finite set.
2580+
/// </summary>
2581+
public Expr MkFiniteSetMap(Expr f, Expr set)
2582+
{
2583+
Debug.Assert(f != null);
2584+
Debug.Assert(set != null);
2585+
2586+
CheckContextMatch(f);
2587+
CheckContextMatch(set);
2588+
return Expr.Create(this, Native.Z3_mk_finite_set_map(nCtx, f.NativeObject, set.NativeObject));
2589+
}
2590+
2591+
/// <summary>
2592+
/// Filter a finite set with a predicate.
2593+
/// </summary>
2594+
public Expr MkFiniteSetFilter(Expr f, Expr set)
2595+
{
2596+
Debug.Assert(f != null);
2597+
Debug.Assert(set != null);
2598+
2599+
CheckContextMatch(f);
2600+
CheckContextMatch(set);
2601+
return Expr.Create(this, Native.Z3_mk_finite_set_filter(nCtx, f.NativeObject, set.NativeObject));
2602+
}
2603+
2604+
/// <summary>
2605+
/// Create a finite set containing integers in the range [low, high].
2606+
/// </summary>
2607+
public Expr MkFiniteSetRange(Expr low, Expr high)
2608+
{
2609+
Debug.Assert(low != null);
2610+
Debug.Assert(high != null);
2611+
2612+
CheckContextMatch(low);
2613+
CheckContextMatch(high);
2614+
return Expr.Create(this, Native.Z3_mk_finite_set_range(nCtx, low.NativeObject, high.NativeObject));
2615+
}
2616+
2617+
#endregion
2618+
24452619
#region Sequence, string and regular expressions
24462620

24472621
/// <summary>

‎src/api/dotnet/FiniteSetSort.cs‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/*++
2+
Copyright (c) 2024 Microsoft Corporation
3+
4+
Module Name:
5+
6+
FiniteSetSort.cs
7+
8+
Abstract:
9+
10+
Z3 Managed API: Finite Set Sorts
11+
12+
Author:
13+
14+
GitHub Copilot
15+
16+
Notes:
17+
18+
--*/
19+
20+
using System.Diagnostics;
21+
using System;
22+
23+
namespace Microsoft.Z3
24+
{
25+
/// <summary>
26+
/// Finite set sorts.
27+
/// </summary>
28+
public class FiniteSetSort : Sort
29+
{
30+
#region Internal
31+
internal FiniteSetSort(Context ctx, IntPtr obj)
32+
: base(ctx, obj)
33+
{
34+
Debug.Assert(ctx != null);
35+
}
36+
37+
internal FiniteSetSort(Context ctx, Sort elemSort)
38+
: base(ctx, Native.Z3_mk_finite_set_sort(ctx.nCtx, elemSort.NativeObject))
39+
{
40+
Debug.Assert(ctx != null);
41+
Debug.Assert(elemSort != null);
42+
}
43+
#endregion
44+
45+
/// <summary>
46+
/// Get the element sort (basis) of this finite set sort.
47+
/// </summary>
48+
public Sort Basis
49+
{
50+
get { return Sort.Create(Context, Native.Z3_get_finite_set_sort_basis(Context.nCtx, NativeObject)); }
51+
}
52+
}
53+
}

‎src/api/java/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
115115
FiniteDomainExpr.java
116116
FiniteDomainNum.java
117117
FiniteDomainSort.java
118+
FiniteSetSort.java
118119
Fixedpoint.java
119120
FPExpr.java
120121
FPNum.java

‎src/api/java/Context.java‎

Lines changed: 139 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2052,6 +2052,145 @@ public final <D extends Sort> BoolExpr mkSetSubset(Expr<ArraySort<D, BoolSort>>
20522052
}
20532053

20542054

2055+
/**
2056+
* Finite Sets
2057+
*/
2058+
2059+
/**
2060+
* Create a finite set sort over the given element sort.
2061+
**/
2062+
public final FiniteSetSort mkFiniteSetSort(Sort elemSort)
2063+
{
2064+
checkContextMatch(elemSort);
2065+
return new FiniteSetSort(this, elemSort);
2066+
}
2067+
2068+
/**
2069+
* Check if a sort is a finite set sort.
2070+
**/
2071+
public final boolean isFiniteSetSort(Sort s)
2072+
{
2073+
checkContextMatch(s);
2074+
return Native.isFiniteSetSort(nCtx(), s.getNativeObject());
2075+
}
2076+
2077+
/**
2078+
* Get the element sort (basis) of a finite set sort.
2079+
**/
2080+
public final Sort getFiniteSetSortBasis(Sort s)
2081+
{
2082+
checkContextMatch(s);
2083+
return Sort.create(this, Native.getFiniteSetSortBasis(nCtx(), s.getNativeObject()));
2084+
}
2085+
2086+
/**
2087+
* Create an empty finite set.
2088+
**/
2089+
public final Expr mkFiniteSetEmpty(Sort setSort)
2090+
{
2091+
checkContextMatch(setSort);
2092+
return Expr.create(this, Native.mkFiniteSetEmpty(nCtx(), setSort.getNativeObject()));
2093+
}
2094+
2095+
/**
2096+
* Create a singleton finite set.
2097+
**/
2098+
public final Expr mkFiniteSetSingleton(Expr elem)
2099+
{
2100+
checkContextMatch(elem);
2101+
return Expr.create(this, Native.mkFiniteSetSingleton(nCtx(), elem.getNativeObject()));
2102+
}
2103+
2104+
/**
2105+
* Create the union of two finite sets.
2106+
**/
2107+
public final Expr mkFiniteSetUnion(Expr s1, Expr s2)
2108+
{
2109+
checkContextMatch(s1);
2110+
checkContextMatch(s2);
2111+
return Expr.create(this, Native.mkFiniteSetUnion(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2112+
}
2113+
2114+
/**
2115+
* Create the intersection of two finite sets.
2116+
**/
2117+
public final Expr mkFiniteSetIntersect(Expr s1, Expr s2)
2118+
{
2119+
checkContextMatch(s1);
2120+
checkContextMatch(s2);
2121+
return Expr.create(this, Native.mkFiniteSetIntersect(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2122+
}
2123+
2124+
/**
2125+
* Create the difference of two finite sets.
2126+
**/
2127+
public final Expr mkFiniteSetDifference(Expr s1, Expr s2)
2128+
{
2129+
checkContextMatch(s1);
2130+
checkContextMatch(s2);
2131+
return Expr.create(this, Native.mkFiniteSetDifference(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2132+
}
2133+
2134+
/**
2135+
* Check for membership in a finite set.
2136+
**/
2137+
public final BoolExpr mkFiniteSetMember(Expr elem, Expr set)
2138+
{
2139+
checkContextMatch(elem);
2140+
checkContextMatch(set);
2141+
return (BoolExpr) Expr.create(this, Native.mkFiniteSetMember(nCtx(), elem.getNativeObject(), set.getNativeObject()));
2142+
}
2143+
2144+
/**
2145+
* Get the cardinality of a finite set.
2146+
**/
2147+
public final Expr mkFiniteSetSize(Expr set)
2148+
{
2149+
checkContextMatch(set);
2150+
return Expr.create(this, Native.mkFiniteSetSize(nCtx(), set.getNativeObject()));
2151+
}
2152+
2153+
/**
2154+
* Check if one finite set is a subset of another.
2155+
**/
2156+
public final BoolExpr mkFiniteSetSubset(Expr s1, Expr s2)
2157+
{
2158+
checkContextMatch(s1);
2159+
checkContextMatch(s2);
2160+
return (BoolExpr) Expr.create(this, Native.mkFiniteSetSubset(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2161+
}
2162+
2163+
/**
2164+
* Map a function over all elements in a finite set.
2165+
**/
2166+
public final Expr mkFiniteSetMap(Expr f, Expr set)
2167+
{
2168+
checkContextMatch(f);
2169+
checkContextMatch(set);
2170+
return Expr.create(this, Native.mkFiniteSetMap(nCtx(), f.getNativeObject(), set.getNativeObject()));
2171+
}
2172+
2173+
/**
2174+
* Filter a finite set with a predicate.
2175+
**/
2176+
public final Expr mkFiniteSetFilter(Expr f, Expr set)
2177+
{
2178+
checkContextMatch(f);
2179+
checkContextMatch(set);
2180+
return Expr.create(this, Native.mkFiniteSetFilter(nCtx(), f.getNativeObject(), set.getNativeObject()));
2181+
}
2182+
2183+
/**
2184+
* Create a finite set containing integers in the range [low, high].
2185+
**/
2186+
public final Expr mkFiniteSetRange(Expr low, Expr high)
2187+
{
2188+
checkContextMatch(low);
2189+
checkContextMatch(high);
2190+
return Expr.create(this, Native.mkFiniteSetRange(nCtx(), low.getNativeObject(), high.getNativeObject()));
2191+
}
2192+
2193+
20552194
/**
20562195
* Sequences, Strings and regular expressions.
20572196
*/

0 commit comments

Comments
 (0)