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

ComplexSort	getComplexSort ()

ComplexSort	mkComplexSort ()

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)

TypeVarSort	mkTypeVariable (Symbol name)

TypeVarSort	mkTypeVariable (String name)

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)

ComplexExpr	mkComplexConst (Symbol name)

ComplexExpr	mkComplexConst (String name)

ComplexExpr	mkComplex (Expr<? extends ArithSort > real, Expr<? extends ArithSort > imag)

RealExpr	mkRealPart (Expr< ComplexSort > value)

RealExpr	mkImagPart (Expr< ComplexSort > value)

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)

BoolExpr	mkDivides (Expr< IntSort > t1, Expr< IntSort > t2)

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 > ArrayExpr< D, R >	mkAsArray (FuncDecl< R > f)

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 FiniteSetSort	mkFiniteSetSort (Sort elemSort)

final boolean	isFiniteSetSort (Sort s)

final Sort	getFiniteSetSortBasis (Sort s)

final Expr	mkFiniteSetEmpty (Sort setSort)

final Expr	mkFiniteSetSingleton (Expr elem)

final Expr	mkFiniteSetUnion (Expr s1, Expr s2)

final Expr	mkFiniteSetIntersect (Expr s1, Expr s2)

final Expr	mkFiniteSetDifference (Expr s1, Expr s2)

final BoolExpr	mkFiniteSetMember (Expr elem, Expr set)

final Expr	mkFiniteSetSize (Expr set)

final BoolExpr	mkFiniteSetSubset (Expr s1, Expr s2)

final Expr	mkFiniteSetMap (Expr f, Expr set)

final Expr	mkFiniteSetFilter (Expr f, Expr set)

final Expr	mkFiniteSetRange (Expr low, Expr high)

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 > SeqExpr< R >	mkSeqPower (Expr< SeqSort< R > > s, Expr< IntSort > n)

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 > IntExpr	mkLastIndexOf (Expr< SeqSort< R > > s, Expr< SeqSort< R > > substr)

final< R extends Sort > SeqExpr< R >	mkSeqMap (Expr<?> f, Expr< SeqSort< R > > s)

final< R extends Sort > SeqExpr< R >	mkSeqMapi (Expr<?> f, Expr< IntSort > i, Expr< SeqSort< R > > s)

final< R extends Sort, A extends Sort > Expr< A >	mkSeqFoldl (Expr<?> f, Expr< A > a, Expr< SeqSort< R > > s)

final< R extends Sort, A extends Sort > Expr< A >	mkSeqFoldli (Expr<?> f, Expr< IntSort > i, Expr< A > a, Expr< SeqSort< R > > s)

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

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

final< R extends Sort > SeqExpr< R >	mkReplaceRe (Expr< SeqSort< R > > s, ReExpr< SeqSort< R > > re, Expr< SeqSort< R > > dst)

final< R extends Sort > SeqExpr< R >	mkReplaceReAll (Expr< SeqSort< R > > s, ReExpr< SeqSort< R > > re, 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 ()

ASTMap	mkASTMap ()

Expr<?>	qeLite (ASTVector vars, Expr<?> body)

Expr<?>	qeModelProject (Model model, Expr<?>[] bounds, Expr<?> body)

Expr<?>	qeModelProjectSkolem (Model model, Expr<?>[] bounds, Expr<?> body, ASTMap map)

Expr<?>	qeModelProjectWithWitness (Model model, Expr<?>[] bounds, Expr<?> body, ASTMap map)

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)

final< R extends Sort > FuncDecl< BoolSort >	mkTransitiveClosure (FuncDecl< BoolSort > f)

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

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

final< R extends Sort > ASTVector	polynomialSubresultants (Expr< R > p, Expr< R > q, Expr< R > x)

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.

                      {
        synchronized (creation_lock) {
            m_ctx = Native.mkContextRc(0);
            init();
        }
    }

◆ Context() [2/3]

Context ( long m_ctx )

inlineprotected

Definition at line 47 of file Context.java.

                                   {
        synchronized (creation_lock) {
            this.m_ctx = m_ctx;
            init();
        }
    }

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

                                                 {
        synchronized (creation_lock) {
            long cfg = Native.mkConfig();
            for (Map.Entry<String, String> kv : settings.entrySet()) {
                Native.setParamValue(cfg, kv.getKey(), kv.getValue());
            }
            m_ctx = Native.mkContextRc(cfg);
            Native.delConfig(cfg);
            init();
        }
    }

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 670 of file Context.java.

    {
        checkContextMatch(f);
        checkContextMatch(args);
        checkContextMatch(body);
        long[] argsNative = AST.arrayToNative(args);
        Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject());
    }

◆ 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 3811 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

◆ andThen() [1/2]

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

inline

Create a simplifier that applies t1 and then t1

Definition at line 3641 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(ts);
 
        long last = 0;
        if (ts != null && ts.length > 0)
        {
            last = ts[ts.length - 1].getNativeObject();
            for (int i = ts.length - 2; i >= 0; i--) {
                last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
                    last);
            }
        }
        if (last != 0)
        {
            last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
                    t1.getNativeObject(), last));
        } else
            return new Simplifier(this, Native.simplifierAndThen(nCtx(),
                    t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 3345 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(ts);
 
        long last = 0;
        if (ts != null && ts.length > 0)
        {
            last = ts[ts.length - 1].getNativeObject();
            for (int i = ts.length - 2; i >= 0; i--) {
                last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
                    last);
            }
        }
        if (last != 0)
        {
            last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
            return new Tactic(this, Native.tacticAndThen(nCtx(),
                    t1.getNativeObject(), last));
        } else
            return new Tactic(this, Native.tacticAndThen(nCtx(),
                    t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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

name	Name of the benchmark. The argument is optional.
logic	The benchmark logic.
status	The status string (sat, unsat, or unknown)
attributes	Other attributes, such as source, difficulty or category.
assumptions	Auxiliary assumptions.
formula	Formula to be checked for consistency in conjunction with assumptions.

Returns: A string representation of the benchmark.

Definition at line 3223 of file Context.java.

    {
 
        return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
                attributes, assumptions.length,
                AST.arrayToNative(assumptions), formula.getNativeObject());
    }

◆ charFromBv()

Expr< CharSort > charFromBv ( BitVecExpr bv )

inline

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

Definition at line 2815 of file Context.java.

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

◆ charToBv()

BitVecExpr charToBv ( Expr< CharSort > ch )

inline

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

Definition at line 2806 of file Context.java.

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

◆ charToInt()

IntExpr charToInt ( Expr< CharSort > ch )

inline

Create an integer (code point) from character.

Definition at line 2797 of file Context.java.

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

◆ close()

void close ( )

inline

Disposes of the context.

Definition at line 4904 of file Context.java.

    {
        if (m_ctx == 0)
            return;
 
        m_RefQueue.forceClear();
 
        m_boolSort = null;
        m_intSort = null;
        m_realSort = null;
        m_complexSort = null;
        m_stringSort = null;
        m_RefQueue = null;
 
        synchronized (creation_lock) {
            Native.delContext(m_ctx);
        }
        m_ctx = 0;
    }

◆ 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 3427 of file Context.java.

    {
        checkContextMatch(p);
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ constProbe()

Probe constProbe ( double val )

inline

Create a probe that always evaluates to val.

Definition at line 3741 of file Context.java.

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

◆ 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 3800 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

Referenced by AstRef.__eq__(), SortRef.cast(), and FiniteSetSortRef.cast().

◆ fail()

Tactic fail ( )

inline

Create a tactic always fails.

Definition at line 3458 of file Context.java.

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

◆ failIf()

Tactic failIf ( Probe p )

inline

Create a tactic that fails if the probe p evaluates to false.

Definition at line 3467 of file Context.java.

    {
        checkContextMatch(p);
        return new Tactic(this,
                Native.tacticFailIf(nCtx(), p.getNativeObject()));
    }

◆ 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 3478 of file Context.java.

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

◆ 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 3788 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

◆ getBoolSort()

BoolSort getBoolSort ( )

inline

Retrieves the Boolean sort of the context.

Definition at line 129 of file Context.java.

    {
        if (m_boolSort == null) {
            m_boolSort = new BoolSort(this);
        }
        return m_boolSort;
    }

◆ getComplexSort()

ComplexSort getComplexSort ( )

inline

Retrieves the Complex sort of the context.

Definition at line 160 of file Context.java.

    {
        if (m_complexSort == null) {
            m_complexSort = new ComplexSort(this);
        }
        return m_complexSort;
    }

◆ getFiniteSetSortBasis()

final Sort getFiniteSetSortBasis ( Sort s )

inline

Get the element sort (basis) of a finite set sort.

Definition at line 2246 of file Context.java.

    {
        checkContextMatch(s);
        return Sort.create(this, Native.getFiniteSetSortBasis(nCtx(), s.getNativeObject()));
    }

Referenced by FiniteSetSort.getBasis().

◆ getIntSort()

IntSort getIntSort ( )

inline

Retrieves the Integer sort of the context.

Definition at line 140 of file Context.java.

    {
        if (m_intSort == null) {
            m_intSort = new IntSort(this);
        }
        return m_intSort;
    }

◆ getNumProbes()

int getNumProbes ( )

inline

The number of supported Probes.

Definition at line 3703 of file Context.java.

    {
        return Native.getNumProbes(nCtx());
    }

◆ getNumSimplifiers()

int getNumSimplifiers ( )

inline

The number of supported simplifiers.

Definition at line 3603 of file Context.java.

    {
        return Native.getNumSimplifiers(nCtx());
    }

◆ getNumTactics()

int getNumTactics ( )

inline

The number of supported tactics.

Definition at line 3306 of file Context.java.

    {
        return Native.getNumTactics(nCtx());
    }

◆ getProbeDescription()

String getProbeDescription ( String name )

inline

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

Definition at line 3725 of file Context.java.

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

◆ getProbeNames()

String[] getProbeNames ( )

inline

The names of all supported Probes.

Definition at line 3711 of file Context.java.

    {
 
        int n = getNumProbes();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.getProbeName(nCtx(), i);
        return res;
    }

◆ getRealSort()

RealSort getRealSort ( )

inline

Retrieves the Real sort of the context.

Definition at line 151 of file Context.java.

    {
        if (m_realSort == null) {
            m_realSort = new RealSort(this);
        }
        return m_realSort;
    }

◆ getSimplifierDescription()

String getSimplifierDescription ( String name )

inline

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

Definition at line 3625 of file Context.java.

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

◆ getSimplifierNames()

String[] getSimplifierNames ( )

inline

The names of all supported simplifiers.

Definition at line 3611 of file Context.java.

    {
 
        int n = getNumSimplifiers();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.getSimplifierName(nCtx(), i);
        return res;
    }

◆ getSimplifyParameterDescriptions()

ParamDescrs getSimplifyParameterDescriptions ( )

inline

Retrieves parameter descriptions for simplifier.

Definition at line 4835 of file Context.java.

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

◆ getStringSort()

SeqSort< CharSort > getStringSort ( )

inline

Retrieves the String sort of the context.

Definition at line 194 of file Context.java.

    {
        if (m_stringSort == null) {
            m_stringSort = mkStringSort();
        }
        return m_stringSort;
    }

◆ getTacticDescription()

String getTacticDescription ( String name )

inline

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

Definition at line 3328 of file Context.java.

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

◆ getTacticNames()

String[] getTacticNames ( )

inline

The names of all supported tactics.

Definition at line 3314 of file Context.java.

    {
 
        int n = getNumTactics();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.getTacticName(nCtx(), i);
        return res;
    }

◆ 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 3762 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

◆ 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 3533 of file Context.java.

    {
        Native.interrupt(nCtx());
    }

◆ intToString()

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

inline

Convert an integer expression to a string.

Definition at line 2401 of file Context.java.

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

◆ isFiniteSetSort()

final boolean isFiniteSetSort ( Sort s )

inline

Check if a sort is a finite set sort.

Definition at line 2237 of file Context.java.

    {
        checkContextMatch(s);
        return Native.isFiniteSetSort(nCtx(), s.getNativeObject());
    }

◆ 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 3775 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

◆ 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 3750 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

◆ mkAdd()

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

inline

Create an expression representing t[0] + t[1] + ....

Definition at line 1033 of file Context.java.

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

◆ 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 2771 of file Context.java.

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

◆ mkAnd()

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

inline

Create an expression representing t[0] and t[1] and ....

Definition at line 1011 of file Context.java.

    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
                AST.arrayToNative(t)));
    }

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 896 of file Context.java.

    {
        checkContextMatch(f);
        checkContextMatch(args);
        return Expr.create(this, f, args);
    }

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 1921 of file Context.java.

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

