Package com.microsoft.z3

Class Context

java.lang.Object
com.microsoft.z3.Context
All Implemented Interfaces:
AutoCloseable
public class Context extends Object implements AutoCloseable
The main interaction with Z3 happens via the Context. For applications that spawn an unbounded number of contexts, the proper use is within a try-with-resources scope so that the Context object gets garbage collected in a predictable way. Contexts maintain all data-structures related to terms and formulas that are created relative to them.

  • Constructor Details

    • Context

      public Context()

    • Context

      protected Context(long m_ctx)

    • Context

      public Context(Map<String,String> settings)
      Constructor. Remarks: The following parameters can be set: - proof (Boolean) Enable proof generation - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting - trace (Boolean) Tracing support for VCC - trace_file_name (String) Trace out file for VCC traces - timeout (unsigned) default timeout (in milliseconds) used for solvers - well_sorted_check type checker - auto_config use heuristics to automatically select solver and configure it - model model generation for solvers, this parameter can be overwritten when creating a solver - model_validate validate models produced by solvers - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver Note that in previous versions of Z3, this constructor was also used to set global and module parameters. For this purpose we should now use Global.setParameter

  • Method Details

    • mkSymbol

      public IntSymbol mkSymbol(int i)
      Creates a new symbol using an integer. Remarks: Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

    • mkSymbol

      public StringSymbol mkSymbol(String name)
      Create a symbol using a string.

    • getBoolSort

      public BoolSort getBoolSort()
      Retrieves the Boolean sort of the context.

    • getIntSort

      public IntSort getIntSort()
      Retrieves the Integer sort of the context.

    • getRealSort

      public RealSort getRealSort()
      Retrieves the Real sort of the context.

    • mkBoolSort

      public BoolSort mkBoolSort()
      Create a new Boolean sort.

    • mkCharSort

      public CharSort mkCharSort()
      Creates character sort object.

    • getStringSort

      public SeqSort<CharSort> getStringSort()
      Retrieves the String sort of the context.

    • mkUninterpretedSort

      public UninterpretedSort mkUninterpretedSort(Symbol s)
      Create a new uninterpreted sort.

    • mkUninterpretedSort

      public UninterpretedSort mkUninterpretedSort(String str)
      Create a new uninterpreted sort.

    • mkIntSort

      public IntSort mkIntSort()
      Create a new integer sort.

    • mkRealSort

      public RealSort mkRealSort()
      Create a real sort.

    • mkBitVecSort

      public BitVecSort mkBitVecSort(int size)
      Create a new bit-vector sort.

    • mkArraySort

      public <D extends Sort, R extends Sort> ArraySort<D,R> mkArraySort(D domain, R range)
      Create a new array sort.

    • mkArraySort

      public <R extends Sort> ArraySort<Sort,R> mkArraySort(Sort[] domains, R range)
      Create a new array sort.

    • mkStringSort

      public SeqSort<CharSort> mkStringSort()
      Create a new string sort

    • mkSeqSort

      public <R extends Sort> SeqSort<R> mkSeqSort(R s)
      Create a new sequence sort

    • mkReSort

      public <R extends Sort> ReSort<R> mkReSort(R s)
      Create a new regular expression sort

    • mkTupleSort

      public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
      Create a new tuple sort.

    • mkEnumSort

      public <R> EnumSort<R> mkEnumSort(Symbol name, Symbol... enumNames)
      Create a new enumeration sort.

    • mkEnumSort

      public <R> EnumSort<R> mkEnumSort(String name, String... enumNames)
      Create a new enumeration sort.

    • mkListSort

      public <R extends Sort> ListSort<R> mkListSort(Symbol name, R elemSort)
      Create a new list sort.

    • mkListSort

      public <R extends Sort> ListSort<R> mkListSort(String name, R elemSort)
      Create a new list sort.

    • mkFiniteDomainSort

      public <R> FiniteDomainSort<R> mkFiniteDomainSort(Symbol name, long size)
      Create a new finite domain sort.

    • mkFiniteDomainSort

      public <R> FiniteDomainSort<R> mkFiniteDomainSort(String name, long size)
      Create a new finite domain sort.

    • mkConstructor

      public <R> Constructor<R> mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
      Create a datatype constructor.
      Parameters:
      name - constructor name
      recognizer - name of recognizer function.
      fieldNames - names of the constructor fields.
      sorts - field sorts, 0 if the field sort refers to a recursive sort.
      sortRefs - reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

    • mkConstructor

      public <R> Constructor<R> mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
      Create a datatype constructor.

    • mkDatatypeSort

      public <R> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<R>[] constructors)
      Create a new datatype sort.

    • mkDatatypeSort

      public <R> DatatypeSort<R> mkDatatypeSort(String name, Constructor<R>[] constructors)
      Create a new datatype sort.

    • mkDatatypeSorts

      public DatatypeSort<Object>[] mkDatatypeSorts(Symbol[] names, Constructor<Object>[][] c)
      Create mutually recursive datatypes.
      Parameters:
      names - names of datatype sorts
      c - list of constructors, one list per sort.

    • mkDatatypeSorts

      public DatatypeSort<Object>[] mkDatatypeSorts(String[] names, Constructor<Object>[][] c)
      Create mutually recursive data-types.

    • mkUpdateField

      public <F extends Sort, R extends Sort> Expr<R> mkUpdateField(FuncDecl<F> field, Expr<R> t, Expr<F> v) throws Z3Exception
      Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remaining fields of t are unchanged.
      Throws:
      Z3Exception

    • mkFuncDecl

      public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort[] domain, R range)
      Creates a new function declaration.

    • mkFuncDecl

      public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort domain, R range)
      Creates a new function declaration.

    • mkFuncDecl

      public <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort[] domain, R range)
      Creates a new function declaration.

    • mkFuncDecl

      public <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort domain, R range)
      Creates a new function declaration.

    • mkRecFuncDecl

      public <R extends Sort> FuncDecl<R> mkRecFuncDecl(Symbol name, Sort[] domain, R range)
      Creates a new recursive function declaration.

    • AddRecDef

      public <R extends Sort> void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> body)
      Bind a definition to a recursive function declaration. The function must have previously been created using MkRecFuncDecl. The body may contain recursive uses of the function or other mutually recursive functions.

    • mkFreshFuncDecl

      public <R extends Sort> FuncDecl<R> mkFreshFuncDecl(String prefix, Sort[] domain, R range)
      Creates a fresh function declaration with a name prefixed with prefix.
      See Also:

    • mkConstDecl

      public <R extends Sort> FuncDecl<R> mkConstDecl(Symbol name, R range)
      Creates a new constant function declaration.

    • mkConstDecl

      public <R extends Sort> FuncDecl<R> mkConstDecl(String name, R range)
      Creates a new constant function declaration.

    • mkFreshConstDecl

      public <R extends Sort> FuncDecl<R> mkFreshConstDecl(String prefix, R range)
      Creates a fresh constant function declaration with a name prefixed with prefix.
      See Also:

    • mkBound

      public <R extends Sort> Expr<R> mkBound(int index, R ty)
      Creates a new bound variable.
      Parameters:
      index - The de-Bruijn index of the variable
      ty - The sort of the variable

    • mkPattern

      @SafeVarargs public final Pattern mkPattern(Expr<?>... terms)
      Create a quantifier pattern.

    • mkConst

      public <R extends Sort> Expr<R> mkConst(Symbol name, R range)
      Creates a new Constant of sort range and named name.

    • mkConst

      public <R extends Sort> Expr<R> mkConst(String name, R range)
      Creates a new Constant of sort range and named name.

    • mkFreshConst

      public <R extends Sort> Expr<R> mkFreshConst(String prefix, R range)
      Creates a fresh Constant of sort range and a name prefixed with prefix.

    • mkConst

      public <R extends Sort> Expr<R> mkConst(FuncDecl<R> f)
      Creates a fresh constant from the FuncDecl f.
      Parameters:
      f - A decl of a 0-arity function

    • mkBoolConst

      public BoolExpr mkBoolConst(Symbol name)
      Create a Boolean constant.

    • mkBoolConst

      public BoolExpr mkBoolConst(String name)
      Create a Boolean constant.

    • mkIntConst

      public IntExpr mkIntConst(Symbol name)
      Creates an integer constant.

    • mkIntConst

      public IntExpr mkIntConst(String name)
      Creates an integer constant.

    • mkRealConst

      public RealExpr mkRealConst(Symbol name)
      Creates a real constant.

    • mkRealConst

      public RealExpr mkRealConst(String name)
      Creates a real constant.

    • mkBVConst

      public BitVecExpr mkBVConst(Symbol name, int size)
      Creates a bit-vector constant.

    • mkBVConst

      public BitVecExpr mkBVConst(String name, int size)
      Creates a bit-vector constant.

    • mkApp

      @SafeVarargs public final <R extends Sort> Expr<R> mkApp(FuncDecl<R> f, Expr<?>... args)
      Create a new function application.

    • mkTrue

      public BoolExpr mkTrue()
      The true Term.

    • mkFalse

      public BoolExpr mkFalse()
      The false Term.

    • mkBool

      public BoolExpr mkBool(boolean value)
      Creates a Boolean value.

    • mkEq

      public BoolExpr mkEq(Expr<?> x, Expr<?> y)
      Creates the equality x = y

    • mkDistinct

      @SafeVarargs public final BoolExpr mkDistinct(Expr<?>... args)
      Creates a distinct term.

    • mkNot

      public BoolExpr mkNot(Expr<BoolSort> a)
      Create an expression representing not(a).

    • mkITE

      public <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<? extends R> t2, Expr<? extends R> t3)
      Create an expression representing an if-then-else: ite(t1, t2, t3).
      Parameters:
      t1 - An expression with Boolean sort
      t2 - An expression
      t3 - An expression with the same sort as t2

    • mkIff

      public BoolExpr mkIff(Expr<BoolSort> t1, Expr<BoolSort> t2)
      Create an expression representing t1 iff t2.

    • mkImplies

      public BoolExpr mkImplies(Expr<BoolSort> t1, Expr<BoolSort> t2)
      Create an expression representing t1 -> t2.

    • mkXor

      public BoolExpr mkXor(Expr<BoolSort> t1, Expr<BoolSort> t2)
      Create an expression representing t1 xor t2.

    • mkAnd

      @SafeVarargs public final BoolExpr mkAnd(Expr<BoolSort>... t)
      Create an expression representing t[0] and t[1] and ....

    • mkOr

      @SafeVarargs public final BoolExpr mkOr(Expr<BoolSort>... t)
      Create an expression representing t[0] or t[1] or ....

    • mkAdd

      @SafeVarargs public final <R extends ArithSort> ArithExpr<R> mkAdd(Expr<? extends R>... t)
      Create an expression representing t[0] + t[1] + ....

    • mkMul

      @SafeVarargs public final <R extends ArithSort> ArithExpr<R> mkMul(Expr<? extends R>... t)
      Create an expression representing t[0] * t[1] * ....

    • mkSub

      @SafeVarargs public final <R extends ArithSort> ArithExpr<R> mkSub(Expr<? extends R>... t)
      Create an expression representing t[0] - t[1] - ....

    • mkUnaryMinus

      public <R extends ArithSort> ArithExpr<R> mkUnaryMinus(Expr<R> t)
      Create an expression representing -t.

    • mkDiv

      public <R extends ArithSort> ArithExpr<R> mkDiv(Expr<? extends R> t1, Expr<? extends R> t2)
      Create an expression representing t1 / t2.

    • mkMod

      public IntExpr mkMod(Expr<IntSort> t1, Expr<IntSort> t2)
      Create an expression representing t1 mod t2. Remarks: The arguments must have int type.

    • mkRem

      public IntExpr mkRem(Expr<IntSort> t1, Expr<IntSort> t2)
      Create an expression representing t1 rem t2. Remarks: The arguments must have int type.

    • mkPower

      public <R extends ArithSort> ArithExpr<R> mkPower(Expr<? extends R> t1, Expr<? extends R> t2)
      Create an expression representing t1 ^ t2.

    • mkLt

      public BoolExpr mkLt(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
      Create an expression representing t1 &lt; t2

    • mkLe

      public BoolExpr mkLe(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
      Create an expression representing t1 &lt;= t2

    • mkGt

      public BoolExpr mkGt(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
      Create an expression representing t1 &gt; t2

    • mkGe

      public BoolExpr mkGe(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
      Create an expression representing t1 &gt;= t2

    • mkInt2Real

      public RealExpr mkInt2Real(Expr<IntSort> t)
      Coerce an integer to a real. Remarks: There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. You can take the floor of a real by creating an auxiliary integer Term k and asserting MakeInt2Real(k) &lt;= t1 &lt; MkInt2Real(k)+1. The argument must be of integer sort.

    • mkReal2Int

      public IntExpr mkReal2Int(Expr<RealSort> t)
      Coerce a real to an integer. Remarks: The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.

    • mkIsInteger

      public BoolExpr mkIsInteger(Expr<RealSort> t)
      Creates an expression that checks whether a real number is an integer.

    • mkBVNot

      public BitVecExpr mkBVNot(Expr<BitVecSort> t)
      Bitwise negation. Remarks: The argument must have a bit-vector sort.

    • mkBVRedAND

      public BitVecExpr mkBVRedAND(Expr<BitVecSort> t)
      Take conjunction of bits in a vector, return vector of length 1. Remarks: The argument must have a bit-vector sort.

    • mkBVRedOR

      public BitVecExpr mkBVRedOR(Expr<BitVecSort> t)
      Take disjunction of bits in a vector, return vector of length 1. Remarks: The argument must have a bit-vector sort.

    • mkBVAND

      public BitVecExpr mkBVAND(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bitwise conjunction. Remarks: The arguments must have a bit-vector sort.

    • mkBVOR

      public BitVecExpr mkBVOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bitwise disjunction. Remarks: The arguments must have a bit-vector sort.

    • mkBVXOR

      public BitVecExpr mkBVXOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bitwise XOR. Remarks: The arguments must have a bit-vector sort.

    • mkBVNAND

      public BitVecExpr mkBVNAND(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bitwise NAND. Remarks: The arguments must have a bit-vector sort.

    • mkBVNOR

      public BitVecExpr mkBVNOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bitwise NOR. Remarks: The arguments must have a bit-vector sort.

    • mkBVXNOR

      public BitVecExpr mkBVXNOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bitwise XNOR. Remarks: The arguments must have a bit-vector sort.

    • mkBVNeg

      public BitVecExpr mkBVNeg(Expr<BitVecSort> t)
      Standard two's complement unary minus. Remarks: The arguments must have a bit-vector sort.

    • mkBVAdd

      public BitVecExpr mkBVAdd(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement addition. Remarks: The arguments must have the same bit-vector sort.

    • mkBVSub

      public BitVecExpr mkBVSub(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement subtraction. Remarks: The arguments must have the same bit-vector sort.

    • mkBVMul

      public BitVecExpr mkBVMul(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement multiplication. Remarks: The arguments must have the same bit-vector sort.

    • mkBVUDiv

      public BitVecExpr mkBVUDiv(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Unsigned division. Remarks: It is defined as the floor of t1/t2 if \c t2 is different from zero. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

    • mkBVSDiv

      public BitVecExpr mkBVSDiv(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Signed division. Remarks: It is defined in the following way: - The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0. - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 &lt; 0. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

    • mkBVURem

      public BitVecExpr mkBVURem(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Unsigned remainder. Remarks: It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

    • mkBVSRem

      public BitVecExpr mkBVSRem(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Signed remainder. Remarks: It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of \c t1. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

    • mkBVSMod

      public BitVecExpr mkBVSMod(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement signed remainder (sign follows divisor). Remarks: If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

    • mkBVULT

      public BoolExpr mkBVULT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Unsigned less-than Remarks: The arguments must have the same bit-vector sort.

    • mkBVSLT

      public BoolExpr mkBVSLT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement signed less-than Remarks: The arguments must have the same bit-vector sort.

    • mkBVULE

      public BoolExpr mkBVULE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Unsigned less-than or equal to. Remarks: The arguments must have the same bit-vector sort.

    • mkBVSLE

      public BoolExpr mkBVSLE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement signed less-than or equal to. Remarks: The arguments must have the same bit-vector sort.

    • mkBVUGE

      public BoolExpr mkBVUGE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Unsigned greater than or equal to. Remarks: The arguments must have the same bit-vector sort.

    • mkBVSGE

      public BoolExpr mkBVSGE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement signed greater than or equal to. Remarks: The arguments must have the same bit-vector sort.

    • mkBVUGT

      public BoolExpr mkBVUGT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Unsigned greater-than. Remarks: The arguments must have the same bit-vector sort.

    • mkBVSGT

      public BoolExpr mkBVSGT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Two's complement signed greater-than. Remarks: The arguments must have the same bit-vector sort.

    • mkConcat

      public BitVecExpr mkConcat(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Bit-vector concatenation. Remarks: The arguments must have a bit-vector sort.
      Returns:
      The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

    • mkExtract

      public BitVecExpr mkExtract(int high, int low, Expr<BitVecSort> t)
      Bit-vector extraction. Remarks: Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. The argument t must have a bit-vector sort.

    • mkSignExt

      public BitVecExpr mkSignExt(int i, Expr<BitVecSort> t)
      Bit-vector sign extension. Remarks: Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i, where \c m is the size of the given bit-vector. The argument t must have a bit-vector sort.

    • mkZeroExt

      public BitVecExpr mkZeroExt(int i, Expr<BitVecSort> t)
      Bit-vector zero extension. Remarks: Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where \c m is the size of the given bit-vector. The argument t must have a bit-vector sort.

    • mkRepeat

      public BitVecExpr mkRepeat(int i, Expr<BitVecSort> t)
      Bit-vector repetition. Remarks: The argument t must have a bit-vector sort.

    • mkBVSHL

      public BitVecExpr mkBVSHL(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Shift left. Remarks: It is equivalent to multiplication by 2^x where \c x is the value of t2. NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The arguments must have a bit-vector sort.

    • mkBVLSHR

      public BitVecExpr mkBVLSHR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Logical shift right Remarks: It is equivalent to unsigned division by 2^x where \c x is the value of t2. NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The arguments must have a bit-vector sort.

    • mkBVASHR

      public BitVecExpr mkBVASHR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Arithmetic shift right Remarks: It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument. NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The arguments must have a bit-vector sort.

    • mkBVRotateLeft

      public BitVecExpr mkBVRotateLeft(int i, Expr<BitVecSort> t)
      Rotate Left. Remarks: Rotate bits of \c t to the left \c i times. The argument t must have a bit-vector sort.

    • mkBVRotateRight

      public BitVecExpr mkBVRotateRight(int i, Expr<BitVecSort> t)
      Rotate Right. Remarks: Rotate bits of \c t to the right \c i times. The argument t must have a bit-vector sort.

    • mkBVRotateLeft

      public BitVecExpr mkBVRotateLeft(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Rotate Left. Remarks: Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.

    • mkBVRotateRight

      public BitVecExpr mkBVRotateRight(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Rotate Right. Remarks: Rotate bits of t1 to the rightt2 times. The arguments must have the same bit-vector sort.

    • mkInt2BV

      public BitVecExpr mkInt2BV(int n, Expr<IntSort> t)
      Create an n bit bit-vector from the integer argument t. Remarks: NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function. The argument must be of integer sort.

    • mkBV2Int

      public IntExpr mkBV2Int(Expr<BitVecSort> t, boolean signed)
      Create an integer from the bit-vector argument t. Remarks: If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t. If \c is_signed is true, \c t1 is treated as a signed bit-vector. NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function. The argument must be of bit-vector sort.

    • mkBVAddNoOverflow

      public BoolExpr mkBVAddNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2, boolean isSigned)
      Create a predicate that checks that the bit-wise addition does not overflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVAddNoUnderflow

      public BoolExpr mkBVAddNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Create a predicate that checks that the bit-wise addition does not underflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVSubNoOverflow

      public BoolExpr mkBVSubNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Create a predicate that checks that the bit-wise subtraction does not overflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVSubNoUnderflow

      public BoolExpr mkBVSubNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2, boolean isSigned)
      Create a predicate that checks that the bit-wise subtraction does not underflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVSDivNoOverflow

      public BoolExpr mkBVSDivNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Create a predicate that checks that the bit-wise signed division does not overflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVNegNoOverflow

      public BoolExpr mkBVNegNoOverflow(Expr<BitVecSort> t)
      Create a predicate that checks that the bit-wise negation does not overflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVMulNoOverflow

      public BoolExpr mkBVMulNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2, boolean isSigned)
      Create a predicate that checks that the bit-wise multiplication does not overflow. Remarks: The arguments must be of bit-vector sort.

    • mkBVMulNoUnderflow

      public BoolExpr mkBVMulNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
      Create a predicate that checks that the bit-wise multiplication does not underflow. Remarks: The arguments must be of bit-vector sort.

    • mkArrayConst

      public <D extends Sort, R extends Sort> ArrayExpr<D,R> mkArrayConst(Symbol name, D domain, R range)
      Create an array constant.

    • mkArrayConst

      public <D extends Sort, R extends Sort> ArrayExpr<D,R> mkArrayConst(String name, D domain, R range)
      Create an array constant.

    • mkSelect

      public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D,R>> a, Expr<D> i)
      Array read. Remarks: The argument a is the array and i is the index of the array that gets read. The node a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range.
      See Also:

    • mkSelect

      public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort,R>> a, Expr<?>[] args)
      Array read. Remarks: The argument a is the array and args are the indices of the array that gets read. The node a must have an array sort [domains -> range], and args must have the sorts domains. The sort of the result is range.
      See Also:

    • mkStore

      public <D extends Sort, R extends Sort> ArrayExpr<D,R> mkStore(Expr<ArraySort<D,R>> a, Expr<D> i, Expr<R> v)
      Array update. Remarks: The node a must have an array sort [domain -> range], i must have sort domain, v must have sort range. The sort of the result is [domain -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).
      See Also:

    • mkStore

      public <R extends Sort> ArrayExpr<Sort,R> mkStore(Expr<ArraySort<Sort,R>> a, Expr<?>[] args, Expr<R> v)
      Array update. Remarks: The node a must have an array sort [domains -> range], i must have sort domain, v must have sort range. The sort of the result is [domains -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for args, where it maps to v (and the select of a with respect to args may be a different value).
      See Also:

    • mkConstArray

      public <D extends Sort, R extends Sort> ArrayExpr<D,R> mkConstArray(D domain, Expr<R> v)
      Create a constant array. Remarks: The resulting term is an array, such that a select on an arbitrary index produces the value v.
      See Also:

    • mkMap

      @SafeVarargs public final <D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D,R2> mkMap(FuncDecl<R2> f, Expr<ArraySort<D,R1>>... args)
      Maps f on the argument arrays. Remarks: Each element of args must be of an array sort [domain_i -> range_i]. The function declaration f must have type range_1 .. range_n -> range. v must have sort range. The sort of the result is [domain_i -> range].
      See Also:

    • mkTermArray

      public <D extends Sort, R extends Sort> Expr<R> mkTermArray(Expr<ArraySort<D,R>> array)
      Access the array default value. Remarks: Produces the default range value, for arrays that can be represented as finite maps with a default range value.

    • mkArrayExt

      public <D extends Sort, R extends Sort> Expr<D> mkArrayExt(Expr<ArraySort<D,R>> arg1, Expr<ArraySort<D,R>> arg2)
      Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.

    • mkSetSort

      public <D extends Sort> SetSort<D> mkSetSort(D ty)
      Create a set type.

    • mkEmptySet

      public <D extends Sort> ArrayExpr<D,BoolSort> mkEmptySet(D domain)
      Create an empty set.

    • mkFullSet

      public <D extends Sort> ArrayExpr<D,BoolSort> mkFullSet(D domain)
      Create the full set.

    • mkSetAdd

      public <D extends Sort> ArrayExpr<D,BoolSort> mkSetAdd(Expr<ArraySort<D,BoolSort>> set, Expr<D> element)
      Add an element to the set.

    • mkSetDel

      public <D extends Sort> ArrayExpr<D,BoolSort> mkSetDel(Expr<ArraySort<D,BoolSort>> set, Expr<D> element)
      Remove an element from a set.

    • mkSetUnion

      @SafeVarargs public final <D extends Sort> ArrayExpr<D,BoolSort> mkSetUnion(Expr<ArraySort<D,BoolSort>>... args)
      Take the union of a list of sets.

    • mkSetIntersection

      @SafeVarargs public final <D extends Sort> ArrayExpr<D,BoolSort> mkSetIntersection(Expr<ArraySort<D,BoolSort>>... args)
      Take the intersection of a list of sets.

    • mkSetDifference

      public <D extends Sort> ArrayExpr<D,BoolSort> mkSetDifference(Expr<ArraySort<D,BoolSort>> arg1, Expr<ArraySort<D,BoolSort>> arg2)
      Take the difference between two sets.

    • mkSetComplement

      public <D extends Sort> ArrayExpr<D,BoolSort> mkSetComplement(Expr<ArraySort<D,BoolSort>> arg)
      Take the complement of a set.

    • mkSetMembership

      public <D extends Sort> BoolExpr mkSetMembership(Expr<D> elem, Expr<ArraySort<D,BoolSort>> set)
      Check for set membership.

    • mkSetSubset

      public <D extends Sort> BoolExpr mkSetSubset(Expr<ArraySort<D,BoolSort>> arg1, Expr<ArraySort<D,BoolSort>> arg2)
      Check for subsetness of sets.

    • mkEmptySeq

      public <R extends Sort> SeqExpr<R> mkEmptySeq(R s)
      Create the empty sequence.

    • mkUnit

      public <R extends Sort> SeqExpr<R> mkUnit(Expr<R> elem)
      Create the singleton sequence.

    • mkString

      public SeqExpr<CharSort> mkString(String s)
      Create a string constant.

    • intToString

      public SeqExpr<CharSort> intToString(Expr<IntSort> e)
      Convert an integer expression to a string.

    • ubvToString

      public SeqExpr<CharSort> ubvToString(Expr<BitVecSort> e)
      Convert an unsigned bitvector expression to a string.

    • sbvToString

      public SeqExpr<CharSort> sbvToString(Expr<BitVecSort> e)
      Convert an signed bitvector expression to a string.

    • stringToInt

      public IntExpr stringToInt(Expr<SeqSort<CharSort>> e)
      Convert an integer expression to a string.

    • mkConcat

      @SafeVarargs public final <R extends Sort> SeqExpr<R> mkConcat(Expr<SeqSort<R>>... t)
      Concatenate sequences.

    • mkLength

      public <R extends Sort> IntExpr mkLength(Expr<SeqSort<R>> s)
      Retrieve the length of a given sequence.

    • mkPrefixOf

      public <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> s2)
      Check for sequence prefix.

    • mkSuffixOf

      public <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> s2)
      Check for sequence suffix.

    • mkContains

      public <R extends Sort> BoolExpr mkContains(Expr<SeqSort<R>> s1, Expr<SeqSort<R>> s2)
      Check for sequence containment of s2 in s1.

    • MkStringLt

      public BoolExpr MkStringLt(SeqSort<CharSort> s1, SeqSort<CharSort> s2)
      Check if the string s1 is lexicographically strictly less than s2.

    • MkStringLe

      public BoolExpr MkStringLe(SeqSort<CharSort> s1, SeqSort<CharSort> s2)
      Check if the string s1 is lexicographically less or equal to s2.

    • mkAt

      public <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<R>> s, Expr<IntSort> index)
      Retrieve sequence of length one at index.

    • mkNth

      public <R extends Sort> Expr<R> mkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
      Retrieve element at index.

    • mkExtract

      public <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<R>> s, Expr<IntSort> offset, Expr<IntSort> length)
      Extract subsequence.

    • mkIndexOf

      public <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<R>> s, Expr<SeqSort<R>> substr, Expr<IntSort> offset)
      Extract index of sub-string starting at offset.

    • mkReplace

      public <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<R>> s, Expr<SeqSort<R>> src, Expr<SeqSort<R>> dst)
      Replace the first occurrence of src by dst in s.

    • mkToRe

      public <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<R>> s)
      Convert a regular expression that accepts sequence s.

    • mkInRe

      public <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<R>> s, Expr<ReSort<R>> re)
      Check for regular expression membership.

    • mkStar

      public <R extends Sort> ReExpr<R> mkStar(Expr<ReSort<R>> re)
      Take the Kleene star of a regular expression.

    • mkPower

      public <R extends Sort> ReExpr<R> mkPower(Expr<ReSort<R>> re, int n)
      Create power regular expression.

    • mkLoop

      public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo, int hi)
      Take the lower and upper-bounded Kleene star of a regular expression.

    • mkLoop

      public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo)
      Take the lower-bounded Kleene star of a regular expression.

    • mkPlus

      public <R extends Sort> ReExpr<R> mkPlus(Expr<ReSort<R>> re)
      Take the Kleene plus of a regular expression.

    • mkOption

      public <R extends Sort> ReExpr<R> mkOption(Expr<ReSort<R>> re)
      Create the optional regular expression.

    • mkComplement

      public <R extends Sort> ReExpr<R> mkComplement(Expr<ReSort<R>> re)
      Create the complement regular expression.

    • mkConcat

      @SafeVarargs public final <R extends Sort> ReExpr<R> mkConcat(ReExpr<R>... t)
      Create the concatenation of regular languages.

    • mkUnion

      @SafeVarargs public final <R extends Sort> ReExpr<R> mkUnion(Expr<ReSort<R>>... t)
      Create the union of regular languages.

    • mkIntersect

      @SafeVarargs public final <R extends Sort> ReExpr<R> mkIntersect(Expr<ReSort<R>>... t)
      Create the intersection of regular languages.

    • mkDiff

      public <R extends Sort> ReExpr<R> mkDiff(Expr<ReSort<R>> a, Expr<ReSort<R>> b)
      Create a difference regular expression.

    • mkEmptyRe

      public <R extends Sort> ReExpr<R> mkEmptyRe(R s)
      Create the empty regular expression. Coresponds to re.none

    • mkFullRe

      public <R extends Sort> ReExpr<R> mkFullRe(R s)
      Create the full regular expression. Corresponds to re.all

    • mkAllcharRe

      public <R extends Sort> ReExpr<R> mkAllcharRe(R s)
      Create regular expression that accepts all characters Corresponds to re.allchar

    • mkRange

      public <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<CharSort>> lo, Expr<SeqSort<CharSort>> hi)
      Create a range expression.

    • mkCharLe

      public BoolExpr mkCharLe(Expr<CharSort> ch1, Expr<CharSort> ch2)
      Create less than or equal to between two characters.

    • charToInt

      public IntExpr charToInt(Expr<CharSort> ch)
      Create an integer (code point) from character.

    • charToBv

      public BitVecExpr charToBv(Expr<CharSort> ch)
      Create a bit-vector (code point) from character.

    • charFromBv

      public Expr<CharSort> charFromBv(BitVecExpr bv)
      Create a character from a bit-vector (code point).

    • mkIsDigit

      public BoolExpr mkIsDigit(Expr<CharSort> ch)
      Create a check if the character is a digit.

    • mkAtMost

      public BoolExpr mkAtMost(Expr<BoolSort>[] args, int k)
      Create an at-most-k constraint.

    • mkAtLeast

      public BoolExpr mkAtLeast(Expr<BoolSort>[] args, int k)
      Create an at-least-k constraint.

    • mkPBLe

      public BoolExpr mkPBLe(int[] coeffs, Expr<BoolSort>[] args, int k)
      Create a pseudo-Boolean less-or-equal constraint.

    • mkPBGe

      public BoolExpr mkPBGe(int[] coeffs, Expr<BoolSort>[] args, int k)
      Create a pseudo-Boolean greater-or-equal constraint.

    • mkPBEq

      public BoolExpr mkPBEq(int[] coeffs, Expr<BoolSort>[] args, int k)
      Create a pseudo-Boolean equal constraint.

    • mkNumeral

      public <R extends Sort> Expr<R> mkNumeral(String v, R ty)
      Create a Term of a given sort.
      Parameters:
      v - A string representing the term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*.
      ty - The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
      Returns:
      A Term with value v and sort ty

    • mkNumeral

      public <R extends Sort> Expr<R> mkNumeral(int v, R ty)
      Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
      Parameters:
      v - Value of the numeral
      ty - Sort of the numeral
      Returns:
      A Term with value v and type ty

    • mkNumeral

      public <R extends Sort> Expr<R> mkNumeral(long v, R ty)
      Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
      Parameters:
      v - Value of the numeral
      ty - Sort of the numeral
      Returns:
      A Term with value v and type ty

    • mkReal

      public RatNum mkReal(int num, int den)
      Create a real from a fraction.
      Parameters:
      num - numerator of rational.
      den - denominator of rational.
      Returns:
      A Term with value num/den and sort Real
      See Also:

    • mkReal

      public RatNum mkReal(String v)
      Create a real numeral.
      Parameters:
      v - A string representing the Term value in decimal notation.
      Returns:
      A Term with value v and sort Real

    • mkReal

      public RatNum mkReal(int v)
      Create a real numeral.
      Parameters:
      v - value of the numeral.
      Returns:
      A Term with value v and sort Real

    • mkReal

      public RatNum mkReal(long v)
      Create a real numeral.
      Parameters:
      v - value of the numeral.
      Returns:
      A Term with value v and sort Real

    • mkInt

      public IntNum mkInt(String v)
      Create an integer numeral.
      Parameters:
      v - A string representing the Term value in decimal notation.

    • mkInt

      public IntNum mkInt(int v)
      Create an integer numeral.
      Parameters:
      v - value of the numeral.
      Returns:
      A Term with value v and sort Integer

    • mkInt

      public IntNum mkInt(long v)
      Create an integer numeral.
      Parameters:
      v - value of the numeral.
      Returns:
      A Term with value v and sort Integer

    • mkBV

      public BitVecNum mkBV(String v, int size)
      Create a bit-vector numeral.
      Parameters:
      v - A string representing the value in decimal notation.
      size - the size of the bit-vector

    • mkBV

      public BitVecNum mkBV(int v, int size)
      Create a bit-vector numeral.
      Parameters:
      v - value of the numeral.
      size - the size of the bit-vector

    • mkBV

      public BitVecNum mkBV(long v, int size)
      Create a bit-vector numeral.
      Parameters:
      v - value of the numeral. *
      size - the size of the bit-vector

    • mkForall

      public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
      Create a universal Quantifier.
      Parameters:
      sorts - the sorts of the bound variables.
      names - names of the bound variables
      body - the body of the quantifier.
      weight - quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
      patterns - array containing the patterns created using MkPattern.
      noPatterns - array containing the anti-patterns created using MkPattern.
      quantifierID - optional symbol to track quantifier.
      skolemID - optional symbol to track skolem constants.
      Returns:
      Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. Note that the bound variables are de-Bruijn indices created using mkBound(int, R). Z3 applies the convention that the last element in names and sorts refers to the variable with index 0, the second to last element of names and sorts refers to the variable with index 1, etc.

    • mkForall

      public Quantifier mkForall(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
      Creates a universal quantifier using a list of constants that will form the set of bound variables.
      See Also:

    • mkExists

      public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
      Creates an existential quantifier using de-Bruijn indexed variables.
      See Also:

    • mkExists

      public Quantifier mkExists(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
      Creates an existential quantifier using a list of constants that will form the set of bound variables.
      See Also:

    • mkQuantifier

      public Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
      Create a Quantifier.
      See Also:

    • mkQuantifier

      public Quantifier mkQuantifier(boolean universal, Expr<?>[] boundConstants, Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
      Create a Quantifier
      See Also:

    • mkLambda

      public <R extends Sort> Lambda<R> mkLambda(Sort[] sorts, Symbol[] names, Expr<R> body)
      Create a lambda expression. sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the lambda. Note that the bound variables are de-Bruijn indices created using mkBound(int, R) Z3 applies the convention that the last element in names and sorts refers to the variable with index 0, the second to last element of names and sorts refers to the variable with index 1, etc.
      Parameters:
      sorts - the sorts of the bound variables.
      names - names of the bound variables.
      body - the body of the quantifier.

    • mkLambda

      public <R extends Sort> Lambda<R> mkLambda(Expr<?>[] boundConstants, Expr<R> body)
      Create a lambda expression. Creates a lambda expression using a list of constants that will form the set of bound variables.

    • setPrintMode

      public void setPrintMode(Z3_ast_print_mode value)
      Selects the format used for pretty-printing expressions. Remarks: The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
      See Also:

    • benchmarkToSMTString

      public String benchmarkToSMTString(String name, String logic, String status, String attributes, Expr<BoolSort>[] assumptions, Expr<BoolSort> formula)
      Convert a benchmark into an SMT-LIB formatted string.
      Parameters:
      name - Name of the benchmark. The argument is optional.
      logic - The benchmark logic.
      status - The status string (sat, unsat, or unknown)
      attributes - Other attributes, such as source, difficulty or category.
      assumptions - Auxiliary assumptions.
      formula - Formula to be checked for consistency in conjunction with assumptions.
      Returns:
      A string representation of the benchmark.

    • parseSMTLIB2String

      public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
      Parse the given string using the SMT-LIB2 parser.
      Returns:
      A conjunction of assertions. If the string contains push/pop commands, the set of assertions returned are the ones in the last scope level.

    • parseSMTLIB2File

      public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
      Parse the given file using the SMT-LIB2 parser.
      See Also:

    • mkGoal

      public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
      Creates a new Goal. Remarks: Note that the Context must have been created with proof generation support if proofs is set to true here.
      Parameters:
      models - Indicates whether model generation should be enabled.
      unsatCores - Indicates whether unsat core generation should be enabled.
      proofs - Indicates whether proof generation should be enabled.

    • mkParams

      public Params mkParams()
      Creates a new ParameterSet.

    • getNumTactics

      public int getNumTactics()
      The number of supported tactics.

    • getTacticNames

      public String[] getTacticNames()
      The names of all supported tactics.

    • getTacticDescription

      public String getTacticDescription(String name)
      Returns a string containing a description of the tactic with the given name.

    • mkTactic

      public Tactic mkTactic(String name)
      Creates a new Tactic.

    • andThen

      public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
      Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1

    • then

      public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
      Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 Remarks: Shorthand for AndThen.

    • orElse

      public Tactic orElse(Tactic t1, Tactic t2)
      Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.

    • tryFor

      public Tactic tryFor(Tactic t, int ms)
      Create a tactic that applies t to a goal for ms milliseconds. Remarks: If t does not terminate within ms milliseconds, then it fails.

    • when

      public Tactic when(Probe p, Tactic t)
      Create a tactic that applies t to a given goal if the probe p evaluates to true. Remarks: If p evaluates to false, then the new tactic behaves like the skip tactic.

    • cond

      public Tactic cond(Probe p, Tactic t1, Tactic t2)
      Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.

    • repeat

      public Tactic repeat(Tactic t, int max)
      Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.

    • skip

      public Tactic skip()
      Create a tactic that just returns the given goal.

    • fail

      public Tactic fail()
      Create a tactic always fails.

    • failIf

      public Tactic failIf(Probe p)
      Create a tactic that fails if the probe p evaluates to false.

    • failIfNotDecided

      public Tactic failIfNotDecided()
      Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').

    • usingParams

      public Tactic usingParams(Tactic t, Params p)
      Create a tactic that applies t using the given set of parameters p.

    • with

      public Tactic with(Tactic t, Params p)
      Create a tactic that applies t using the given set of parameters p. Remarks: Alias for UsingParams

    • parOr

      public Tactic parOr(Tactic... t)
      Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).

    • parAndThen

      public Tactic parAndThen(Tactic t1, Tactic t2)
      Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.

    • interrupt

      public void interrupt()
      Interrupt the execution of a Z3 procedure. Remarks: This procedure can be used to interrupt: solvers, simplifiers and tactics.

    • getNumProbes

      public int getNumProbes()
      The number of supported Probes.

    • getProbeNames

      public String[] getProbeNames()
      The names of all supported Probes.

    • getProbeDescription

      public String getProbeDescription(String name)
      Returns a string containing a description of the probe with the given name.

    • mkProbe

      public Probe mkProbe(String name)
      Creates a new Probe.

    • constProbe

      public Probe constProbe(double val)
      Create a probe that always evaluates to val.

    • lt

      public Probe lt(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value returned by p1 is less than the value returned by p2

    • gt

      public Probe gt(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value returned by p1 is greater than the value returned by p2

    • le

      public Probe le(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value returned by p1 is less than or equal the value returned by p2

    • ge

      public Probe ge(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value returned by p1 is greater than or equal the value returned by p2

    • eq

      public Probe eq(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value returned by p1 is equal to the value returned by p2

    • and

      public Probe and(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value p1 and p2 evaluate to true.

    • or

      public Probe or(Probe p1, Probe p2)
      Create a probe that evaluates to true when the value p1 or p2 evaluate to true.

    • not

      public Probe not(Probe p)
      Create a probe that evaluates to true when the value p does not evaluate to true.

    • mkSolver

      public Solver mkSolver()
      Creates a new (incremental) solver. Remarks: This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

    • mkSolver

      public Solver mkSolver(Symbol logic)
      Creates a new (incremental) solver. Remarks: This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

    • mkSolver

      public Solver mkSolver(String logic)
      Creates a new (incremental) solver.
      See Also:

    • mkSimpleSolver

      public Solver mkSimpleSolver()
      Creates a new (incremental) solver.

    • mkSolver

      public Solver mkSolver(Tactic t)
      Creates a solver that is implemented using the given tactic. Remarks: The solver supports the commands Push and Pop, but it will always solve each check from scratch.

    • mkFixedpoint

      public Fixedpoint mkFixedpoint()
      Create a Fixedpoint context.

    • mkOptimize

      public Optimize mkOptimize()
      Create a Optimize context.

    • mkFPRoundingModeSort

      public FPRMSort mkFPRoundingModeSort()
      Create the floating-point RoundingMode sort.
      Throws:
      Z3Exception

    • mkFPRoundNearestTiesToEven

      public FPRMExpr mkFPRoundNearestTiesToEven()
      Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
      Throws:
      Z3Exception

    • mkFPRNE

      public FPRMNum mkFPRNE()
      Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
      Throws:
      Z3Exception

    • mkFPRoundNearestTiesToAway

      public FPRMNum mkFPRoundNearestTiesToAway()
      Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
      Throws:
      Z3Exception

    • mkFPRNA

      public FPRMNum mkFPRNA()
      Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
      Throws:
      Z3Exception

    • mkFPRoundTowardPositive

      public FPRMNum mkFPRoundTowardPositive()
      Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
      Throws:
      Z3Exception

    • mkFPRTP

      public FPRMNum mkFPRTP()
      Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
      Throws:
      Z3Exception

    • mkFPRoundTowardNegative

      public FPRMNum mkFPRoundTowardNegative()
      Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
      Throws:
      Z3Exception

    • mkFPRTN

      public FPRMNum mkFPRTN()
      Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
      Throws:
      Z3Exception

    • mkFPRoundTowardZero

      public FPRMNum mkFPRoundTowardZero()
      Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
      Throws:
      Z3Exception

    • mkFPRTZ

      public FPRMNum mkFPRTZ()
      Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
      Throws:
      Z3Exception

    • mkFPSort

      public FPSort mkFPSort(int ebits, int sbits)
      Create a FloatingPoint sort.
      Parameters:
      ebits - exponent bits in the FloatingPoint sort.
      sbits - significand bits in the FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSortHalf

      public FPSort mkFPSortHalf()
      Create the half-precision (16-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSort16

      public FPSort mkFPSort16()
      Create the half-precision (16-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSortSingle

      public FPSort mkFPSortSingle()
      Create the single-precision (32-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSort32

      public FPSort mkFPSort32()
      Create the single-precision (32-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSortDouble

      public FPSort mkFPSortDouble()
      Create the double-precision (64-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSort64

      public FPSort mkFPSort64()
      Create the double-precision (64-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSortQuadruple

      public FPSort mkFPSortQuadruple()
      Create the quadruple-precision (128-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPSort128

      public FPSort mkFPSort128()
      Create the quadruple-precision (128-bit) FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPNaN

      public FPNum mkFPNaN(FPSort s)
      Create a NaN of sort s.
      Parameters:
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPInf

      public FPNum mkFPInf(FPSort s, boolean negative)
      Create a floating-point infinity of sort s.
      Parameters:
      s - FloatingPoint sort.
      negative - indicates whether the result should be negative.
      Throws:
      Z3Exception

    • mkFPZero

      public FPNum mkFPZero(FPSort s, boolean negative)
      Create a floating-point zero of sort s.
      Parameters:
      s - FloatingPoint sort.
      negative - indicates whether the result should be negative.
      Throws:
      Z3Exception

    • mkFPNumeral

      public FPNum mkFPNumeral(float v, FPSort s)
      Create a numeral of FloatingPoint sort from a float.
      Parameters:
      v - numeral value.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPNumeral

      public FPNum mkFPNumeral(double v, FPSort s)
      Create a numeral of FloatingPoint sort from a double.
      Parameters:
      v - numeral value.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPNumeral

      public FPNum mkFPNumeral(int v, FPSort s)
      Create a numeral of FloatingPoint sort from an int.
      Parameters:
      v - numeral value.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPNumeral

      public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
      Create a numeral of FloatingPoint sort from a sign bit and two integers.
      Parameters:
      sgn - the sign.
      exp - the exponent.
      sig - the significand.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPNumeral

      public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
      Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
      Parameters:
      sgn - the sign.
      exp - the exponent.
      sig - the significand.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFP

      public FPNum mkFP(float v, FPSort s)
      Create a numeral of FloatingPoint sort from a float.
      Parameters:
      v - numeral value.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFP

      public FPNum mkFP(double v, FPSort s)
      Create a numeral of FloatingPoint sort from a double.
      Parameters:
      v - numeral value.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFP

      public FPNum mkFP(int v, FPSort s)
      Create a numeral of FloatingPoint sort from an int.
      Parameters:
      v - numeral value.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFP

      public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
      Create a numeral of FloatingPoint sort from a sign bit and two integers.
      Parameters:
      sgn - the sign.
      exp - the exponent.
      sig - the significand.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFP

      public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
      Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
      Parameters:
      sgn - the sign.
      exp - the exponent.
      sig - the significand.
      s - FloatingPoint sort.
      Throws:
      Z3Exception

    • mkFPAbs

      public FPExpr mkFPAbs(Expr<FPSort> t)
      Floating-point absolute value
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPNeg

      public FPExpr mkFPNeg(Expr<FPSort> t)
      Floating-point negation
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPAdd

      public FPExpr mkFPAdd(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point addition
      Parameters:
      rm - rounding mode term
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPSub

      public FPExpr mkFPSub(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point subtraction
      Parameters:
      rm - rounding mode term
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPMul

      public FPExpr mkFPMul(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point multiplication
      Parameters:
      rm - rounding mode term
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPDiv

      public FPExpr mkFPDiv(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point division
      Parameters:
      rm - rounding mode term
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPFMA

      public FPExpr mkFPFMA(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2, Expr<FPSort> t3)
      Floating-point fused multiply-add
      Parameters:
      rm - rounding mode term
      t1 - floating-point term
      t2 - floating-point term
      t3 - floating-point term Remarks: The result is round((t1 * t2) + t3)
      Throws:
      Z3Exception

    • mkFPSqrt

      public FPExpr mkFPSqrt(Expr<FPRMSort> rm, Expr<FPSort> t)
      Floating-point square root
      Parameters:
      rm - rounding mode term
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPRem

      public FPExpr mkFPRem(Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point remainder
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPRoundToIntegral

      public FPExpr mkFPRoundToIntegral(Expr<FPRMSort> rm, Expr<FPSort> t)
      Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
      Parameters:
      rm - term of RoundingMode sort
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPMin

      public FPExpr mkFPMin(Expr<FPSort> t1, Expr<FPSort> t2)
      Minimum of floating-point numbers.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPMax

      public FPExpr mkFPMax(Expr<FPSort> t1, Expr<FPSort> t2)
      Maximum of floating-point numbers.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPLEq

      public BoolExpr mkFPLEq(Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point less than or equal.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPLt

      public BoolExpr mkFPLt(Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point less than.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPGEq

      public BoolExpr mkFPGEq(Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point greater than or equal.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPGt

      public BoolExpr mkFPGt(Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point greater than.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term
      Throws:
      Z3Exception

    • mkFPEq

      public BoolExpr mkFPEq(Expr<FPSort> t1, Expr<FPSort> t2)
      Floating-point equality.
      Parameters:
      t1 - floating-point term
      t2 - floating-point term Remarks: Note that this is IEEE 754 equality (as opposed to standard =).
      Throws:
      Z3Exception

    • mkFPIsNormal

      public BoolExpr mkFPIsNormal(Expr<FPSort> t)
      Predicate indicating whether t is a normal floating-point number.\
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPIsSubnormal

      public BoolExpr mkFPIsSubnormal(Expr<FPSort> t)
      Predicate indicating whether t is a subnormal floating-point number.\
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPIsZero

      public BoolExpr mkFPIsZero(Expr<FPSort> t)
      Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPIsInfinite

      public BoolExpr mkFPIsInfinite(Expr<FPSort> t)
      Predicate indicating whether t is a floating-point number representing +oo or -oo.
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPIsNaN

      public BoolExpr mkFPIsNaN(Expr<FPSort> t)
      Predicate indicating whether t is a NaN.
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPIsNegative

      public BoolExpr mkFPIsNegative(Expr<FPSort> t)
      Predicate indicating whether t is a negative floating-point number.
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFPIsPositive

      public BoolExpr mkFPIsPositive(Expr<FPSort> t)
      Predicate indicating whether t is a positive floating-point number.
      Parameters:
      t - floating-point term
      Throws:
      Z3Exception

    • mkFP

      public FPExpr mkFP(Expr<BitVecSort> sgn, Expr<BitVecSort> sig, Expr<BitVecSort> exp)
      Create an expression of FloatingPoint sort from three bit-vector expressions.
      Parameters:
      sgn - bit-vector term (of size 1) representing the sign.
      sig - bit-vector term representing the significand.
      exp - bit-vector term representing the exponent. Remarks: This is the operator named `fp' in the SMT FP theory definition. Note that sgn is required to be a bit-vector of size 1. Significand and exponent are required to be greater than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments.
      Throws:
      Z3Exception

    • mkFPToFP

      public FPExpr mkFPToFP(Expr<BitVecSort> bv, FPSort s)
      Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
      Parameters:
      bv - bit-vector value (of size m).
      s - FloatingPoint sort (ebits+sbits == m) Remarks: Produces a term that represents the conversion of a bit-vector term bv to a floating-point term of sort s. The bit-vector size of bv (m) must be equal to ebits+sbits of s. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.
      Throws:
      Z3Exception

    • mkFPToFP

      public FPExpr mkFPToFP(Expr<FPRMSort> rm, FPExpr t, FPSort s)
      Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
      Parameters:
      rm - RoundingMode term.
      t - FloatingPoint term.
      s - FloatingPoint sort. Remarks: Produces a term that represents the conversion of a floating-point term t to a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.
      Throws:
      Z3Exception

    • mkFPToFP

      public FPExpr mkFPToFP(Expr<FPRMSort> rm, RealExpr t, FPSort s)
      Conversion of a term of real sort into a term of FloatingPoint sort.
      Parameters:
      rm - RoundingMode term.
      t - term of Real sort.
      s - FloatingPoint sort. Remarks: Produces a term that represents the conversion of term t of real sort into a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.
      Throws:
      Z3Exception

    • mkFPToFP

      public FPExpr mkFPToFP(Expr<FPRMSort> rm, Expr<BitVecSort> t, FPSort s, boolean signed)
      Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
      Parameters:
      rm - RoundingMode term.
      t - term of bit-vector sort.
      s - FloatingPoint sort.
      signed - flag indicating whether t is interpreted as signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the bit-vector term t into a floating-point term of sort s. The bit-vector t is taken to be in signed 2's complement format (when signed==true, otherwise unsigned). If necessary, the result will be rounded according to rounding mode rm.
      Throws:
      Z3Exception

    • mkFPToFP

      public FPExpr mkFPToFP(FPSort s, Expr<FPRMSort> rm, Expr<FPSort> t)
      Conversion of a floating-point number to another FloatingPoint sort s.
      Parameters:
      s - FloatingPoint sort
      rm - floating-point rounding mode term
      t - floating-point term Remarks: Produces a term that represents the conversion of a floating-point term t to a different FloatingPoint sort s. If necessary, rounding according to rm is applied.
      Throws:
      Z3Exception

    • mkFPToBV

      public BitVecExpr mkFPToBV(Expr<FPRMSort> rm, Expr<FPSort> t, int sz, boolean signed)
      Conversion of a floating-point term into a bit-vector.
      Parameters:
      rm - RoundingMode term.
      t - FloatingPoint term
      sz - Size of the resulting bit-vector.
      signed - Indicates whether the result is a signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the floating-point term t into a bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm.
      Throws:
      Z3Exception

    • mkFPToReal

      public RealExpr mkFPToReal(Expr<FPSort> t)
      Conversion of a floating-point term into a real-numbered term.
      Parameters:
      t - FloatingPoint term Remarks: Produces a term that represents the conversion of the floating-point term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.
      Throws:
      Z3Exception

    • mkFPToIEEEBV

      public BitVecExpr mkFPToIEEEBV(Expr<FPSort> t)
      Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
      Parameters:
      t - FloatingPoint term. Remarks: The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.
      Throws:
      Z3Exception

    • mkFPToFP

      public BitVecExpr mkFPToFP(Expr<FPRMSort> rm, Expr<IntSort> exp, Expr<RealSort> sig, FPSort s)
      Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
      Parameters:
      rm - RoundingMode term.
      exp - Exponent term of Int sort.
      sig - Significand term of Real sort.
      s - FloatingPoint sort. Remarks: Produces a term that represents the conversion of sig * 2^exp into a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.
      Throws:
      Z3Exception

    • mkLinearOrder

      public <R extends Sort> FuncDecl<BoolSort> mkLinearOrder(R sort, int index)
      Creates or a linear order.
      Parameters:
      index - The index of the order.
      sort - The sort of the order.

    • mkPartialOrder

      public <R extends Sort> FuncDecl<BoolSort> mkPartialOrder(R sort, int index)
      Creates or a partial order.
      Parameters:
      index - The index of the order.
      sort - The sort of the order.

    • wrapAST

      public AST wrapAST(long nativeObject)
      Wraps an AST. Remarks: This function is used for transitions between native and managed objects. Note that nativeObject must be a native object obtained from Z3 (e.g., through UnwrapAST) and that it must have a correct reference count.
      Parameters:
      nativeObject - The native pointer to wrap.
      See Also:

    • unwrapAST

      public long unwrapAST(AST a)
      Unwraps an AST. Remarks: This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,
      Parameters:
      a - The AST to unwrap.
      See Also:

    • SimplifyHelp

      public String SimplifyHelp()
      Return a string describing all available parameters to Expr.Simplify.

    • getSimplifyParameterDescriptions

      public ParamDescrs getSimplifyParameterDescriptions()
      Retrieves parameter descriptions for simplifier.

    • updateParamValue

      public void updateParamValue(String id, String value)
      Update a mutable configuration parameter. Remarks: The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -ini? Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

    • nCtx

      public long nCtx()

    • getConstructorDRQ

      public IDecRefQueue<Constructor<?>> getConstructorDRQ()

    • getConstructorListDRQ

      public IDecRefQueue<ConstructorList<?>> getConstructorListDRQ()

    • getASTDRQ

      public IDecRefQueue<AST> getASTDRQ()

    • getASTMapDRQ

      public IDecRefQueue<com.microsoft.z3.ASTMap> getASTMapDRQ()

    • getASTVectorDRQ

      public IDecRefQueue<ASTVector> getASTVectorDRQ()

    • getApplyResultDRQ

      public IDecRefQueue<ApplyResult> getApplyResultDRQ()

    • getFuncEntryDRQ

      public IDecRefQueue<FuncInterp.Entry<?>> getFuncEntryDRQ()

    • getFuncInterpDRQ

      public IDecRefQueue<FuncInterp<?>> getFuncInterpDRQ()

    • getGoalDRQ

      public IDecRefQueue<Goal> getGoalDRQ()

    • getModelDRQ

      public IDecRefQueue<Model> getModelDRQ()

    • getParamsDRQ

      public IDecRefQueue<Params> getParamsDRQ()

    • getParamDescrsDRQ

      public IDecRefQueue<ParamDescrs> getParamDescrsDRQ()

    • getProbeDRQ

      public IDecRefQueue<Probe> getProbeDRQ()

    • getSolverDRQ

      public IDecRefQueue<Solver> getSolverDRQ()

    • getStatisticsDRQ

      public IDecRefQueue<Statistics> getStatisticsDRQ()

    • getTacticDRQ

      public IDecRefQueue<Tactic> getTacticDRQ()

    • getFixedpointDRQ

      public IDecRefQueue<Fixedpoint> getFixedpointDRQ()

    • getOptimizeDRQ

      public IDecRefQueue<Optimize> getOptimizeDRQ()

    • close

      public void close()
      Disposes of the context.
      Specified by:
      close in interface AutoCloseable