diff --git a/src/api/go/char.go b/src/api/go/char.go new file mode 100644 index 000000000..846101f96 --- /dev/null +++ b/src/api/go/char.go @@ -0,0 +1,43 @@ +package z3 + +/* +#include "z3.h" +*/ +import "C" + +// Char operations + +// MkCharSort creates the character sort (Unicode characters). +func (c *Context) MkCharSort() *Sort { + return newSort(c, C.Z3_mk_char_sort(c.ptr)) +} + +// MkChar creates a character literal from a Unicode code point. +func (c *Context) MkChar(ch uint) *Expr { + return newExpr(c, C.Z3_mk_char(c.ptr, C.uint(ch))) +} + +// MkCharLe creates a character less-than-or-equal predicate (ch1 ≤ ch2). +func (c *Context) MkCharLe(ch1, ch2 *Expr) *Expr { + return newExpr(c, C.Z3_mk_char_le(c.ptr, ch1.ptr, ch2.ptr)) +} + +// MkCharToInt converts a character to its integer (Unicode code point) value. +func (c *Context) MkCharToInt(ch *Expr) *Expr { + return newExpr(c, C.Z3_mk_char_to_int(c.ptr, ch.ptr)) +} + +// MkCharToBV converts a character to a bit-vector. +func (c *Context) MkCharToBV(ch *Expr) *Expr { + return newExpr(c, C.Z3_mk_char_to_bv(c.ptr, ch.ptr)) +} + +// MkCharFromBV converts a bit-vector to a character. +func (c *Context) MkCharFromBV(bv *Expr) *Expr { + return newExpr(c, C.Z3_mk_char_from_bv(c.ptr, bv.ptr)) +} + +// MkCharIsDigit creates a predicate that is true if the character is a decimal digit. +func (c *Context) MkCharIsDigit(ch *Expr) *Expr { + return newExpr(c, C.Z3_mk_char_is_digit(c.ptr, ch.ptr)) +} diff --git a/src/api/go/relations.go b/src/api/go/relations.go new file mode 100644 index 000000000..637c6ab5b --- /dev/null +++ b/src/api/go/relations.go @@ -0,0 +1,38 @@ +package z3 + +/* +#include "z3.h" +*/ +import "C" + +// Special relation constructors + +// MkLinearOrder creates a linear (total) order relation over the given sort. +// The id parameter distinguishes multiple linear orders over the same sort. +func (c *Context) MkLinearOrder(s *Sort, id uint) *FuncDecl { + return newFuncDecl(c, C.Z3_mk_linear_order(c.ptr, s.ptr, C.uint(id))) +} + +// MkPartialOrder creates a partial order relation over the given sort. +// The id parameter distinguishes multiple partial orders over the same sort. +func (c *Context) MkPartialOrder(s *Sort, id uint) *FuncDecl { + return newFuncDecl(c, C.Z3_mk_partial_order(c.ptr, s.ptr, C.uint(id))) +} + +// MkPiecewiseLinearOrder creates a piecewise linear order relation over the given sort. +// The id parameter distinguishes multiple piecewise linear orders over the same sort. +func (c *Context) MkPiecewiseLinearOrder(s *Sort, id uint) *FuncDecl { + return newFuncDecl(c, C.Z3_mk_piecewise_linear_order(c.ptr, s.ptr, C.uint(id))) +} + +// MkTreeOrder creates a tree order relation over the given sort. +// The id parameter distinguishes multiple tree orders over the same sort. +func (c *Context) MkTreeOrder(s *Sort, id uint) *FuncDecl { + return newFuncDecl(c, C.Z3_mk_tree_order(c.ptr, s.ptr, C.uint(id))) +} + +// MkTransitiveClosure creates the transitive closure of a binary relation. +// The resulting relation is recursive. +func (c *Context) MkTransitiveClosure(f *FuncDecl) *FuncDecl { + return newFuncDecl(c, C.Z3_mk_transitive_closure(c.ptr, f.ptr)) +} diff --git a/src/api/go/set.go b/src/api/go/set.go new file mode 100644 index 000000000..53b1be672 --- /dev/null +++ b/src/api/go/set.go @@ -0,0 +1,77 @@ +package z3 + +/* +#include "z3.h" +*/ +import "C" + +// Regular (array-encoded) Set operations + +// MkSetSort creates a set sort with the given element sort. +func (c *Context) MkSetSort(elemSort *Sort) *Sort { + return newSort(c, C.Z3_mk_set_sort(c.ptr, elemSort.ptr)) +} + +// MkEmptySet creates an empty set of the given element sort. +func (c *Context) MkEmptySet(elemSort *Sort) *Expr { + return newExpr(c, C.Z3_mk_empty_set(c.ptr, elemSort.ptr)) +} + +// MkFullSet creates the full set (universe) of the given element sort. +func (c *Context) MkFullSet(elemSort *Sort) *Expr { + return newExpr(c, C.Z3_mk_full_set(c.ptr, elemSort.ptr)) +} + +// MkSetAdd adds an element to a set. +func (c *Context) MkSetAdd(set, elem *Expr) *Expr { + return newExpr(c, C.Z3_mk_set_add(c.ptr, set.ptr, elem.ptr)) +} + +// MkSetDel removes an element from a set. +func (c *Context) MkSetDel(set, elem *Expr) *Expr { + return newExpr(c, C.Z3_mk_set_del(c.ptr, set.ptr, elem.ptr)) +} + +// MkSetUnion creates the union of two or more sets. +func (c *Context) MkSetUnion(sets ...*Expr) *Expr { + if len(sets) == 0 { + return nil + } + cSets := make([]C.Z3_ast, len(sets)) + for i, s := range sets { + cSets[i] = s.ptr + } + return newExpr(c, C.Z3_mk_set_union(c.ptr, C.uint(len(sets)), &cSets[0])) +} + +// MkSetIntersect creates the intersection of two or more sets. +func (c *Context) MkSetIntersect(sets ...*Expr) *Expr { + if len(sets) == 0 { + return nil + } + cSets := make([]C.Z3_ast, len(sets)) + for i, s := range sets { + cSets[i] = s.ptr + } + return newExpr(c, C.Z3_mk_set_intersect(c.ptr, C.uint(len(sets)), &cSets[0])) +} + +// MkSetDifference creates the set difference (set1 \ set2). +func (c *Context) MkSetDifference(set1, set2 *Expr) *Expr { + return newExpr(c, C.Z3_mk_set_difference(c.ptr, set1.ptr, set2.ptr)) +} + +// MkSetComplement creates the complement of a set. +func (c *Context) MkSetComplement(set *Expr) *Expr { + return newExpr(c, C.Z3_mk_set_complement(c.ptr, set.ptr)) +} + +// MkSetMember creates a membership predicate: elem ∈ set. +func (c *Context) MkSetMember(elem, set *Expr) *Expr { + return newExpr(c, C.Z3_mk_set_member(c.ptr, elem.ptr, set.ptr)) +} + +// MkSetSubset creates a subset predicate: set1 ⊆ set2. +func (c *Context) MkSetSubset(set1, set2 *Expr) *Expr { + return newExpr(c, C.Z3_mk_set_subset(c.ptr, set1.ptr, set2.ptr)) +} diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 22887729c..d02f4f287 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -4616,6 +4616,38 @@ public class Context implements AutoCloseable { ); } + /** + * Creates a piecewise linear order. + * @param index The index of the order. + * @param sort The sort of the order. + */ + public final FuncDecl mkPiecewiseLinearOrder(R sort, int index) { + return (FuncDecl) FuncDecl.create( + this, + Native.mkPiecewiseLinearOrder( + nCtx(), + sort.getNativeObject(), + index + ) + ); + } + + /** + * Creates a tree order. + * @param index The index of the order. + * @param sort The sort of the order. + */ + public final FuncDecl mkTreeOrder(R sort, int index) { + return (FuncDecl) FuncDecl.create( + this, + Native.mkTreeOrder( + nCtx(), + sort.getNativeObject(), + index + ) + ); + } + /** * Return the nonzero subresultants of p and q with respect to the "variable" x. * Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable. diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 8f9fc4ff1..f336fe30b 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -1957,10 +1957,46 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { return new FuncDeclImpl(check(Z3.mk_partial_order(contextPtr, sort.ptr, index))); } + function mkLinearOrder(sort: Sort, index: number): FuncDecl { + return new FuncDeclImpl(check(Z3.mk_linear_order(contextPtr, sort.ptr, index))); + } + + function mkPiecewiseLinearOrder(sort: Sort, index: number): FuncDecl { + return new FuncDeclImpl(check(Z3.mk_piecewise_linear_order(contextPtr, sort.ptr, index))); + } + + function mkTreeOrder(sort: Sort, index: number): FuncDecl { + return new FuncDeclImpl(check(Z3.mk_tree_order(contextPtr, sort.ptr, index))); + } + function mkTransitiveClosure(f: FuncDecl): FuncDecl { return new FuncDeclImpl(check(Z3.mk_transitive_closure(contextPtr, f.ptr))); } + function mkChar(ch: number): Expr { + return new ExprImpl(check(Z3.mk_char(contextPtr, ch))); + } + + function mkCharLe(ch1: Expr, ch2: Expr): Bool { + return new BoolImpl(check(Z3.mk_char_le(contextPtr, ch1.ast, ch2.ast))); + } + + function mkCharToInt(ch: Expr): Arith { + return new ArithImpl(check(Z3.mk_char_to_int(contextPtr, ch.ast))); + } + + function mkCharToBV(ch: Expr): Expr { + return new ExprImpl(check(Z3.mk_char_to_bv(contextPtr, ch.ast))); + } + + function mkCharFromBV(bv: Expr): Expr { + return new ExprImpl(check(Z3.mk_char_from_bv(contextPtr, bv.ast))); + } + + function mkCharIsDigit(ch: Expr): Bool { + return new BoolImpl(check(Z3.mk_char_is_digit(contextPtr, ch.ast))); + } + async function polynomialSubresultants( p: Arith, q: Arith, @@ -5490,7 +5526,16 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { Full, mkPartialOrder, + mkLinearOrder, + mkPiecewiseLinearOrder, + mkTreeOrder, mkTransitiveClosure, + mkChar, + mkCharLe, + mkCharToInt, + mkCharToBV, + mkCharFromBV, + mkCharIsDigit, polynomialSubresultants, }; cleanup.register(ctx, () => Z3.del_context(contextPtr)); diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index fcdba0aa4..6eef81044 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -933,6 +933,30 @@ export interface Context { */ mkPartialOrder(sort: Sort, index: number): FuncDecl; + /** + * Create a linear (total) order relation over a sort. + * @param sort The sort of the relation + * @param index The index of the relation + * @category Operations + */ + mkLinearOrder(sort: Sort, index: number): FuncDecl; + + /** + * Create a piecewise linear order relation over a sort. + * @param sort The sort of the relation + * @param index The index of the relation + * @category Operations + */ + mkPiecewiseLinearOrder(sort: Sort, index: number): FuncDecl; + + /** + * Create a tree order relation over a sort. + * @param sort The sort of the relation + * @param index The index of the relation + * @category Operations + */ + mkTreeOrder(sort: Sort, index: number): FuncDecl; + /** * Create the transitive closure of a binary relation. * The resulting relation is recursive. @@ -941,6 +965,49 @@ export interface Context { */ mkTransitiveClosure(f: FuncDecl): FuncDecl; + /** + * Create a character literal from a Unicode code point. + * @param ch The Unicode code point + * @category Characters + */ + mkChar(ch: number): Expr; + + /** + * Create a character less-than-or-equal predicate (ch1 ≤ ch2). + * @param ch1 First character + * @param ch2 Second character + * @category Characters + */ + mkCharLe(ch1: Expr, ch2: Expr): Bool; + + /** + * Convert a character to its integer (Unicode code point) value. + * @param ch The character expression + * @category Characters + */ + mkCharToInt(ch: Expr): Arith; + + /** + * Convert a character to a bit-vector. + * @param ch The character expression + * @category Characters + */ + mkCharToBV(ch: Expr): Expr; + + /** + * Convert a bit-vector to a character. + * @param bv The bit-vector expression + * @category Characters + */ + mkCharFromBV(bv: Expr): Expr; + + /** + * Create a predicate that is true if the character is a decimal digit. + * @param ch The character expression + * @category Characters + */ + mkCharIsDigit(ch: Expr): Bool; + /** * Return the nonzero subresultants of p and q with respect to the "variable" x. * Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable. diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp index ec3efa86b..3df98ac01 100644 --- a/src/api/julia/z3jl.cpp +++ b/src/api/julia/z3jl.cpp @@ -320,6 +320,20 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) m.method("finite_set_map", &finite_set_map); m.method("finite_set_filter", &finite_set_filter); m.method("finite_set_range", &finite_set_range); + m.method("empty_set", &empty_set); + m.method("full_set", &full_set); + m.method("set_add", &set_add); + m.method("set_del", &set_del); + m.method("set_union", &set_union); + m.method("set_intersect", &set_intersect); + m.method("set_difference", &set_difference); + m.method("set_complement", &set_complement); + m.method("set_member", &set_member); + m.method("set_subset", &set_subset); + m.method("linear_order", &linear_order); + m.method("partial_order", &partial_order); + m.method("piecewise_linear_order", &piecewise_linear_order); + m.method("tree_order", &tree_order); // ------------------------------------------------------------------------- @@ -629,7 +643,13 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(context, string_sort) .MM(context, seq_sort) .MM(context, re_sort) + .MM(context, char_sort) .MM(context, finite_set_sort) + .method("set_sort", [](context &c, sort s) { + Z3_sort r = Z3_mk_set_sort(c, s); + c.check_error(); + return sort(c, r); + }) .method("array_sort", static_cast(&context::array_sort)) .method("array_sort", static_cast(&context::array_sort)) .method("fpa_sort", static_cast(&context::fpa_sort)) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 261bc2f3c..55adc362c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1350,6 +1350,15 @@ struct let mk_range = Z3native.mk_finite_set_range end +module SpecialRelation = +struct + let mk_linear_order = Z3native.mk_linear_order + let mk_partial_order = Z3native.mk_partial_order + let mk_piecewise_linear_order = Z3native.mk_piecewise_linear_order + let mk_tree_order = Z3native.mk_tree_order + let mk_transitive_closure = Z3native.mk_transitive_closure +end + module FloatingPoint = struct module RoundingMode = diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 90f731901..572659030 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2140,6 +2140,31 @@ sig end +(** Special relation constructors *) +module SpecialRelation : +sig + (** Create a linear (total) order relation over the given sort. + The [id] parameter distinguishes multiple linear orders over the same sort. *) + val mk_linear_order : context -> Sort.sort -> int -> FuncDecl.func_decl + + (** Create a partial order relation over the given sort. + The [id] parameter distinguishes multiple partial orders over the same sort. *) + val mk_partial_order : context -> Sort.sort -> int -> FuncDecl.func_decl + + (** Create a piecewise linear order relation over the given sort. + The [id] parameter distinguishes multiple piecewise linear orders over the same sort. *) + val mk_piecewise_linear_order : context -> Sort.sort -> int -> FuncDecl.func_decl + + (** Create a tree order relation over the given sort. + The [id] parameter distinguishes multiple tree orders over the same sort. *) + val mk_tree_order : context -> Sort.sort -> int -> FuncDecl.func_decl + + (** Create the transitive closure of a binary relation. + The resulting relation is recursive. *) + val mk_transitive_closure : context -> FuncDecl.func_decl -> FuncDecl.func_decl + +end + (** Floating-Point Arithmetic *) module FloatingPoint : sig