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

fix #5033

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-26 03:42:13 -08:00
parent 5c47f244e9
commit 06caf57a86
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -566,6 +566,7 @@ public class Context implements AutoCloseable {
/**
* Create a quantifier pattern.
**/
@SafeVarargs
public Pattern mkPattern(Expr<?>... terms)
{
if (terms.length == 0)
@ -687,6 +688,7 @@ public class Context implements AutoCloseable {
/**
* Create a new function application.
**/
@SafeVarargs
public <R extends Sort> Expr<R> mkApp(FuncDecl<R> f, Expr<?>... args)
{
checkContextMatch(f);
@ -732,6 +734,7 @@ public class Context implements AutoCloseable {
/**
* Creates a {@code distinct} term.
**/
@SafeVarargs
public <R extends Sort> BoolExpr mkDistinct(Expr<R>... args)
{
checkContextMatch(args);
@ -800,6 +803,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t[0] and t[1] and ...}.
**/
@SafeVarargs
public BoolExpr mkAnd(Expr<BoolSort>... t)
{
checkContextMatch(t);
@ -810,6 +814,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t[0] or t[1] or ...}.
**/
@SafeVarargs
public BoolExpr mkOr(Expr<BoolSort>... t)
{
checkContextMatch(t);
@ -820,6 +825,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t[0] + t[1] + ...}.
**/
@SafeVarargs
public <R extends ArithSort> ArithExpr<R> mkAdd(Expr<R>... t)
{
checkContextMatch(t);
@ -830,6 +836,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t[0] * t[1] * ...}.
**/
@SafeVarargs
public <R extends ArithSort> ArithExpr<R> mkMul(Expr<R>... t)
{
checkContextMatch(t);
@ -840,6 +847,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t[0] - t[1] - ...}.
**/
@SafeVarargs
public <R extends ArithSort> ArithExpr<R> mkSub(Expr<R>... t)
{
checkContextMatch(t);
@ -1814,6 +1822,7 @@ public class Context implements AutoCloseable {
* @see #mkStore
**/
@SafeVarargs
public <D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D, R2> mkMap(FuncDecl<R2> f, Expr<ArraySort<D, R1>>... args)
{
checkContextMatch(f);
@ -1903,6 +1912,7 @@ public class Context implements AutoCloseable {
/**
* Take the union of a list of sets.
**/
@SafeVarargs
public <D extends Sort> ArrayExpr<D, BoolSort> mkSetUnion(Expr<ArraySort<D, BoolSort>>... args)
{
checkContextMatch(args);
@ -1914,6 +1924,7 @@ public class Context implements AutoCloseable {
/**
* Take the intersection of a list of sets.
**/
@SafeVarargs
public <D extends Sort> ArrayExpr<D, BoolSort> mkSetIntersection(Expr<ArraySort<D, BoolSort>>... args)
{
checkContextMatch(args);
@ -2018,6 +2029,7 @@ public class Context implements AutoCloseable {
/**
* Concatenate sequences.
*/
@SafeVarargs
public <R extends Sort> SeqExpr<R> mkConcat(Expr<SeqSort<R>>... t)
{
checkContextMatch(t);
@ -2182,6 +2194,7 @@ public class Context implements AutoCloseable {
/**
* Create the concatenation of regular languages.
*/
@SafeVarargs
public <R extends Sort> ReExpr<R> mkConcat(ReExpr<R>... t)
{
checkContextMatch(t);
@ -2191,6 +2204,7 @@ public class Context implements AutoCloseable {
/**
* Create the union of regular languages.
*/
@SafeVarargs
public <R extends Sort> ReExpr<R> mkUnion(Expr<ReSort<R>>... t)
{
checkContextMatch(t);
@ -2200,6 +2214,7 @@ public class Context implements AutoCloseable {
/**
* Create the intersection of regular languages.
*/
@SafeVarargs
public <R extends Sort> ReExpr<R> mkIntersect(Expr<ReSort<R>>... t)
{
checkContextMatch(t);