◆ 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 1912 of file Context.java.

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

◆ 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 2089 of file Context.java.

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

◆ 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 246 of file Context.java.

    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new ArraySort<>(this, domain, range);
    }

◆ mkArraySort() [2/2]

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

inline

Create a new array sort.

Definition at line 257 of file Context.java.

    {
        checkContextMatch(domains);
        checkContextMatch(range);
        return new ArraySort<>(this, domains, range);
    }

◆ mkAsArray()

final< D extends Sort, R extends Sort > ArrayExpr< D, R > mkAsArray ( FuncDecl< R > f )

inline

Create an as-array expression from a function declaration.

Parameters

f	the function declaration to lift into an array. Must have exactly one domain sort.

See also: #mkTermArray(Expr); #mkMap(FuncDecl, Expr[])

Definition at line 2080 of file Context.java.

    {
        checkContextMatch(f);
        return (ArrayExpr<D, R>) Expr.create(this, Native.mkAsArray(nCtx(), f.getNativeObject()));
    }

◆ mkASTMap()

ASTMap mkASTMap ( )

inline

Creates an empty map from ASTs to ASTs.

Definition at line 3541 of file Context.java.

    {
        return new ASTMap(this);
    }

◆ 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 2509 of file Context.java.

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

◆ mkAtLeast()

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

inline

Create an at-least-k constraint.

Definition at line 2842 of file Context.java.

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

◆ mkAtMost()

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

inline

Create an at-most-k constraint.

Definition at line 2833 of file Context.java.

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

◆ mkBitVecSort()

BitVecSort mkBitVecSort ( int size )

inline

Create a new bit-vector sort.

Definition at line 238 of file Context.java.

    {
        return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
    }

◆ mkBool()

BoolExpr mkBool ( boolean value )

inline

Creates a Boolean value.

Definition at line 922 of file Context.java.

    {
        return value ? mkTrue() : mkFalse();
    }

Referenced by UserPropagatorBase.conflict().

◆ mkBoolConst() [1/2]

BoolExpr mkBoolConst ( String name )

inline

Create a Boolean constant.

Definition at line 805 of file Context.java.

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

◆ mkBoolConst() [2/2]

BoolExpr mkBoolConst ( Symbol name )

inline

Create a Boolean constant.

Definition at line 797 of file Context.java.

    {
        return (BoolExpr) mkConst(name, getBoolSort());
    }

◆ mkBoolSort()

BoolSort mkBoolSort ( )

inline

Create a new Boolean sort.

Definition at line 177 of file Context.java.

    {
        return new BoolSort(this);
    }

◆ mkBound()

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

inline

Creates a new bound variable.

Parameters

index	The de-Bruijn index of the variable
ty	The sort of the variable

Definition at line 730 of file Context.java.

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

◆ mkBV() [1/3]

BitVecNum mkBV	(	int	v,
		int	size
	)

inline

Create a bit-vector numeral.

Parameters

v	value of the numeral.
size	the size of the bit-vector

Definition at line 3035 of file Context.java.

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

◆ mkBV() [2/3]

BitVecNum mkBV	(	long	v,
		int	size
	)

inline

Create a bit-vector numeral.

Parameters

v	value of the numeral. *
size	the size of the bit-vector

Definition at line 3045 of file Context.java.

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

◆ mkBV() [3/3]

BitVecNum mkBV	(	String	v,
		int	size
	)

inline

Create a bit-vector numeral.

Parameters

v	A string representing the value in decimal notation.
size	the size of the bit-vector

Definition at line 3025 of file Context.java.

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

◆ 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 1792 of file Context.java.

    {
        checkContextMatch(t);
        return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
            (signed)));
    }

◆ 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 1355 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvadd(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1804 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned)));
    }

◆ 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 1818 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkBVAND()

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

inline

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

Definition at line 1266 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1700 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvashr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkBVConst() [1/2]

BitVecExpr mkBVConst	(	String	name,
		int	size
	)

inline

Creates a bit-vector constant.

Definition at line 887 of file Context.java.

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

◆ mkBVConst() [2/2]

BitVecExpr mkBVConst	(	Symbol	name,
		int	size
	)

inline

Creates a bit-vector constant.

Definition at line 879 of file Context.java.

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

◆ 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 1680 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1381 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvmul(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1886 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned)));
    }

◆ 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 1900 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkBVNAND()

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

inline

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

Definition at line 1305 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnand(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1344 of file Context.java.

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

◆ 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 1874 of file Context.java.

    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
                t.getNativeObject()));
    }

◆ mkBVNOR()

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

inline

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

Definition at line 1318 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkBVNot()

BitVecExpr mkBVNot ( Expr< BitVecSort > t )

inline

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

Definition at line 1231 of file Context.java.

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

◆ mkBVOR()

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

inline

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

Definition at line 1279 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1242 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredand(nCtx(),
                t.getNativeObject()));
    }

◆ 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 1254 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkBvredor(nCtx(),
                t.getNativeObject()));
    }

◆ 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 1738 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1713 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
                t.getNativeObject()));
    }

◆ mkBVRotateRight() [1/2]

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

inline

Rotate Right. Remarks: Rotate bits of t1 to the rightt2 times. The arguments must have the same bit-vector sort.

Definition at line 1753 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1725 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
                t.getNativeObject()));
    }

◆ mkBVSDiv()

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

inline

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

The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.
The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0.

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

Definition at line 1417 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1860 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1542 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1568 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1661 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvshl(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1516 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1490 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1464 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1450 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1368 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsub(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1832 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1846 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
                .getNativeObject(), t2.getNativeObject(), (isSigned)));
    }

