Z3
Public Member Functions | Protected Member Functions
Context Class Reference
+ Inheritance diagram for Context:

Public Member Functions

 Context ()
 
 Context (Map< String, String > settings)
 
IntSymbol mkSymbol (int i)
 
StringSymbol mkSymbol (String name)
 
BoolSort getBoolSort ()
 
IntSort getIntSort ()
 
RealSort getRealSort ()
 
BoolSort mkBoolSort ()
 
CharSort mkCharSort ()
 
SeqSort< CharSort > getStringSort ()
 
UninterpretedSort mkUninterpretedSort (Symbol s)
 
UninterpretedSort mkUninterpretedSort (String str)
 
IntSort mkIntSort ()
 
RealSort mkRealSort ()
 
BitVecSort mkBitVecSort (int size)
 
final< D extends Sort, R extends Sort > ArraySort< D, R > mkArraySort (D domain, R range)
 
final< R extends Sort > ArraySort< Sort, R > mkArraySort (Sort[] domains, R range)
 
SeqSort< CharSort > mkStringSort ()
 
final< R extends Sort > SeqSort< R > mkSeqSort (R s)
 
final< R extends Sort > ReSort< R > mkReSort (R s)
 
TupleSort mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 
final< R > EnumSort< R > mkEnumSort (Symbol name, Symbol... enumNames)
 
final< R > EnumSort< R > mkEnumSort (String name, String... enumNames)
 
final< R extends Sort > ListSort< R > mkListSort (Symbol name, R elemSort)
 
final< R extends Sort > ListSort< R > mkListSort (String name, R elemSort)
 
final< R > FiniteDomainSort< R > mkFiniteDomainSort (Symbol name, long size)
 
final< R > FiniteDomainSort< R > mkFiniteDomainSort (String name, long size)
 
final< R > Constructor< R > mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
final< R > Constructor< R > mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
 
final< R > DatatypeSort< R > mkDatatypeSort (Symbol name, Constructor< R >[] constructors)
 
final< R > DatatypeSort< R > mkDatatypeSort (String name, Constructor< R >[] constructors)
 
DatatypeSort< Object >[] mkDatatypeSorts (Symbol[] names, Constructor< Object >[][] c)
 
DatatypeSort< Object >[] mkDatatypeSorts (String[] names, Constructor< Object >[][] c)
 
final< F extends Sort, R extends Sort > Expr< R > mkUpdateField (FuncDecl< F > field, Expr< R > t, Expr< F > v) throws Z3Exception
 
final< R extends Sort > FuncDecl< R > mkFuncDecl (Symbol name, Sort[] domain, R range)
 
final< R extends Sort > FuncDecl< R > mkPropagateFunction (Symbol name, Sort[] domain, R range)
 
final< R extends Sort > FuncDecl< R > mkFuncDecl (Symbol name, Sort domain, R range)
 
final< R extends Sort > FuncDecl< R > mkFuncDecl (String name, Sort[] domain, R range)
 
final< R extends Sort > FuncDecl< R > mkFuncDecl (String name, Sort domain, R range)
 
final< R extends Sort > FuncDecl< R > mkRecFuncDecl (Symbol name, Sort[] domain, R range)
 
final< R extends Sort > void AddRecDef (FuncDecl< R > f, Expr<?>[] args, Expr< R > body)
 
final< R extends Sort > FuncDecl< R > mkFreshFuncDecl (String prefix, Sort[] domain, R range)
 
final< R extends Sort > FuncDecl< R > mkConstDecl (Symbol name, R range)
 
final< R extends Sort > FuncDecl< R > mkConstDecl (String name, R range)
 
final< R extends Sort > FuncDecl< R > mkFreshConstDecl (String prefix, R range)
 
final< R extends Sort > Expr< R > mkBound (int index, R ty)
 
final Pattern mkPattern (Expr<?>... terms)
 
final< R extends Sort > Expr< R > mkConst (Symbol name, R range)
 
final< R extends Sort > Expr< R > mkConst (String name, R range)
 
final< R extends Sort > Expr< R > mkFreshConst (String prefix, R range)
 
final< R extends Sort > Expr< R > mkConst (FuncDecl< R > f)
 
BoolExpr mkBoolConst (Symbol name)
 
BoolExpr mkBoolConst (String name)
 
IntExpr mkIntConst (Symbol name)
 
IntExpr mkIntConst (String name)
 
RealExpr mkRealConst (Symbol name)
 
RealExpr mkRealConst (String name)
 
BitVecExpr mkBVConst (Symbol name, int size)
 
BitVecExpr mkBVConst (String name, int size)
 
final< R extends Sort > Expr< R > mkApp (FuncDecl< R > f, Expr<?>... args)
 
BoolExpr mkTrue ()
 
BoolExpr mkFalse ()
 
BoolExpr mkBool (boolean value)
 
BoolExpr mkEq (Expr<?> x, Expr<?> y)
 
final BoolExpr mkDistinct (Expr<?>... args)
 
final BoolExpr mkNot (Expr< BoolSort > a)
 
final< R extends Sort > Expr< R > mkITE (Expr< BoolSort > t1, Expr<? extends R > t2, Expr<? extends R > t3)
 
BoolExpr mkIff (Expr< BoolSort > t1, Expr< BoolSort > t2)
 
BoolExpr mkImplies (Expr< BoolSort > t1, Expr< BoolSort > t2)
 
BoolExpr mkXor (Expr< BoolSort > t1, Expr< BoolSort > t2)
 
final BoolExpr mkAnd (Expr< BoolSort >... t)
 
final BoolExpr mkOr (Expr< BoolSort >... t)
 
final< R extends ArithSort > ArithExpr< R > mkAdd (Expr<? extends R >... t)
 
final< R extends ArithSort > ArithExpr< R > mkMul (Expr<? extends R >... t)
 
final< R extends ArithSort > ArithExpr< R > mkSub (Expr<? extends R >... t)
 
final< R extends ArithSort > ArithExpr< R > mkUnaryMinus (Expr< R > t)
 
final< R extends ArithSort > ArithExpr< R > mkDiv (Expr<? extends R > t1, Expr<? extends R > t2)
 
IntExpr mkMod (Expr< IntSort > t1, Expr< IntSort > t2)
 
IntExpr mkRem (Expr< IntSort > t1, Expr< IntSort > t2)
 
final< R extends ArithSort > ArithExpr< R > mkPower (Expr<? extends R > t1, Expr<? extends R > t2)
 
