Package com.microsoft.z3

Class Context

  • All Implemented Interfaces:
    java.lang.AutoCloseable
    public class Context
extends java.lang.Object
implements java.lang.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 Detail

      • Context

        public Context()

      • Context

        protected Context​(long m_ctx)

      • Context

        public Context​(java.util.Map<java.lang.String,​java.lang.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 Detail

      • 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​(java.lang.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​(java.lang.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​(java.lang.String name,
                                  java.lang.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​(java.lang.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​(java.lang.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​(java.lang.String name,
                                        java.lang.String recognizer,
                                        java.lang.String[] fieldNames,
                                        Sort[] sorts,
                                        int[] sortRefs)
        Create a datatype constructor.

      • mkDatatypeSort

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

      • mkDatatypeSorts

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

      • mkDatatypeSorts

        public DatatypeSort<java.lang.Object>[] mkDatatypeSorts​(java.lang.String[] names,
                                                        Constructor<java.lang.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​(java.lang.String name,
                                               Sort[] domain,
                                               R range)
        Creates a new function declaration.

      • mkFuncDecl

        public <R extends Sort> FuncDecl<R> mkFuncDecl​(java.lang.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.

      • 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​(java.lang.String name,
                                                R range)
        Creates a new constant function declaration.

      • 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​(java.lang.String name,
                                        R range)
        Creates a new Constant of sort range and named name.

      • mkFreshConst

        public <R extends Sort> Expr<R> mkFreshConst​(java.lang.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​(java.lang.String name)
        Create a Boolean constant.

      • mkIntConst

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

      • mkIntConst

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

      • mkRealConst

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

      • mkRealConst

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

      • mkBVConst

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

      • mkBVConst

        public BitVecExpr mkBVConst​(java.lang.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.

      • 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

      • 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.

      • 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.

      • mkBVNeg

        public BitVecExpr mkBVNeg​(Expr<BitVecSort> t)
        Standard two's complement unary minus. Remarks: The arguments must have a 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.

      • 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.

      • 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.

      • 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​(java.lang.String name,
                                                                               D domain,
                                                                               R range)
        Create an array constant.

      • 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:
        mkArraySort(Sort[], Sort), mkSelect(com.microsoft.z3.Expr<com.microsoft.z3.ArraySort<D, R>>, com.microsoft.z3.Expr<D>)

      • 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.

      • 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​(java.lang.String s)
        Create a string constant.

      • 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.

      • mkToRe

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

      • mkStar

        public <R extends Sort> ReExpr<R> mkStar​(Expr<ReSort<R>> re)
        Take the Kleene star of a 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.

      • 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

      • 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​(java.lang.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:
        mkNumeral(String,Sort)

      • mkReal

        public RatNum mkReal​(java.lang.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​(java.lang.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​(java.lang.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:
        #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

      • 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:
        #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

      • 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:
        #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

      • 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:
        #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

      • 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:
        #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)

      • 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:
        AST.toString(), Pattern.toString(), FuncDecl.toString(), Sort.toString()

      • benchmarkToSMTString

        public java.lang.String benchmarkToSMTString​(java.lang.String name,
                                             java.lang.String logic,
                                             java.lang.String status,
                                             java.lang.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​(java.lang.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.

      • 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 java.lang.String[] getTacticNames()
        The names of all supported tactics.

      • getTacticDescription

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

      • mkTactic

        public Tactic mkTactic​(java.lang.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 java.lang.String[] getProbeNames()
        The names of all supported Probes.

      • getProbeDescription

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

      • mkProbe

        public Probe mkProbe​(java.lang.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​(java.lang.String logic)
        Creates a new (incremental) solver.
        See Also:
        mkSolver(Symbol)

      • 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

      • 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

      • 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

      • 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

      • 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:
        Native.incRef(long, long), unwrapAST(com.microsoft.z3.AST)

      • 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:
        Native.incRef(long, long), wrapAST(long)

      • SimplifyHelp

        public java.lang.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​(java.lang.String id,
                             java.lang.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()

      • getASTMapDRQ

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

      • close

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