◆ 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 1396 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 1529 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1555 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1503 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1477 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1432 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvurem(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkBVXNOR()

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

inline

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

Definition at line 1331 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkBVXOR()

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

inline

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

Definition at line 1292 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvxor(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkCharLe()

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

inline

Create less than or equal to between two characters.

Definition at line 2788 of file Context.java.

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

◆ mkCharSort()

CharSort mkCharSort ( )

inline

Creates character sort object.

Definition at line 186 of file Context.java.

    {
        return new CharSort(this);
    }

◆ mkComplement()

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

inline

Create the complement regular expression.

Definition at line 2702 of file Context.java.

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

◆ mkComplex()

ComplexExpr mkComplex	(	Expr<? extends ArithSort >	real,
		Expr<? extends ArithSort >	imag
	)

inline

Constructs a Complex expression from Int or Real components.

Definition at line 855 of file Context.java.

    {
        checkContextMatch(real);
        checkContextMatch(imag);
        return new ComplexExpr(this, Native.mkComplex(nCtx(), real.getNativeObject(), imag.getNativeObject()));
    }

◆ mkComplexConst() [1/2]

ComplexExpr mkComplexConst ( String name )

inline

Creates a Complex constant.

Definition at line 849 of file Context.java.

    {
        return (ComplexExpr) mkConst(name, getComplexSort());
    }

◆ mkComplexConst() [2/2]

ComplexExpr mkComplexConst ( Symbol name )

inline

Creates a Complex constant.

Definition at line 843 of file Context.java.

    {
        return (ComplexExpr) mkConst(name, getComplexSort());
    }

◆ mkComplexSort()

ComplexSort mkComplexSort ( )

inline

Creates the Complex sort.

Definition at line 169 of file Context.java.

    {
        return new ComplexSort(this);
    }

◆ 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 1586 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkConcat(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkConcat() [2/3]

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

inline

Concatenate sequences.

Definition at line 2434 of file Context.java.

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

◆ mkConcat() [3/3]

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

inline

Create the concatenation of regular languages.

Definition at line 2712 of file Context.java.

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

◆ mkConst() [1/3]

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

inline

Creates a fresh constant from the FuncDecl f.

Parameters

f	A decl of a 0-arity function

Definition at line 789 of file Context.java.

    {
        return mkApp(f, (Expr<?>[]) null);
    }

◆ 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 769 of file Context.java.

    {
        return mkConst(mkSymbol(name), range);
    }

◆ 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 754 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(range);
 
        return (Expr<R>) Expr.create(
                this,
                Native.mkConst(nCtx(), name.getNativeObject(),
                        range.getNativeObject()));
    }

◆ 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 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 2029 of file Context.java.

    {
        checkContextMatch(domain);
        checkContextMatch(v);
        return new ArrayExpr<>(this, Native.mkConstArray(nCtx(),
                domain.getNativeObject(), v.getNativeObject()));
    }

◆ mkConstDecl() [1/2]

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

inline

Creates a new constant function declaration.

Definition at line 706 of file Context.java.

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

◆ mkConstDecl() [2/2]

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

inline

Creates a new constant function declaration.

Definition at line 696 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(range);
        return new FuncDecl<>(this, name, null, range);
    }

◆ 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 381 of file Context.java.

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

◆ mkConstructor() [2/2]

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

inline

Create a datatype constructor.

Parameters

name	constructor name
recognizer	name of recognizer function.
fieldNames	names of the constructor fields.
sorts	field sorts, 0 if the field sort refers to a recursive sort.
sortRefs	reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

Definition at line 371 of file Context.java.

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

◆ 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 2480 of file Context.java.

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

◆ mkDatatypeSort() [1/2]

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

inline

Create a new datatype sort.

Definition at line 400 of file Context.java.

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

◆ mkDatatypeSort() [2/2]

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

inline

Create a new datatype sort.

Definition at line 390 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(constructors);
        return new DatatypeSort<>(this, name, constructors);
    }

◆ mkDatatypeSorts() [1/2]

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

inline

Create mutually recursive data-types.

Definition at line 486 of file Context.java.

    {
        return mkDatatypeSorts(mkSymbols(names), c);
    }

◆ mkDatatypeSorts() [2/2]

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

inline

Create mutually recursive datatypes.

Parameters

names	names of datatype sorts
c	list of constructors, one list per sort.

Definition at line 460 of file Context.java.

    {
        checkContextMatch(names);
        int n = names.length;
        ConstructorList<Object>[] cla = new ConstructorList[n];
        long[] n_constr = new long[n];
        for (int i = 0; i < n; i++)
        {
            Constructor<Object>[] constructor = c[i];
 
            checkContextMatch(constructor);
            cla[i] = new ConstructorList<>(this, constructor);
            n_constr[i] = cla[i].getNativeObject();
        }
        long[] n_res = new long[n];
        Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
                n_constr);
        DatatypeSort<Object>[] res = new DatatypeSort[n];
        for (int i = 0; i < n; i++)
            res[i] = new DatatypeSort<>(this, n_res[i]);
        return res;
    }

◆ 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 2741 of file Context.java.

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

◆ mkDistinct()

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

inline

Creates a distinct term.

Definition at line 942 of file Context.java.

    {
        checkContextMatch(args);
        return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
                AST.arrayToNative(args)));
    }

◆ 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 1075 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr<R>) Expr.create(this, Native.mkDiv(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkDivides()

BoolExpr mkDivides	(	Expr< IntSort >	t1,
		Expr< IntSort >	t2
	)

inline

Creates an integer divisibility predicate (t1 divides t2). Remarks: Both arguments must have integer sort.

Definition at line 1219 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkDivides(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
    }

◆ mkEmptyRe()

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

inline

Create the empty regular expression. Corresponds to re.none

Definition at line 2752 of file Context.java.

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

◆ mkEmptySeq()

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

inline

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

Definition at line 2367 of file Context.java.

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

◆ mkEmptySet()

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

inline

Create an empty set.

Definition at line 2109 of file Context.java.

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

◆ mkEnumSort() [1/2]

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

inline

Create a new enumeration sort.

Definition at line 316 of file Context.java.

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

◆ mkEnumSort() [2/2]

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

inline

Create a new enumeration sort.

Definition at line 305 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(enumNames);
        return new EnumSort<>(this, name, enumNames);
    }

◆ mkEq()

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

inline

Creates the equality x = y

Definition at line 930 of file Context.java.

    {
        checkContextMatch(x);
        checkContextMatch(y);
        return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
                y.getNativeObject()));
    }

◆ 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 3113 of file Context.java.

    {
 
        return Quantifier.of(this, false, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }

◆ 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 3100 of file Context.java.

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

◆ 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 2528 of file Context.java.

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

◆ 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 1602 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
                t.getNativeObject()));
    }

◆ mkFalse()

BoolExpr mkFalse ( )

inline

The false Term.

Definition at line 914 of file Context.java.

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

◆ mkFiniteDomainSort() [1/2]

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

inline

Create a new finite domain sort.

Definition at line 354 of file Context.java.

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

◆ mkFiniteDomainSort() [2/2]

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

inline

Create a new finite domain sort.

Definition at line 344 of file Context.java.

    {
        checkContextMatch(name);
        return new FiniteDomainSort<>(this, name, size);
    }

◆ mkFiniteSetDifference()

final Expr mkFiniteSetDifference	(	Expr	s1,
		Expr	s2
	)

inline

Create the difference of two finite sets.