BoolExpr mkLt (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
BoolExpr mkLe (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
BoolExpr mkGt (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
BoolExpr mkGe (Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
 
RealExpr mkInt2Real (Expr< IntSort > t)
 
IntExpr mkReal2Int (Expr< RealSort > t)
 
BoolExpr mkIsInteger (Expr< RealSort > t)
 
BitVecExpr mkBVNot (Expr< BitVecSort > t)
 
BitVecExpr mkBVRedAND (Expr< BitVecSort > t)
 
BitVecExpr mkBVRedOR (Expr< BitVecSort > t)
 
BitVecExpr mkBVAND (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVXOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVNAND (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVNOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVXNOR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVNeg (Expr< BitVecSort > t)
 
BitVecExpr mkBVAdd (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSub (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVMul (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVUDiv (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSDiv (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVURem (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSRem (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVSMod (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVULT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSLT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVULE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSLE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVUGE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSGE (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVUGT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSGT (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkConcat (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkExtract (int high, int low, Expr< BitVecSort > t)
 
BitVecExpr mkSignExt (int i, Expr< BitVecSort > t)
 
BitVecExpr mkZeroExt (int i, Expr< BitVecSort > t)
 
BitVecExpr mkRepeat (int i, Expr< BitVecSort > t)
 
BitVecExpr mkBVSHL (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVLSHR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVASHR (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVRotateLeft (int i, Expr< BitVecSort > t)
 
BitVecExpr mkBVRotateRight (int i, Expr< BitVecSort > t)
 
BitVecExpr mkBVRotateLeft (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkBVRotateRight (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BitVecExpr mkInt2BV (int n, Expr< IntSort > t)
 
IntExpr mkBV2Int (Expr< BitVecSort > t, boolean signed)
 
BoolExpr mkBVAddNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
 
BoolExpr mkBVAddNoUnderflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSubNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVSubNoUnderflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
 
BoolExpr mkBVSDivNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
BoolExpr mkBVNegNoOverflow (Expr< BitVecSort > t)
 
BoolExpr mkBVMulNoOverflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
 
BoolExpr mkBVMulNoUnderflow (Expr< BitVecSort > t1, Expr< BitVecSort > t2)
 
final< D extends Sort, R extends Sort > ArrayExpr< D, R > mkArrayConst (Symbol name, D domain, R range)
 
final< D extends Sort, R extends Sort > ArrayExpr< D, R > mkArrayConst (String name, D domain, R range)
 
final< D extends Sort, R extends Sort > Expr< R > mkSelect (Expr< ArraySort< D, R >> a, Expr< D > i)
 
final< R extends Sort > Expr< R > mkSelect (Expr< ArraySort< Sort, R >> a, Expr<?>[] args)
 
final< D extends Sort, R extends Sort > ArrayExpr< D, R > mkStore (Expr< ArraySort< D, R >> a, Expr< D > i, Expr< R > v)
 
final< R extends Sort > ArrayExpr< Sort, R > mkStore (Expr< ArraySort< Sort, R >> a, Expr<?>[] args, Expr< R > v)
 
final< D extends Sort, R extends Sort > ArrayExpr< D, R > mkConstArray (D domain, Expr< R > v)
 
final< D extends Sort, R1 extends Sort, R2 extends Sort > ArrayExpr< D, R2 > mkMap (FuncDecl< R2 > f, Expr< ArraySort< D, R1 >>... args)
 
final< D extends Sort, R extends Sort > Expr< R > mkTermArray (Expr< ArraySort< D, R >> array)
 
final< D extends Sort, R extends Sort > Expr< D > mkArrayExt (Expr< ArraySort< D, R >> arg1, Expr< ArraySort< D, R >> arg2)
 
final< D extends Sort > SetSort< D > mkSetSort (D ty)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkEmptySet (D domain)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkFullSet (D domain)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetAdd (Expr< ArraySort< D, BoolSort >> set, Expr< D > element)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetDel (Expr< ArraySort< D, BoolSort >> set, Expr< D > element)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetUnion (Expr< ArraySort< D, BoolSort >>... args)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetIntersection (Expr< ArraySort< D, BoolSort >>... args)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetDifference (Expr< ArraySort< D, BoolSort >> arg1, Expr< ArraySort< D, BoolSort >> arg2)
 
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetComplement (Expr< ArraySort< D, BoolSort >> arg)
 
final< D extends Sort > BoolExpr mkSetMembership (Expr< D > elem, Expr< ArraySort< D, BoolSort >> set)
 
final< D extends Sort > BoolExpr mkSetSubset (Expr< ArraySort< D, BoolSort >> arg1, Expr< ArraySort< D, BoolSort >> arg2)
 
final< R extends Sort > SeqExpr< R > mkEmptySeq (R s)
 
final< R extends Sort > SeqExpr< R > mkUnit (Expr< R > elem)
 
SeqExpr< CharSort > mkString (String s)
 
SeqExpr< CharSort > intToString (Expr< IntSort > e)
 
SeqExpr< CharSort > ubvToString (Expr< BitVecSort > e)
 
SeqExpr< CharSort > sbvToString (Expr< BitVecSort > e)
 
IntExpr stringToInt (Expr< SeqSort< CharSort >> e)
 
final< R extends Sort > SeqExpr< R > mkConcat (Expr< SeqSort< R >>... t)
 
final< R extends Sort > IntExpr mkLength (Expr< SeqSort< R >> s)
 
final< R extends Sort > BoolExpr mkPrefixOf (Expr< SeqSort< R >> s1, Expr< SeqSort< R >> s2)
 
final< R extends Sort > BoolExpr mkSuffixOf (Expr< SeqSort< R >> s1, Expr< SeqSort< R >> s2)
 
final< R extends Sort > BoolExpr mkContains (Expr< SeqSort< R >> s1, Expr< SeqSort< R >> s2)
 
BoolExpr MkStringLt (Expr< SeqSort< CharSort >> s1, Expr< SeqSort< CharSort >> s2)
 
BoolExpr MkStringLe (Expr< SeqSort< CharSort >> s1, Expr< SeqSort< CharSort >> s2)
 
final< R extends Sort > SeqExpr< R > mkAt (Expr< SeqSort< R >> s, Expr< IntSort > index)
 
final< R extends Sort > Expr< R > mkNth (Expr< SeqSort< R >> s, Expr< IntSort > index)
 
final< R extends Sort > SeqExpr< R > mkExtract (Expr< SeqSort< R >> s, Expr< IntSort > offset, Expr< IntSort > length)
 
final< R extends Sort > IntExpr mkIndexOf (Expr< SeqSort< R >> s, Expr< SeqSort< R >> substr, Expr< IntSort > offset)
 
final< R extends Sort > SeqExpr< R > mkReplace (Expr< SeqSort< R >> s, Expr< SeqSort< R >> src, Expr< SeqSort< R >> dst)
 
final< R extends Sort > ReExpr< SeqSort< R > > mkToRe (Expr< SeqSort< R >> s)
 
final< R extends Sort > BoolExpr mkInRe (Expr< SeqSort< R >> s, ReExpr< SeqSort< R >> re)
 
final< R extends Sort > ReExpr< R > mkStar (Expr< ReSort< R >> re)
 
final< R extends Sort > ReExpr< R > mkPower (Expr< ReSort< R >> re, int n)
 
final< R extends Sort > ReExpr< R > mkLoop (Expr< ReSort< R >> re, int lo, int hi)
 
final< R extends Sort > ReExpr< R > mkLoop (Expr< ReSort< R >> re, int lo)
 
final< R extends Sort > ReExpr< R > mkPlus (Expr< ReSort< R >> re)
 
final< R extends Sort > ReExpr< R > mkOption (Expr< ReSort< R >> re)
 
final< R extends Sort > ReExpr< R > mkComplement (Expr< ReSort< R >> re)
 
final< R extends Sort > ReExpr< R > mkConcat (ReExpr< R >... t)
 
final< R extends Sort > ReExpr< R > mkUnion (Expr< ReSort< R >>... t)
 
final< R extends Sort > ReExpr< R > mkIntersect (Expr< ReSort< R >>... t)
 
final< R extends Sort > ReExpr< R > mkDiff (Expr< ReSort< R >> a, Expr< ReSort< R >> b)
 
final< R extends Sort > ReExpr< R > mkEmptyRe (ReSort< R > s)
 
final< R extends Sort > ReExpr< R > mkFullRe (ReSort< R > s)
 
final< R extends Sort > ReExpr< R > mkAllcharRe (ReSort< R > s)
 
final ReExpr< SeqSort< CharSort > > mkRange (Expr< SeqSort< CharSort >> lo, Expr< SeqSort< CharSort >> hi)
 
BoolExpr mkCharLe (Expr< CharSort > ch1, Expr< CharSort > ch2)
 
IntExpr charToInt (Expr< CharSort > ch)
 
BitVecExpr charToBv (Expr< CharSort > ch)
 
Expr< CharSort > charFromBv (BitVecExpr bv)
 
BoolExpr mkIsDigit (Expr< CharSort > ch)
 
BoolExpr mkAtMost (Expr< BoolSort >[] args, int k)
 
BoolExpr mkAtLeast (Expr< BoolSort >[] args, int k)
 
BoolExpr mkPBLe (int[] coeffs, Expr< BoolSort >[] args, int k)
 
BoolExpr mkPBGe (int[] coeffs, Expr< BoolSort >[] args, int k)
 
BoolExpr mkPBEq (int[] coeffs, Expr< BoolSort >[] args, int k)
 
final< R extends Sort > Expr< R > mkNumeral (String v, R ty)
 
final< R extends Sort > Expr< R > mkNumeral (int v, R ty)
 
final< R extends Sort > Expr< R > mkNumeral (long v, R ty)
 
RatNum mkReal (int num, int den)
 
RatNum mkReal (String v)
 
RatNum mkReal (int v)
 
RatNum mkReal (long v)
 
IntNum mkInt (String v)
 
IntNum mkInt (int v)
 
IntNum mkInt (long v)
 
BitVecNum mkBV (String v, int size)
 
BitVecNum mkBV (int v, int size)
 
BitVecNum mkBV (long v, int size)
 
Quantifier mkForall (Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkForall (Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkExists (Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
Quantifier mkQuantifier (boolean universal, Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
final< R extends Sort > Lambda< R > mkLambda (Sort[] sorts, Symbol[] names, Expr< R > body)
 
final< R extends Sort > Lambda< R > mkLambda (Expr<?>[] boundConstants, Expr< R > body)
 
void setPrintMode (Z3_ast_print_mode value)
 
String benchmarkToSMTString (String name, String logic, String status, String attributes, Expr< BoolSort >[] assumptions, Expr< BoolSort > formula)
 
BoolExpr[] parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
 
BoolExpr[] parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
 
Goal mkGoal (boolean models, boolean unsatCores, boolean proofs)
 
Params mkParams ()
 
int getNumTactics ()
 
String[] getTacticNames ()
 
String getTacticDescription (String name)
 
Tactic mkTactic (String name)
 
Tactic andThen (Tactic t1, Tactic t2, Tactic... ts)
 
Tactic then (Tactic t1, Tactic t2, Tactic... ts)
 
Tactic orElse (Tactic t1, Tactic t2)
 
Tactic tryFor (Tactic t, int ms)
 
Tactic when (Probe p, Tactic t)
 
Tactic cond (Probe p, Tactic t1, Tactic t2)
 
Tactic repeat (Tactic t, int max)
 
Tactic skip ()
 
Tactic fail ()
 
Tactic failIf (Probe p)
 
Tactic failIfNotDecided ()
 
Tactic usingParams (Tactic t, Params p)
 
Tactic with (Tactic t, Params p)
 
Tactic parOr (Tactic... t)
 
Tactic parAndThen (Tactic t1, Tactic t2)
 
void interrupt ()
 
int getNumSimplifiers ()
 
String[] getSimplifierNames ()
 
String getSimplifierDescription (String name)
 
Simplifier mkSimplifier (String name)
 
Simplifier andThen (Simplifier t1, Simplifier t2, Simplifier... ts)
 
Simplifier then (Simplifier t1, Simplifier t2, Simplifier... ts)
 
Simplifier usingParams (Simplifier t, Params p)
 
Simplifier with (Simplifier t, Params p)
 
int getNumProbes ()
 
String[] getProbeNames ()
 
String getProbeDescription (String name)
 
Probe mkProbe (String name)
 
Probe constProbe (double val)
 
Probe lt (Probe p1, Probe p2)
 
Probe gt (Probe p1, Probe p2)
 
Probe le (Probe p1, Probe p2)
 
Probe ge (Probe p1, Probe p2)
 
Probe eq (Probe p1, Probe p2)
 
Probe and (Probe p1, Probe p2)
 
Probe or (Probe p1, Probe p2)
 
Probe not (Probe p)
 
Solver mkSolver ()
 
Solver mkSolver (Symbol logic)
 
Solver mkSolver (String logic)
 
Solver mkSimpleSolver ()
 
Solver mkSolver (Tactic t)
 
Solver mkSolver (Solver s, Simplifier simp)
 
Fixedpoint mkFixedpoint ()
 
Optimize mkOptimize ()
 
FPRMSort mkFPRoundingModeSort ()
 
FPRMExpr mkFPRoundNearestTiesToEven ()
 
FPRMNum mkFPRNE ()
 
FPRMNum mkFPRoundNearestTiesToAway ()
 
FPRMNum mkFPRNA ()
 
FPRMNum mkFPRoundTowardPositive ()
 
FPRMNum mkFPRTP ()
 
FPRMNum mkFPRoundTowardNegative ()
 
FPRMNum mkFPRTN ()
 
FPRMNum mkFPRoundTowardZero ()
 
FPRMNum mkFPRTZ ()
 
FPSort mkFPSort (int ebits, int sbits)
 
FPSort mkFPSortHalf ()
 
FPSort mkFPSort16 ()
 
FPSort mkFPSortSingle ()
 
FPSort mkFPSort32 ()
 
FPSort mkFPSortDouble ()
 
FPSort mkFPSort64 ()
 
FPSort mkFPSortQuadruple ()
 
FPSort mkFPSort128 ()
 
FPNum mkFPNaN (FPSort s)
 
FPNum mkFPInf (FPSort s, boolean negative)
 
FPNum mkFPZero (FPSort s, boolean negative)
 
FPNum mkFPNumeral (float v, FPSort s)
 
FPNum mkFPNumeral (double v, FPSort s)
 
FPNum mkFPNumeral (int v, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFPNumeral (boolean sgn, long exp, long sig, FPSort s)
 
FPNum mkFP (float v, FPSort s)
 
FPNum mkFP (double v, FPSort s)
 
FPNum mkFP (int v, FPSort s)
 
FPNum mkFP (boolean sgn, int exp, int sig, FPSort s)
 
FPNum mkFP (boolean sgn, long exp, long sig, FPSort s)
 
FPExpr mkFPAbs (Expr< FPSort > t)
 
FPExpr mkFPNeg (Expr< FPSort > t)
 
FPExpr mkFPAdd (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPSub (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPMul (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPDiv (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPFMA (Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2, Expr< FPSort > t3)
 
FPExpr mkFPSqrt (Expr< FPRMSort > rm, Expr< FPSort > t)
 
FPExpr mkFPRem (Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPRoundToIntegral (Expr< FPRMSort > rm, Expr< FPSort > t)
 
FPExpr mkFPMin (Expr< FPSort > t1, Expr< FPSort > t2)
 
FPExpr mkFPMax (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPLEq (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPLt (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPGEq (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPGt (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPEq (Expr< FPSort > t1, Expr< FPSort > t2)
 
BoolExpr mkFPIsNormal (Expr< FPSort > t)
 
BoolExpr mkFPIsSubnormal (Expr< FPSort > t)
 
BoolExpr mkFPIsZero (Expr< FPSort > t)
 
BoolExpr mkFPIsInfinite (Expr< FPSort > t)
 
BoolExpr mkFPIsNaN (Expr< FPSort > t)
 
BoolExpr mkFPIsNegative (Expr< FPSort > t)
 
BoolExpr mkFPIsPositive (Expr< FPSort > t)
 
FPExpr mkFP (Expr< BitVecSort > sgn, Expr< BitVecSort > sig, Expr< BitVecSort > exp)
 
FPExpr mkFPToFP (Expr< BitVecSort > bv, FPSort s)
 
FPExpr mkFPToFP (Expr< FPRMSort > rm, FPExpr t, FPSort s)
 
FPExpr mkFPToFP (Expr< FPRMSort > rm, RealExpr t, FPSort s)
 
FPExpr mkFPToFP (Expr< FPRMSort > rm, Expr< BitVecSort > t, FPSort s, boolean signed)
 
FPExpr mkFPToFP (FPSort s, Expr< FPRMSort > rm, Expr< FPSort > t)
 
BitVecExpr mkFPToBV (Expr< FPRMSort > rm, Expr< FPSort > t, int sz, boolean signed)
 
RealExpr mkFPToReal (Expr< FPSort > t)
 
BitVecExpr mkFPToIEEEBV (Expr< FPSort > t)
 
BitVecExpr mkFPToFP (Expr< FPRMSort > rm, Expr< IntSort > exp, Expr< RealSort > sig, FPSort s)
 
final< R extends Sort > FuncDecl< BoolSort > mkLinearOrder (R sort, int index)
 
final< R extends Sort > FuncDecl< BoolSort > mkPartialOrder (R sort, int index)
 
AST wrapAST (long nativeObject)
 
long unwrapAST (AST a)
 
String SimplifyHelp ()
 
ParamDescrs getSimplifyParameterDescriptions ()
 
void updateParamValue (String id, String value)
 
long nCtx ()
 
void close ()
 

Protected Member Functions

 Context (long m_ctx)
 

Detailed Description

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.

Definition at line 36 of file Context.java.

Constructor & Destructor Documentation

◆ Context() [1/3]

Context ( )
inline

Definition at line 40 of file Context.java.

40  {
41  synchronized (creation_lock) {
42  m_ctx = Native.mkContextRc(0);
43  init();
44  }
45  }

◆ Context() [2/3]

Context ( long  m_ctx)
inlineprotected

Definition at line 47 of file Context.java.

47  {
48  synchronized (creation_lock) {
49  this.m_ctx = m_ctx;
50  init();
51  }
52  }

◆ Context() [3/3]

Context ( Map< String, String >  settings)
inline

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

Definition at line 72 of file Context.java.

72  {
73  synchronized (creation_lock) {
74  long cfg = Native.mkConfig();
75  for (Map.Entry<String, String> kv : settings.entrySet()) {
76  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
77  }
78  m_ctx = Native.mkContextRc(cfg);
79  Native.delConfig(cfg);
80  init();
81  }
82  }
z3py.Map
def Map(f, *args)
Definition: z3py.py:4869
z3py.String
def String(name, ctx=None)
Definition: z3py.py:11061

Member Function Documentation

◆ AddRecDef()

final<R extends Sort> void AddRecDef ( FuncDecl< R >  f,
Expr<?>[]  args,
Expr< R >  body 
)
inline

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.

Definition at line 524 of file Context.java.

525  {
526  checkContextMatch(f);
527  checkContextMatch(args);
528  checkContextMatch(body);
529  long[] argsNative = AST.arrayToNative(args);
530  Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject());
531  }

◆ and()

Probe and ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value

p1

and

p2

evaluate to

true

.

Definition at line 3311 of file Context.java.

3312  {
3313  checkContextMatch(p1);
3314  checkContextMatch(p2);
3315  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3316  p2.getNativeObject()));
3317  }

◆ andThen() [1/2]

Simplifier andThen ( Simplifier  t1,
Simplifier  t2,
Simplifier...  ts 
)
inline

Create a simplifier that applies

t1

and then

t1

Definition at line 3141 of file Context.java.

3143  {
3144  checkContextMatch(t1);
3145  checkContextMatch(t2);
3146  checkContextMatch(ts);
3147 
3148  long last = 0;
3149  if (ts != null && ts.length > 0)
3150  {
3151  last = ts[ts.length - 1].getNativeObject();
3152  for (int i = ts.length - 2; i >= 0; i--) {
3153  last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
3154  last);
3155  }
3156  }
3157  if (last != 0)
3158  {
3159  last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
3160  return new Simplifier(this, Native.simplifierAndThen(nCtx(),
3161  t1.getNativeObject(), last));
3162  } else
3163  return new Simplifier(this, Native.simplifierAndThen(nCtx(),
3164  t1.getNativeObject(), t2.getNativeObject()));
3165  }

◆ andThen() [2/2]

Tactic andThen ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Definition at line 2907 of file Context.java.

2909  {
2910  checkContextMatch(t1);
2911  checkContextMatch(t2);
2912  checkContextMatch(ts);
2913 
2914  long last = 0;
2915  if (ts != null && ts.length > 0)
2916  {
2917  last = ts[ts.length - 1].getNativeObject();
2918  for (int i = ts.length - 2; i >= 0; i--) {
2919  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2920  last);
2921  }
2922  }
2923  if (last != 0)
2924  {
2925  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2926  return new Tactic(this, Native.tacticAndThen(nCtx(),
2927  t1.getNativeObject(), last));
2928  } else
2929  return new Tactic(this, Native.tacticAndThen(nCtx(),
2930  t1.getNativeObject(), t2.getNativeObject()));
2931  }

◆ benchmarkToSMTString()

String benchmarkToSMTString ( String  name,
String  logic,
String  status,
String  attributes,
Expr< BoolSort >[]  assumptions,
Expr< BoolSort >  formula 
)
inline

Convert a benchmark into an SMT-LIB formatted string.

Parameters
nameName of the benchmark. The argument is optional.
logicThe benchmark logic.
statusThe status string (sat, unsat, or unknown)
attributesOther attributes, such as source, difficulty or category.
assumptionsAuxiliary assumptions.
formulaFormula to be checked for consistency in conjunction with assumptions.
Returns
A string representation of the benchmark.

Definition at line 2785 of file Context.java.

2788  {
2789 
2790  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2791  attributes, assumptions.length,
2792  AST.arrayToNative(assumptions), formula.getNativeObject());
2793  }

◆ charFromBv()

Expr<CharSort> charFromBv ( BitVecExpr  bv)
inline

Create a character from a bit-vector (code point).

Definition at line 2377 of file Context.java.

2378  {
2379  checkContextMatch(bv);
2380  return (Expr<CharSort>) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject()));
2381  }

◆ charToBv()

BitVecExpr charToBv ( Expr< CharSort >  ch)
inline

Create a bit-vector (code point) from character.

Definition at line 2368 of file Context.java.

2369  {
2370  checkContextMatch(ch);
2371  return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject()));
2372  }

◆ charToInt()

IntExpr charToInt ( Expr< CharSort >  ch)
inline

Create an integer (code point) from character.

Definition at line 2359 of file Context.java.

2360  {
2361  checkContextMatch(ch);
2362  return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject()));
2363  }

◆ close()

void close ( )
inline

Disposes of the context.

Definition at line 4330 of file Context.java.

4331  {
4332  if (m_ctx == 0)
4333  return;
4334 
4335  m_RefQueue.forceClear();
4336 
4337  m_boolSort = null;
4338  m_intSort = null;
4339  m_realSort = null;
4340  m_stringSort = null;
4341  m_RefQueue = null;
4342 
4343  synchronized (creation_lock) {
4344  Native.delContext(m_ctx);
4345  }
4346  m_ctx = 0;
4347  }

◆ cond()

Tactic cond ( Probe  p,
Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies

t1

to a given goal if the probe

p

evaluates to true and

t2

otherwise.

Definition at line 2989 of file Context.java.

2990  {
2991  checkContextMatch(p);
2992  checkContextMatch(t1);
2993  checkContextMatch(t2);
2994  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2995  t1.getNativeObject(), t2.getNativeObject()));
2996  }

◆ constProbe()

Probe constProbe ( double  val)
inline

Create a probe that always evaluates to

val

.

Definition at line 3241 of file Context.java.

3242  {
3243  return new Probe(this, Native.probeConst(nCtx(), val));
3244  }

◆ eq()

Probe eq ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is equal to the value returned by

p2

Definition at line 3300 of file Context.java.

3301  {
3302  checkContextMatch(p1);
3303  checkContextMatch(p2);
3304  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3305  p2.getNativeObject()));
3306  }

Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), and BoolSortRef.cast().

◆ fail()

Tactic fail ( )
inline

Create a tactic always fails.

Definition at line 3020 of file Context.java.

3021  {
3022  return new Tactic(this, Native.tacticFail(nCtx()));
3023  }

◆ failIf()

Tactic failIf ( Probe  p)
inline

Create a tactic that fails if the probe

p

evaluates to false.

Definition at line 3029 of file Context.java.

3030  {
3031  checkContextMatch(p);
3032  return new Tactic(this,
3033  Native.tacticFailIf(nCtx(), p.getNativeObject()));
3034  }

◆ failIfNotDecided()

Tactic failIfNotDecided ( )
inline

Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’).

Definition at line 3040 of file Context.java.

3041  {
3042  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
3043  }

◆ ge()

Probe ge ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is greater than or equal the value returned by

p2

Definition at line 3288 of file Context.java.

3289  {
3290  checkContextMatch(p1);
3291  checkContextMatch(p2);
3292  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3293  p2.getNativeObject()));
3294  }

◆ getBoolSort()

BoolSort getBoolSort ( )
inline

Retrieves the Boolean sort of the context.

Definition at line 128 of file Context.java.

129  {
130  if (m_boolSort == null) {
131  m_boolSort = new BoolSort(this);
132  }
133  return m_boolSort;
134  }
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1731

◆ getIntSort()

IntSort getIntSort ( )
inline

Retrieves the Integer sort of the context.

Definition at line 139 of file Context.java.

140  {
141  if (m_intSort == null) {
142  m_intSort = new IntSort(this);
143  }
144  return m_intSort;
145  }
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:3188

◆ getNumProbes()

int getNumProbes ( )
inline

The number of supported Probes.

Definition at line 3203 of file Context.java.

3204  {
3205  return Native.getNumProbes(nCtx());
3206  }

◆ getNumSimplifiers()

int getNumSimplifiers ( )
inline

The number of supported simplifiers.

Definition at line 3103 of file Context.java.

3104  {
3105  return Native.getNumSimplifiers(nCtx());
3106  }

◆ getNumTactics()

int getNumTactics ( )
inline

The number of supported tactics.

Definition at line 2868 of file Context.java.

2869  {
2870  return Native.getNumTactics(nCtx());
2871  }

◆ getProbeDescription()

String getProbeDescription ( String  name)
inline

Returns a string containing a description of the probe with the given name.

Definition at line 3225 of file Context.java.

3226  {
3227  return Native.probeGetDescr(nCtx(), name);
3228  }

◆ getProbeNames()

String [] getProbeNames ( )
inline

The names of all supported Probes.

Definition at line 3211 of file Context.java.

3212  {
3213 
3214  int n = getNumProbes();
3215  String[] res = new String[n];
3216  for (int i = 0; i < n; i++)
3217  res[i] = Native.getProbeName(nCtx(), i);
3218  return res;
3219  }

◆ getRealSort()

RealSort getRealSort ( )
inline

Retrieves the Real sort of the context.

Definition at line 150 of file Context.java.

151  {
152  if (m_realSort == null) {
153  m_realSort = new RealSort(this);
154  }
155  return m_realSort;
156  }
z3py.RealSort
def RealSort(ctx=None)
Definition: z3py.py:3205

◆ getSimplifierDescription()

String getSimplifierDescription ( String  name)
inline

Returns a string containing a description of the simplifier with the given name.

Definition at line 3125 of file Context.java.

3126  {
3127  return Native.simplifierGetDescr(nCtx(), name);
3128  }

◆ getSimplifierNames()

String [] getSimplifierNames ( )
inline

The names of all supported simplifiers.

Definition at line 3111 of file Context.java.

3112  {
3113 
3114  int n = getNumSimplifiers();
3115  String[] res = new String[n];
3116  for (int i = 0; i < n; i++)
3117  res[i] = Native.getSimplifierName(nCtx(), i);
3118  return res;
3119  }

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )
inline

Retrieves parameter descriptions for simplifier.

Definition at line 4269 of file Context.java.

4270  {
4271  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
4272  }

◆ getStringSort()

SeqSort<CharSort> getStringSort ( )
inline

Retrieves the String sort of the context.

Definition at line 178 of file Context.java.

179  {
180  if (m_stringSort == null) {
181  m_stringSort = mkStringSort();
182  }
183  return m_stringSort;
184  }
com.microsoft.z3.Context.mkStringSort
SeqSort< CharSort > mkStringSort()
Definition: Context.java:251

◆ getTacticDescription()

String getTacticDescription ( String  name)
inline

Returns a string containing a description of the tactic with the given name.

Definition at line 2890 of file Context.java.

2891  {
2892  return Native.tacticGetDescr(nCtx(), name);
2893  }

◆ getTacticNames()

String [] getTacticNames ( )
inline

The names of all supported tactics.

Definition at line 2876 of file Context.java.

2877  {
2878 
2879  int n = getNumTactics();
2880  String[] res = new String[n];
2881  for (int i = 0; i < n; i++)
2882  res[i] = Native.getTacticName(nCtx(), i);
2883  return res;
2884  }

◆ gt()

Probe gt ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is greater than the value returned by

p2

Definition at line 3262 of file Context.java.

3263  {
3264  checkContextMatch(p1);
3265  checkContextMatch(p2);
3266  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
3267  p2.getNativeObject()));
3268  }

◆ interrupt()

void interrupt ( )
inline

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

Definition at line 3095 of file Context.java.

3096  {
3097  Native.interrupt(nCtx());
3098  }

◆ intToString()

SeqExpr<CharSort> intToString ( Expr< IntSort >  e)
inline

Convert an integer expression to a string.

Definition at line 2048 of file Context.java.

2049  {
2050  return (SeqExpr<CharSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
2051  }

◆ le()

Probe le ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is less than or equal the value returned by

p2

Definition at line 3275 of file Context.java.

3276  {
3277  checkContextMatch(p1);
3278  checkContextMatch(p2);
3279  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
3280  p2.getNativeObject()));
3281  }

◆ lt()

Probe lt ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value returned by

p1

is less than the value returned by

p2

Definition at line 3250 of file Context.java.

3251  {
3252  checkContextMatch(p1);
3253  checkContextMatch(p2);
3254  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
3255  p2.getNativeObject()));
3256  }

◆ mkAdd()

final<R extends ArithSort> ArithExpr<R> mkAdd ( Expr<? extends R >...  t)
inline

Create an expression representing

t[0] + t[1] + ...

.

Definition at line 853 of file Context.java.

854  {
855  checkContextMatch(t);
856  return (ArithExpr<R>) Expr.create(this,
857  Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
858  }

◆ mkAllcharRe()

final<R extends Sort> ReExpr<R> mkAllcharRe ( ReSort< R >  s)
inline

Create regular expression that accepts all characters R has to be a sequence sort. Corresponds to re.allchar

Definition at line 2333 of file Context.java.

2334  {
2335  return (ReExpr<R>) Expr.create(this, Native.mkReAllchar(nCtx(), s.getNativeObject()));
2336  }

◆ mkAnd()

final BoolExpr mkAnd ( Expr< BoolSort >...  t)
inline

Create an expression representing

t[0] and t[1] and ...
com.microsoft.z3.Context.and
Probe and(Probe p1, Probe p2)
Definition: Context.java:3311

.

Definition at line 831 of file Context.java.

832  {
833  checkContextMatch(t);
834  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
835  AST.arrayToNative(t)));
836  }

Referenced by Goal.AsBoolExpr().

◆ mkApp()

final<R extends Sort> Expr<R> mkApp ( FuncDecl< R >  f,
Expr<?>...  args 
)
inline

Create a new function application.

Definition at line 716 of file Context.java.

717  {
718  checkContextMatch(f);
719  checkContextMatch(args);
720  return Expr.create(this, f, args);
721  }

Referenced by ListSort< R extends Sort >.getNil().

◆ mkArrayConst() [1/2]

final<D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst ( String  name,
D  domain,
R  range 
)
inline

Create an array constant.

Definition at line 1720 of file Context.java.

1722  {
1723  return (ArrayExpr<D, R>) mkConst(mkSymbol(name), mkArraySort(domain, range));
1724  }
com.microsoft.z3.Context.mkArraySort
final< D extends Sort, R extends Sort > ArraySort< D, R > mkArraySort(D domain, R range)
Definition: Context.java:230
com.microsoft.z3.Context.mkConst
final< R extends Sort > Expr< R > mkConst(Symbol name, R range)
Definition: Context.java:608
com.microsoft.z3.Context.mkSymbol
IntSymbol mkSymbol(int i)
Definition: Context.java:94
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4136

◆ mkArrayConst() [2/2]

final<D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst ( Symbol  name,
D  domain,
R  range 
)
inline

Create an array constant.

Definition at line 1711 of file Context.java.

1713  {
1714  return (ArrayExpr<D, R>) mkConst(name, mkArraySort(domain, range));
1715  }

◆ mkArrayExt()

final<D extends Sort, R extends Sort> Expr<D> mkArrayExt ( Expr< ArraySort< D, R >>  arg1,
Expr< ArraySort< D, R >>  arg2 
)
inline

Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.

Definition at line 1875 of file Context.java.

1876  {
1877  checkContextMatch(arg1);
1878  checkContextMatch(arg2);
1879  return (Expr<D>) Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1880  }

◆ mkArraySort() [1/2]

final<D extends Sort, R extends Sort> ArraySort<D, R> mkArraySort ( D  domain,
R  range 
)
inline

Create a new array sort.

Definition at line 230 of file Context.java.

231  {
232  checkContextMatch(domain);
233  checkContextMatch(range);
234  return new ArraySort<>(this, domain, range);
235  }

◆ mkArraySort() [2/2]

final<R extends Sort> ArraySort<Sort, R> mkArraySort ( Sort[]  domains,
R  range 
)
inline

Create a new array sort.

Definition at line 241 of file Context.java.

242  {
243  checkContextMatch(domains);
244  checkContextMatch(range);
245  return new ArraySort<>(this, domains, range);
246  }

◆ mkAt()

final<R extends Sort> SeqExpr<R> mkAt ( Expr< SeqSort< R >>  s,
Expr< IntSort >  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2147 of file Context.java.

2148  {
2149  checkContextMatch(s, index);
2150  return (SeqExpr<R>) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2151  }

◆ mkAtLeast()

BoolExpr mkAtLeast ( Expr< BoolSort >[]  args,
int  k 
)
inline

Create an at-least-k constraint.

Definition at line 2404 of file Context.java.

2405  {
2406  checkContextMatch(args);
2407  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2408  }

◆ mkAtMost()

BoolExpr mkAtMost ( Expr< BoolSort >[]  args,
int  k 
)
inline

Create an at-most-k constraint.

Definition at line 2395 of file Context.java.

2396  {
2397  checkContextMatch(args);
2398  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2399  }

◆ mkBitVecSort()

BitVecSort mkBitVecSort ( int  size)
inline

Create a new bit-vector sort.

Definition at line 222 of file Context.java.

223  {
224  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
225  }
z3py.BitVecSort
def BitVecSort(sz, ctx=None)
Definition: z3py.py:4051

◆ mkBool()

BoolExpr mkBool ( boolean  value)
inline

Creates a Boolean value.

Definition at line 742 of file Context.java.

743  {
744  return value ? mkTrue() : mkFalse();
745  }

Referenced by UserPropagatorBase.conflict().

◆ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( String  name)
inline

Create a Boolean constant.

Definition at line 659 of file Context.java.

660  {
661  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
662  }

◆ mkBoolConst() [2/2]

BoolExpr mkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 651 of file Context.java.

652  {
653  return (BoolExpr) mkConst(name, getBoolSort());
654  }

◆ mkBoolSort()

BoolSort mkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 161 of file Context.java.

162  {
163  return new BoolSort(this);
164  }

◆ mkBound()

final<R extends Sort> Expr<R> mkBound ( int  index,
R  ty 
)
inline

Creates a new bound variable.

Parameters
indexThe de-Bruijn index of the variable
tyThe sort of the variable

Definition at line 584 of file Context.java.

585  {
586  return (Expr<R>) Expr.create(this,
587  Native.mkBound(nCtx(), index, ty.getNativeObject()));
588  }

◆ mkBV() [1/3]

BitVecNum mkBV ( int  v,
int  size 
)
inline

Create a bit-vector numeral.

Parameters
vvalue of the numeral.
sizethe size of the bit-vector

Definition at line 2597 of file Context.java.

2598  {
2599  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2600  }
com.microsoft.z3.Context.mkBitVecSort
BitVecSort mkBitVecSort(int size)
Definition: Context.java:222
com.microsoft.z3.Context.mkNumeral
final< R extends Sort > Expr< R > mkNumeral(String v, R ty)
Definition: Context.java:2448

◆ mkBV() [2/3]

BitVecNum mkBV ( long  v,
int  size 
)
inline

Create a bit-vector numeral.

Parameters
vvalue of the numeral. *
sizethe size of the bit-vector

Definition at line 2607 of file Context.java.

2608  {
2609  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2610  }

◆ mkBV() [3/3]

BitVecNum mkBV ( String  v,
int  size 
)
inline

Create a bit-vector numeral.

Parameters
vA string representing the value in decimal notation.
sizethe size of the bit-vector

Definition at line 2587 of file Context.java.

2588  {
2589  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2590  }

◆ mkBV2Int()

IntExpr mkBV2Int ( Expr< BitVecSort >  t,
boolean signed   
)
inline

Create an integer from the bit-vector argument

t

. Remarks: If is_signed is false, then the bit-vector 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 is_signed is true, 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.

Definition at line 1591 of file Context.java.

1592  {
1593  checkContextMatch(t);
1594  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1595  (signed)));
1596  }

◆ mkBVAdd()

BitVecExpr mkBVAdd ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement addition. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1154 of file Context.java.

1155  {
1156  checkContextMatch(t1);
1157  checkContextMatch(t2);
1158  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1159  t1.getNativeObject(), t2.getNativeObject()));
1160  }

◆ mkBVAddNoOverflow()

BoolExpr mkBVAddNoOverflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise addition does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1603 of file Context.java.

1605  {
1606  checkContextMatch(t1);
1607  checkContextMatch(t2);
1608  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1609  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1610  }

◆ mkBVAddNoUnderflow()

BoolExpr mkBVAddNoUnderflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Create a predicate that checks that the bit-wise addition does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1617 of file Context.java.

1619  {
1620  checkContextMatch(t1);
1621  checkContextMatch(t2);
1622  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1623  t1.getNativeObject(), t2.getNativeObject()));
1624  }

◆ mkBVAND()

BitVecExpr mkBVAND ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Bitwise conjunction. Remarks: The arguments must have a bit-vector sort.

Definition at line 1065 of file Context.java.

1066  {
1067  checkContextMatch(t1);
1068  checkContextMatch(t2);
1069  return new BitVecExpr(this, Native.mkBvand(nCtx(),
1070  t1.getNativeObject(), t2.getNativeObject()));
1071  }

◆ mkBVASHR()

BitVecExpr mkBVASHR ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

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.

Definition at line 1499 of file Context.java.

1500  {
1501  checkContextMatch(t1);
1502  checkContextMatch(t2);
1503  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1504  t1.getNativeObject(), t2.getNativeObject()));
1505  }

◆ mkBVConst() [1/2]

BitVecExpr mkBVConst ( String  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 707 of file Context.java.

708  {
709  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
710  }

◆ mkBVConst() [2/2]

BitVecExpr mkBVConst ( Symbol  name,
int  size 
)
inline

Creates a bit-vector constant.

Definition at line 699 of file Context.java.

700  {
701  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
702  }

◆ mkBVLSHR()

BitVecExpr mkBVLSHR ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Logical shift right Remarks: It is equivalent to unsigned division by

2^x

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

Definition at line 1479 of file Context.java.

1480  {
1481  checkContextMatch(t1);
1482  checkContextMatch(t2);
1483  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1484  t1.getNativeObject(), t2.getNativeObject()));
1485  }

◆ mkBVMul()

BitVecExpr mkBVMul ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement multiplication. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1180 of file Context.java.

1181  {
1182  checkContextMatch(t1);
1183  checkContextMatch(t2);
1184  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1185  t1.getNativeObject(), t2.getNativeObject()));
1186  }

◆ mkBVMulNoOverflow()

BoolExpr mkBVMulNoOverflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise multiplication does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1685 of file Context.java.

1687  {
1688  checkContextMatch(t1);
1689  checkContextMatch(t2);
1690  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1691  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1692  }

◆ mkBVMulNoUnderflow()

BoolExpr mkBVMulNoUnderflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Create a predicate that checks that the bit-wise multiplication does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1699 of file Context.java.

1701  {
1702  checkContextMatch(t1);
1703  checkContextMatch(t2);
1704  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1705  t1.getNativeObject(), t2.getNativeObject()));
1706  }

◆ mkBVNAND()

BitVecExpr mkBVNAND ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Bitwise NAND. Remarks: The arguments must have a bit-vector sort.

Definition at line 1104 of file Context.java.

1105  {
1106  checkContextMatch(t1);
1107  checkContextMatch(t2);
1108  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1109  t1.getNativeObject(), t2.getNativeObject()));
1110  }

◆ mkBVNeg()

BitVecExpr mkBVNeg ( Expr< BitVecSort >  t)
inline

Standard two's complement unary minus. Remarks: The arguments must have a bit-vector sort.

Definition at line 1143 of file Context.java.

1144  {
1145  checkContextMatch(t);
1146  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1147  }

◆ mkBVNegNoOverflow()

BoolExpr mkBVNegNoOverflow ( Expr< BitVecSort >  t)
inline

Create a predicate that checks that the bit-wise negation does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1673 of file Context.java.

1674  {
1675  checkContextMatch(t);
1676  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1677  t.getNativeObject()));
1678  }

◆ mkBVNOR()

BitVecExpr mkBVNOR ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Bitwise NOR. Remarks: The arguments must have a bit-vector sort.

Definition at line 1117 of file Context.java.

1118  {
1119  checkContextMatch(t1);
1120  checkContextMatch(t2);
1121  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1122  t1.getNativeObject(), t2.getNativeObject()));
1123  }

◆ mkBVNot()

BitVecExpr mkBVNot ( Expr< BitVecSort >  t)
inline

Bitwise negation. Remarks: The argument must have a bit-vector sort.

Definition at line 1030 of file Context.java.

1031  {
1032  checkContextMatch(t);
1033  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
1034  }

◆ mkBVOR()

BitVecExpr mkBVOR ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Bitwise disjunction. Remarks: The arguments must have a bit-vector sort.

Definition at line 1078 of file Context.java.

1079  {
1080  checkContextMatch(t1);
1081  checkContextMatch(t2);
1082  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1083  t2.getNativeObject()));
1084  }

◆ mkBVRedAND()

BitVecExpr mkBVRedAND ( Expr< BitVecSort >  t)
inline

Take conjunction of bits in a vector, return vector of length 1.

Remarks: The argument must have a bit-vector sort.

Definition at line 1041 of file Context.java.

1042  {
1043  checkContextMatch(t);
1044  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
1045  t.getNativeObject()));
1046  }

◆ mkBVRedOR()

BitVecExpr mkBVRedOR ( Expr< BitVecSort >  t)
inline

Take disjunction of bits in a vector, return vector of length 1.

Remarks: The argument must have a bit-vector sort.

Definition at line 1053 of file Context.java.

1054  {
1055  checkContextMatch(t);
1056  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1057  t.getNativeObject()));
1058  }

◆ mkBVRotateLeft() [1/2]

BitVecExpr mkBVRotateLeft ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Rotate Left. Remarks: Rotate bits of

t1

to the left

t2

times. The arguments must have the same bit-vector sort.

Definition at line 1537 of file Context.java.

1539  {
1540  checkContextMatch(t1);
1541  checkContextMatch(t2);
1542  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1543  t1.getNativeObject(), t2.getNativeObject()));
1544  }

◆ mkBVRotateLeft() [2/2]

BitVecExpr mkBVRotateLeft ( int  i,
Expr< BitVecSort >  t 
)
inline

Rotate Left. Remarks: Rotate bits of t to the left i times. The argument

t

must have a bit-vector sort.

Definition at line 1512 of file Context.java.

1513  {
1514  checkContextMatch(t);
1515  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1516  t.getNativeObject()));
1517  }

◆ mkBVRotateRight() [1/2]

BitVecExpr mkBVRotateRight ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Rotate Right. Remarks: Rotate bits of

t1

to the right

t2

times. The arguments must have the same bit-vector sort.

Definition at line 1552 of file Context.java.

1554  {
1555  checkContextMatch(t1);
1556  checkContextMatch(t2);
1557  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1558  t1.getNativeObject(), t2.getNativeObject()));
1559  }

◆ mkBVRotateRight() [2/2]

BitVecExpr mkBVRotateRight ( int  i,
Expr< BitVecSort >  t 
)
inline

Rotate Right. Remarks: Rotate bits of t to the right i times. The argument

t

must have a bit-vector sort.

Definition at line 1524 of file Context.java.

1525  {
1526  checkContextMatch(t);
1527  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1528  t.getNativeObject()));
1529  }

◆ mkBVSDiv()

BitVecExpr mkBVSDiv ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Signed division. Remarks: It is defined in the following way:

If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1216 of file Context.java.

1217  {
1218  checkContextMatch(t1);
1219  checkContextMatch(t2);
1220  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1221  t1.getNativeObject(), t2.getNativeObject()));
1222  }