Definition at line 2293 of file Context.java.

    {
        checkContextMatch(s1);
        checkContextMatch(s2);
        return Expr.create(this, Native.mkFiniteSetDifference(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }

◆ mkFiniteSetEmpty()

final Expr mkFiniteSetEmpty ( Sort setSort )

inline

Create an empty finite set.

Definition at line 2255 of file Context.java.

    {
        checkContextMatch(setSort);
        return Expr.create(this, Native.mkFiniteSetEmpty(nCtx(), setSort.getNativeObject()));
    }

◆ mkFiniteSetFilter()

final Expr mkFiniteSetFilter	(	Expr	f,
		Expr	set
	)

inline

Filter a finite set with a predicate.

Definition at line 2342 of file Context.java.

    {
        checkContextMatch(f);
        checkContextMatch(set);
        return Expr.create(this, Native.mkFiniteSetFilter(nCtx(), f.getNativeObject(), set.getNativeObject()));
    }

◆ mkFiniteSetIntersect()

final Expr mkFiniteSetIntersect	(	Expr	s1,
		Expr	s2
	)

inline

Create the intersection of two finite sets.

Definition at line 2283 of file Context.java.

    {
        checkContextMatch(s1);
        checkContextMatch(s2);
        return Expr.create(this, Native.mkFiniteSetIntersect(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }

◆ mkFiniteSetMap()

final Expr mkFiniteSetMap	(	Expr	f,
		Expr	set
	)

inline

Map a function over all elements in a finite set.

Definition at line 2332 of file Context.java.

    {
        checkContextMatch(f);
        checkContextMatch(set);
        return Expr.create(this, Native.mkFiniteSetMap(nCtx(), f.getNativeObject(), set.getNativeObject()));
    }

◆ mkFiniteSetMember()

final BoolExpr mkFiniteSetMember	(	Expr	elem,
		Expr	set
	)

inline

Check for membership in a finite set.

Definition at line 2303 of file Context.java.

    {
        checkContextMatch(elem);
        checkContextMatch(set);
        return (BoolExpr) Expr.create(this, Native.mkFiniteSetMember(nCtx(), elem.getNativeObject(), set.getNativeObject()));
    }

◆ mkFiniteSetRange()

final Expr mkFiniteSetRange	(	Expr	low,
		Expr	high
	)

inline

Create a finite set containing integers in the range [low, high].

Definition at line 2352 of file Context.java.

    {
        checkContextMatch(low);
        checkContextMatch(high);
        return Expr.create(this, Native.mkFiniteSetRange(nCtx(), low.getNativeObject(), high.getNativeObject()));
    }

◆ mkFiniteSetSingleton()

final Expr mkFiniteSetSingleton ( Expr elem )

inline

Create a singleton finite set.

Definition at line 2264 of file Context.java.

    {
        checkContextMatch(elem);
        return Expr.create(this, Native.mkFiniteSetSingleton(nCtx(), elem.getNativeObject()));
    }

◆ mkFiniteSetSize()

final Expr mkFiniteSetSize ( Expr set )

inline

Get the cardinality of a finite set.

Definition at line 2313 of file Context.java.

    {
        checkContextMatch(set);
        return Expr.create(this, Native.mkFiniteSetSize(nCtx(), set.getNativeObject()));
    }

◆ mkFiniteSetSort()

final FiniteSetSort mkFiniteSetSort ( Sort elemSort )

inline

Finite Sets Create a finite set sort over the given element sort.

Definition at line 2228 of file Context.java.

    {
        checkContextMatch(elemSort);
        return new FiniteSetSort(this, elemSort);
    }

◆ mkFiniteSetSubset()

final BoolExpr mkFiniteSetSubset	(	Expr	s1,
		Expr	s2
	)

inline

Check if one finite set is a subset of another.

Definition at line 2322 of file Context.java.

    {
        checkContextMatch(s1);
        checkContextMatch(s2);
        return (BoolExpr) Expr.create(this, Native.mkFiniteSetSubset(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }

◆ mkFiniteSetUnion()

final Expr mkFiniteSetUnion	(	Expr	s1,
		Expr	s2
	)

inline

Create the union of two finite sets.

Definition at line 2273 of file Context.java.

    {
        checkContextMatch(s1);
        checkContextMatch(s2);
        return Expr.create(this, Native.mkFiniteSetUnion(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
    }

◆ mkFixedpoint()

Fixedpoint mkFixedpoint ( )

inline

Create a Fixedpoint context.

Definition at line 3909 of file Context.java.

    {
        return new Fixedpoint(this);
    }

◆ 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 3087 of file Context.java.

    {
 
        return Quantifier.of(this, true, boundConstants, body, weight,
                patterns, noPatterns, quantifierID, skolemID);
    }

◆ 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

sorts	the sorts of the bound variables.
names	names of the bound variables
body	the body of the quantifier.
weight	quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patterns	array containing the patterns created using `MkPattern`.
noPatterns	array containing the anti-patterns created using `MkPattern`.
quantifierID	optional symbol to track quantifier.
skolemID	optional symbol to track skolem constants.

Returns: Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. Note that the bound variables are de-Bruijn indices created using {#mkBound}. 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 3075 of file Context.java.

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

◆ 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

sgn	the sign.
exp	the exponent.
sig	the significand.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4239 of file Context.java.

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

◆ 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

sgn	the sign.
exp	the exponent.
sig	the significand.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4252 of file Context.java.

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

◆ mkFP() [3/6]

FPNum mkFP	(	double	v,
		FPSort	s
	)

inline

Create a numeral of FloatingPoint sort from a double.

Parameters

v	numeral value.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4214 of file Context.java.

    {
        return mkFPNumeral(v, s);
    }

◆ 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

sgn	bit-vector term (of size 1) representing the sign.
sig	bit-vector term representing the significand.
exp	bit-vector term representing the exponent. Remarks: This is the operator named ‘fp’ in the SMT FP theory definition. Note that sgn is required to be a bit-vector of size 1. Significand and exponent are required to be greater than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments.

Exceptions

Z3Exception

Definition at line 4537 of file Context.java.

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

◆ mkFP() [5/6]

FPNum mkFP	(	float	v,
		FPSort	s
	)

inline

Create a numeral of FloatingPoint sort from a float.

Parameters

v	numeral value.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4203 of file Context.java.

    {
        return mkFPNumeral(v, s);
    }

◆ mkFP() [6/6]

FPNum mkFP	(	int	v,
		FPSort	s
	)

inline

Create a numeral of FloatingPoint sort from an int.

Parameters

v	numeral value.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4226 of file Context.java.

    {
        return mkFPNumeral(v, s);
    }

◆ mkFPAbs()

FPExpr mkFPAbs ( Expr< FPSort > t )

inline

Floating-point absolute value

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4263 of file Context.java.

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

◆ mkFPAdd()

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

inline

Floating-point addition

Parameters

rm	rounding mode term
t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4285 of file Context.java.

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

◆ mkFPDiv()

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

inline

Floating-point division

Parameters

rm	rounding mode term
t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4321 of file Context.java.

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

◆ mkFPEq()

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

inline

Floating-point equality.

Parameters

t1	floating-point term
t2	floating-point term Remarks: Note that this is IEEE 754 equality (as opposed to standard =).

Exceptions

Z3Exception

Definition at line 4449 of file Context.java.

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

◆ mkFPFMA()

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

inline

Floating-point fused multiply-add

Parameters

rm	rounding mode term
t1	floating-point term
t2	floating-point term
t3	floating-point term Remarks: The result is round((t1 * t2) + t3)

Exceptions

Z3Exception

Definition at line 4336 of file Context.java.

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

◆ mkFPGEq()

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

inline

Floating-point greater than or equal.

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4425 of file Context.java.

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

◆ mkFPGt()

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

inline

Floating-point greater than.

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4436 of file Context.java.

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

◆ mkFPInf()

FPNum mkFPInf	(	FPSort	s,
		boolean	negative
	)

inline

Create a floating-point infinity of sort s.

Parameters

s	FloatingPoint sort.
negative	indicates whether the result should be negative.

Exceptions

Z3Exception

Definition at line 4122 of file Context.java.

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

◆ mkFPIsInfinite()

BoolExpr mkFPIsInfinite ( Expr< FPSort > t )

inline

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

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4489 of file Context.java.

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

◆ mkFPIsNaN()

BoolExpr mkFPIsNaN ( Expr< FPSort > t )

inline

Predicate indicating whether t is a NaN.

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4499 of file Context.java.

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

◆ mkFPIsNegative()

BoolExpr mkFPIsNegative ( Expr< FPSort > t )

inline

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

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4509 of file Context.java.

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

◆ mkFPIsNormal()

BoolExpr mkFPIsNormal ( Expr< FPSort > t )

inline

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

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4459 of file Context.java.

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

◆ mkFPIsPositive()

BoolExpr mkFPIsPositive ( Expr< FPSort > t )

inline

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

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4519 of file Context.java.

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

◆ mkFPIsSubnormal()

BoolExpr mkFPIsSubnormal ( Expr< FPSort > t )

inline

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

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4469 of file Context.java.

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

◆ 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

t	floating-point term

Exceptions

Z3Exception

Definition at line 4479 of file Context.java.

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

◆ mkFPLEq()

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

inline

Floating-point less than or equal.

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4403 of file Context.java.

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

◆ mkFPLt()

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

inline

Floating-point less than.

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4414 of file Context.java.

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

◆ mkFPMax()

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

inline

Maximum of floating-point numbers.

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4392 of file Context.java.

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

◆ mkFPMin()

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

inline

Minimum of floating-point numbers.

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4381 of file Context.java.

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

◆ mkFPMul()

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

inline

Floating-point multiplication

Parameters

rm	rounding mode term
t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4309 of file Context.java.

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

◆ mkFPNaN()

FPNum mkFPNaN ( FPSort s )

inline

Create a NaN of sort s.

Parameters

s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4111 of file Context.java.

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

◆ mkFPNeg()

FPExpr mkFPNeg ( Expr< FPSort > t )

inline

Floating-point negation

Parameters

t	floating-point term

Exceptions

Z3Exception

Definition at line 4273 of file Context.java.

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

◆ 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

sgn	the sign.
exp	the exponent.
sig	the significand.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4179 of file Context.java.

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

◆ 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

sgn	the sign.
exp	the exponent.
sig	the significand.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4192 of file Context.java.

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

◆ mkFPNumeral() [3/5]

FPNum mkFPNumeral	(	double	v,
		FPSort	s
	)

inline

Create a numeral of FloatingPoint sort from a double.

Parameters

v	numeral value.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4155 of file Context.java.

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

◆ mkFPNumeral() [4/5]

FPNum mkFPNumeral	(	float	v,
		FPSort	s
	)

inline

Create a numeral of FloatingPoint sort from a float.

Parameters

v	numeral value.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4144 of file Context.java.

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

◆ mkFPNumeral() [5/5]

FPNum mkFPNumeral	(	int	v,
		FPSort	s
	)

inline

Create a numeral of FloatingPoint sort from an int.

Parameters

v	numeral value.
s	FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4166 of file Context.java.

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

◆ mkFPRem()

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

inline

Floating-point remainder

Parameters

t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4358 of file Context.java.

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

◆ mkFPRNA()

FPRMNum mkFPRNA ( )

inline

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

Exceptions

Z3Exception

Definition at line 3963 of file Context.java.

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

◆ mkFPRNE()

FPRMNum mkFPRNE ( )

inline

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

Exceptions

Z3Exception

Definition at line 3945 of file Context.java.

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

◆ mkFPRoundingModeSort()

FPRMSort mkFPRoundingModeSort ( )

inline

Create the floating-point RoundingMode sort.

Exceptions

Z3Exception

Definition at line 3927 of file Context.java.

    {
        return new FPRMSort(this);
    }

◆ mkFPRoundNearestTiesToAway()

FPRMNum mkFPRoundNearestTiesToAway ( )

inline

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

Exceptions

Z3Exception

Definition at line 3954 of file Context.java.

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

◆ mkFPRoundNearestTiesToEven()

FPRMExpr mkFPRoundNearestTiesToEven ( )

inline

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

Exceptions

Z3Exception

Definition at line 3936 of file Context.java.

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

◆ 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

rm	term of RoundingMode sort
t	floating-point term

Exceptions

Z3Exception

Definition at line 4370 of file Context.java.

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

◆ mkFPRoundTowardNegative()

FPRMNum mkFPRoundTowardNegative ( )

inline

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

Exceptions

Z3Exception

Definition at line 3990 of file Context.java.

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

◆ mkFPRoundTowardPositive()

FPRMNum mkFPRoundTowardPositive ( )

inline

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

Exceptions

Z3Exception

Definition at line 3972 of file Context.java.

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

◆ mkFPRoundTowardZero()

FPRMNum mkFPRoundTowardZero ( )

inline

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

Exceptions

Z3Exception

Definition at line 4008 of file Context.java.

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

◆ mkFPRTN()

FPRMNum mkFPRTN ( )

inline

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

Exceptions

Z3Exception

Definition at line 3999 of file Context.java.

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

◆ mkFPRTP()

FPRMNum mkFPRTP ( )

inline

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

Exceptions

Z3Exception

Definition at line 3981 of file Context.java.

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

◆ mkFPRTZ()

FPRMNum mkFPRTZ ( )

inline

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

Exceptions

Z3Exception

Definition at line 4017 of file Context.java.

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

◆ mkFPSort()

FPSort mkFPSort	(	int	ebits,
		int	sbits
	)

inline

Create a FloatingPoint sort.

Parameters

ebits	exponent bits in the FloatingPoint sort.
sbits	significand bits in the FloatingPoint sort.

Exceptions

Z3Exception

Definition at line 4028 of file Context.java.

    {
        return new FPSort(this, ebits, sbits);
    }

◆ mkFPSort128()

FPSort mkFPSort128 ( )

inline

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

Exceptions

Z3Exception

Definition at line 4100 of file Context.java.

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

◆ mkFPSort16()

FPSort mkFPSort16 ( )

inline

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

Exceptions

Z3Exception

Definition at line 4046 of file Context.java.

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

◆ mkFPSort32()

FPSort mkFPSort32 ( )

inline

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

Exceptions

Z3Exception

Definition at line 4064 of file Context.java.

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

◆ mkFPSort64()

FPSort mkFPSort64 ( )

inline

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

Exceptions

Z3Exception

Definition at line 4082 of file Context.java.

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

◆ mkFPSortDouble()

FPSort mkFPSortDouble ( )

inline

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

Exceptions

Z3Exception

Definition at line 4073 of file Context.java.

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

◆ mkFPSortHalf()

FPSort mkFPSortHalf ( )

inline

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

Exceptions

Z3Exception

Definition at line 4037 of file Context.java.

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

◆ mkFPSortQuadruple()

FPSort mkFPSortQuadruple ( )

inline

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

Exceptions

Z3Exception

Definition at line 4091 of file Context.java.

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

◆ mkFPSortSingle()

FPSort mkFPSortSingle ( )

inline

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

Exceptions

Z3Exception

Definition at line 4055 of file Context.java.

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

◆ mkFPSqrt()

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

inline

Floating-point square root

Parameters

rm	rounding mode term
t	floating-point term

Exceptions

Z3Exception

Definition at line 4347 of file Context.java.

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

◆ mkFPSub()

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

inline

Floating-point subtraction

Parameters

rm	rounding mode term
t1	floating-point term
t2	floating-point term

Exceptions

Z3Exception

Definition at line 4297 of file Context.java.

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

◆ 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

rm	RoundingMode term.
t	FloatingPoint term
sz	Size of the resulting bit-vector.
signed	Indicates whether the result is a signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the floating-point term t into a bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm.

Exceptions

Z3Exception

Definition at line 4638 of file Context.java.

    {
        if (signed)
            return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
        else
            return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
    }

◆ 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

bv	bit-vector value (of size m).
s	FloatingPoint sort (ebits+sbits == m) Remarks: Produces a term that represents the conversion of a bit-vector term bv to a floating-point term of sort s. The bit-vector size of bv (m) must be equal to ebits+sbits of s. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.

Exceptions

Z3Exception

Definition at line 4553 of file Context.java.

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

◆ 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

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

Exceptions

Z3Exception

Definition at line 4603 of file Context.java.

    {
        if (signed)
            return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
        else
            return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
    }

◆ 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

rm	RoundingMode term.
exp	Exponent term of Int sort.
sig	Significand term of Real sort.
s	FloatingPoint sort. Remarks: Produces a term that represents the conversion of sig * 2^exp into a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.

Exceptions

Z3Exception

Definition at line 4688 of file Context.java.

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

◆ 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

rm	RoundingMode term.
t	FloatingPoint term.
s	FloatingPoint sort. Remarks: Produces a term that represents the conversion of a floating-point term t to a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.

Exceptions

Z3Exception

Definition at line 4569 of file Context.java.

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

◆ 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

rm	RoundingMode term.
t	term of Real sort.
s	FloatingPoint sort. Remarks: Produces a term that represents the conversion of term t of real sort into a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.

Exceptions

Z3Exception

Definition at line 4585 of file Context.java.

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

◆ 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

s	FloatingPoint sort
rm	floating-point rounding mode term
t	floating-point term Remarks: Produces a term that represents the conversion of a floating-point term t to a different FloatingPoint sort s. If necessary, rounding according to rm is applied.

Exceptions

Z3Exception

Definition at line 4621 of file Context.java.

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

◆ mkFPToIEEEBV()

BitVecExpr mkFPToIEEEBV ( Expr< FPSort > t )

inline

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

Parameters

t	FloatingPoint term. Remarks: The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.

Exceptions

Z3Exception

Definition at line 4670 of file Context.java.

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

◆ mkFPToReal()

RealExpr mkFPToReal ( Expr< FPSort > t )

inline

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

Parameters

t	FloatingPoint term Remarks: Produces a term that represents the conversion of the floating-point term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.

Exceptions

Z3Exception

Definition at line 4655 of file Context.java.

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

◆ mkFPZero()

FPNum mkFPZero	(	FPSort	s,
		boolean	negative
	)

inline

Create a floating-point zero of sort s.

Parameters

s	FloatingPoint sort.
negative	indicates whether the result should be negative.

Exceptions

Z3Exception

Definition at line 4133 of file Context.java.

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

◆ 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 778 of file Context.java.

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

◆ 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 718 of file Context.java.

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

◆ 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 685 of file Context.java.

    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, prefix, domain, range);
    }

◆ mkFullRe()

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

inline

Create the full regular expression. Corresponds to re.all

Definition at line 2761 of file Context.java.

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

◆ mkFullSet()

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

inline

Create the full set.

Definition at line 2119 of file Context.java.

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

◆ 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 643 of file Context.java.

    {
        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl<>(this, mkSymbol(name), q, range);
    }

◆ 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 632 of file Context.java.

    {
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, mkSymbol(name), domain, range);
    }

◆ 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 619 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        Sort[] q = new Sort[] { domain };
        return new FuncDecl<>(this, name, q, range);
    }

◆ 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 593 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, name, domain, range);
    }

◆ mkGe()

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

inline

Create an expression representing t1 >= t2

Definition at line 1159 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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

models	Indicates whether model generation should be enabled.
unsatCores	Indicates whether unsat core generation should be enabled.
proofs	Indicates whether proof generation should be enabled.

Definition at line 3290 of file Context.java.

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

◆ mkGt()

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

inline

Create an expression representing t1 > t2

Definition at line 1148 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ mkIff()

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

inline

Create an expression representing t1 iff t2.

Definition at line 977 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ mkImagPart()

RealExpr mkImagPart ( Expr< ComplexSort > value )

inline

Returns the Real-valued imaginary component of a Complex expression.

Definition at line 870 of file Context.java.

    {
        checkContextMatch(value);
        return new RealExpr(this, Native.mkImagPart(nCtx(), value.getNativeObject()));
    }

◆ mkImplies()

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

inline

Create an expression representing t1 -> t2.

Definition at line 988 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkImplies(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 2537 of file Context.java.

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

◆ mkInRe()

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

inline

Check for regular expression membership.

Definition at line 2641 of file Context.java.

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

◆ mkInt() [1/3]

IntNum mkInt ( int v )

inline

Create an integer numeral.

Parameters

v	value of the numeral.

Returns: A Term with value v and sort Integer

Definition at line 3000 of file Context.java.

    {
 
        return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
                .getNativeObject()));
    }

◆ mkInt() [2/3]

IntNum mkInt ( long v )

inline

Create an integer numeral.

Parameters

v	value of the numeral.

Returns: A Term with value v and sort Integer

Definition at line 3013 of file Context.java.

    {
 
        return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
                .getNativeObject()));
    }