◆ mkBVSDivNoOverflow()

BoolExpr mkBVSDivNoOverflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Create a predicate that checks that the bit-wise signed division does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1659 of file Context.java.

1661  {
1662  checkContextMatch(t1);
1663  checkContextMatch(t2);
1664  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1665  t1.getNativeObject(), t2.getNativeObject()));
1666  }

◆ mkBVSGE()

BoolExpr mkBVSGE ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement signed greater than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1341 of file Context.java.

1342  {
1343  checkContextMatch(t1);
1344  checkContextMatch(t2);
1345  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1346  t2.getNativeObject()));
1347  }

◆ mkBVSGT()

BoolExpr mkBVSGT ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement signed greater-than. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1367 of file Context.java.

1368  {
1369  checkContextMatch(t1);
1370  checkContextMatch(t2);
1371  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1372  t2.getNativeObject()));
1373  }

◆ mkBVSHL()

BitVecExpr mkBVSHL ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Shift left. Remarks: It is equivalent to multiplication by

2^x

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

Definition at line 1460 of file Context.java.

1461  {
1462  checkContextMatch(t1);
1463  checkContextMatch(t2);
1464  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1465  t1.getNativeObject(), t2.getNativeObject()));
1466  }

◆ mkBVSLE()

BoolExpr mkBVSLE ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement signed less-than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1315 of file Context.java.

1316  {
1317  checkContextMatch(t1);
1318  checkContextMatch(t2);
1319  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1320  t2.getNativeObject()));
1321  }

◆ mkBVSLT()

BoolExpr mkBVSLT ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement signed less-than Remarks: The arguments must have the same bit-vector sort.

Definition at line 1289 of file Context.java.

1290  {
1291  checkContextMatch(t1);
1292  checkContextMatch(t2);
1293  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1294  t2.getNativeObject()));
1295  }

◆ mkBVSMod()

BitVecExpr mkBVSMod ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

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.

Definition at line 1263 of file Context.java.

1264  {
1265  checkContextMatch(t1);
1266  checkContextMatch(t2);
1267  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1268  t1.getNativeObject(), t2.getNativeObject()));
1269  }

◆ mkBVSRem()

BitVecExpr mkBVSRem ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

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

If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1249 of file Context.java.

1250  {
1251  checkContextMatch(t1);
1252  checkContextMatch(t2);
1253  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1254  t1.getNativeObject(), t2.getNativeObject()));
1255  }

◆ mkBVSub()

BitVecExpr mkBVSub ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Two's complement subtraction. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1167 of file Context.java.

1168  {
1169  checkContextMatch(t1);
1170  checkContextMatch(t2);
1171  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1172  t1.getNativeObject(), t2.getNativeObject()));
1173  }

◆ mkBVSubNoOverflow()

BoolExpr mkBVSubNoOverflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Create a predicate that checks that the bit-wise subtraction does not overflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1631 of file Context.java.

1633  {
1634  checkContextMatch(t1);
1635  checkContextMatch(t2);
1636  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1637  t1.getNativeObject(), t2.getNativeObject()));
1638  }

◆ mkBVSubNoUnderflow()

BoolExpr mkBVSubNoUnderflow ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2,
boolean  isSigned 
)
inline

Create a predicate that checks that the bit-wise subtraction does not underflow. Remarks: The arguments must be of bit-vector sort.

Definition at line 1645 of file Context.java.

1647  {
1648  checkContextMatch(t1);
1649  checkContextMatch(t2);
1650  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1651  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1652  }

◆ mkBVUDiv()

BitVecExpr mkBVUDiv ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Unsigned division. Remarks: It is defined as the floor of

t1/t2

if t2 is different from zero. If

t2

is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1195 of file Context.java.

1196  {
1197  checkContextMatch(t1);
1198  checkContextMatch(t2);
1199  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1200  t1.getNativeObject(), t2.getNativeObject()));
1201  }

◆ mkBVUGE()

BoolExpr mkBVUGE ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Unsigned greater than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1328 of file Context.java.

1329  {
1330  checkContextMatch(t1);
1331  checkContextMatch(t2);
1332  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1333  t2.getNativeObject()));
1334  }

◆ mkBVUGT()

BoolExpr mkBVUGT ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Unsigned greater-than. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1354 of file Context.java.

1355  {
1356  checkContextMatch(t1);
1357  checkContextMatch(t2);
1358  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1359  t2.getNativeObject()));
1360  }

◆ mkBVULE()

BoolExpr mkBVULE ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Unsigned less-than or equal to. Remarks: The arguments must have the same bit-vector sort.

Definition at line 1302 of file Context.java.

1303  {
1304  checkContextMatch(t1);
1305  checkContextMatch(t2);
1306  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1307  t2.getNativeObject()));
1308  }

◆ mkBVULT()

BoolExpr mkBVULT ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Unsigned less-than Remarks: The arguments must have the same bit-vector sort.

Definition at line 1276 of file Context.java.

1277  {
1278  checkContextMatch(t1);
1279  checkContextMatch(t2);
1280  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1281  t2.getNativeObject()));
1282  }

◆ mkBVURem()

BitVecExpr mkBVURem ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

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.

Definition at line 1231 of file Context.java.

1232  {
1233  checkContextMatch(t1);
1234  checkContextMatch(t2);
1235  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1236  t1.getNativeObject(), t2.getNativeObject()));
1237  }

◆ mkBVXNOR()

BitVecExpr mkBVXNOR ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Bitwise XNOR. Remarks: The arguments must have a bit-vector sort.

Definition at line 1130 of file Context.java.

1131  {
1132  checkContextMatch(t1);
1133  checkContextMatch(t2);
1134  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1135  t1.getNativeObject(), t2.getNativeObject()));
1136  }

◆ mkBVXOR()

BitVecExpr mkBVXOR ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

Bitwise XOR. Remarks: The arguments must have a bit-vector sort.

Definition at line 1091 of file Context.java.

1092  {
1093  checkContextMatch(t1);
1094  checkContextMatch(t2);
1095  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1096  t1.getNativeObject(), t2.getNativeObject()));
1097  }

◆ mkCharLe()

BoolExpr mkCharLe ( Expr< CharSort >  ch1,
Expr< CharSort >  ch2 
)
inline

Create less than or equal to between two characters.

Definition at line 2350 of file Context.java.

2351  {
2352  checkContextMatch(ch1, ch2);
2353  return (BoolExpr) Expr.create(this, Native.mkCharLe(nCtx(), ch1.getNativeObject(), ch2.getNativeObject()));
2354  }

◆ mkCharSort()

CharSort mkCharSort ( )
inline

Creates character sort object.

Definition at line 170 of file Context.java.

171  {
172  return new CharSort(this);
173  }
z3py.CharSort
def CharSort(ctx=None)
Definition: z3py.py:10888

◆ mkComplement()

final<R extends Sort> ReExpr<R> mkComplement ( Expr< ReSort< R >>  re)
inline

Create the complement regular expression.

Definition at line 2264 of file Context.java.

2265  {
2266  checkContextMatch(re);
2267  return (ReExpr<R>) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2268  }

◆ mkConcat() [1/3]

BitVecExpr mkConcat ( Expr< BitVecSort >  t1,
Expr< BitVecSort >  t2 
)
inline

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

Definition at line 1385 of file Context.java.

1386  {
1387  checkContextMatch(t1);
1388  checkContextMatch(t2);
1389  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1390  t1.getNativeObject(), t2.getNativeObject()));
1391  }

◆ mkConcat() [2/3]

final<R extends Sort> SeqExpr<R> mkConcat ( Expr< SeqSort< R >>...  t)
inline

Concatenate sequences.

Definition at line 2081 of file Context.java.

2082  {
2083  checkContextMatch(t);
2084  return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2085  }

◆ mkConcat() [3/3]

final<R extends Sort> ReExpr<R> mkConcat ( ReExpr< R >...  t)
inline

Create the concatenation of regular languages.

Definition at line 2274 of file Context.java.

2275  {
2276  checkContextMatch(t);
2277  return (ReExpr<R>) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2278  }

◆ mkConst() [1/3]

final<R extends Sort> Expr<R> mkConst ( FuncDecl< R >  f)
inline

Creates a fresh constant from the FuncDecl

f

.

Parameters
fA decl of a 0-arity function

Definition at line 643 of file Context.java.

644  {
645  return mkApp(f, (Expr<?>[]) null);
646  }
com.microsoft.z3.Context.mkApp
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:716

◆ mkConst() [2/3]

final<R extends Sort> Expr<R> mkConst ( String  name,
R  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 623 of file Context.java.

624  {
625  return mkConst(mkSymbol(name), range);
626  }

◆ mkConst() [3/3]

final<R extends Sort> Expr<R> mkConst ( Symbol  name,
R  range 
)
inline

Creates a new Constant of sort

range

and named

name

.

Definition at line 608 of file Context.java.

609  {
610  checkContextMatch(name);
611  checkContextMatch(range);
612 
613  return (Expr<R>) Expr.create(
614  this,
615  Native.mkConst(nCtx(), name.getNativeObject(),
616  range.getNativeObject()));
617  }

◆ mkConstArray()

final<D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray ( D  domain,
Expr< R >  v 
)
inline

Create a constant array. Remarks: The resulting term is an array, such that a

select
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3954

on an arbitrary index produces the value

v

.

See also
mkArraySort(Sort[], R)
mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)

Definition at line 1828 of file Context.java.

1829  {
1830  checkContextMatch(domain);
1831  checkContextMatch(v);
1832  return new ArrayExpr<>(this, Native.mkConstArray(nCtx(),
1833  domain.getNativeObject(), v.getNativeObject()));
1834  }

◆ mkConstDecl() [1/2]

final<R extends Sort> FuncDecl<R> mkConstDecl ( String  name,
R  range 
)
inline

Creates a new constant function declaration.

Definition at line 560 of file Context.java.

561  {
562  checkContextMatch(range);
563  return new FuncDecl<>(this, mkSymbol(name), null, range);
564  }

◆ mkConstDecl() [2/2]

final<R extends Sort> FuncDecl<R> mkConstDecl ( Symbol  name,
R  range 
)
inline

Creates a new constant function declaration.

Definition at line 550 of file Context.java.

551  {
552  checkContextMatch(name);
553  checkContextMatch(range);
554  return new FuncDecl<>(this, name, null, range);
555  }

◆ mkConstructor() [1/2]

final<R> Constructor<R> mkConstructor ( String  name,
String  recognizer,
String[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Definition at line 365 of file Context.java.

367  {
368  return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs);
369  }

◆ mkConstructor() [2/2]

final<R> Constructor<R> mkConstructor ( Symbol  name,
Symbol  recognizer,
Symbol[]  fieldNames,
Sort[]  sorts,
int[]  sortRefs 
)
inline

Create a datatype constructor.

Parameters
nameconstructor name
recognizername of recognizer function.
fieldNamesnames of the constructor fields.
sortsfield sorts, 0 if the field sort refers to a recursive sort.
sortRefsreference 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.

Definition at line 355 of file Context.java.

358  {
359  return of(this, name, recognizer, fieldNames, sorts, sortRefs);
360  }

◆ mkContains()

final<R extends Sort> BoolExpr mkContains ( Expr< SeqSort< R >>  s1,
Expr< SeqSort< R >>  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2118 of file Context.java.

2119  {
2120  checkContextMatch(s1, s2);
2121  return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2122  }

◆ mkDatatypeSort() [1/2]

final<R> DatatypeSort<R> mkDatatypeSort ( String  name,
Constructor< R >[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 384 of file Context.java.

386  {
387  checkContextMatch(constructors);
388  return new DatatypeSort<>(this, mkSymbol(name), constructors);
389  }

◆ mkDatatypeSort() [2/2]

final<R> DatatypeSort<R> mkDatatypeSort ( Symbol  name,
Constructor< R >[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 374 of file Context.java.

375  {
376  checkContextMatch(name);
377  checkContextMatch(constructors);
378  return new DatatypeSort<>(this, name, constructors);
379  }

◆ mkDatatypeSorts() [1/2]

DatatypeSort<Object> [] mkDatatypeSorts ( String[]  names,
Constructor< Object >  c[][] 
)
inline

Create mutually recursive data-types.

Definition at line 422 of file Context.java.

424  {
425  return mkDatatypeSorts(mkSymbols(names), c);
426  }
com.microsoft.z3.Context.mkDatatypeSorts
DatatypeSort< Object >[] mkDatatypeSorts(Symbol[] names, Constructor< Object >[][] c)
Definition: Context.java:396

◆ mkDatatypeSorts() [2/2]

DatatypeSort<Object> [] mkDatatypeSorts ( Symbol[]  names,
Constructor< Object >  c[][] 
)
inline

Create mutually recursive datatypes.

Parameters
namesnames of datatype sorts
clist of constructors, one list per sort.

Definition at line 396 of file Context.java.

397  {
398  checkContextMatch(names);
399  int n = names.length;
400  ConstructorList<Object>[] cla = new ConstructorList[n];
401  long[] n_constr = new long[n];
402  for (int i = 0; i < n; i++)
403  {
404  Constructor<Object>[] constructor = c[i];
405 
406  checkContextMatch(constructor);
407  cla[i] = new ConstructorList<>(this, constructor);
408  n_constr[i] = cla[i].getNativeObject();
409  }
410  long[] n_res = new long[n];
411  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
412  n_constr);
413  DatatypeSort<Object>[] res = new DatatypeSort[n];
414  for (int i = 0; i < n; i++)
415  res[i] = new DatatypeSort<>(this, n_res[i]);
416  return res;
417  }
z3py.DatatypeSort
def DatatypeSort(name, ctx=None)
Definition: z3py.py:5404

◆ mkDiff()

final<R extends Sort> ReExpr<R> mkDiff ( Expr< ReSort< R >>  a,
Expr< ReSort< R >>  b 
)
inline

Create a difference regular expression.

Definition at line 2303 of file Context.java.

2304  {
2305  checkContextMatch(a, b);
2306  return (ReExpr<R>) Expr.create(this, Native.mkReDiff(nCtx(), a.getNativeObject(), b.getNativeObject()));
2307  }

◆ mkDistinct()

final BoolExpr mkDistinct ( Expr<?>...  args)
inline

Creates a

distinct
z3::distinct
expr distinct(expr_vector const &args)
Definition: z3++.h:2447

term.

Definition at line 762 of file Context.java.

763  {
764  checkContextMatch(args);
765  return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
766  AST.arrayToNative(args)));
767  }

◆ mkDiv()

final<R extends ArithSort> ArithExpr<R> mkDiv ( Expr<? extends R >  t1,
Expr<? extends R >  t2 
)
inline

Create an expression representing

t1 / t2

.

Definition at line 895 of file Context.java.

896  {
897  checkContextMatch(t1);
898  checkContextMatch(t2);
899  return (ArithExpr<R>) Expr.create(this, Native.mkDiv(nCtx(),
900  t1.getNativeObject(), t2.getNativeObject()));
901  }

◆ mkEmptyRe()

final<R extends Sort> ReExpr<R> mkEmptyRe ( ReSort< R >  s)
inline

Create the empty regular expression. Corresponds to re.none

Definition at line 2314 of file Context.java.

2315  {
2316  return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2317  }

◆ mkEmptySeq()

final<R extends Sort> SeqExpr<R> mkEmptySeq ( R  s)
inline

Sequences, Strings and regular expressions. Create the empty sequence.

Definition at line 2014 of file Context.java.

2015  {
2016  checkContextMatch(s);
2017  return (SeqExpr<R>) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
2018  }

◆ mkEmptySet()

final<D extends Sort> ArrayExpr<D, BoolSort> mkEmptySet ( D  domain)
inline

Create an empty set.

Definition at line 1895 of file Context.java.

1896  {
1897  checkContextMatch(domain);
1898  return (ArrayExpr<D, BoolSort>) Expr.create(this,
1899  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1900  }

◆ mkEnumSort() [1/2]

final<R> EnumSort<R> mkEnumSort ( String  name,
String...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 300 of file Context.java.

302  {
303  return new EnumSort<>(this, mkSymbol(name), mkSymbols(enumNames));
304  }

◆ mkEnumSort() [2/2]

final<R> EnumSort<R> mkEnumSort ( Symbol  name,
Symbol...  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 289 of file Context.java.

291  {
292  checkContextMatch(name);
293  checkContextMatch(enumNames);
294  return new EnumSort<>(this, name, enumNames);
295  }

◆ mkEq()

BoolExpr mkEq ( Expr<?>  x,
Expr<?>  y 
)
inline

Creates the equality

x = y

Definition at line 750 of file Context.java.

751  {
752  checkContextMatch(x);
753  checkContextMatch(y);
754  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
755  y.getNativeObject()));
756  }

◆ mkExists() [1/2]

Quantifier mkExists ( Expr<?>[]  boundConstants,
Expr< BoolSort >  body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates an existential quantifier using a list of constants that will form the set of bound variables.

See also
mkForall(Sort[],Symbol[],Expr<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2675 of file Context.java.

2678  {
2679 
2680  return Quantifier.of(this, false, boundConstants, body, weight,
2681  patterns, noPatterns, quantifierID, skolemID);
2682  }

◆ mkExists() [2/2]

Quantifier mkExists ( Sort[]  sorts,
Symbol[]  names,
Expr< BoolSort >  body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates an existential quantifier using de-Bruijn indexed variables.

See also
mkForall(Sort[],Symbol[],Expr<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2662 of file Context.java.

2665  {
2666 
2667  return Quantifier.of(this, false, sorts, names, body, weight,
2668  patterns, noPatterns, quantifierID, skolemID);
2669  }

◆ mkExtract() [1/2]

final<R extends Sort> SeqExpr<R> mkExtract ( Expr< SeqSort< R >>  s,
Expr< IntSort >  offset,
Expr< IntSort >  length 
)
inline

Extract subsequence.

Definition at line 2166 of file Context.java.

2167  {
2168  checkContextMatch(s, offset, length);
2169  return (SeqExpr<R>) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2170  }

◆ mkExtract() [2/2]

BitVecExpr mkExtract ( int  high,
int  low,
Expr< BitVecSort >  t 
)
inline

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.

Definition at line 1401 of file Context.java.

1403  {
1404  checkContextMatch(t);
1405  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1406  t.getNativeObject()));
1407  }

◆ mkFalse()

BoolExpr mkFalse ( )
inline

The false Term.

Definition at line 734 of file Context.java.

735  {
736  return new BoolExpr(this, Native.mkFalse(nCtx()));
737  }

◆ mkFiniteDomainSort() [1/2]

final<R> FiniteDomainSort<R> mkFiniteDomainSort ( String  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 338 of file Context.java.

340  {
341  return new FiniteDomainSort<>(this, mkSymbol(name), size);
342  }

◆ mkFiniteDomainSort() [2/2]

final<R> FiniteDomainSort<R> mkFiniteDomainSort ( Symbol  name,
long  size 
)
inline

Create a new finite domain sort.

Definition at line 328 of file Context.java.

330  {
331  checkContextMatch(name);
332  return new FiniteDomainSort<>(this, name, size);
333  }

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3409 of file Context.java.

3410  {
3411  return new Fixedpoint(this);
3412  }

◆ mkForall() [1/2]

Quantifier mkForall ( Expr<?>[]  boundConstants,
Expr< BoolSort >  body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Creates a universal quantifier using a list of constants that will form the set of bound variables.

See also
mkForall(Sort[],Symbol[],Expr<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2649 of file Context.java.

2652  {
2653 
2654  return Quantifier.of(this, true, boundConstants, body, weight,
2655  patterns, noPatterns, quantifierID, skolemID);
2656  }

◆ mkForall() [2/2]

Quantifier mkForall ( Sort[]  sorts,
Symbol[]  names,
Expr< BoolSort >  body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a universal Quantifier.

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables
bodythe body of the quantifier.
weightquantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patternsarray containing the patterns created using
MkPattern
.
noPatternsarray containing the anti-patterns created using
MkPattern
.
quantifierIDoptional symbol to track quantifier.
skolemIDoptional 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}. 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.

Definition at line 2637 of file Context.java.

2640  {
2641  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2642  noPatterns, quantifierID, skolemID);
2643  }

◆ mkFP() [1/6]

FPNum mkFP ( boolean  sgn,
int  exp,
int  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3739 of file Context.java.

3740  {
3741  return mkFPNumeral(sgn, exp, sig, s);
3742  }
com.microsoft.z3.Context.mkFPNumeral
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3644

◆ mkFP() [2/6]

FPNum mkFP ( boolean  sgn,
long  exp,
long  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3752 of file Context.java.

3753  {
3754  return mkFPNumeral(sgn, exp, sig, s);
3755  }

◆ mkFP() [3/6]

FPNum mkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3714 of file Context.java.

3715  {
3716  return mkFPNumeral(v, s);
3717  }

◆ mkFP() [4/6]

FPExpr mkFP ( Expr< BitVecSort >  sgn,
Expr< BitVecSort >  sig,
Expr< BitVecSort >  exp 
)
inline

Create an expression of FloatingPoint sort from three bit-vector expressions.

Parameters
sgnbit-vector term (of size 1) representing the sign.
sigbit-vector term representing the significand.
expbit-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.
Exceptions
Z3Exception

Definition at line 4037 of file Context.java.

4038  {
4039  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
4040  }

◆ mkFP() [5/6]

FPNum mkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3703 of file Context.java.

3704  {
3705  return mkFPNumeral(v, s);
3706  }

◆ mkFP() [6/6]

FPNum mkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3726 of file Context.java.

3727  {
3728  return mkFPNumeral(v, s);
3729  }

◆ mkFPAbs()

FPExpr mkFPAbs ( Expr< FPSort >  t)
inline

Floating-point absolute value

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3763 of file Context.java.

3764  {
3765  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3766  }

◆ mkFPAdd()

FPExpr mkFPAdd ( Expr< FPRMSort >  rm,
Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point addition

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3785 of file Context.java.

3786  {
3787  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3788  }

◆ mkFPDiv()

FPExpr mkFPDiv ( Expr< FPRMSort >  rm,
Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point division

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3821 of file Context.java.

3822  {
3823  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3824  }

◆ mkFPEq()

BoolExpr mkFPEq ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point equality.

Parameters
t1floating-point term
t2floating-point term Remarks: Note that this is IEEE 754 equality (as opposed to standard =).
Exceptions
Z3Exception

Definition at line 3949 of file Context.java.

3950  {
3951  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3952  }

◆ mkFPFMA()

FPExpr mkFPFMA ( Expr< FPRMSort >  rm,
Expr< FPSort >  t1,
Expr< FPSort >  t2,
Expr< FPSort >  t3 
)
inline

Floating-point fused multiply-add

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
t3floating-point term Remarks: The result is round((t1 * t2) + t3)
Exceptions
Z3Exception

Definition at line 3836 of file Context.java.

3837  {
3838  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3839  }

◆ mkFPGEq()

BoolExpr mkFPGEq ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3925 of file Context.java.

3926  {
3927  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3928  }

◆ mkFPGt()

BoolExpr mkFPGt ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3936 of file Context.java.

3937  {
3938  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3939  }

◆ mkFPInf()

FPNum mkFPInf ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point infinity of sort s.

Parameters
sFloatingPoint sort.
negativeindicates whether the result should be negative.
Exceptions
Z3Exception

Definition at line 3622 of file Context.java.

3623  {
3624  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3625  }

◆ mkFPIsInfinite()

BoolExpr mkFPIsInfinite ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a floating-point number representing +oo or -oo.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3989 of file Context.java.

3990  {
3991  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3992  }

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3999 of file Context.java.

4000  {
4001  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
4002  }

◆ mkFPIsNegative()

BoolExpr mkFPIsNegative ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a negative floating-point number.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 4009 of file Context.java.

4010  {
4011  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
4012  }

◆ mkFPIsNormal()

BoolExpr mkFPIsNormal ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a normal floating-point number.\

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3959 of file Context.java.

3960  {
3961  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3962  }

◆ mkFPIsPositive()

BoolExpr mkFPIsPositive ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a positive floating-point number.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 4019 of file Context.java.

4020  {
4021  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
4022  }

◆ mkFPIsSubnormal()

BoolExpr mkFPIsSubnormal ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a subnormal floating-point number.\

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3969 of file Context.java.

3970  {
3971  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3972  }

◆ mkFPIsZero()

BoolExpr mkFPIsZero ( Expr< FPSort >  t)
inline

Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3979 of file Context.java.

3980  {
3981  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3982  }

◆ mkFPLEq()

BoolExpr mkFPLEq ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3903 of file Context.java.

3904  {
3905  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3906  }

◆ mkFPLt()

BoolExpr mkFPLt ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3914 of file Context.java.

3915  {
3916  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3917  }

◆ mkFPMax()

FPExpr mkFPMax ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3892 of file Context.java.

3893  {
3894  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3895  }

◆ mkFPMin()

FPExpr mkFPMin ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3881 of file Context.java.

3882  {
3883  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3884  }

◆ mkFPMul()

FPExpr mkFPMul ( Expr< FPRMSort >  rm,
Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point multiplication

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3809 of file Context.java.

3810  {
3811  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3812  }

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3611 of file Context.java.

3612  {
3613  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3614  }

◆ mkFPNeg()

FPExpr mkFPNeg ( Expr< FPSort >  t)
inline

Floating-point negation

Parameters
tfloating-point term
Exceptions
Z3Exception

Definition at line 3773 of file Context.java.

3774  {
3775  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3776  }

◆ mkFPNumeral() [1/5]

FPNum mkFPNumeral ( boolean  sgn,
int  exp,
int  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3679 of file Context.java.

3680  {
3681  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3682  }

◆ mkFPNumeral() [2/5]

FPNum mkFPNumeral ( boolean  sgn,
long  exp,
long  sig,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

Parameters
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3692 of file Context.java.

3693  {
3694  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3695  }

◆ mkFPNumeral() [3/5]

FPNum mkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a double.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3655 of file Context.java.

3656  {
3657  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3658  }

◆ mkFPNumeral() [4/5]

FPNum mkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3644 of file Context.java.

3645  {
3646  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3647  }

◆ mkFPNumeral() [5/5]

FPNum mkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3666 of file Context.java.

3667  {
3668  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3669  }

◆ mkFPRem()

FPExpr mkFPRem ( Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3858 of file Context.java.

3859  {
3860  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3861  }

◆ mkFPRNA()

FPRMNum mkFPRNA ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Exceptions
Z3Exception

Definition at line 3463 of file Context.java.

3464  {
3465  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3466  }

◆ mkFPRNE()

FPRMNum mkFPRNE ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Exceptions
Z3Exception

Definition at line 3445 of file Context.java.

3446  {
3447  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3448  }

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Exceptions
Z3Exception

Definition at line 3427 of file Context.java.

3428  {
3429  return new FPRMSort(this);
3430  }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Exceptions
Z3Exception

Definition at line 3454 of file Context.java.

3455  {
3456  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3457  }

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )
inline

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Exceptions
Z3Exception

Definition at line 3436 of file Context.java.

3437  {
3438  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3439  }

◆ mkFPRoundToIntegral()

FPExpr mkFPRoundToIntegral ( Expr< FPRMSort >  rm,
Expr< FPSort >  t 
)
inline

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.

Parameters
rmterm of RoundingMode sort
tfloating-point term
Exceptions
Z3Exception

Definition at line 3870 of file Context.java.

3871  {
3872  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3873  }

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.

Exceptions
Z3Exception

Definition at line 3490 of file Context.java.

3491  {
3492  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3493  }

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.

Exceptions
Z3Exception

Definition at line 3472 of file Context.java.

3473  {
3474  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3475  }

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.

Exceptions
Z3Exception

Definition at line 3508 of file Context.java.

3509  {
3510  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3511  }

◆ mkFPRTN()

FPRMNum mkFPRTN ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.

Exceptions
Z3Exception

Definition at line 3499 of file Context.java.

3500  {
3501  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3502  }

◆ mkFPRTP()

FPRMNum mkFPRTP ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.

Exceptions
Z3Exception

Definition at line 3481 of file Context.java.

3482  {
3483  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3484  }

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )
inline

Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.

Exceptions
Z3Exception

Definition at line 3517 of file Context.java.

3518  {
3519  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3520  }

◆ mkFPSort()

FPSort mkFPSort ( int  ebits,
int  sbits 
)
inline

Create a FloatingPoint sort.

Parameters
ebitsexponent bits in the FloatingPoint sort.
sbitssignificand bits in the FloatingPoint sort.
Exceptions
Z3Exception

Definition at line 3528 of file Context.java.

3529  {
3530  return new FPSort(this, ebits, sbits);
3531  }
z3py.FPSort
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:10034

◆ mkFPSort128()

FPSort mkFPSort128 ( )
inline

Create the quadruple-precision (128-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3600 of file Context.java.

3601  {
3602  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3603  }

◆ mkFPSort16()

FPSort mkFPSort16 ( )
inline

Create the half-precision (16-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3546 of file Context.java.

3547  {
3548  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3549  }

◆ mkFPSort32()

FPSort mkFPSort32 ( )
inline

Create the single-precision (32-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3564 of file Context.java.

3565  {
3566  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3567  }

◆ mkFPSort64()

FPSort mkFPSort64 ( )
inline

Create the double-precision (64-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3582 of file Context.java.

3583  {
3584  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3585  }

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )
inline

Create the double-precision (64-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3573 of file Context.java.

3574  {
3575  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3576  }

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )
inline

Create the half-precision (16-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3537 of file Context.java.

3538  {
3539  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3540  }

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )
inline

Create the quadruple-precision (128-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3591 of file Context.java.

3592  {
3593  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3594  }

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )
inline

Create the single-precision (32-bit) FloatingPoint sort.

Exceptions
Z3Exception

Definition at line 3555 of file Context.java.

3556  {
3557  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3558  }

◆ mkFPSqrt()

FPExpr mkFPSqrt ( Expr< FPRMSort >  rm,
Expr< FPSort >  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term
Exceptions
Z3Exception

Definition at line 3847 of file Context.java.

3848  {
3849  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3850  }

◆ mkFPSub()

FPExpr mkFPSub ( Expr< FPRMSort >  rm,
Expr< FPSort >  t1,
Expr< FPSort >  t2 
)
inline

Floating-point subtraction

Parameters
rmrounding mode term
t1floating-point term
t2floating-point term
Exceptions
Z3Exception

Definition at line 3797 of file Context.java.

3798  {
3799  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3800  }

◆ mkFPToBV()

BitVecExpr mkFPToBV ( Expr< FPRMSort >  rm,
Expr< FPSort >  t,
int  sz,
boolean signed   
)
inline

Conversion of a floating-point term into a bit-vector.

Parameters
rmRoundingMode term.
tFloatingPoint term
szSize of the resulting bit-vector.
signedIndicates 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.
Exceptions
Z3Exception

Definition at line 4138 of file Context.java.

4139  {
4140  if (signed)
4141  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
4142  else
4143  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
4144  }

◆ mkFPToFP() [1/6]

FPExpr mkFPToFP ( Expr< BitVecSort >  bv,
FPSort  s 
)
inline

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Parameters
bvbit-vector value (of size m).
sFloatingPoint 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.
Exceptions
Z3Exception

Definition at line 4053 of file Context.java.

4054  {
4055  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
4056  }

◆ mkFPToFP() [2/6]

FPExpr mkFPToFP ( Expr< FPRMSort >  rm,
Expr< BitVecSort >  t,
FPSort  s,
boolean signed   
)
inline

Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

Parameters
rmRoundingMode term.
tterm of bit-vector sort.
sFloatingPoint sort.
signedflag 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.
Exceptions
Z3Exception

Definition at line 4103 of file Context.java.

4104  {
4105  if (signed)
4106  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
4107  else
4108  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
4109  }

◆ mkFPToFP() [3/6]

BitVecExpr mkFPToFP ( Expr< FPRMSort >  rm,
Expr< IntSort >  exp,
Expr< RealSort >  sig,
FPSort  s 
)
inline

Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.

Parameters
rmRoundingMode term.
expExponent term of Int sort.
sigSignificand term of Real sort.
sFloatingPoint 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.
Exceptions
Z3Exception

Definition at line 4188 of file Context.java.

4189  {
4190  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
4191  }

◆ mkFPToFP() [4/6]

FPExpr mkFPToFP ( Expr< FPRMSort >  rm,
FPExpr  t,
FPSort  s 
)
inline

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Parameters
rmRoundingMode term.
tFloatingPoint term.
sFloatingPoint 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.
Exceptions
Z3Exception

Definition at line 4069 of file Context.java.

4070  {
4071  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
4072  }

◆ mkFPToFP() [5/6]

FPExpr mkFPToFP ( Expr< FPRMSort >  rm,
RealExpr  t,
FPSort  s 
)
inline

Conversion of a term of real sort into a term of FloatingPoint sort.

Parameters
rmRoundingMode term.
tterm of Real sort.
sFloatingPoint 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.
Exceptions
Z3Exception

Definition at line 4085 of file Context.java.

4086  {
4087  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
4088  }

◆ mkFPToFP() [6/6]

FPExpr mkFPToFP ( FPSort  s,
Expr< FPRMSort >  rm,
Expr< FPSort >  t 
)
inline

Conversion of a floating-point number to another FloatingPoint sort s.

Parameters
sFloatingPoint sort
rmfloating-point rounding mode term
tfloating-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.
Exceptions
Z3Exception

Definition at line 4121 of file Context.java.

4122  {
4123  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
4124  }

◆ mkFPToIEEEBV()

BitVecExpr mkFPToIEEEBV ( Expr< FPSort >  t)
inline

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

Parameters
tFloatingPoint 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.
Exceptions
Z3Exception

Definition at line 4170 of file Context.java.

4171  {
4172  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
4173  }

◆ mkFPToReal()

RealExpr mkFPToReal ( Expr< FPSort >  t)
inline

Conversion of a floating-point term into a real-numbered term.

Parameters
tFloatingPoint 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.
Exceptions
Z3Exception

Definition at line 4155 of file Context.java.

4156  {
4157  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
4158  }

◆ mkFPZero()

FPNum mkFPZero ( FPSort  s,
boolean  negative 
)
inline

Create a floating-point zero of sort s.

Parameters
sFloatingPoint sort.
negativeindicates whether the result should be negative.
Exceptions
Z3Exception

Definition at line 3633 of file Context.java.

3634  {
3635  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3636  }

◆ mkFreshConst()

final<R extends Sort> Expr<R> mkFreshConst ( String  prefix,
R  range 
)
inline

Creates a fresh Constant of sort

range

and a name prefixed with

prefix

.

Definition at line 632 of file Context.java.

633  {
634  checkContextMatch(range);
635  return (Expr<R>) Expr.create(this,
636  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
637  }

◆ mkFreshConstDecl()

final<R extends Sort> FuncDecl<R> mkFreshConstDecl ( String  prefix,
R  range 
)
inline

Creates a fresh constant function declaration with a name prefixed with

prefix

.

See also
#mkFuncDecl(String,Sort,Sort)
#mkFuncDecl(String,Sort[],Sort)

Definition at line 572 of file Context.java.

574  {
575  checkContextMatch(range);
576  return new FuncDecl<>(this, prefix, null, range);
577  }

◆ mkFreshFuncDecl()

final<R extends Sort> FuncDecl<R> mkFreshFuncDecl ( String  prefix,
Sort[]  domain,
R  range 
)
inline

Creates a fresh function declaration with a name prefixed with

prefix

.

See also
#mkFuncDecl(String,Sort,Sort)
#mkFuncDecl(String,Sort[],Sort)

Definition at line 539 of file Context.java.

541  {
542  checkContextMatch(domain);
543  checkContextMatch(range);
544  return new FuncDecl<>(this, prefix, domain, range);
545  }

◆ mkFullRe()

final<R extends Sort> ReExpr<R> mkFullRe ( ReSort< R >  s)
inline

Create the full regular expression. Corresponds to re.all

Definition at line 2323 of file Context.java.

2324  {
2325  return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
2326  }

◆ mkFullSet()

final<D extends Sort> ArrayExpr<D, BoolSort> mkFullSet ( D  domain)
inline

Create the full set.

Definition at line 1905 of file Context.java.

1906  {
1907  checkContextMatch(domain);
1908  return (ArrayExpr<D, BoolSort>) Expr.create(this,
1909  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1910  }

◆ mkFuncDecl() [1/4]

final<R extends Sort> FuncDecl<R> mkFuncDecl ( String  name,
Sort  domain,
R  range 
)
inline

Creates a new function declaration.

Definition at line 497 of file Context.java.

499  {
500  checkContextMatch(domain);
501  checkContextMatch(range);
502  Sort[] q = new Sort[] { domain };
503  return new FuncDecl<>(this, mkSymbol(name), q, range);
504  }

◆ mkFuncDecl() [2/4]

final<R extends Sort> FuncDecl<R> mkFuncDecl ( String  name,
Sort[]  domain,
R  range 
)
inline

Creates a new function declaration.

Definition at line 486 of file Context.java.

488  {
489  checkContextMatch(domain);
490  checkContextMatch(range);
491  return new FuncDecl<>(this, mkSymbol(name), domain, range);
492  }

◆ mkFuncDecl() [3/4]

final<R extends Sort> FuncDecl<R> mkFuncDecl ( Symbol  name,
Sort  domain,
R  range 
)
inline

Creates a new function declaration.

Definition at line 473 of file Context.java.

475  {
476  checkContextMatch(name);
477  checkContextMatch(domain);
478  checkContextMatch(range);
479  Sort[] q = new Sort[] { domain };
480  return new FuncDecl<>(this, name, q, range);
481  }

◆ mkFuncDecl() [4/4]

final<R extends Sort> FuncDecl<R> mkFuncDecl ( Symbol  name,
Sort[]  domain,
R  range 
)
inline

Creates a new function declaration.

Definition at line 447 of file Context.java.

448  {
449  checkContextMatch(name);
450  checkContextMatch(domain);
451  checkContextMatch(range);
452  return new FuncDecl<>(this, name, domain, range);
453  }

◆ mkGe()

BoolExpr mkGe ( Expr<? extends ArithSort >  t1,
Expr<? extends ArithSort >  t2 
)
inline

Create an expression representing

t1 &gt;= t2
com.microsoft.z3.Context.gt
Probe gt(Probe p1, Probe p2)
Definition: Context.java:3262

Definition at line 979 of file Context.java.

980  {
981  checkContextMatch(t1);
982  checkContextMatch(t2);
983  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
984  t2.getNativeObject()));
985  }

◆ mkGoal()

Goal mkGoal ( boolean  models,
boolean  unsatCores,
boolean  proofs 
)
inline

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
modelsIndicates whether model generation should be enabled.
unsatCoresIndicates whether unsat core generation should be enabled.
proofsIndicates whether proof generation should be enabled.

Definition at line 2852 of file Context.java.

2853  {
2854  return new Goal(this, models, unsatCores, proofs);
2855  }

◆ mkGt()

BoolExpr mkGt ( Expr<? extends ArithSort >  t1,
Expr<? extends ArithSort >  t2 
)
inline

Create an expression representing

t1 &gt; t2

Definition at line 968 of file Context.java.

969  {
970  checkContextMatch(t1);
971  checkContextMatch(t2);
972  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
973  t2.getNativeObject()));
974  }

◆ mkIff()

BoolExpr mkIff ( Expr< BoolSort >  t1,
Expr< BoolSort >  t2 
)
inline

Create an expression representing

t1 iff t2

.

Definition at line 797 of file Context.java.

798  {
799  checkContextMatch(t1);
800  checkContextMatch(t2);
801  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
802  t2.getNativeObject()));
803  }

◆ mkImplies()

BoolExpr mkImplies ( Expr< BoolSort >  t1,
Expr< BoolSort >  t2 
)
inline

Create an expression representing

t1 -> t2

.

Definition at line 808 of file Context.java.

809  {
810  checkContextMatch(t1);
811  checkContextMatch(t2);
812  return new BoolExpr(this, Native.mkImplies(nCtx(),
813  t1.getNativeObject(), t2.getNativeObject()));
814  }

◆ mkIndexOf()

final<R extends Sort> IntExpr mkIndexOf ( Expr< SeqSort< R >>  s,
Expr< SeqSort< R >>  substr,
Expr< IntSort >  offset 
)
inline

Extract index of sub-string starting at offset.

Definition at line 2175 of file Context.java.

2176  {
2177  checkContextMatch(s, substr, offset);
2178  return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2179  }

◆ mkInRe()

final<R extends Sort> BoolExpr mkInRe ( Expr< SeqSort< R >>  s,
ReExpr< SeqSort< R >>  re 
)
inline

Check for regular expression membership.

Definition at line 2203 of file Context.java.

2204  {
2205  checkContextMatch(s, re);
2206  return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2207  }

◆ mkInt() [1/3]

IntNum mkInt ( int  v)
inline

Create an integer numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Integer

Definition at line 2562 of file Context.java.

2563  {
2564 
2565  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2566  .getNativeObject()));
2567  }

◆ mkInt() [2/3]

IntNum mkInt ( long  v)
inline

Create an integer numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Integer

Definition at line 2575 of file Context.java.

2576  {
2577 
2578  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2579  .getNativeObject()));
2580  }

◆ mkInt() [3/3]

IntNum mkInt ( String  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2549 of file Context.java.

2550  {
2551 
2552  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2553  .getNativeObject()));
2554  }

◆ mkInt2BV()

BitVecExpr mkInt2BV ( int  n,
Expr< IntSort >  t 
)
inline

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.

Definition at line 1570 of file Context.java.

1571  {
1572  checkContextMatch(t);
1573  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1574  t.getNativeObject()));
1575  }

◆ mkInt2Real()

RealExpr mkInt2Real ( Expr< IntSort >  t)
inline

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.

Definition at line 997 of file Context.java.

998  {
999  checkContextMatch(t);
1000  return new RealExpr(this,
1001  Native.mkInt2real(nCtx(), t.getNativeObject()));
1002  }

◆ mkIntConst() [1/2]

IntExpr mkIntConst ( String  name)
inline

Creates an integer constant.

Definition at line 675 of file Context.java.

676  {
677  return (IntExpr) mkConst(name, getIntSort());
678  }

◆ mkIntConst() [2/2]

IntExpr mkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 667 of file Context.java.

668  {
669  return (IntExpr) mkConst(name, getIntSort());
670  }

◆ mkIntersect()

final<R extends Sort> ReExpr<R> mkIntersect ( Expr< ReSort< R >>...  t)
inline

Create the intersection of regular languages.

Definition at line 2294 of file Context.java.

2295  {
2296  checkContextMatch(t);
2297  return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2298  }

◆ mkIntSort()

IntSort mkIntSort ( )
inline

Create a new integer sort.

Definition at line 206 of file Context.java.

207  {
208  return new IntSort(this);
209  }

◆ mkIsDigit()

BoolExpr mkIsDigit ( Expr< CharSort >  ch)
inline

Create a check if the character is a digit.

Definition at line 2386 of file Context.java.

2387  {
2388  checkContextMatch(ch);
2389  return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject()));
2390  }

◆ mkIsInteger()

BoolExpr mkIsInteger ( Expr< RealSort >  t)
inline

Creates an expression that checks whether a real number is an integer.

Definition at line 1019 of file Context.java.

1020  {
1021  checkContextMatch(t);
1022  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
1023  }

◆ mkITE()

final<R extends Sort> Expr<R> mkITE ( Expr< BoolSort >  t1,
Expr<? extends R >  t2,
Expr<? extends R >  t3 
)
inline

Create an expression representing an if-then-else:

ite(t1, t2, t3)
z3::ite
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
Definition: z3++.h:2094

.

Parameters
t1An expression with Boolean sort
t2An expression
t3An expression with the same sort as
t2

Definition at line 785 of file Context.java.

786  {
787  checkContextMatch(t1);
788  checkContextMatch(t2);
789  checkContextMatch(t3);
790  return (Expr<R>) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
791  t2.getNativeObject(), t3.getNativeObject()));
792  }

◆ mkLambda() [1/2]

final<R extends Sort> Lambda<R> mkLambda ( Expr<?>[]  boundConstants,
Expr< R >  body 
)
inline

Create a lambda expression.

Creates a lambda expression using a list of constants that will form the set of bound variables.

Definition at line 2747 of file Context.java.

2748  {
2749  return Lambda.of(this, boundConstants, body);
2750  }
z3py.Lambda
def Lambda(vs, body)
Definition: z3py.py:2311

◆ mkLambda() [2/2]

final<R extends Sort> Lambda<R> mkLambda ( Sort[]  sorts,
Symbol[]  names,
Expr< R >  body 
)
inline

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} 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
sortsthe sorts of the bound variables.
namesnames of the bound variables.
bodythe body of the quantifier.

Definition at line 2736 of file Context.java.

2737  {
2738  return Lambda.of(this, sorts, names, body);
2739  }

◆ mkLe()

BoolExpr mkLe ( Expr<? extends ArithSort >  t1,
Expr<? extends ArithSort >  t2 
)
inline

Create an expression representing

t1 &lt;= t2

Definition at line 957 of file Context.java.

958  {
959  checkContextMatch(t1);
960  checkContextMatch(t2);
961  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
962  t2.getNativeObject()));
963  }