◆ mkInt() [3/3]

IntNum mkInt ( String v )

inline

Create an integer numeral.

Parameters

v	A string representing the Term value in decimal notation.

Definition at line 2987 of file Context.java.

    {
 
        return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
                .getNativeObject()));
    }

◆ 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 1771 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
                t.getNativeObject()));
    }

◆ 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) <= t1 < MkInt2Real(k)+1. The argument must be of integer sort.

Definition at line 1177 of file Context.java.

    {
        checkContextMatch(t);
        return new RealExpr(this,
                Native.mkInt2real(nCtx(), t.getNativeObject()));
    }

◆ mkIntConst() [1/2]

IntExpr mkIntConst ( String name )

inline

Creates an integer constant.

Definition at line 821 of file Context.java.

    {
        return (IntExpr) mkConst(name, getIntSort());
    }

◆ mkIntConst() [2/2]

IntExpr mkIntConst ( Symbol name )

inline

Creates an integer constant.

Definition at line 813 of file Context.java.

    {
        return (IntExpr) mkConst(name, getIntSort());
    }

◆ mkIntersect()

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

inline

Create the intersection of regular languages.

Definition at line 2732 of file Context.java.

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

◆ mkIntSort()

IntSort mkIntSort ( )

inline

Create a new integer sort.

Definition at line 222 of file Context.java.

    {
        return new IntSort(this);
    }

◆ mkIsDigit()

BoolExpr mkIsDigit ( Expr< CharSort > ch )

inline

Create a check if the character is a digit.

Definition at line 2824 of file Context.java.

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

◆ mkIsInteger()

BoolExpr mkIsInteger ( Expr< RealSort > t )

inline

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

Definition at line 1199 of file Context.java.

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

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

Parameters

t1	An expression with Boolean sort
t2	An expression
t3	An expression with the same sort as `t2`

Definition at line 965 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(t3);
        return (Expr<R>) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
                t2.getNativeObject(), t3.getNativeObject()));
    }

◆ 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 3185 of file Context.java.

     {
         return Lambda.of(this, boundConstants, body);
     }

◆ 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

sorts	the sorts of the bound variables.
names	names of the bound variables.
body	the body of the quantifier.

Definition at line 3174 of file Context.java.

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

◆ mkLastIndexOf()

final< R extends Sort > IntExpr mkLastIndexOf	(	Expr< SeqSort< R > >	s,
		Expr< SeqSort< R > >	substr
	)

inline

Extract the last index of sub-string.

Definition at line 2546 of file Context.java.

    {
        checkContextMatch(s, substr);
        return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject()));
    }

◆ mkLe()

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

inline

Create an expression representing t1 <= t2

Definition at line 1137 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ mkLength()

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

inline

Retrieve the length of a given sequence.

Definition at line 2444 of file Context.java.

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

◆ mkLinearOrder()

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

inline

Creates or a linear order.

Parameters

index	The index of the order.
sort	The sort of the order.

Definition at line 4698 of file Context.java.

                                                                                      {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkLinearOrder(
                        nCtx(),
                        sort.getNativeObject(),
                        index
                )
        );
    }

◆ mkListSort() [1/2]

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

inline

Create a new list sort.

Definition at line 335 of file Context.java.

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