◆ mkLength()

final<R extends Sort> IntExpr mkLength ( Expr< SeqSort< R >>  s)
inline

Retrieve the length of a given sequence.

Definition at line 2091 of file Context.java.

2092  {
2093  checkContextMatch(s);
2094  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
2095  }

◆ mkLinearOrder()

final<R extends Sort> FuncDecl<BoolSort> mkLinearOrder ( R  sort,
int  index 
)
inline

Creates or a linear order.

Parameters
indexThe index of the order.
sortThe sort of the order.

Definition at line 4198 of file Context.java.

4198  {
4199  return (FuncDecl<BoolSort>) FuncDecl.create(
4200  this,
4201  Native.mkLinearOrder(
4202  nCtx(),
4203  sort.getNativeObject(),
4204  index
4205  )
4206  );
4207  }

◆ mkListSort() [1/2]

final<R extends Sort> ListSort<R> mkListSort ( String  name,
R  elemSort 
)
inline

Create a new list sort.

Definition at line 319 of file Context.java.

320  {
321  checkContextMatch(elemSort);
322  return new ListSort<>(this, mkSymbol(name), elemSort);
323  }

◆ mkListSort() [2/2]

final<R extends Sort> ListSort<R> mkListSort ( Symbol  name,
R  elemSort 
)
inline

Create a new list sort.

Definition at line 309 of file Context.java.

310  {
311  checkContextMatch(name);
312  checkContextMatch(elemSort);
313  return new ListSort<>(this, name, elemSort);
314  }

◆ mkLoop() [1/2]

final<R extends Sort> ReExpr<R> mkLoop ( Expr< ReSort< R >>  re,
int  lo 
)
inline

Take the lower-bounded Kleene star of a regular expression.

Definition at line 2237 of file Context.java.

2238  {
2239  return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2240  }

◆ mkLoop() [2/2]

final<R extends Sort> ReExpr<R> mkLoop ( Expr< ReSort< R >>  re,
int  lo,
int  hi 
)
inline

Take the lower and upper-bounded Kleene star of a regular expression.

Definition at line 2229 of file Context.java.

2230  {
2231  return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2232  }

◆ mkLt()

BoolExpr mkLt ( Expr<? extends ArithSort >  t1,
Expr<? extends ArithSort >  t2 
)
inline

Create an expression representing

t1 &lt; t2

Definition at line 946 of file Context.java.

947  {
948  checkContextMatch(t1);
949  checkContextMatch(t2);
950  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
951  t2.getNativeObject()));
952  }

◆ mkMap()

final<D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D, R2> mkMap ( FuncDecl< R2 >  f,
Expr< ArraySort< D, R1 >>...  args 
)
inline

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
mkArraySort(Sort[], R)
mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)

Definition at line 1850 of file Context.java.

1851  {
1852  checkContextMatch(f);
1853  checkContextMatch(args);
1854  return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
1855  f.getNativeObject(), AST.arrayLength(args),
1856  AST.arrayToNative(args)));
1857  }

◆ mkMod()

IntExpr mkMod ( Expr< IntSort >  t1,
Expr< IntSort >  t2 
)
inline

Create an expression representing

t1 mod t2
z3::mod
expr mod(expr const &a, expr const &b)
Definition: z3++.h:1641

. Remarks: The arguments must have int type.

Definition at line 908 of file Context.java.

909  {
910  checkContextMatch(t1);
911  checkContextMatch(t2);
912  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
913  t2.getNativeObject()));
914  }

◆ mkMul()

final<R extends ArithSort> ArithExpr<R> mkMul ( Expr<? extends R >...  t)
inline

Create an expression representing

t[0] * t[1] * ...

.

Definition at line 864 of file Context.java.

865  {
866  checkContextMatch(t);
867  return (ArithExpr<R>) Expr.create(this,
868  Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
869  }

◆ mkNot()

final BoolExpr mkNot ( Expr< BoolSort >  a)
inline

Create an expression representing

not(a)
com.microsoft.z3.Context.not
Probe not(Probe p)
Definition: Context.java:3333

.

Definition at line 772 of file Context.java.

773  {
774  checkContextMatch(a);
775  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
776  }

◆ mkNth()

final<R extends Sort> Expr<R> mkNth ( Expr< SeqSort< R >>  s,
Expr< IntSort >  index 
)
inline

Retrieve element at index.

Definition at line 2156 of file Context.java.

2157  {
2158  checkContextMatch(s, index);
2159  return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
2160  }

◆ mkNumeral() [1/3]

final<R extends Sort> Expr<R> mkNumeral ( int  v,
R  ty 
)
inline

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
vValue of the numeral
tySort of the numeral
Returns
A Term with value
v
and type
ty

Definition at line 2465 of file Context.java.

2466  {
2467  checkContextMatch(ty);
2468  return (Expr<R>) Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2469  }

◆ mkNumeral() [2/3]

final<R extends Sort> Expr<R> mkNumeral ( long  v,
R  ty 
)
inline

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
vValue of the numeral
tySort of the numeral
Returns
A Term with value
v
and type
ty

Definition at line 2481 of file Context.java.

2482  {
2483  checkContextMatch(ty);
2484  return (Expr<R>) Expr.create(this,
2485  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2486  }

◆ mkNumeral() [3/3]

final<R extends Sort> Expr<R> mkNumeral ( String  v,
R  ty 
)
inline

Create a Term of a given sort.

Parameters
vA 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]*
.
tyThe 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

Definition at line 2448 of file Context.java.

2449  {
2450  checkContextMatch(ty);
2451  return (Expr<R>) Expr.create(this,
2452  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2453  }

◆ mkOptimize()

Optimize mkOptimize ( )
inline

Create a Optimize context.

Definition at line 3417 of file Context.java.

3418  {
3419  return new Optimize(this);
3420  }

◆ mkOption()

final<R extends Sort> ReExpr<R> mkOption ( Expr< ReSort< R >>  re)
inline

Create the optional regular expression.

Definition at line 2255 of file Context.java.

2256  {
2257  checkContextMatch(re);
2258  return (ReExpr<R>) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2259  }

◆ mkOr()

final BoolExpr mkOr ( Expr< BoolSort >...  t)
inline

Create an expression representing

t[0] or t[1] or ...
com.microsoft.z3.Context.or
Probe or(Probe p1, Probe p2)
Definition: Context.java:3322

.

Definition at line 842 of file Context.java.

843  {
844  checkContextMatch(t);
845  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
846  AST.arrayToNative(t)));
847  }

◆ mkParams()

Params mkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2860 of file Context.java.

2861  {
2862  return new Params(this);
2863  }

◆ mkPartialOrder()

final<R extends Sort> FuncDecl<BoolSort> mkPartialOrder ( R  sort,
int  index 
)
inline

Creates or a partial order.

Parameters
indexThe index of the order.
sortThe sort of the order.

Definition at line 4214 of file Context.java.

4214  {
4215  return (FuncDecl<BoolSort>) FuncDecl.create(
4216  this,
4217  Native.mkPartialOrder(
4218  nCtx(),
4219  sort.getNativeObject(),
4220  index
4221  )
4222  );
4223  }

◆ mkPattern()

final Pattern mkPattern ( Expr<?>...  terms)
inline

Create a quantifier pattern.

Definition at line 594 of file Context.java.

595  {
596  if (terms.length == 0)
597  throw new Z3Exception("Cannot create a pattern from zero terms");
598 
599  long[] termsNative = AST.arrayToNative(terms);
600  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
601  termsNative));
602  }

◆ mkPBEq()

BoolExpr mkPBEq ( int[]  coeffs,
Expr< BoolSort >[]  args,
int  k 
)
inline

Create a pseudo-Boolean equal constraint.

Definition at line 2431 of file Context.java.

2432  {
2433  checkContextMatch(args);
2434  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2435  }

◆ mkPBGe()

BoolExpr mkPBGe ( int[]  coeffs,
Expr< BoolSort >[]  args,
int  k 
)
inline

Create a pseudo-Boolean greater-or-equal constraint.

Definition at line 2422 of file Context.java.

2423  {
2424  checkContextMatch(args);
2425  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2426  }

◆ mkPBLe()

BoolExpr mkPBLe ( int[]  coeffs,
Expr< BoolSort >[]  args,
int  k 
)
inline

Create a pseudo-Boolean less-or-equal constraint.

Definition at line 2413 of file Context.java.

2414  {
2415  checkContextMatch(args);
2416  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2417  }

◆ mkPlus()

final<R extends Sort> ReExpr<R> mkPlus ( Expr< ReSort< R >>  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2246 of file Context.java.

2247  {
2248  checkContextMatch(re);
2249  return (ReExpr<R>) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2250  }

◆ mkPower() [1/2]

final<R extends Sort> ReExpr<R> mkPower ( Expr< ReSort< R >>  re,
int  n 
)
inline

Create power regular expression.

Definition at line 2221 of file Context.java.

2222  {
2223  return (ReExpr<R>) Expr.create(this, Native.mkRePower(nCtx(), re.getNativeObject(), n));
2224  }

◆ mkPower() [2/2]

final<R extends ArithSort> ArithExpr<R> mkPower ( Expr<? extends R >  t1,
Expr<? extends R >  t2 
)
inline

Create an expression representing

t1 ^ t2

.

Definition at line 932 of file Context.java.

934  {
935  checkContextMatch(t1);
936  checkContextMatch(t2);
937  return (ArithExpr<R>) Expr.create(
938  this,
939  Native.mkPower(nCtx(), t1.getNativeObject(),
940  t2.getNativeObject()));
941  }

◆ mkPrefixOf()

final<R extends Sort> BoolExpr mkPrefixOf ( Expr< SeqSort< R >>  s1,
Expr< SeqSort< R >>  s2 
)
inline

Check for sequence prefix.

Definition at line 2100 of file Context.java.

2101  {
2102  checkContextMatch(s1, s2);
2103  return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2104  }

◆ mkProbe()

Probe mkProbe ( String  name)
inline

Creates a new Probe.

Definition at line 3233 of file Context.java.

3234  {
3235  return new Probe(this, name);
3236  }

◆ mkPropagateFunction()

final<R extends Sort> FuncDecl<R> mkPropagateFunction ( Symbol  name,
Sort[]  domain,
R  range 
)
inline

Definition at line 455 of file Context.java.

456  {
457  checkContextMatch(name);
458  checkContextMatch(domain);
459  checkContextMatch(range);
460  long f = Native.solverPropagateDeclare(
461  this.nCtx(),
462  name.getNativeObject(),
463  AST.arrayLength(domain),
464  AST.arrayToNative(domain),
465  range.getNativeObject());
466  return new FuncDecl<>(this, f);
467  }

◆ mkQuantifier() [1/2]

Quantifier mkQuantifier ( boolean  universal,
Expr<?>[]  boundConstants,
Expr< BoolSort >  body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier

See also
mkForall(Sort[],Symbol[],Expr<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2706 of file Context.java.

2709  {
2710 
2711  if (universal)
2712  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2713  quantifierID, skolemID);
2714  else
2715  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2716  quantifierID, skolemID);
2717  }
com.microsoft.z3.Context.mkForall
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2637
com.microsoft.z3.Context.mkExists
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2662

◆ mkQuantifier() [2/2]

Quantifier mkQuantifier ( boolean  universal,
Sort[]  sorts,
Symbol[]  names,
Expr< BoolSort >  body,
int  weight,
Pattern[]  patterns,
Expr<?>[]  noPatterns,
Symbol  quantifierID,
Symbol  skolemID 
)
inline

Create a Quantifier.

See also
mkForall(Sort[],Symbol[],Expr<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol)

Definition at line 2688 of file Context.java.

2692  {
2693 
2694  if (universal)
2695  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2696  quantifierID, skolemID);
2697  else
2698  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2699  quantifierID, skolemID);
2700  }

◆ mkRange()

final ReExpr<SeqSort<CharSort> > mkRange ( Expr< SeqSort< CharSort >>  lo,
Expr< SeqSort< CharSort >>  hi 
)
inline

Create a range expression.

Definition at line 2341 of file Context.java.

2342  {
2343  checkContextMatch(lo, hi);
2344  return (ReExpr<SeqSort<CharSort>>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2345  }

◆ mkReal() [1/4]

RatNum mkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

Parameters
numnumerator of rational.
dendenominator of rational.
Returns
A Term with value
num
/
den
and sort Real
See also
mkNumeral(String v, R ty)

Definition at line 2497 of file Context.java.

2498  {
2499  if (den == 0) {
2500  throw new Z3Exception("Denominator is zero");
2501  }
2502 
2503  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2504  }

◆ mkReal() [2/4]

RatNum mkReal ( int  v)
inline

Create a real numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Real

Definition at line 2525 of file Context.java.

2526  {
2527 
2528  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2529  .getNativeObject()));
2530  }

◆ mkReal() [3/4]

RatNum mkReal ( long  v)
inline

Create a real numeral.

Parameters
vvalue of the numeral.
Returns
A Term with value
v
and sort Real

Definition at line 2538 of file Context.java.

2539  {
2540 
2541  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2542  .getNativeObject()));
2543  }

◆ mkReal() [4/4]

RatNum mkReal ( String  v)
inline

Create a real numeral.

Parameters
vA string representing the Term value in decimal notation.
Returns
A Term with value
v
and sort Real

Definition at line 2512 of file Context.java.

2513  {
2514 
2515  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2516  .getNativeObject()));
2517  }

◆ mkReal2Int()

IntExpr mkReal2Int ( Expr< RealSort >  t)
inline

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.

Definition at line 1010 of file Context.java.

1011  {
1012  checkContextMatch(t);
1013  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
1014  }

◆ mkRealConst() [1/2]

RealExpr mkRealConst ( String  name)
inline

Creates a real constant.

Definition at line 691 of file Context.java.

692  {
693  return (RealExpr) mkConst(name, getRealSort());
694  }

◆ mkRealConst() [2/2]

RealExpr mkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 683 of file Context.java.

684  {
685  return (RealExpr) mkConst(name, getRealSort());
686  }

◆ mkRealSort()

RealSort mkRealSort ( )
inline

Create a real sort.

Definition at line 214 of file Context.java.

215  {
216  return new RealSort(this);
217  }

◆ mkRecFuncDecl()

final<R extends Sort> FuncDecl<R> mkRecFuncDecl ( Symbol  name,
Sort[]  domain,
R  range 
)
inline

Creates a new recursive function declaration.

Definition at line 509 of file Context.java.

510  {
511  checkContextMatch(name);
512  checkContextMatch(domain);
513  checkContextMatch(range);
514  return new FuncDecl<>(this, name, domain, range, true);
515  }

◆ mkRem()

IntExpr mkRem ( Expr< IntSort >  t1,
Expr< IntSort >  t2 
)
inline

Create an expression representing

t1 rem t2
z3::rem
expr rem(expr const &a, expr const &b)
Definition: z3++.h:1657

. Remarks: The arguments must have int type.

Definition at line 921 of file Context.java.

922  {
923  checkContextMatch(t1);
924  checkContextMatch(t2);
925  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
926  t2.getNativeObject()));
927  }

◆ mkRepeat()

BitVecExpr mkRepeat ( int  i,
Expr< BitVecSort >  t 
)
inline

Bit-vector repetition. Remarks: The argument

t

must have a bit-vector sort.

Definition at line 1442 of file Context.java.

1443  {
1444  checkContextMatch(t);
1445  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1446  t.getNativeObject()));
1447  }

◆ mkReplace()

final<R extends Sort> SeqExpr<R> mkReplace ( Expr< SeqSort< R >>  s,
Expr< SeqSort< R >>  src,
Expr< SeqSort< R >>  dst 
)
inline

Replace the first occurrence of src by dst in s.

Definition at line 2184 of file Context.java.

2185  {
2186  checkContextMatch(s, src, dst);
2187  return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2188  }

◆ mkReSort()

final<R extends Sort> ReSort<R> mkReSort ( R  s)
inline

Create a new regular expression sort

Definition at line 267 of file Context.java.

268  {
269  return new ReSort<>(this, Native.mkReSort(nCtx(), s.getNativeObject()));
270  }

◆ mkSelect() [1/2]

final<D extends Sort, R extends Sort> Expr<R> mkSelect ( Expr< ArraySort< D, R >>  a,
Expr< D >  i 
)
inline

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
mkArraySort(Sort[], R)
mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)

Definition at line 1738 of file Context.java.

1739  {
1740  checkContextMatch(a);
1741  checkContextMatch(i);
1742  return (Expr<R>) Expr.create(
1743  this,
1744  Native.mkSelect(nCtx(), a.getNativeObject(),
1745  i.getNativeObject()));
1746  }

◆ mkSelect() [2/2]

final<R extends Sort> Expr<R> mkSelect ( Expr< ArraySort< Sort, R >>  a,
Expr<?>[]  args 
)
inline

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
mkArraySort(Sort[], R)
mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)

Definition at line 1760 of file Context.java.

1761  {
1762  checkContextMatch(a);
1763  checkContextMatch(args);
1764  return (Expr<R>) Expr.create(
1765  this,
1766  Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
1767  }

◆ mkSeqSort()

final<R extends Sort> SeqSort<R> mkSeqSort ( R  s)
inline

Create a new sequence sort

Definition at line 259 of file Context.java.

260  {
261  return new SeqSort<>(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
262  }

◆ mkSetAdd()

final<D extends Sort> ArrayExpr<D, BoolSort> mkSetAdd ( Expr< ArraySort< D, BoolSort >>  set,
Expr< D >  element 
)
inline

Add an element to the set.

Definition at line 1915 of file Context.java.

1916  {
1917  checkContextMatch(set);
1918  checkContextMatch(element);
1919  return (ArrayExpr<D, BoolSort>) Expr.create(this,
1920  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1921  element.getNativeObject()));
1922  }

◆ mkSetComplement()

final<D extends Sort> ArrayExpr<D, BoolSort> mkSetComplement ( Expr< ArraySort< D, BoolSort >>  arg)
inline

Take the complement of a set.

Definition at line 1975 of file Context.java.

1976  {
1977  checkContextMatch(arg);
1978  return (ArrayExpr<D, BoolSort>)Expr.create(this,
1979  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1980  }

◆ mkSetDel()

final<D extends Sort> ArrayExpr<D, BoolSort> mkSetDel ( Expr< ArraySort< D, BoolSort >>  set,
Expr< D >  element 
)
inline

Remove an element from a set.

Definition at line 1927 of file Context.java.

1928  {
1929  checkContextMatch(set);
1930  checkContextMatch(element);
1931  return (ArrayExpr<D, BoolSort>)Expr.create(this,
1932  Native.mkSetDel(nCtx(), set.getNativeObject(),
1933  element.getNativeObject()));
1934  }

◆ mkSetDifference()

final<D extends Sort> ArrayExpr<D, BoolSort> mkSetDifference ( Expr< ArraySort< D, BoolSort >>  arg1,
Expr< ArraySort< D, BoolSort >>  arg2 
)
inline

Take the difference between two sets.

Definition at line 1963 of file Context.java.

1964  {
1965  checkContextMatch(arg1);
1966  checkContextMatch(arg2);
1967  return (ArrayExpr<D, BoolSort>) Expr.create(this,
1968  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1969  arg2.getNativeObject()));
1970  }

◆ mkSetIntersection()

final<D extends Sort> ArrayExpr<D, BoolSort> mkSetIntersection ( Expr< ArraySort< D, BoolSort >>...  args)
inline

Take the intersection of a list of sets.

Definition at line 1952 of file Context.java.

1953  {
1954  checkContextMatch(args);
1955  return (ArrayExpr<D, BoolSort>) Expr.create(this,
1956  Native.mkSetIntersect(nCtx(), args.length,
1957  AST.arrayToNative(args)));
1958  }

◆ mkSetMembership()

final<D extends Sort> BoolExpr mkSetMembership ( Expr< D >  elem,
Expr< ArraySort< D, BoolSort >>  set 
)
inline

Check for set membership.

Definition at line 1985 of file Context.java.

1986  {
1987  checkContextMatch(elem);
1988  checkContextMatch(set);
1989  return (BoolExpr) Expr.create(this,
1990  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1991  set.getNativeObject()));
1992  }

◆ mkSetSort()

final<D extends Sort> SetSort<D> mkSetSort ( D  ty)
inline

Create a set type.

Definition at line 1886 of file Context.java.

1887  {
1888  checkContextMatch(ty);
1889  return new SetSort<>(this, ty);
1890  }

◆ mkSetSubset()

final<D extends Sort> BoolExpr mkSetSubset ( Expr< ArraySort< D, BoolSort >>  arg1,
Expr< ArraySort< D, BoolSort >>  arg2 
)
inline

Check for subsetness of sets.

Definition at line 1997 of file Context.java.

1998  {
1999  checkContextMatch(arg1);
2000  checkContextMatch(arg2);
2001  return (BoolExpr) Expr.create(this,
2002  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
2003  arg2.getNativeObject()));
2004  }

◆ mkSetUnion()

final<D extends Sort> ArrayExpr<D, BoolSort> mkSetUnion ( Expr< ArraySort< D, BoolSort >>...  args)
inline

Take the union of a list of sets.

Definition at line 1940 of file Context.java.

1941  {
1942  checkContextMatch(args);
1943  return (ArrayExpr<D, BoolSort>)Expr.create(this,
1944  Native.mkSetUnion(nCtx(), args.length,
1945  AST.arrayToNative(args)));
1946  }

◆ mkSignExt()

BitVecExpr mkSignExt ( int  i,
Expr< BitVecSort >  t 
)
inline

Bit-vector sign extension. Remarks: Sign-extends the given bit-vector to the (signed) equivalent bitvector of size

m+i

, where m is the size of the given bit-vector. The argument

t

must have a bit-vector sort.

Definition at line 1416 of file Context.java.

1417  {
1418  checkContextMatch(t);
1419  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1420  t.getNativeObject()));
1421  }

◆ mkSimpleSolver()

Solver mkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3380 of file Context.java.

3381  {
3382  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3383  }

◆ mkSimplifier()

Simplifier mkSimplifier ( String  name)
inline

Creates a new Simplifier.

Definition at line 3133 of file Context.java.

3134  {
3135  return new Simplifier(this, name);
3136  }

◆ mkSolver() [1/5]

Solver mkSolver ( )
inline

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.

Definition at line 3346 of file Context.java.

3347  {
3348  return mkSolver((Symbol) null);
3349  }

Referenced by Tactic.getSolver().

◆ mkSolver() [2/5]

Solver mkSolver ( Solver  s,
Simplifier  simp 
)
inline

Creates a solver that is uses the simplifier pre-processing.

Definition at line 3401 of file Context.java.

3402  {
3403  return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.getNativeObject()));
3404  }

◆ mkSolver() [3/5]

Solver mkSolver ( String  logic)
inline

Creates a new (incremental) solver.

See also
mkSolver(Symbol)

Definition at line 3372 of file Context.java.

3373  {
3374  return mkSolver(mkSymbol(logic));
3375  }

◆ mkSolver() [4/5]

Solver mkSolver ( Symbol  logic)
inline

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.

Definition at line 3358 of file Context.java.

3359  {
3360 
3361  if (logic == null)
3362  return new Solver(this, Native.mkSolver(nCtx()));
3363  else
3364  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3365  logic.getNativeObject()));
3366  }

◆ mkSolver() [5/5]

Solver mkSolver ( Tactic  t)
inline

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.

Definition at line 3391 of file Context.java.

3392  {
3393 
3394  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3395  t.getNativeObject()));
3396  }

◆ mkStar()

final<R extends Sort> ReExpr<R> mkStar ( Expr< ReSort< R >>  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2212 of file Context.java.

2213  {
2214  checkContextMatch(re);
2215  return (ReExpr<R>) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2216  }

◆ mkStore() [1/2]

final<D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore ( Expr< ArraySort< D, R >>  a,
Expr< D >  i,
Expr< R >  v 
)
inline

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[], R)
mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)

Definition at line 1785 of file Context.java.