◆ mkListSort() [2/2]

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

inline

Create a new list sort.

Definition at line 325 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(elemSort);
        return new ListSort<>(this, name, elemSort);
    }

◆ 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 2675 of file Context.java.

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

◆ 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 2667 of file Context.java.

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

◆ mkLt()

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

inline

Create an expression representing t1 < t2

Definition at line 1126 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 2051 of file Context.java.

    {
        checkContextMatch(f);
        checkContextMatch(args);
        return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
                f.getNativeObject(), AST.arrayLength(args),
                AST.arrayToNative(args)));
    }

◆ mkMod()

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

inline

Create an expression representing t1 mod t2. Remarks: The arguments must have int type.

Definition at line 1088 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ mkMul()

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

inline

Create an expression representing t[0] * t[1] * ....

Definition at line 1044 of file Context.java.

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

◆ mkNot()

final BoolExpr mkNot ( Expr< BoolSort > a )

inline

Create an expression representing not(a).

Definition at line 952 of file Context.java.

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

◆ mkNth()

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

inline

Retrieve element at index.

Definition at line 2518 of file Context.java.

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

◆ 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

v	Value of the numeral
ty	Sort of the numeral

Returns: A Term with value v and type ty

Definition at line 2903 of file Context.java.

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

◆ 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

v	Value of the numeral
ty	Sort of the numeral

Returns: A Term with value v and type ty

Definition at line 2919 of file Context.java.

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

◆ mkNumeral() [3/3]

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

inline

Create a Term of a given sort.

Parameters

v	A string representing the term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form `[num]* / [num]*`.
ty	The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.

Returns: A Term with value v and sort ty

Definition at line 2886 of file Context.java.

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

◆ mkOptimize()

Optimize mkOptimize ( )

inline

Create a Optimize context.

Definition at line 3917 of file Context.java.

    {
        return new Optimize(this);
    }

◆ mkOption()

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

inline

Create the optional regular expression.

Definition at line 2693 of file Context.java.

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

◆ mkOr()

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

inline

Create an expression representing t[0] or t[1] or ....

Definition at line 1022 of file Context.java.

    {
        checkContextMatch(t);
        return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
                AST.arrayToNative(t)));
    }

◆ mkParams()

Params mkParams ( )

inline

Creates a new ParameterSet.

Definition at line 3298 of file Context.java.

    {
        return new Params(this);
    }

◆ mkPartialOrder()

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

inline

Creates a partial order.

Parameters

index	The index of the order.
sort	The sort of the order.

Definition at line 4714 of file Context.java.

                                                                                       {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkPartialOrder(
                    nCtx(),
                    sort.getNativeObject(),
                    index
                )
        );
    }

◆ mkPattern()

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

inline

Create a quantifier pattern.

Definition at line 740 of file Context.java.

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

◆ mkPBEq()

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

inline

Create a pseudo-Boolean equal constraint.

Definition at line 2869 of file Context.java.

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

◆ mkPBGe()

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

inline

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

Definition at line 2860 of file Context.java.

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

◆ mkPBLe()

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

inline

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

Definition at line 2851 of file Context.java.

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

◆ mkPiecewiseLinearOrder()

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

inline

Creates a piecewise linear order.

Parameters

index	The index of the order.
sort	The sort of the order.

Definition at line 4745 of file Context.java.

                                                                                               {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkPiecewiseLinearOrder(
                    nCtx(),
                    sort.getNativeObject(),
                    index
                )
        );
    }

◆ mkPlus()

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

inline

Take the Kleene plus of a regular expression.

Definition at line 2684 of file Context.java.

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

◆ mkPower() [1/2]

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

inline

Create power regular expression.

Definition at line 2659 of file Context.java.

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

◆ 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 1112 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return (ArithExpr<R>) Expr.create(
                this,
                Native.mkPower(nCtx(), t1.getNativeObject(),
                        t2.getNativeObject()));
    }

◆ mkPrefixOf()

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

inline

Check for sequence prefix.

Definition at line 2462 of file Context.java.

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

◆ mkProbe()

Probe mkProbe ( String name )

inline

Creates a new Probe.

Definition at line 3733 of file Context.java.

    {
        return new Probe(this, name);
    }

◆ mkPropagateFunction()

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

inline

Definition at line 601 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        long f = Native.solverPropagateDeclare(
            this.nCtx(), 
            name.getNativeObject(), 
            AST.arrayLength(domain), 
            AST.arrayToNative(domain),
            range.getNativeObject());
        return new FuncDecl<>(this, f);
    }

◆ 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 3144 of file Context.java.

    {
 
        if (universal)
            return mkForall(boundConstants, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
        else
            return mkExists(boundConstants, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
    }

◆ 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 3126 of file Context.java.

    {
 
        if (universal)
            return mkForall(sorts, names, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
        else
            return mkExists(sorts, names, body, weight, patterns, noPatterns,
                    quantifierID, skolemID);
    }

◆ mkRange()

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

inline

Create a range expression.

Definition at line 2779 of file Context.java.

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

◆ mkReal() [1/4]

RatNum mkReal	(	int	num,
		int	den
	)

inline

Create a real from a fraction.

Parameters

num	numerator of rational.
den	denominator of rational.

Returns: A Term with value num/den and sort Real

See also: #mkNumeral(String v, R ty)

Definition at line 2935 of file Context.java.

    {
        if (den == 0) {
            throw new Z3Exception("Denominator is zero");
        }
 
        return new RatNum(this, Native.mkReal(nCtx(), num, den));
    }

◆ mkReal() [2/4]

RatNum mkReal ( int v )

inline

Create a real numeral.

Parameters

v	value of the numeral.

Returns: A Term with value v and sort Real

Definition at line 2963 of file Context.java.

    {
 
        return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
                .getNativeObject()));
    }

◆ mkReal() [3/4]

RatNum mkReal ( long v )

inline

Create a real numeral.

Parameters

v	value of the numeral.

Returns: A Term with value v and sort Real

Definition at line 2976 of file Context.java.

    {
 
        return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
                .getNativeObject()));
    }

◆ mkReal() [4/4]

RatNum mkReal ( String v )

inline

Create a real numeral.

Parameters

v	A string representing the Term value in decimal notation.

Returns: A Term with value v and sort Real

Definition at line 2950 of file Context.java.

    {
 
        return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
                .getNativeObject()));
    }

◆ 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 1190 of file Context.java.

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

◆ mkRealConst() [1/2]

RealExpr mkRealConst ( String name )

inline

Creates a real constant.

Definition at line 837 of file Context.java.

    {
        return (RealExpr) mkConst(name, getRealSort());
    }

◆ mkRealConst() [2/2]

RealExpr mkRealConst ( Symbol name )

inline

Creates a real constant.

Definition at line 829 of file Context.java.

    {
        return (RealExpr) mkConst(name, getRealSort());
    }

◆ mkRealPart()

RealExpr mkRealPart ( Expr< ComplexSort > value )

inline

Returns the Real-valued real component of a Complex expression.

Definition at line 863 of file Context.java.

    {
        checkContextMatch(value);
        return new RealExpr(this, Native.mkRealPart(nCtx(), value.getNativeObject()));
    }

◆ mkRealSort()

RealSort mkRealSort ( )

inline

Create a real sort.

Definition at line 230 of file Context.java.

    {
        return new RealSort(this);
    }

◆ mkRecFuncDecl()

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

inline

Creates a new recursive function declaration.

Definition at line 655 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(domain);
        checkContextMatch(range);
        return new FuncDecl<>(this, name, domain, range, true);
    }

◆ mkRem()

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

inline

Create an expression representing t1 rem t2. Remarks: The arguments must have int type.

Definition at line 1101 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1643 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
                t.getNativeObject()));
    }

◆ 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 2595 of file Context.java.

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

◆ mkReplaceAll()

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

inline

Replace all occurrences of src by dst in s.

Definition at line 2604 of file Context.java.

    {
        checkContextMatch(s, src, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceAll(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
    }

◆ mkReplaceRe()

final< R extends Sort > SeqExpr< R > mkReplaceRe	(	Expr< SeqSort< R > >	s,
		ReExpr< SeqSort< R > >	re,
		Expr< SeqSort< R > >	dst
	)

inline

Replace the first occurrence of regular expression re with dst in s.

Definition at line 2613 of file Context.java.

    {
        checkContextMatch(s, re, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceRe(nCtx(), s.getNativeObject(), re.getNativeObject(), dst.getNativeObject()));
    }

◆ mkReplaceReAll()

final< R extends Sort > SeqExpr< R > mkReplaceReAll	(	Expr< SeqSort< R > >	s,
		ReExpr< SeqSort< R > >	re,
		Expr< SeqSort< R > >	dst
	)

inline

Replace all occurrences of regular expression re with dst in s.

Definition at line 2622 of file Context.java.

    {
        checkContextMatch(s, re, dst);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceReAll(nCtx(), s.getNativeObject(), re.getNativeObject(), dst.getNativeObject()));
    }

◆ mkReSort()

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

inline

Create a new regular expression sort

Definition at line 283 of file Context.java.

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

◆ 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 1939 of file Context.java.

    {
        checkContextMatch(a);
        checkContextMatch(i);
        return (Expr<R>) Expr.create(
                this,
                Native.mkSelect(nCtx(), a.getNativeObject(),
                        i.getNativeObject()));
    }

◆ 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 1961 of file Context.java.

    {
        checkContextMatch(a);
        checkContextMatch(args);
        return (Expr<R>) Expr.create(
                this,
                Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
    }

◆ mkSeqFoldl()

final< R extends Sort, A extends Sort > Expr< A > mkSeqFoldl	(	Expr<?>	f,
		Expr< A >	a,
		Expr< SeqSort< R > >	s
	)

inline

Left fold of function f over sequence s with accumulator a. Applies f to accumulate values from left to right over the sequence.

Definition at line 2576 of file Context.java.

    {
        checkContextMatch(f, a, s);
        return (Expr<A>) Expr.create(this, Native.mkSeqFoldl(nCtx(), f.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
    }

◆ mkSeqFoldli()

final< R extends Sort, A extends Sort > Expr< A > mkSeqFoldli	(	Expr<?>	f,
		Expr< IntSort >	i,
		Expr< A >	a,
		Expr< SeqSort< R > >	s
	)

inline

Left fold of function f over sequence s with accumulator a starting at index i. Applies f to accumulate values from left to right over the sequence, tracking the index starting from i.

Definition at line 2586 of file Context.java.

    {
        checkContextMatch(f, i, a, s);
        return (Expr<A>) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
    }

◆ mkSeqMap()

final< R extends Sort > SeqExpr< R > mkSeqMap	(	Expr<?>	f,
		Expr< SeqSort< R > >	s
	)

inline

Map function f over sequence s. Returns a new sequence where f is applied to each element of s.

Definition at line 2556 of file Context.java.

    {
        checkContextMatch(f, s);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqMap(nCtx(), f.getNativeObject(), s.getNativeObject()));
    }

◆ mkSeqMapi()

final< R extends Sort > SeqExpr< R > mkSeqMapi	(	Expr<?>	f,
		Expr< IntSort >	i,
		Expr< SeqSort< R > >	s
	)

inline

Map function f over sequence s starting at index i. Returns a new sequence where f is applied to each element of s along with its index starting from i.

Definition at line 2566 of file Context.java.

    {
        checkContextMatch(f, i, s);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqMapi(nCtx(), f.getNativeObject(), i.getNativeObject(), s.getNativeObject()));
    }

◆ mkSeqPower()

final< R extends Sort > SeqExpr< R > mkSeqPower	(	Expr< SeqSort< R > >	s,
		Expr< IntSort >	n
	)

inline

Retrieve the sequence s concatenated n times with itself.

Definition at line 2453 of file Context.java.

    {
        checkContextMatch(s, n);
        return (SeqExpr<R>) Expr.create(this, Native.mkSeqPower(nCtx(), s.getNativeObject(), n.getNativeObject()));
    }

◆ mkSeqSort()

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

inline

Create a new sequence sort

Definition at line 275 of file Context.java.

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

◆ 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 2129 of file Context.java.

    {
        checkContextMatch(set);
        checkContextMatch(element);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkSetAdd(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }

◆ mkSetComplement()

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

inline

Take the complement of a set.

Definition at line 2189 of file Context.java.

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

◆ 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 2141 of file Context.java.

    {
        checkContextMatch(set);
        checkContextMatch(element);
        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                Native.mkSetDel(nCtx(), set.getNativeObject(),
                        element.getNativeObject()));
    }

◆ 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 2177 of file Context.java.

    {
        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }

◆ 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 2166 of file Context.java.

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

◆ mkSetMembership()

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

inline

Check for set membership.

Definition at line 2199 of file Context.java.

    {
        checkContextMatch(elem);
        checkContextMatch(set);
        return (BoolExpr) Expr.create(this,
                Native.mkSetMember(nCtx(), elem.getNativeObject(),
                        set.getNativeObject()));
    }

◆ mkSetSort()

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

inline

Create a set type.

Definition at line 2100 of file Context.java.

    {
        checkContextMatch(ty);
        return new SetSort<>(this, ty);
    }

◆ 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 2211 of file Context.java.

    {
        checkContextMatch(arg1);
        checkContextMatch(arg2);
        return (BoolExpr) Expr.create(this,
                Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
                        arg2.getNativeObject()));
    }

◆ 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 2154 of file Context.java.

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

◆ 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 1617 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
                t.getNativeObject()));
    }

◆ mkSimpleSolver()

Solver mkSimpleSolver ( )

inline

Creates a new (incremental) solver.

Definition at line 3880 of file Context.java.

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

◆ mkSimplifier()

Simplifier mkSimplifier ( String name )

inline

Creates a new Simplifier.

Definition at line 3633 of file Context.java.

    {
        return new Simplifier(this, name);
    }

◆ 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 3846 of file Context.java.

    {
        return mkSolver((Symbol) null);
    }

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 3901 of file Context.java.

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

◆ mkSolver() [3/5]

Solver mkSolver ( String logic )

inline

Creates a new (incremental) solver.

See also: #mkSolver(Symbol)

Definition at line 3872 of file Context.java.

    {
        return mkSolver(mkSymbol(logic));
    }

◆ 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 3858 of file Context.java.

    {
 
        if (logic == null)
            return new Solver(this, Native.mkSolver(nCtx()));
        else
            return new Solver(this, Native.mkSolverForLogic(nCtx(),
                    logic.getNativeObject()));
    }

◆ 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 3891 of file Context.java.

    {
 
        return new Solver(this, Native.mkSolverFromTactic(nCtx(),
                t.getNativeObject()));
    }

◆ mkStar()

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

inline

Take the Kleene star of a regular expression.

Definition at line 2650 of file Context.java.

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

◆ 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 1986 of file Context.java.

    {
        checkContextMatch(a);
        checkContextMatch(i);
        checkContextMatch(v);
        return new ArrayExpr<>(this, Native.mkStore(nCtx(), a.getNativeObject(),
                i.getNativeObject(), v.getNativeObject()));
    }

◆ 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 2011 of file Context.java.

    {
        checkContextMatch(a);
        checkContextMatch(args);
        checkContextMatch(v);
        return new ArrayExpr<>(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
                             args.length, AST.arrayToNative(args), v.getNativeObject()));
    }

◆ mkString()

SeqExpr< CharSort > mkString ( String s )

inline

Create a string constant.

Definition at line 2385 of file Context.java.

    {
        StringBuilder buf = new StringBuilder();
        for (int i = 0; i < s.length(); i += Character.charCount(s.codePointAt(i))) {
            int code = s.codePointAt(i);
            if (code <= 32 || 127 < code) 
                buf.append(String.format("\\u{%x}", code));
            else
                buf.append(s.charAt(i));
        }
        return (SeqExpr<CharSort>) Expr.create(this, Native.mkString(nCtx(), buf.toString()));
    }

◆ 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 2499 of file Context.java.

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

◆ 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 2490 of file Context.java.

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

◆ mkStringSort()

SeqSort< CharSort > mkStringSort ( )

inline

Create a new string sort

Definition at line 267 of file Context.java.

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

◆ mkSub()

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

inline

Create an expression representing t[0] - t[1] - ....

Definition at line 1055 of file Context.java.

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

◆ mkSuffixOf()

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

inline

Check for sequence suffix.

Definition at line 2471 of file Context.java.

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

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

    {
        return new IntSymbol(this, i);
    }

◆ mkSymbol() [2/2]

StringSymbol mkSymbol ( String name )

inline

Create a symbol using a string.

Definition at line 102 of file Context.java.

    {
        return new StringSymbol(this, name);
    }

◆ mkTactic()

Tactic mkTactic ( String name )

inline

Creates a new Tactic.

Definition at line 3336 of file Context.java.

    {
        return new Tactic(this, name);
    }

Referenced by Goal.simplify(), and 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 2066 of file Context.java.

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

◆ 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 2631 of file Context.java.

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

◆ mkTransitiveClosure()

final< R extends Sort > FuncDecl< BoolSort > mkTransitiveClosure ( FuncDecl< BoolSort > f )

inline

Create the transitive closure of a binary relation. The resulting relation is recursive.

Parameters

f	function declaration of a binary relation

Definition at line 4730 of file Context.java.

                                                                                               {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkTransitiveClosure(
                    nCtx(),
                    f.getNativeObject()
                )
        );
    }

◆ mkTreeOrder()

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

inline

Creates a tree order.

Parameters

index	The index of the order.
sort	The sort of the order.

Definition at line 4761 of file Context.java.

                                                                                    {
        return (FuncDecl<BoolSort>) FuncDecl.create(
                this,
                Native.mkTreeOrder(
                    nCtx(),
                    sort.getNativeObject(),
                    index
                )
        );
    }

◆ mkTrue()

BoolExpr mkTrue ( )

inline

The true Term.

Definition at line 906 of file Context.java.

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

Referenced by Goal.AsBoolExpr().

◆ mkTupleSort()

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

inline

Create a new tuple sort.

Definition at line 292 of file Context.java.

    {
        checkContextMatch(name);
        checkContextMatch(fieldNames);
        checkContextMatch(fieldSorts);
        return new TupleSort(this, name, fieldNames.length, fieldNames,
                fieldSorts);
    }

◆ mkTypeVariable() [1/2]

TypeVarSort mkTypeVariable ( String name )

inline

Create a type variable for use in polymorphic functions and datatypes. Type variables can be used as sort parameters in polymorphic datatypes.

Parameters

name	name of the type variable

Returns: a new type variable sort

Definition at line 510 of file Context.java.

    {
        return mkTypeVariable(mkSymbol(name));
    }

◆ mkTypeVariable() [2/2]

TypeVarSort mkTypeVariable ( Symbol name )

inline

Create a type variable for use in polymorphic functions and datatypes. Type variables can be used as sort parameters in polymorphic datatypes.

Parameters

name	name of the type variable

Returns: a new type variable sort

Definition at line 498 of file Context.java.

    {
        checkContextMatch(name);
        return new TypeVarSort(this, name);
    }

◆ mkUnaryMinus()

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

inline

Create an expression representing -t.

Definition at line 1065 of file Context.java.

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

◆ mkUninterpretedSort() [1/2]

UninterpretedSort mkUninterpretedSort ( String str )

inline

Create a new uninterpreted sort.

Definition at line 214 of file Context.java.

    {
        return mkUninterpretedSort(mkSymbol(str));
    }

◆ mkUninterpretedSort() [2/2]

UninterpretedSort mkUninterpretedSort ( Symbol s )

inline

Create a new uninterpreted sort.

Definition at line 205 of file Context.java.

    {
        checkContextMatch(s);
        return new UninterpretedSort(this, s);
    }

◆ mkUnion()

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

inline