1786  {
1787  checkContextMatch(a);
1788  checkContextMatch(i);
1789  checkContextMatch(v);
1790  return new ArrayExpr<>(this, Native.mkStore(nCtx(), a.getNativeObject(),
1791  i.getNativeObject(), v.getNativeObject()));
1792  }

◆ mkStore() [2/2]

final<R extends Sort> ArrayExpr<Sort, R> mkStore ( Expr< ArraySort< Sort, R >>  a,
Expr<?>[]  args,
Expr< R >  v 
)
inline

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
mkArraySort(Sort[], R)
mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)

Definition at line 1810 of file Context.java.

1811  {
1812  checkContextMatch(a);
1813  checkContextMatch(args);
1814  checkContextMatch(v);
1815  return new ArrayExpr<>(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
1816  args.length, AST.arrayToNative(args), v.getNativeObject()));
1817  }

◆ mkString()

SeqExpr<CharSort> mkString ( String  s)
inline

Create a string constant.

Definition at line 2032 of file Context.java.

2033  {
2034  StringBuilder buf = new StringBuilder();
2035  for (int i = 0; i < s.length(); ++i) {
2036  int code = s.codePointAt(i);
2037  if (code <= 32 || 127 < code)
2038  buf.append(String.format("\\u{%x}", code));
2039  else
2040  buf.append(s.charAt(i));
2041  }
2042  return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), buf.toString()));
2043  }

◆ MkStringLe()

BoolExpr MkStringLe ( Expr< SeqSort< CharSort >>  s1,
Expr< SeqSort< CharSort >>  s2 
)
inline

Check if the string s1 is lexicographically less or equal to s2.

Definition at line 2137 of file Context.java.

2138  {
2139  checkContextMatch(s1, s2);
2140  return new BoolExpr(this, Native.mkStrLe(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2141  }

◆ MkStringLt()

BoolExpr MkStringLt ( Expr< SeqSort< CharSort >>  s1,
Expr< SeqSort< CharSort >>  s2 
)
inline

Check if the string s1 is lexicographically strictly less than s2.

Definition at line 2128 of file Context.java.

2129  {
2130  checkContextMatch(s1, s2);
2131  return new BoolExpr(this, Native.mkStrLt(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2132  }

◆ mkStringSort()

SeqSort<CharSort> mkStringSort ( )
inline

Create a new string sort

Definition at line 251 of file Context.java.

252  {
253  return new SeqSort<>(this, Native.mkStringSort(nCtx()));
254  }

◆ mkSub()

final<R extends ArithSort> ArithExpr<R> mkSub ( Expr<? extends R >...  t)
inline

Create an expression representing

t[0] - t[1] - ...

.

Definition at line 875 of file Context.java.

876  {
877  checkContextMatch(t);
878  return (ArithExpr<R>) Expr.create(this,
879  Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
880  }

◆ mkSuffixOf()

final<R extends Sort> BoolExpr mkSuffixOf ( Expr< SeqSort< R >>  s1,
Expr< SeqSort< R >>  s2 
)
inline

Check for sequence suffix.

Definition at line 2109 of file Context.java.

2110  {
2111  checkContextMatch(s1, s2);
2112  return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2113  }

◆ mkSymbol() [1/2]

IntSymbol mkSymbol ( int  i)
inline

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.

Definition at line 94 of file Context.java.

95  {
96  return new IntSymbol(this, i);
97  }

◆ mkSymbol() [2/2]

StringSymbol mkSymbol ( String  name)
inline

Create a symbol using a string.

Definition at line 102 of file Context.java.

103  {
104  return new StringSymbol(this, name);
105  }

◆ mkTactic()

Tactic mkTactic ( String  name)
inline

Creates a new Tactic.

Definition at line 2898 of file Context.java.

2899  {
2900  return new Tactic(this, name);
2901  }

Referenced by Goal.simplify().

◆ mkTermArray()

final<D extends Sort, R extends Sort> Expr<R> mkTermArray ( Expr< ArraySort< D, R >>  array)
inline

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.

Definition at line 1865 of file Context.java.

1866  {
1867  checkContextMatch(array);
1868  return (Expr<R>) Expr.create(this,
1869  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1870  }

◆ mkToRe()

final<R extends Sort> ReExpr<SeqSort<R> > mkToRe ( Expr< SeqSort< R >>  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2193 of file Context.java.

2194  {
2195  checkContextMatch(s);
2196  return (ReExpr<SeqSort<R>>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2197  }

◆ mkTrue()

BoolExpr mkTrue ( )
inline

The true Term.

Definition at line 726 of file Context.java.

727  {
728  return new BoolExpr(this, Native.mkTrue(nCtx()));
729  }

Referenced by Goal.AsBoolExpr().

◆ mkTupleSort()

TupleSort mkTupleSort ( Symbol  name,
Symbol[]  fieldNames,
Sort[]  fieldSorts 
)
inline

Create a new tuple sort.

Definition at line 276 of file Context.java.

278  {
279  checkContextMatch(name);
280  checkContextMatch(fieldNames);
281  checkContextMatch(fieldSorts);
282  return new TupleSort(this, name, fieldNames.length, fieldNames,
283  fieldSorts);
284  }
z3py.TupleSort
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5409

◆ mkUnaryMinus()

final<R extends ArithSort> ArithExpr<R> mkUnaryMinus ( Expr< R >  t)
inline

Create an expression representing

-t

.

Definition at line 885 of file Context.java.

886  {
887  checkContextMatch(t);
888  return (ArithExpr<R>) Expr.create(this,
889  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
890  }

◆ mkUninterpretedSort() [1/2]

UninterpretedSort mkUninterpretedSort ( String  str)
inline

Create a new uninterpreted sort.

Definition at line 198 of file Context.java.

199  {
200  return mkUninterpretedSort(mkSymbol(str));
201  }
com.microsoft.z3.Context.mkUninterpretedSort
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:189

◆ mkUninterpretedSort() [2/2]

UninterpretedSort mkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 189 of file Context.java.

190  {
191  checkContextMatch(s);
192  return new UninterpretedSort(this, s);
193  }

◆ mkUnion()

final<R extends Sort> ReExpr<R> mkUnion ( Expr< ReSort< R >>...  t)
inline

Create the union of regular languages.

Definition at line 2284 of file Context.java.

2285  {
2286  checkContextMatch(t);
2287  return (ReExpr<R>) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2288  }

◆ mkUnit()

final<R extends Sort> SeqExpr<R> mkUnit ( Expr< R >  elem)
inline

Create the singleton sequence.

Definition at line 2023 of file Context.java.

2024  {
2025  checkContextMatch(elem);
2026  return (SeqExpr<R>) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
2027  }

◆ mkUpdateField()

final<F extends Sort, R extends Sort> Expr<R> mkUpdateField ( FuncDecl< F >  field,
Expr< R >  t,
Expr< F >  v 
) throws Z3Exception
inline

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.

Definition at line 434 of file Context.java.

436  {
437  return (Expr<R>) Expr.create(this,
438  Native.datatypeUpdateField
439  (nCtx(), field.getNativeObject(),
440  t.getNativeObject(), v.getNativeObject()));
441  }

◆ mkXor()

BoolExpr mkXor ( Expr< BoolSort >  t1,
Expr< BoolSort >  t2 
)
inline

Create an expression representing

t1 xor t2

.

Definition at line 819 of file Context.java.

820  {
821  checkContextMatch(t1);
822  checkContextMatch(t2);
823  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
824  t2.getNativeObject()));
825  }

◆ mkZeroExt()

BitVecExpr mkZeroExt ( int  i,
Expr< BitVecSort >  t 
)
inline

Bit-vector zero extension. Remarks: Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size

m+i

, where m is the size of the given bit-vector. The argument

t

must have a bit-vector sort.

Definition at line 1430 of file Context.java.

1431  {
1432  checkContextMatch(t);
1433  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1434  t.getNativeObject()));
1435  }

◆ nCtx()

long nCtx ( )
inline

Definition at line 4288 of file Context.java.

4289  {
4290  if (m_ctx == 0)
4291  throw new Z3Exception("Context closed");
4292  return m_ctx;
4293  }

Referenced by UserPropagatorBase.add(), ASTVector.ASTVector(), UserPropagatorBase.consequence(), AST.equals(), FuncDecl< R extends Sort >.equals(), Sort.equals(), FPRMSort.FPRMSort(), FPSort.FPSort(), UserPropagatorBase.nextSplit(), Quantifier.of(), Lambda< R extends Sort >.of(), ASTVector.set(), AST.translate(), ASTVector.translate(), Goal.translate(), Solver.translate(), and UserPropagatorBase.UserPropagatorBase().

◆ not()

Probe not ( Probe  p)
inline

Create a probe that evaluates to

true

when the value

p

does not evaluate to

true

.

Definition at line 3333 of file Context.java.

3334  {
3335  checkContextMatch(p);
3336  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3337  }

◆ or()

Probe or ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to

true

when the value

p1

or

p2

evaluate to

true

.

Definition at line 3322 of file Context.java.

3323  {
3324  checkContextMatch(p1);
3325  checkContextMatch(p2);
3326  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3327  p2.getNativeObject()));
3328  }

◆ orElse()

Tactic orElse ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that first applies

t1

to a Goal and if it fails then returns the result of

t2

applied to the Goal.

Definition at line 2949 of file Context.java.

2950  {
2951  checkContextMatch(t1);
2952  checkContextMatch(t2);
2953  return new Tactic(this, Native.tacticOrElse(nCtx(),
2954  t1.getNativeObject(), t2.getNativeObject()));
2955  }

◆ parAndThen()

Tactic parAndThen ( Tactic  t1,
Tactic  t2 
)
inline

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.

Definition at line 3082 of file Context.java.

3083  {
3084  checkContextMatch(t1);
3085  checkContextMatch(t2);
3086  return new Tactic(this, Native.tacticParAndThen(nCtx(),
3087  t1.getNativeObject(), t2.getNativeObject()));
3088  }

◆ parOr()

Tactic parOr ( Tactic...  t)
inline

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

Definition at line 3071 of file Context.java.

3072  {
3073  checkContextMatch(t);
3074  return new Tactic(this, Native.tacticParOr(nCtx(),
3075  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
3076  }

◆ parseSMTLIB2File()

BoolExpr [] parseSMTLIB2File ( String  fileName,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl<?>[]  decls 
)
inline

Parse the given file using the SMT-LIB2 parser.

See also
parseSMTLIB2String

Definition at line 2825 of file Context.java.

2827  {
2828  int csn = Symbol.arrayLength(sortNames);
2829  int cs = Sort.arrayLength(sorts);
2830  int cdn = Symbol.arrayLength(declNames);
2831  int cd = AST.arrayLength(decls);
2832  if (csn != cs || cdn != cd)
2833  throw new Z3Exception("Argument size mismatch");
2834  ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2835  fileName, AST.arrayLength(sorts),
2836  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2837  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2838  AST.arrayToNative(decls)));
2839  return v.ToBoolExprArray();
2840  }

◆ parseSMTLIB2String()

BoolExpr [] parseSMTLIB2String ( String  str,
Symbol[]  sortNames,
Sort[]  sorts,
Symbol[]  declNames,
FuncDecl<?>[]  decls 
)
inline

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.

Definition at line 2804 of file Context.java.

2806  {
2807  int csn = Symbol.arrayLength(sortNames);
2808  int cs = Sort.arrayLength(sorts);
2809  int cdn = Symbol.arrayLength(declNames);
2810  int cd = AST.arrayLength(decls);
2811  if (csn != cs || cdn != cd) {
2812  throw new Z3Exception("Argument size mismatch");
2813  }
2814  ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2815  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2816  AST.arrayToNative(sorts), AST.arrayLength(decls),
2817  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2818  return v.ToBoolExprArray();
2819  }

◆ repeat()

Tactic repeat ( Tactic  t,
int  max 
)
inline

Create a tactic that keeps applying

t

until the goal is not modified anymore or the maximum number of iterations

max
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1967

is reached.

Definition at line 3002 of file Context.java.

3003  {
3004  checkContextMatch(t);
3005  return new Tactic(this, Native.tacticRepeat(nCtx(),
3006  t.getNativeObject(), max));
3007  }

◆ sbvToString()

SeqExpr<CharSort> sbvToString ( Expr< BitVecSort >  e)
inline

Convert an signed bitvector expression to a string.

Definition at line 2064 of file Context.java.

2065  {
2066  return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
2067  }

◆ setPrintMode()

void setPrintMode ( Z3_ast_print_mode  value)
inline

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

Definition at line 2767 of file Context.java.

2768  {
2769  Native.setAstPrintMode(nCtx(), value.toInt());
2770  }

◆ SimplifyHelp()

String SimplifyHelp ( )
inline

Return a string describing all available parameters to

Expr.Simplify

.

Definition at line 4261 of file Context.java.

4262  {
4263  return Native.simplifyGetHelp(nCtx());
4264  }

◆ skip()

Tactic skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 3012 of file Context.java.

3013  {
3014  return new Tactic(this, Native.tacticSkip(nCtx()));
3015  }

◆ stringToInt()

IntExpr stringToInt ( Expr< SeqSort< CharSort >>  e)
inline

Convert an integer expression to a string.

Definition at line 2072 of file Context.java.

2073  {
2074  return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
2075  }

◆ then() [1/2]

Simplifier then ( Simplifier  t1,
Simplifier  t2,
Simplifier...  ts 
)
inline

Create a simplifier that applies

t1

and then

t2

Remarks: Shorthand for

AndThen
z3py.AndThen
def AndThen(*ts, **ks)
Definition: z3py.py:8430

.

Definition at line 3172 of file Context.java.

3173  {
3174  return andThen(t1, t2, ts);
3175  }
com.microsoft.z3.Context.andThen
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2907

◆ then() [2/2]

Tactic then ( Tactic  t1,
Tactic  t2,
Tactic...  ts 
)
inline

Create a tactic that applies

t1

to a Goal and then

t2

to every subgoal produced by

t1

Remarks: Shorthand for

AndThen

.

Definition at line 2939 of file Context.java.

2940  {
2941  return andThen(t1, t2, ts);
2942  }

◆ tryFor()

Tactic tryFor ( Tactic  t,
int  ms 
)
inline

Create a tactic that applies

t

to a goal for

ms

milliseconds. Remarks: If

t

does not terminate within

ms

milliseconds, then it fails.

Definition at line 2963 of file Context.java.

2964  {
2965  checkContextMatch(t);
2966  return new Tactic(this, Native.tacticTryFor(nCtx(),
2967  t.getNativeObject(), ms));
2968  }

◆ ubvToString()

SeqExpr<CharSort> ubvToString ( Expr< BitVecSort >  e)
inline

Convert an unsigned bitvector expression to a string.

Definition at line 2056 of file Context.java.

2057  {
2058  return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
2059  }

◆ unwrapAST()

long unwrapAST ( AST  a)
inline

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

See also
Native::incRef
wrapAST
Parameters
aThe AST to unwrap.

Definition at line 4252 of file Context.java.

4253  {
4254  return a.getNativeObject();
4255  }

◆ updateParamValue()

void updateParamValue ( String  id,
String  value 
)
inline

Update a mutable configuration parameter. Remarks: The list of all configuration parameters can be obtained using the Z3 executable:

z3.exe -ini?
z3
Z3 C++ namespace.
Definition: z3++.h:49

Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

Definition at line 4282 of file Context.java.

4283  {
4284  Native.updateParamValue(nCtx(), id, value);
4285  }

◆ usingParams() [1/2]

Simplifier usingParams ( Simplifier  t,
Params  p 
)
inline

Create a simplifier that applies

t

using the given set of parameters

p

.

Definition at line 3181 of file Context.java.

3182  {
3183  checkContextMatch(t);
3184  checkContextMatch(p);
3185  return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
3186  t.getNativeObject(), p.getNativeObject()));
3187  }

◆ usingParams() [2/2]

Tactic usingParams ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

.

Definition at line 3049 of file Context.java.

3050  {
3051  checkContextMatch(t);
3052  checkContextMatch(p);
3053  return new Tactic(this, Native.tacticUsingParams(nCtx(),
3054  t.getNativeObject(), p.getNativeObject()));
3055  }

◆ when()

Tactic when ( Probe  p,
Tactic  t 
)
inline

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.

Definition at line 2976 of file Context.java.

2977  {
2978  checkContextMatch(t);
2979  checkContextMatch(p);
2980  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2981  t.getNativeObject()));
2982  }

◆ with() [1/2]

Simplifier with ( Simplifier  t,
Params  p 
)
inline

Create a simplifier that applies

t

using the given set of parameters

p

. Remarks: Alias for

UsingParams

Definition at line 3195 of file Context.java.

3196  {
3197  return usingParams(t, p);
3198  }
com.microsoft.z3.Context.usingParams
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:3049

◆ with() [2/2]

Tactic with ( Tactic  t,
Params  p 
)
inline

Create a tactic that applies

t

using the given set of parameters

p

. Remarks: Alias for

UsingParams

Definition at line 3063 of file Context.java.

3064  {
3065  return usingParams(t, p);
3066  }

◆ wrapAST()

AST wrapAST ( long  nativeObject)
inline

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.

See also
Native::incRef
unwrapAST
Parameters
nativeObjectThe native pointer to wrap.

Definition at line 4235 of file Context.java.

4236  {
4237  return AST.create(this, nativeObject);
4238  }
Generated on Thu Oct 10 2024 23:21:50 for Z3 by doxygen 1.9.1