Create the union of regular languages.

Definition at line 2722 of file Context.java.

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

◆ mkUnit()

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

inline

Create the singleton sequence.

Definition at line 2376 of file Context.java.

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

◆ 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 580 of file Context.java.

    {
        return (Expr<R>) Expr.create(this,
                            Native.datatypeUpdateField
                            (nCtx(), field.getNativeObject(),
                             t.getNativeObject(), v.getNativeObject()));
    }

◆ mkXor()

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

inline

Create an expression representing t1 xor t2.

Definition at line 999 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
                t2.getNativeObject()));
    }

◆ 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 1631 of file Context.java.

    {
        checkContextMatch(t);
        return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
                t.getNativeObject()));
    }

◆ nCtx()

long nCtx ( )

inline

Definition at line 4854 of file Context.java.

    {
        if (m_ctx == 0)
            throw new Z3Exception("Context closed");
        return m_ctx;
    }

Referenced by Fixedpoint.add(), Goal.add(), UserPropagatorBase.add(), ASTVector.ASTVector(), UserPropagatorBase.consequence(), AST.equals(), FuncDecl< R extends Sort >.equals(), Sort.equals(), FPRMSort.FPRMSort(), FPSort.FPSort(), RCFNum.mkE(), RCFNum.mkInfinitesimal(), RCFNum.mkPi(), RCFNum.mkRoots(), UserPropagatorBase.nextSplit(), Quantifier.of(), Quantifier.of(), Lambda< R extends Sort >.of(), Lambda< R extends Sort >.of(), OnClause.OnClause(), RCFNum.RCFNum(), RCFNum.RCFNum(), 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 3833 of file Context.java.

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

◆ 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 3822 of file Context.java.

    {
        checkContextMatch(p1);
        checkContextMatch(p2);
        return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
                p2.getNativeObject()));
    }

◆ 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 3387 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticOrElse(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 3520 of file Context.java.

    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new Tactic(this, Native.tacticParAndThen(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

◆ 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 3509 of file Context.java.

    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticParOr(nCtx(),
                Tactic.arrayLength(t), Tactic.arrayToNative(t)));
    }

◆ 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 3263 of file Context.java.

    {
        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd)
            throw new Z3Exception("Argument size mismatch");
        ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
                fileName, AST.arrayLength(sorts),
                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
                AST.arrayToNative(decls)));
        return v.ToBoolExprArray();
    }

◆ 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 3242 of file Context.java.

    {
        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd) {
            throw new Z3Exception("Argument size mismatch");
        }
        ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
                str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
                AST.arrayToNative(sorts), AST.arrayLength(decls),
                Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
        return v.ToBoolExprArray();
    }

◆ polynomialSubresultants()

final< R extends Sort > ASTVector polynomialSubresultants	(	Expr< R >	p,
		Expr< R >	q,
		Expr< R >	x
	)

inline

Return the nonzero subresultants of p and q with respect to the "variable" x. Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable.

Parameters

p	arithmetic term
q	arithmetic term
x	variable

Definition at line 4779 of file Context.java.

                                                                                                     {
        return new ASTVector(
                this,
                Native.polynomialSubresultants(
                    nCtx(),
                    p.getNativeObject(),
                    q.getNativeObject(),
                    x.getNativeObject()
                )
        );
    }

◆ qeLite()

Expr<?> qeLite	(	ASTVector	vars,
		Expr<?>	body
	)

inline

Performs best-effort quantifier elimination for the variables in vars.

Definition at line 3550 of file Context.java.

    {
        checkContextMatch(vars);
        checkContextMatch(body);
        return Expr.create(this, Native.qeLite(nCtx(), vars.getNativeObject(),
                body.getNativeObject()));
    }

◆ qeModelProject()

Expr<?> qeModelProject	(	Model	model,
		Expr<?>[]	bounds,
		Expr<?>	body
	)

inline

Projects the bound applications from body using model.

Definition at line 3561 of file Context.java.

    {
        checkContextMatch(model);
        checkContextMatch(bounds);
        checkContextMatch(body);
        return Expr.create(this, Native.qeModelProject(nCtx(), model.getNativeObject(),
                bounds.length, AST.arrayToNative(bounds), body.getNativeObject()));
    }

◆ qeModelProjectSkolem()

Expr<?> qeModelProjectSkolem	(	Model	model,
		Expr<?>[]	bounds,
		Expr<?>	body,
		ASTMap	map
	)

inline

Projects bound applications and records Skolem terms in map.

Definition at line 3573 of file Context.java.

    {
        checkContextMatch(model);
        checkContextMatch(bounds);
        checkContextMatch(body);
        checkContextMatch(map);
        return Expr.create(this, Native.qeModelProjectSkolem(nCtx(),
                model.getNativeObject(), bounds.length, AST.arrayToNative(bounds),
                body.getNativeObject(), map.getNativeObject()));
    }

◆ qeModelProjectWithWitness()

Expr<?> qeModelProjectWithWitness	(	Model	model,
		Expr<?>[]	bounds,
		Expr<?>	body,
		ASTMap	map
	)

inline

Projects bound applications and records witnesses in map.

Definition at line 3588 of file Context.java.

    {
        checkContextMatch(model);
        checkContextMatch(bounds);
        checkContextMatch(body);
        checkContextMatch(map);
        return Expr.create(this, Native.qeModelProjectWithWitness(nCtx(),
                model.getNativeObject(), bounds.length, AST.arrayToNative(bounds),
                body.getNativeObject(), map.getNativeObject()));
    }

◆ 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 is reached.

Definition at line 3440 of file Context.java.

    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticRepeat(nCtx(),
                t.getNativeObject(), max));
    }

◆ sbvToString()

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

inline

Convert an signed bitvector expression to a string.

Definition at line 2417 of file Context.java.

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

◆ 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 3205 of file Context.java.

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

◆ SimplifyHelp()

String SimplifyHelp ( )

inline

Return a string describing all available parameters to Expr.Simplify.

Definition at line 4827 of file Context.java.

    {
        return Native.simplifyGetHelp(nCtx());
    }

◆ skip()

Tactic skip ( )

inline

Create a tactic that just returns the given goal.

Definition at line 3450 of file Context.java.

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

◆ stringToInt()

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

inline

Convert an integer expression to a string.

Definition at line 2425 of file Context.java.

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

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

Definition at line 3672 of file Context.java.

    {
        return andThen(t1, t2, ts);
    }

◆ 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 3377 of file Context.java.

    {
        return andThen(t1, t2, ts);
    }

◆ 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 3401 of file Context.java.

    {
        checkContextMatch(t);
        return new Tactic(this, Native.tacticTryFor(nCtx(),
                t.getNativeObject(), ms));
    }

◆ ubvToString()

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

inline

Convert an unsigned bitvector expression to a string.

Definition at line 2409 of file Context.java.

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

◆ 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

a	The AST to unwrap.

Definition at line 4818 of file Context.java.

    {
        return a.getNativeObject();
    }

◆ 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? 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 4848 of file Context.java.

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

◆ 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 3681 of file Context.java.

    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
                t.getNativeObject(), p.getNativeObject()));
    }

◆ 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 3487 of file Context.java.

    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Tactic(this, Native.tacticUsingParams(nCtx(),
                t.getNativeObject(), p.getNativeObject()));
    }

◆ 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 3414 of file Context.java.

    {
        checkContextMatch(t);
        checkContextMatch(p);
        return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
                t.getNativeObject()));
    }

◆ 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 3695 of file Context.java.

    {
        return usingParams(t, p);
    }

◆ 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 3501 of file Context.java.

    {
        return usingParams(t, p);
    }

◆ 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

nativeObject The native pointer to wrap.

Definition at line 4801 of file Context.java.

    {
        return AST.create(this, nativeObject);
    }

Public Member Functions

Protected Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Context() [1/3]

◆ Context() [2/3]

◆ Context() [3/3]

Member Function Documentation

◆ AddRecDef()

◆ and()

◆ andThen() [1/2]

◆ andThen() [2/2]

◆ benchmarkToSMTString()

◆ charFromBv()

◆ charToBv()

◆ charToInt()

◆ close()

◆ cond()

◆ constProbe()

◆ eq()

◆ fail()

◆ failIf()

◆ failIfNotDecided()

◆ ge()

◆ getBoolSort()

◆ getComplexSort()

◆ getFiniteSetSortBasis()

◆ getIntSort()

◆ getNumProbes()

◆ getNumSimplifiers()

◆ getNumTactics()

◆ getProbeDescription()

◆ getProbeNames()

◆ getRealSort()

◆ getSimplifierDescription()

◆ getSimplifierNames()

◆ getSimplifyParameterDescriptions()

◆ getStringSort()

◆ getTacticDescription()

◆ getTacticNames()

◆ gt()

◆ interrupt()

◆ intToString()

◆ isFiniteSetSort()

◆ le()

◆ lt()

◆ mkAdd()

◆ mkAllcharRe()

◆ mkAnd()

◆ mkApp()

◆ mkArrayConst() [1/2]

◆ mkArrayConst() [2/2]

◆ mkArrayExt()

◆ mkArraySort() [1/2]

◆ mkArraySort() [2/2]

◆ mkAsArray()

◆ mkASTMap()

◆ mkAt()

◆ mkAtLeast()

◆ mkAtMost()

◆ mkBitVecSort()

◆ mkBool()

◆ mkBoolConst() [1/2]

◆ mkBoolConst() [2/2]

◆ mkBoolSort()

◆ mkBound()

◆ mkBV() [1/3]

◆ mkBV() [2/3]

◆ mkBV() [3/3]

◆ mkBV2Int()

◆ mkBVAdd()

◆ mkBVAddNoOverflow()

◆ mkBVAddNoUnderflow()

◆ mkBVAND()

◆ mkBVASHR()

◆ mkBVConst() [1/2]

◆ mkBVConst() [2/2]

◆ mkBVLSHR()

◆ mkBVMul()

◆ mkBVMulNoOverflow()