Context Class Reference

The main interaction with Z3 happens via the Context. More...

Inheritance diagram for Context:

Public Member Functions
	Context ()
	Constructor.
	Context (Dictionary< string, string > settings)
	Constructor.
IntSymbol	MkSymbol (int i)
	Creates a new symbol using an integer.
StringSymbol	MkSymbol (string name)
	Create a symbol using a string.
BoolSort	MkBoolSort ()
	Create a new Boolean sort.
UninterpretedSort	MkUninterpretedSort (Symbol s)
	Create a new uninterpreted sort.
UninterpretedSort	MkUninterpretedSort (string str)
	Create a new uninterpreted sort.
IntSort	MkIntSort ()
	Create a new integer sort.
RealSort	MkRealSort ()
	Create a real sort.
ComplexSort	MkComplexSort ()
	Creates the Complex sort.
BitVecSort	MkBitVecSort (uint size)
	Create a new bit-vector sort.
SeqSort	MkSeqSort (Sort s)
	Create a new sequence sort.
ReSort	MkReSort (SeqSort s)
	Create a new regular expression sort.
ArraySort	MkArraySort (Sort domain, Sort range)
	Create a new array sort.
ArraySort	MkArraySort (Sort[] domain, Sort range)
	Create a new n-ary array sort.
TupleSort	MkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
	Create a new tuple sort.
EnumSort	MkEnumSort (Symbol name, params Symbol[] enumNames)
	Create a new enumeration sort.
EnumSort	MkEnumSort (string name, params string[] enumNames)
	Create a new enumeration sort.
ListSort	MkListSort (Symbol name, Sort elemSort)
	Create a new list sort.
ListSort	MkListSort (string name, Sort elemSort)
	Create a new list sort.
FiniteDomainSort	MkFiniteDomainSort (Symbol name, ulong size)
	Create a new finite domain sort. Returns The result is a sort
FiniteDomainSort	MkFiniteDomainSort (string name, ulong size)
	Create a new finite domain sort. Returns The result is a sort Elements of the sort are created using See also MkNumeral(ulong, Sort) , and the elements range from 0 to size-1.
Constructor	MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
	Create a datatype constructor.
Constructor	MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
	Create a datatype constructor.
DatatypeSort	MkDatatypeSort (Symbol name, Constructor[] constructors)
	Create a new datatype sort.
DatatypeSort	MkDatatypeSort (string name, Constructor[] constructors)
	Create a new datatype sort.
DatatypeSort	MkDatatypeSortRef (Symbol name, Sort[] parameters=null)
	Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or parametric datatypes.
DatatypeSort	MkDatatypeSortRef (string name, Sort[] parameters=null)
	Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or parametric datatypes.
DatatypeSort[]	MkDatatypeSorts (Symbol[] names, Constructor[][] c)
	Create mutually recursive datatypes.
DatatypeSort[]	MkDatatypeSorts (string[] names, Constructor[][] c)
	Create mutually recursive data-types.
Sort	MkTypeVariable (Symbol name)
	Create a type variable sort for use as a parameter in polymorphic datatypes.
Sort	MkTypeVariable (string name)
	Create a type variable sort for use as a parameter in polymorphic datatypes.
DatatypeSort	MkPolymorphicDatatypeSort (Symbol name, Sort[] typeParams, Constructor[] constructors)
	Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts created with MkTypeVariable(string).
DatatypeSort	MkPolymorphicDatatypeSort (string name, Sort[] typeParams, Constructor[] constructors)
	Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts created with MkTypeVariable(string).
Expr	MkUpdateField (FuncDecl field, Expr t, Expr v)
	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.
FuncDecl	MkFuncDecl (Symbol name, Sort[] domain, Sort range)
	Creates a new function declaration.
FuncDecl	MkFuncDecl (Symbol name, Sort domain, Sort range)
	Creates a new function declaration.
FuncDecl	MkFuncDecl (string name, Sort[] domain, Sort range)
	Creates a new function declaration.
FuncDecl	MkRecFuncDecl (string name, Sort[] domain, Sort range)
	Creates a new recursive function declaration.
void	AddRecDef (FuncDecl f, Expr[] args, Expr body)
	Bind a definition to a recursive function declaration. The function must have previously been created using MkRecFuncDecl. The body may contain recursive uses of the function or other mutually recursive functions.
FuncDecl	MkFuncDecl (string name, Sort domain, Sort range)
	Creates a new function declaration.
FuncDecl	MkFreshFuncDecl (string prefix, Sort[] domain, Sort range)
	Creates a fresh function declaration with a name prefixed with prefix .
FuncDecl	MkConstDecl (Symbol name, Sort range)
	Creates a new constant function declaration.
FuncDecl	MkConstDecl (string name, Sort range)
	Creates a new constant function declaration.
FuncDecl	MkFreshConstDecl (string prefix, Sort range)
	Creates a fresh constant function declaration with a name prefixed with prefix .
FuncDecl	MkUserPropagatorFuncDecl (string name, Sort[] domain, Sort range)
	Declare a function to be processed by the user propagator plugin.
Expr	MkBound (uint index, Sort ty)
	Creates a new bound variable.
Pattern	MkPattern (params Expr[] terms)
	Create a quantifier pattern.
Expr	MkConst (Symbol name, Sort range)
	Creates a new Constant of sort range and named name .
Expr	MkConst (string name, Sort range)
	Creates a new Constant of sort range and named name .
Expr	MkFreshConst (string prefix, Sort range)
	Creates a fresh Constant of sort range and a name prefixed with prefix .
Expr	MkConst (FuncDecl f)
	Creates a fresh constant from the FuncDecl f .
BoolExpr	MkBoolConst (Symbol name)
	Create a Boolean constant.
BoolExpr	MkBoolConst (string name)
	Create a Boolean constant.
IntExpr	MkIntConst (Symbol name)
	Creates an integer constant.
IntExpr	MkIntConst (string name)
	Creates an integer constant.
RealExpr	MkRealConst (Symbol name)
	Creates a real constant.
RealExpr	MkRealConst (string name)
	Creates a real constant.
ComplexExpr	MkComplexConst (Symbol name)
	Creates a Complex constant.
ComplexExpr	MkComplexConst (string name)
	Creates a Complex constant.
ComplexExpr	MkComplex (ArithExpr real, ArithExpr imag)
	Constructs a Complex expression from Int or Real components.
RealExpr	MkRealPart (ArithExpr value)
	Returns the Real-valued real component of a Complex expression.
RealExpr	MkImagPart (ArithExpr value)
	Returns the Real-valued imaginary component of a Complex expression.
BitVecExpr	MkBVConst (Symbol name, uint size)
	Creates a bit-vector constant.
BitVecExpr	MkBVConst (string name, uint size)
	Creates a bit-vector constant.
Expr	MkApp (FuncDecl f, params Expr[] args)
	Create a new function application.
Expr	MkApp (FuncDecl f, IEnumerable< Expr > args)
	Create a new function application.
BoolExpr	MkTrue ()
	The true Term.
BoolExpr	MkFalse ()
	The false Term.
BoolExpr	MkBool (bool value)
	Creates a Boolean value.
BoolExpr	MkEq (Expr x, Expr y)
	Creates the equality x = y .
BoolExpr	MkDistinct (params Expr[] args)
	Creates a distinct term.
BoolExpr	MkDistinct (IEnumerable< Expr > args)
	Creates a distinct term.
BoolExpr	MkNot (BoolExpr a)
	Mk an expression representing not(a).
Expr	MkITE (BoolExpr t1, Expr t2, Expr t3)
	Create an expression representing an if-then-else: ite(t1, t2, t3).
BoolExpr	MkIff (BoolExpr t1, BoolExpr t2)
	Create an expression representing t1 iff t2.
BoolExpr	MkImplies (BoolExpr t1, BoolExpr t2)
	Create an expression representing t1 -> t2.
BoolExpr	MkXor (BoolExpr t1, BoolExpr t2)
	Create an expression representing t1 xor t2.
BoolExpr	MkXor (IEnumerable< BoolExpr > args)
	Create an expression representing t1 xor t2 xor t3 ... .
BoolExpr	MkAnd (params BoolExpr[] ts)
	Create an expression representing t[0] and t[1] and ....
BoolExpr	MkAnd (IEnumerable< BoolExpr > t)
	Create an expression representing t[0] and t[1] and ....
BoolExpr	MkOr (params BoolExpr[] ts)
	Create an expression representing t[0] or t[1] or ....
BoolExpr	MkOr (IEnumerable< BoolExpr > ts)
	Create an expression representing t[0] or t[1] or ....
ArithExpr	MkAdd (params ArithExpr[] ts)
	Create an expression representing t[0] + t[1] + ....
ArithExpr	MkAdd (IEnumerable< ArithExpr > ts)
	Create an expression representing t[0] + t[1] + ....
ArithExpr	MkMul (params ArithExpr[] ts)
	Create an expression representing t[0] * t[1] * ....
ArithExpr	MkMul (IEnumerable< ArithExpr > ts)
	Create an expression representing t[0] * t[1] * ....
ArithExpr	MkSub (params ArithExpr[] ts)
	Create an expression representing t[0] - t[1] - ....
ArithExpr	MkUnaryMinus (ArithExpr t)
	Create an expression representing -t.
ArithExpr	MkDiv (ArithExpr t1, ArithExpr t2)
	Create an expression representing t1 / t2.
IntExpr	MkMod (IntExpr t1, IntExpr t2)
	Create an expression representing t1 mod t2.
IntExpr	MkRem (IntExpr t1, IntExpr t2)
	Create an expression representing t1 rem t2.
ArithExpr	MkPower (ArithExpr t1, ArithExpr t2)
	Create an expression representing t1 ^ t2.
BoolExpr	MkLt (ArithExpr t1, ArithExpr t2)
	Create an expression representing t1 < t2
BoolExpr	MkLe (ArithExpr t1, ArithExpr t2)
	Create an expression representing t1 <= t2
BoolExpr	MkGt (ArithExpr t1, ArithExpr t2)
	Create an expression representing t1 > t2
BoolExpr	MkGe (ArithExpr t1, ArithExpr t2)
	Create an expression representing t1 >= t2
RealExpr	MkInt2Real (IntExpr t)
	Coerce an integer to a real.
IntExpr	MkReal2Int (RealExpr t)
	Coerce a real to an integer.
BoolExpr	MkIsInteger (RealExpr t)
	Creates an expression that checks whether a real number is an integer.
BitVecExpr	MkBVNot (BitVecExpr t)
	Bitwise negation.
BitVecExpr	MkBVRedAND (BitVecExpr t)
	Take conjunction of bits in a vector, return vector of length 1.
BitVecExpr	MkBVRedOR (BitVecExpr t)
	Take disjunction of bits in a vector, return vector of length 1.
BitVecExpr	MkBVAND (BitVecExpr t1, BitVecExpr t2)
	Bitwise conjunction.
BitVecExpr	MkBVOR (BitVecExpr t1, BitVecExpr t2)
	Bitwise disjunction.
BitVecExpr	MkBVXOR (BitVecExpr t1, BitVecExpr t2)
	Bitwise XOR.
BitVecExpr	MkBVNAND (BitVecExpr t1, BitVecExpr t2)
	Bitwise NAND.
BitVecExpr	MkBVNOR (BitVecExpr t1, BitVecExpr t2)
	Bitwise NOR.
BitVecExpr	MkBVXNOR (BitVecExpr t1, BitVecExpr t2)
	Bitwise XNOR.
BitVecExpr	MkBVNeg (BitVecExpr t)
	Standard two's complement unary minus.
BitVecExpr	MkBVAdd (BitVecExpr t1, BitVecExpr t2)
	Two's complement addition.
BitVecExpr	MkBVSub (BitVecExpr t1, BitVecExpr t2)
	Two's complement subtraction.
BitVecExpr	MkBVMul (BitVecExpr t1, BitVecExpr t2)
	Two's complement multiplication.
BitVecExpr	MkBVUDiv (BitVecExpr t1, BitVecExpr t2)
	Unsigned division.
BitVecExpr	MkBVSDiv (BitVecExpr t1, BitVecExpr t2)
	Signed division.
BitVecExpr	MkBVURem (BitVecExpr t1, BitVecExpr t2)
	Unsigned remainder.
BitVecExpr	MkBVSRem (BitVecExpr t1, BitVecExpr t2)
	Signed remainder.
BitVecExpr	MkBVSMod (BitVecExpr t1, BitVecExpr t2)
	Two's complement signed remainder (sign follows divisor).
BoolExpr	MkBVULT (BitVecExpr t1, BitVecExpr t2)
	Unsigned less-than.
BoolExpr	MkBVSLT (BitVecExpr t1, BitVecExpr t2)
	Two's complement signed less-than.
BoolExpr	MkBVULE (BitVecExpr t1, BitVecExpr t2)
	Unsigned less-than or equal to.
BoolExpr	MkBVSLE (BitVecExpr t1, BitVecExpr t2)
	Two's complement signed less-than or equal to.
BoolExpr	MkBVUGE (BitVecExpr t1, BitVecExpr t2)
	Unsigned greater than or equal to.
BoolExpr	MkBVSGE (BitVecExpr t1, BitVecExpr t2)
	Two's complement signed greater than or equal to.
BoolExpr	MkBVUGT (BitVecExpr t1, BitVecExpr t2)
	Unsigned greater-than.
BoolExpr	MkBVSGT (BitVecExpr t1, BitVecExpr t2)
	Two's complement signed greater-than.
BitVecExpr	MkConcat (BitVecExpr t1, BitVecExpr t2)
	Bit-vector concatenation.
BitVecExpr	MkExtract (uint high, uint low, BitVecExpr t)
	Bit-vector extraction.
BitVecExpr	MkSignExt (uint i, BitVecExpr t)
	Bit-vector sign extension.
BitVecExpr	MkZeroExt (uint i, BitVecExpr t)
	Bit-vector zero extension.
BitVecExpr	MkRepeat (uint i, BitVecExpr t)
	Bit-vector repetition.
BitVecExpr	MkBVSHL (BitVecExpr t1, BitVecExpr t2)
	Shift left.
BitVecExpr	MkBVLSHR (BitVecExpr t1, BitVecExpr t2)
	Logical shift right.
BitVecExpr	MkBVASHR (BitVecExpr t1, BitVecExpr t2)
	Arithmetic shift right.
BitVecExpr	MkBVRotateLeft (uint i, BitVecExpr t)
	Rotate Left.
BitVecExpr	MkBVRotateRight (uint i, BitVecExpr t)
	Rotate Right.
BitVecExpr	MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
	Rotate Left.
BitVecExpr	MkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
	Rotate Right.
BitVecExpr	MkInt2BV (uint n, IntExpr t)
	Create an n bit bit-vector from the integer argument t .
IntExpr	MkBV2Int (BitVecExpr t, bool signed)
	Create an integer from the bit-vector argument t .
BoolExpr	MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
	Create a predicate that checks that the bit-wise addition does not overflow.
BoolExpr	MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
	Create a predicate that checks that the bit-wise addition does not underflow.
BoolExpr	MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
	Create a predicate that checks that the bit-wise subtraction does not overflow.
BoolExpr	MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
	Create a predicate that checks that the bit-wise subtraction does not underflow.
BoolExpr	MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
	Create a predicate that checks that the bit-wise signed division does not overflow.
BoolExpr	MkBVNegNoOverflow (BitVecExpr t)
	Create a predicate that checks that the bit-wise negation does not overflow.
BoolExpr	MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
	Create a predicate that checks that the bit-wise multiplication does not overflow.
BoolExpr	MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
	Create a predicate that checks that the bit-wise multiplication does not underflow.
ArrayExpr	MkArrayConst (Symbol name, Sort domain, Sort range)
	Create an array constant.
ArrayExpr	MkArrayConst (string name, Sort domain, Sort range)
	Create an array constant.
Expr	MkSelect (ArrayExpr a, Expr i)
	Array read.
Expr	MkSelect (ArrayExpr a, params Expr[] args)
	Array read.
ArrayExpr	MkStore (ArrayExpr a, Expr i, Expr v)
	Array update.
ArrayExpr	MkStore (ArrayExpr a, Expr[] args, Expr v)
	Array update.
ArrayExpr	MkConstArray (Sort domain, Expr v)
	Create a constant array.
ArrayExpr	MkMap (FuncDecl f, params ArrayExpr[] args)
	Maps f on the argument arrays.
Expr	MkTermArray (ArrayExpr array)
	Access the array default value.
Expr	MkArrayExt (ArrayExpr arg1, ArrayExpr arg2)
	Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
SetSort	MkSetSort (Sort ty)
	Create a set type.
ArrayExpr	MkEmptySet (Sort domain)
	Create an empty set.
ArrayExpr	MkFullSet (Sort domain)
	Create the full set.
ArrayExpr	MkSetAdd (ArrayExpr set, Expr element)
	Add an element to the set.
ArrayExpr	MkSetDel (ArrayExpr set, Expr element)
	Remove an element from a set.
ArrayExpr	MkSetUnion (params ArrayExpr[] args)
	Take the union of a list of sets.
ArrayExpr	MkSetIntersection (params ArrayExpr[] args)
	Take the intersection of a list of sets.
ArrayExpr	MkSetDifference (ArrayExpr arg1, ArrayExpr arg2)
	Take the difference between two sets.
ArrayExpr	MkSetComplement (ArrayExpr arg)
	Take the complement of a set.
BoolExpr	MkSetMembership (Expr elem, ArrayExpr set)
	Check for set membership.
BoolExpr	MkSetSubset (ArrayExpr arg1, ArrayExpr arg2)
	Check for subsetness of sets.
FiniteSetSort	MkFiniteSetSort (Sort elemSort)
	Create a finite set sort over the given element sort.
bool	IsFiniteSetSort (Sort s)
	Check if a sort is a finite set sort.
Sort	GetFiniteSetSortBasis (Sort s)
	Get the element sort (basis) of a finite set sort.
Expr	MkFiniteSetEmpty (Sort setSort)
	Create an empty finite set.
Expr	MkFiniteSetSingleton (Expr elem)
	Create a singleton finite set.
Expr	MkFiniteSetUnion (Expr s1, Expr s2)
	Create the union of two finite sets.
Expr	MkFiniteSetIntersect (Expr s1, Expr s2)
	Create the intersection of two finite sets.
Expr	MkFiniteSetDifference (Expr s1, Expr s2)
	Create the difference of two finite sets.
BoolExpr	MkFiniteSetMember (Expr elem, Expr set)
	Check for membership in a finite set.
Expr	MkFiniteSetSize (Expr set)
	Get the cardinality of a finite set.
BoolExpr	MkFiniteSetSubset (Expr s1, Expr s2)
	Check if one finite set is a subset of another.
Expr	MkFiniteSetMap (Expr f, Expr set)
	Map a function over all elements in a finite set.
Expr	MkFiniteSetFilter (Expr f, Expr set)
	Filter a finite set with a predicate.
Expr	MkFiniteSetRange (Expr low, Expr high)
	Create a finite set containing integers in the range [low, high].
SeqExpr	MkEmptySeq (Sort s)
	Create the empty sequence.
SeqExpr	MkUnit (Expr elem)
	Create the singleton sequence.
SeqExpr	MkString (string s)
	Create a string constant.
SeqExpr	IntToString (Expr e)
	Convert an integer expression to a string.
SeqExpr	UbvToString (Expr e)
	Convert a bit-vector expression, represented as an unsigned number, to a string.
SeqExpr	SbvToString (Expr e)
	Convert a bit-vector expression, represented as an signed number, to a string.
IntExpr	StringToInt (Expr e)
	Convert an integer expression to a string.
SeqExpr	MkConcat (params SeqExpr[] t)
	Concatenate sequences.
IntExpr	MkLength (SeqExpr s)
	Retrieve the length of a given sequence.
SeqExpr	MkSeqPower (SeqExpr s, Expr n)
	Retrieve the sequence s concatenated n times with itself.
BoolExpr	MkPrefixOf (SeqExpr s1, SeqExpr s2)
	Check for sequence prefix.
BoolExpr	MkSuffixOf (SeqExpr s1, SeqExpr s2)
	Check for sequence suffix.
BoolExpr	MkContains (SeqExpr s1, SeqExpr s2)
	Check for sequence containment of s2 in s1.
BoolExpr	MkStringLt (SeqExpr s1, SeqExpr s2)
	Check if the string s1 is lexicographically strictly less than s2.
BoolExpr	MkStringLe (SeqExpr s1, SeqExpr s2)
	Check if the string s1 is lexicographically less or equal to s2.
SeqExpr	MkAt (SeqExpr s, Expr index)
	Retrieve sequence of length one at index.
Expr	MkNth (SeqExpr s, Expr index)
	Retrieve element at index.
SeqExpr	MkExtract (SeqExpr s, IntExpr offset, IntExpr length)
	Extract subsequence.
IntExpr	MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset)
	Extract index of sub-string starting at offset.
SeqExpr	MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst)
	Replace the first occurrence of src by dst in s.
Expr	MkSeqMap (Expr f, SeqExpr s)
	Map function f over the sequence s.
Expr	MkSeqMapi (Expr f, Expr i, SeqExpr s)
	Map function f over the sequence s at index i.
Expr	MkSeqFoldLeft (Expr f, Expr a, SeqExpr s)
	Fold left the function f over the sequence s with initial value a.
Expr	MkSeqFoldLeftI (Expr f, Expr i, Expr a, SeqExpr s)
	Fold left with index the function f over the sequence s with initial value a starting at index i.
ReExpr	MkToRe (SeqExpr s)
	Convert a regular expression that accepts sequence s.
BoolExpr	MkInRe (SeqExpr s, ReExpr re)
	Check for regular expression membership.
ReExpr	MkStar (ReExpr re)
	Take the Kleene star of a regular expression.
ReExpr	MkLoop (ReExpr re, uint lo, uint hi=0)
	Take the bounded Kleene star of a regular expression.
ReExpr	MkPlus (ReExpr re)
	Take the Kleene plus of a regular expression.
ReExpr	MkOption (ReExpr re)
	Create the optional regular expression.
ReExpr	MkComplement (ReExpr re)
	Create the complement regular expression.
ReExpr	MkConcat (params ReExpr[] t)
	Create the concatenation of regular languages.
ReExpr	MkUnion (params ReExpr[] t)
	Create the union of regular languages.
ReExpr	MkIntersect (params ReExpr[] t)
	Create the intersection of regular languages.
ReExpr	MkDiff (ReExpr a, ReExpr b)
	Create a difference regular expression.
ReExpr	MkEmptyRe (Sort s)
	Create the empty regular expression. The sort s should be a regular expression.
ReExpr	MkFullRe (Sort s)
	Create the full regular expression. The sort s should be a regular expression.
ReExpr	MkRange (SeqExpr lo, SeqExpr hi)
	Create a range expression.
BoolExpr	MkCharLe (Expr ch1, Expr ch2)
	Create less than or equal to between two characters.
IntExpr	CharToInt (Expr ch)
	Create an integer (code point) from character.
BitVecExpr	CharToBV (Expr ch)
	Create a bit-vector (code point) from character.
Expr	CharFromBV (BitVecExpr bv)
	Create a character from a bit-vector (code point).
BoolExpr	MkIsDigit (Expr ch)
	Create a check if the character is a digit.
BoolExpr	MkAtMost (IEnumerable< BoolExpr > args, uint k)
	Create an at-most-k constraint.
BoolExpr	MkAtLeast (IEnumerable< BoolExpr > args, uint k)
	Create an at-least-k constraint.
BoolExpr	MkPBLe (int[] coeffs, BoolExpr[] args, int k)
	Create a pseudo-Boolean less-or-equal constraint.
BoolExpr	MkPBGe (int[] coeffs, BoolExpr[] args, int k)
	Create a pseudo-Boolean greater-or-equal constraint.
BoolExpr	MkPBEq (int[] coeffs, BoolExpr[] args, int k)
	Create a pseudo-Boolean equal constraint.
Expr	MkNumeral (string v, Sort ty)
	Create a Term of a given sort.
Expr	MkNumeral (int v, Sort ty)
	Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Expr	MkNumeral (uint v, Sort ty)
	Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Expr	MkNumeral (long v, Sort ty)
	Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Expr	MkNumeral (ulong v, Sort ty)
	Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
RatNum	MkReal (int num, int den)
	Create a real from a fraction.
RatNum	MkReal (string v)
	Create a real numeral.
RatNum	MkReal (int v)
	Create a real numeral.
RatNum	MkReal (uint v)
	Create a real numeral.
RatNum	MkReal (long v)
	Create a real numeral.
RatNum	MkReal (ulong v)
	Create a real numeral.
IntNum	MkInt (string v)
	Create an integer numeral.
IntNum	MkInt (int v)
	Create an integer numeral.
IntNum	MkInt (uint v)
	Create an integer numeral.
IntNum	MkInt (long v)
	Create an integer numeral.
IntNum	MkInt (ulong v)
	Create an integer numeral.
BitVecNum	MkBV (string v, uint size)
	Create a bit-vector numeral.
BitVecNum	MkBV (int v, uint size)
	Create a bit-vector numeral.
BitVecNum	MkBV (uint v, uint size)
	Create a bit-vector numeral.
BitVecNum	MkBV (long v, uint size)
	Create a bit-vector numeral.
BitVecNum	MkBV (ulong v, uint size)
	Create a bit-vector numeral.
BitVecNum	MkBV (bool[] bits)
	Create a bit-vector numeral.
Quantifier	MkForall (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
	Create a universal Quantifier.
Quantifier	MkForall (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
	Create a universal Quantifier.
Quantifier	MkExists (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
	Create an existential Quantifier.
Quantifier	MkExists (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
	Create an existential Quantifier.
Quantifier	MkQuantifier (bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
	Create a Quantifier.
Quantifier	MkQuantifier (bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
	Create a Quantifier.
Lambda	MkLambda (Sort[] sorts, Symbol[] names, Expr body)
	Create a lambda expression.
Lambda	MkLambda (Expr[] boundConstants, Expr body)
	Create a lambda expression.
BoolExpr[]	ParseSMTLIB2String (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
	Parse the given string using the SMT-LIB2 parser.
BoolExpr[]	ParseSMTLIB2File (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
	Parse the given file using the SMT-LIB2 parser.
string	BenchmarkToSmtlibString (string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
	Convert a benchmark into SMT-LIB2 formatted string.
Goal	MkGoal (bool models=true, bool unsatCores=false, bool proofs=false)
	Creates a new Goal.
Params	MkParams ()
	Creates a new ParameterSet.
string	TacticDescription (string name)
	Returns a string containing a description of the tactic with the given name.
Tactic	MkTactic (string name)
	Creates a new Tactic.
Tactic	AndThen (Tactic t1, Tactic t2, params Tactic[] ts)
	Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Tactic	Then (Tactic t1, Tactic t2, params Tactic[] ts)
	Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Tactic	OrElse (Tactic t1, Tactic t2)
	Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.
Tactic	TryFor (Tactic t, uint ms)
	Create a tactic that applies t to a goal for ms milliseconds.
Tactic	When (Probe p, Tactic t)
	Create a tactic that applies t to a given goal if the probe p evaluates to true.
Tactic	Cond (Probe p, Tactic t1, Tactic t2)
	Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.
Tactic	Repeat (Tactic t, uint max=uint.MaxValue)
	Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
Tactic	Skip ()
	Create a tactic that just returns the given goal.
Tactic	Fail ()
	Create a tactic always fails.
Tactic	FailIf (Probe p)
	Create a tactic that fails if the probe p evaluates to false.
Tactic	FailIfNotDecided ()
	Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’).
Tactic	UsingParams (Tactic t, Params p)
	Create a tactic that applies t using the given set of parameters p .
Tactic	With (Tactic t, Params p)
	Create a tactic that applies t using the given set of parameters p .
Tactic	ParOr (params Tactic[] t)
	Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).
Tactic	ParAndThen (Tactic t1, Tactic t2)
	Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.
void	Interrupt ()
	Interrupt the execution of a Z3 procedure.
ASTMap	MkASTMap ()
	Creates an empty map from ASTs to ASTs.
Expr	QeLite (ASTVector vars, Expr body)
	Performs best-effort quantifier elimination for the variables in vars .
Expr	QeModelProject (Model model, Expr[] bounds, Expr body)
	Projects the bound applications from body using model .
Expr	QeModelProjectSkolem (Model model, Expr[] bounds, Expr body, ASTMap map)
	Projects bound applications and records Skolem terms in map .
Expr	QeModelProjectWithWitness (Model model, Expr[] bounds, Expr body, ASTMap map)
	Projects bound applications and records witnesses in map .
string	SimplifierDescription (string name)
	Returns a string containing a description of the simplifier with the given name.
Simplifier	MkSimplifier (string name)
	Creates a new Tactic.
Simplifier	AndThen (Simplifier t1, Simplifier t2, params Simplifier[] ts)
	Create a simplifier that applies t1 and then t2 .
Simplifier	Then (Simplifier t1, Simplifier t2, params Simplifier[] ts)
	Create a simplifier that applies t1 and then then t2 .
Simplifier	UsingParams (Simplifier t, Params p)
	Create a tactic that applies t using the given set of parameters p .
string	ProbeDescription (string name)
	Returns a string containing a description of the probe with the given name.
Probe	MkProbe (string name)
	Creates a new Probe.
Probe	ConstProbe (double val)
	Create a probe that always evaluates to val .
Probe	Lt (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2
Probe	Gt (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2
Probe	Le (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the value returned by p2
Probe	Ge (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the value returned by p2
Probe	Eq (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2
Probe	And (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
Probe	Or (Probe p1, Probe p2)
	Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
Probe	Not (Probe p)
	Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Solver	MkSolver (Symbol logic=null)
	Creates a new (incremental) solver.
Solver	MkSolver (string logic)
	Creates a new (incremental) solver.
Solver	MkSimpleSolver ()
	Creates a new (incremental) solver.
Solver	MkSolver (Solver s, Simplifier t)
	Creates a solver that uses an incremental simplifier.
Solver	MkSolver (Tactic t)
	Creates a solver that is implemented using the given tactic.
Fixedpoint	MkFixedpoint ()
	Create a Fixedpoint context.
Optimize	MkOptimize ()
	Create an Optimization context.
FPRMSort	MkFPRoundingModeSort ()
	Create the floating-point RoundingMode sort.
FPRMExpr	MkFPRoundNearestTiesToEven ()
	Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
FPRMNum	MkFPRNE ()
	Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
FPRMNum	MkFPRoundNearestTiesToAway ()
	Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
FPRMNum	MkFPRNA ()
	Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
FPRMNum	MkFPRoundTowardPositive ()
	Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
FPRMNum	MkFPRTP ()
	Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
FPRMNum	MkFPRoundTowardNegative ()
	Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
FPRMNum	MkFPRTN ()
	Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
FPRMNum	MkFPRoundTowardZero ()
	Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
FPRMNum	MkFPRTZ ()
	Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
FPSort	MkFPSort (uint ebits, uint sbits)
	Create a FloatingPoint sort.
FPSort	MkFPSortHalf ()
	Create the half-precision (16-bit) FloatingPoint sort.
FPSort	MkFPSort16 ()
	Create the half-precision (16-bit) FloatingPoint sort.
FPSort	MkFPSortSingle ()
	Create the single-precision (32-bit) FloatingPoint sort.
FPSort	MkFPSort32 ()
	Create the single-precision (32-bit) FloatingPoint sort.
FPSort	MkFPSortDouble ()
	Create the double-precision (64-bit) FloatingPoint sort.
FPSort	MkFPSort64 ()
	Create the double-precision (64-bit) FloatingPoint sort.
FPSort	MkFPSortQuadruple ()
	Create the quadruple-precision (128-bit) FloatingPoint sort.
FPSort	MkFPSort128 ()
	Create the quadruple-precision (128-bit) FloatingPoint sort.
FPNum	MkFPNaN (FPSort s)
	Create a NaN of sort s.
FPNum	MkFPInf (FPSort s, bool negative)
	Create a floating-point infinity of sort s.
FPNum	MkFPZero (FPSort s, bool negative)
	Create a floating-point zero of sort s.
FPNum	MkFPNumeral (float v, FPSort s)
	Create a numeral of FloatingPoint sort from a float.
FPNum	MkFPNumeral (double v, FPSort s)
	Create a numeral of FloatingPoint sort from a float.
FPNum	MkFPNumeral (int v, FPSort s)
	Create a numeral of FloatingPoint sort from an int.
FPNum	MkFPNumeral (bool sgn, uint sig, int exp, FPSort s)
	Create a numeral of FloatingPoint sort from a sign bit and two integers.
FPNum	MkFPNumeral (bool sgn, Int64 exp, UInt64 sig, FPSort s)
	Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
FPNum	MkFP (float v, FPSort s)
	Create a numeral of FloatingPoint sort from a float.
FPNum	MkFP (double v, FPSort s)
	Create a numeral of FloatingPoint sort from a float.
FPNum	MkFP (int v, FPSort s)
	Create a numeral of FloatingPoint sort from an int.
FPNum	MkFP (bool sgn, int exp, uint sig, FPSort s)
	Create a numeral of FloatingPoint sort from a sign bit and two integers.
FPNum	MkFP (bool sgn, Int64 exp, UInt64 sig, FPSort s)
	Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
FPExpr	MkFPAbs (FPExpr t)
	Floating-point absolute value.
FPExpr	MkFPNeg (FPExpr t)
	Floating-point negation.
FPExpr	MkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
	Floating-point addition.
FPExpr	MkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
	Floating-point subtraction.
FPExpr	MkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
	Floating-point multiplication.
FPExpr	MkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
	Floating-point division.
FPExpr	MkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
	Floating-point fused multiply-add.
FPExpr	MkFPSqrt (FPRMExpr rm, FPExpr t)
	Floating-point square root.
FPExpr	MkFPRem (FPExpr t1, FPExpr t2)
	Floating-point remainder.
FPExpr	MkFPRoundToIntegral (FPRMExpr rm, FPExpr t)
	Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
FPExpr	MkFPMin (FPExpr t1, FPExpr t2)
	Minimum of floating-point numbers.
FPExpr	MkFPMax (FPExpr t1, FPExpr t2)
	Maximum of floating-point numbers.
BoolExpr	MkFPLEq (FPExpr t1, FPExpr t2)
	Floating-point less than or equal.
BoolExpr	MkFPLt (FPExpr t1, FPExpr t2)
	Floating-point less than.
BoolExpr	MkFPGEq (FPExpr t1, FPExpr t2)
	Floating-point greater than or equal.
BoolExpr	MkFPGt (FPExpr t1, FPExpr t2)
	Floating-point greater than.
BoolExpr	MkFPEq (FPExpr t1, FPExpr t2)
	Floating-point equality.
BoolExpr	MkFPIsNormal (FPExpr t)
	Predicate indicating whether t is a normal floating-point number.
BoolExpr	MkFPIsSubnormal (FPExpr t)
	Predicate indicating whether t is a subnormal floating-point number.
BoolExpr	MkFPIsZero (FPExpr t)
	Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
BoolExpr	MkFPIsInfinite (FPExpr t)
	Predicate indicating whether t is a floating-point number representing +oo or -oo.
BoolExpr	MkFPIsNaN (FPExpr t)
	Predicate indicating whether t is a NaN.
BoolExpr	MkFPIsNegative (FPExpr t)
	Predicate indicating whether t is a negative floating-point number.
BoolExpr	MkFPIsPositive (FPExpr t)
	Predicate indicating whether t is a positive floating-point number.
FPExpr	MkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
	Create an expression of FloatingPoint sort from three bit-vector expressions.
FPExpr	MkFPToFP (BitVecExpr bv, FPSort s)
	Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
FPExpr	MkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
	Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
FPExpr	MkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
	Conversion of a term of real sort into a term of FloatingPoint sort.
FPExpr	MkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
	Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
FPExpr	MkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
	Conversion of a floating-point number to another FloatingPoint sort s.
BitVecExpr	MkFPToBV (FPRMExpr rm, FPExpr t, uint sz, bool sign)
	Conversion of a floating-point term into a bit-vector.
RealExpr	MkFPToReal (FPExpr t)
	Conversion of a floating-point term into a real-numbered term.
BitVecExpr	MkFPToIEEEBV (FPExpr t)
	Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
BitVecExpr	MkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
	Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
AST	WrapAST (IntPtr nativeObject)
	Wraps an AST.
IntPtr	UnwrapAST (AST a)
	Unwraps an AST.
FuncDecl	MkPartialOrder (Sort a, uint index)
	Create a partial order relation over a sort.
FuncDecl	MkTransitiveClosure (FuncDecl f)
	Create the transitive closure of a binary relation.
ASTVector	PolynomialSubresultants (Expr p, Expr q, Expr x)
	Return the nonzero subresultants of p and q with respect to the "variable" x.
string	SimplifyHelp ()
	Return a string describing all available parameters to Expr.Simplify.
void	UpdateParamValue (string id, string value)
	Update a mutable configuration parameter.
void	Dispose ()
	Disposes of the context.

Properties
BoolSort	BoolSort [get]
	Retrieves the Boolean sort of the context.
IntSort	IntSort [get]
	Retrieves the Integer sort of the context.
RealSort	RealSort [get]
	Retrieves the Real sort of the context.
ComplexSort	ComplexSort [get]
	Retrieves the Complex sort of the context.
CharSort	CharSort [get]
	Retrieves the character sort of the context.
SeqSort	StringSort [get]
	Retrieves the String sort of the context.
Z3_ast_print_mode	PrintMode [get, set]
	Selects the format used for pretty-printing expressions.
uint	NumTactics [get]
	The number of supported tactics.
string[]	TacticNames [get]
	The names of all supported tactics.
uint	NumSimplifiers [get]
	The number of supported simplifiers.
string[]	SimplifierNames [get]
	The names of all supported tactics.
uint	NumProbes [get]
	The number of supported Probes.
string[]	ProbeNames [get]
	The names of all supported Probes.
ParamDescrs	SimplifyParameterDescriptions [get]
	Retrieves parameter descriptions for simplifier.

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 33 of file Context.cs.

Constructor & Destructor Documentation

Context() [1/2]

Context ( )

inline

Constructor.

Definition at line 39 of file Context.cs.

            : base()
        {
            lock (creation_lock)
            {
                m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                InitContext();
            }
        }

Context() [2/2]

Context ( Dictionary< string, string >  settings )

inline

Constructor.

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 68 of file Context.cs.

            : base()
        {
            Debug.Assert(settings != null);
 
            lock (creation_lock)
            {
                IntPtr cfg = Native.Z3_mk_config();
                foreach (KeyValuePair<string, string> kv in settings)
                    Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
                m_ctx = Native.Z3_mk_context_rc(cfg);
                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                Native.Z3_del_config(cfg);
                InitContext();
            }
        }

Member Function Documentation

AddRecDef()

void AddRecDef ( FuncDecl  f, Expr[]  args, Expr  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 721 of file Context.cs.

        {
            CheckContextMatch(f);
            CheckContextMatch<Expr>(args);
            CheckContextMatch(body);
            IntPtr[] argsNative = AST.ArrayToNative(args);
            Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
        }

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 4394 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
        }

AndThen() [1/2]

Simplifier AndThen ( Simplifier  t1, Simplifier  t2, params Simplifier[]  ts  )

inline

Create a simplifier that applies t1 and then t2 .

Definition at line 4211 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch<Simplifier>(ts);
 
            IntPtr last = IntPtr.Zero;
            if (ts != null && ts.Length > 0)
            {
                last = ts[ts.Length - 1].NativeObject;
                for (int i = ts.Length - 2; i >= 0; i--)
                    last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
            }
            if (last != IntPtr.Zero)
            {
                last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
                return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
            }
            else
                return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
        }

AndThen() [2/2]

Tactic AndThen ( Tactic  t1, Tactic  t2, params Tactic[]  ts  )

inline

Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .

Definition at line 3891 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch<Tactic>(ts);
 
            IntPtr last = IntPtr.Zero;
            if (ts != null && ts.Length > 0)
            {
                last = ts[ts.Length - 1].NativeObject;
                for (int i = ts.Length - 2; i >= 0; i--)
                    last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
            }
            if (last != IntPtr.Zero)
            {
                last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
                return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
            }
            else
                return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by Context.Then(), and Context.Then().

BenchmarkToSmtlibString()

string BenchmarkToSmtlibString ( string  name, string  logic, string  status, string  attributes, BoolExpr[]  assumptions, BoolExpr  formula  )

inline

Convert a benchmark into SMT-LIB2 formatted string.

Parameters

name	Name of the benchmark. May be null.
logic	The benchmark logic. May be null.
status	Status string, such as "sat", "unsat", or "unknown".
attributes	Other attributes, such as source, difficulty or category. May be null.
assumptions	Auxiliary assumptions.
formula	Formula to be checked for consistency in conjunction with assumptions.

Returns

A string representation of the benchmark in SMT-LIB2 format.

Definition at line 3798 of file Context.cs.

        {
            Debug.Assert(assumptions != null);
            Debug.Assert(formula != null);
 
            return Native.Z3_benchmark_to_smtlib_string(
                nCtx,
                name,
                logic,
                status,
                attributes,
                (uint)(assumptions?.Length ?? 0),
                AST.ArrayToNative(assumptions),
                formula.NativeObject);
        }

Referenced by Solver.ToSmt2().

CharFromBV()

Expr CharFromBV ( BitVecExpr  bv )

inline

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

Definition at line 3167 of file Context.cs.

        {
            Debug.Assert(bv != null);
            return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
        }

CharToBV()

BitVecExpr CharToBV ( Expr  ch )

inline

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

Definition at line 3158 of file Context.cs.

        {
            Debug.Assert(ch != null);
            return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
        }

CharToInt()

IntExpr CharToInt ( Expr  ch )

inline

Create an integer (code point) from character.

Definition at line 3149 of file Context.cs.

        {
            Debug.Assert(ch != null);
            return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
        }

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 3983 of file Context.cs.

        {
            Debug.Assert(p != null);
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(p);
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
        }

ConstProbe()

Probe ConstProbe ( double  val )

inline

Create a probe that always evaluates to val .

Definition at line 4314 of file Context.cs.

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

Dispose()

void Dispose ( )

inline

Disposes of the context.

Definition at line 5471 of file Context.cs.

        {
            // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
 
            if (m_boolSort != null) m_boolSort.Dispose();
            if (m_intSort != null) m_intSort.Dispose();
            if (m_realSort != null) m_realSort.Dispose();
            if (m_complexSort != null) m_complexSort.Dispose();
            if (m_stringSort != null) m_stringSort.Dispose();
            if (m_charSort != null) m_charSort.Dispose();
            m_boolSort = null;
            m_intSort = null;
            m_realSort = null;
            m_complexSort = null;
            m_stringSort = null;
            m_charSort = null;
            if (m_ctx != IntPtr.Zero)
            {
                // Suppress the finalizer before performing cleanup so that it cannot
                // run concurrently or redundantly if cleanup raises an exception.
                GC.SuppressFinalize(this);
                IntPtr ctx;
                // Keep a local reference to the error handler delegate to ensure it stays
                // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
                // the field reference; without the local variable the GC could collect the
                // delegate before the native destructor finishes using the handler.
                Native.Z3_error_handler errHandler;
                lock (this)
                {
                    ctx = m_ctx;
                    errHandler = m_n_err_handler;
                    m_n_err_handler = null;
                    m_ctx = IntPtr.Zero;
                }
                // ctx is non-zero only for the thread that wins the lock and zeros m_ctx,
                // preventing double-free when Dispose() is called concurrently.
                if (ctx != IntPtr.Zero)
                {
                    if (!is_external)
                    {
                        Native.Z3_del_context(ctx);
                        GC.KeepAlive(errHandler);
                    }
                    if (m_memPressureAdded)
                    {
                        GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
                        m_memPressureAdded = false;
                    }
                }
            }
        }

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 4380 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
        }

Fail()

Tactic Fail ( )

inline

Create a tactic always fails.

Definition at line 4019 of file Context.cs.

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

FailIf()

Tactic FailIf ( Probe  p )

inline

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

Definition at line 4028 of file Context.cs.

        {
            Debug.Assert(p != null);
 
            CheckContextMatch(p);
            return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
        }

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 4040 of file Context.cs.

        {
 
            return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(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 4366 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
        }

GetFiniteSetSortBasis()

Sort GetFiniteSetSortBasis ( Sort  s )

inline

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

Definition at line 2579 of file Context.cs.

        {
            Debug.Assert(s != null);
 
            CheckContextMatch(s);
            return Sort.Create(this, Native.Z3_get_finite_set_sort_basis(nCtx, s.NativeObject));
        }

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 4338 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
        }

Interrupt()

void Interrupt ( )

inline

Interrupt the execution of a Z3 procedure.

This procedure can be used to interrupt: solvers, simplifiers and tactics.

Definition at line 4100 of file Context.cs.

        {
            Native.Z3_interrupt(nCtx);
        }

IntToString()

SeqExpr IntToString ( Expr  e )

inline

Convert an integer expression to a string.

Definition at line 2758 of file Context.cs.

        {
            Debug.Assert(e != null);
            Debug.Assert(e is ArithExpr);
            return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
        }

IsFiniteSetSort()

bool IsFiniteSetSort ( Sort  s )

inline

Check if a sort is a finite set sort.

Definition at line 2568 of file Context.cs.

        {
            Debug.Assert(s != null);
 
            CheckContextMatch(s);
            return Native.Z3_is_finite_set_sort(nCtx, s.NativeObject) != 0;
        }

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 4352 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
        }

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 4324 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
        }

MkAdd() [1/2]

ArithExpr MkAdd ( IEnumerable< ArithExpr >  ts )

inline

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

Definition at line 1225 of file Context.cs.

        {
            Debug.Assert(ts != null);
            return MkAdd(ts.ToArray());
        }

MkAdd() [2/2]

ArithExpr MkAdd ( params ArithExpr[]  ts )

inline

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

Definition at line 1213 of file Context.cs.

        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<ArithExpr>(ts);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }

Referenced by Context.MkAdd(), and ArithExpr.operator+().

MkAnd() [1/2]

BoolExpr MkAnd ( IEnumerable< BoolExpr >  t )

inline

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

Definition at line 1179 of file Context.cs.

        {
            Debug.Assert(t != null);
            return MkAnd(t.ToArray());
        }

MkAnd() [2/2]

BoolExpr MkAnd ( params BoolExpr[]  ts )

inline

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

Definition at line 1167 of file Context.cs.

        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }

Referenced by Goal.AsBoolExpr(), Context.MkAnd(), and BoolExpr.operator&().

MkApp() [1/2]

Expr MkApp ( FuncDecl  f, IEnumerable< Expr >  args  )

inline

Create a new function application.

Definition at line 1015 of file Context.cs.

        {
            Debug.Assert(f != null);
            return MkApp(f, args?.ToArray());
        }

MkApp() [2/2]

Expr MkApp ( FuncDecl  f, params Expr[]  args  )

inline

Create a new function application.

Definition at line 1003 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(args == null || args.All(a => a != null));
            CheckContextMatch(f);
            CheckContextMatch<Expr>(args);
            return Expr.Create(this, f, args);
        }

Referenced by EnumSort.Const(), Context.MkApp(), and Context.MkConst().

MkArrayConst() [1/2]

ArrayExpr MkArrayConst ( string  name, Sort  domain, Sort  range  )

inline

Create an array constant.

Definition at line 2227 of file Context.cs.

        {
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            using var symbol = MkSymbol(name);
            using var sort = MkArraySort(domain, range);
            return (ArrayExpr)MkConst(symbol, sort);
        }

MkArrayConst() [2/2]

ArrayExpr MkArrayConst ( Symbol  name, Sort  domain, Sort  range  )

inline

Create an array constant.

Definition at line 2214 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            using var sort = MkArraySort(domain, range);
            return (ArrayExpr)MkConst(name, sort);
        }

MkArrayExt()

Expr MkArrayExt ( ArrayExpr  arg1, ArrayExpr  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 2403 of file Context.cs.

        {
            Debug.Assert(arg1 != null);
            Debug.Assert(arg2 != null);
 
            CheckContextMatch(arg1);
            CheckContextMatch(arg2);
            return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
        }

MkArraySort() [1/2]

ArraySort MkArraySort ( Sort  domain, Sort  range  )

inline

Create a new array sort.

Definition at line 293 of file Context.cs.

        {
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(domain);
            CheckContextMatch(range);
            return new ArraySort(this, domain, range);
        }

Referenced by Context.MkArrayConst(), and Context.MkArrayConst().

MkArraySort() [2/2]

ArraySort MkArraySort ( Sort[]  domain, Sort  range  )

inline

Create a new n-ary array sort.

Definition at line 306 of file Context.cs.

        {
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            return new ArraySort(this, domain, range);
        }

MkASTMap()

ASTMap MkASTMap ( )

inline

Creates an empty map from ASTs to ASTs.

Definition at line 4110 of file Context.cs.

        {
            return new ASTMap(this);
        }

MkAt()

SeqExpr MkAt ( SeqExpr  s, Expr  index  )

inline

Retrieve sequence of length one at index.

Definition at line 2887 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(index != null);
            CheckContextMatch(s, index);
            return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
        }

MkAtLeast()

BoolExpr MkAtLeast ( IEnumerable< BoolExpr >  args, uint  k  )

inline

Create an at-least-k constraint.

Definition at line 3201 of file Context.cs.

        {
            Debug.Assert(args != null);
            var ts = args.ToArray();
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
                                                          AST.ArrayToNative(ts), k));
        }

MkAtMost()

BoolExpr MkAtMost ( IEnumerable< BoolExpr >  args, uint  k  )

inline

Create an at-most-k constraint.

Definition at line 3189 of file Context.cs.

        {
            Debug.Assert(args != null);
            var ts = args.ToArray();
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
                                                          AST.ArrayToNative(ts), k));
        }

MkBitVecSort()

BitVecSort MkBitVecSort ( uint  size )

inline

Create a new bit-vector sort.

Definition at line 267 of file Context.cs.

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

Referenced by Context.MkBV(), Context.MkBV(), Context.MkBV(), Context.MkBV(), Context.MkBV(), Context.MkBVConst(), and Context.MkBVConst().

MkBool()

BoolExpr MkBool ( bool  value )

inline

Creates a Boolean value.

Definition at line 1041 of file Context.cs.

        {
            return value ? MkTrue() : MkFalse();
        }

MkBoolConst() [1/2]

BoolExpr MkBoolConst ( string  name )

inline

Create a Boolean constant.

Definition at line 900 of file Context.cs.

        {
            using var symbol = MkSymbol(name);
            return (BoolExpr)MkConst(symbol, BoolSort);
        }

MkBoolConst() [2/2]

BoolExpr MkBoolConst ( Symbol  name )

inline

Create a Boolean constant.

Definition at line 890 of file Context.cs.

        {
            Debug.Assert(name != null);
 
            return (BoolExpr)MkConst(name, BoolSort);
        }

MkBoolSort()

BoolSort MkBoolSort ( )

inline

Create a new Boolean sort.

Definition at line 216 of file Context.cs.

        {
            return new BoolSort(this);
        }

MkBound()

Expr MkBound ( uint  index, Sort  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 815 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
        }

MkBV() [1/6]

BitVecNum MkBV ( bool[]  bits )

inline

Create a bit-vector numeral.

Parameters

bits	An array of bits representing the bit-vector. Least significant bit is at position 0.

Definition at line 3518 of file Context.cs.

        {
            byte[] _bits = new byte[bits.Length];
            for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0);
            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
        }

MkBV() [2/6]

BitVecNum MkBV ( int  v, uint  size  )

inline

Create a bit-vector numeral.

Parameters

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

Definition at line 3475 of file Context.cs.

        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }

MkBV() [3/6]

BitVecNum MkBV ( long  v, uint  size  )

inline

Create a bit-vector numeral.

Parameters

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

Definition at line 3497 of file Context.cs.

        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }

MkBV() [4/6]

BitVecNum MkBV ( string  v, uint  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 3464 of file Context.cs.

        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }

MkBV() [5/6]

BitVecNum MkBV ( uint  v, uint  size  )

inline

Create a bit-vector numeral.

Parameters

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

Definition at line 3486 of file Context.cs.

        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }

MkBV() [6/6]

BitVecNum MkBV ( ulong  v, uint  size  )

inline

Create a bit-vector numeral.

Parameters

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

Definition at line 3508 of file Context.cs.

        {
            using var sort = MkBitVecSort(size);
            return (BitVecNum)MkNumeral(v, sort);
        }

MkBV2Int()

IntExpr MkBV2Int ( BitVecExpr  t, bool signed    )

inline

Create an integer from the bit-vector argument t .

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 2075 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0)));
        }

MkBVAdd()

BitVecExpr MkBVAdd ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1563 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVAddNoOverflow()

BoolExpr MkBVAddNoOverflow ( BitVecExpr  t1, BitVecExpr  t2, bool  isSigned  )

inline

Create a predicate that checks that the bit-wise addition does not overflow.

The arguments must be of bit-vector sort.

Definition at line 2089 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
        }

MkBVAddNoUnderflow()

BoolExpr MkBVAddNoUnderflow ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Create a predicate that checks that the bit-wise addition does not underflow.

The arguments must be of bit-vector sort.

Definition at line 2105 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVAND()

BitVecExpr MkBVAND ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1467 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVASHR()

BitVecExpr MkBVASHR ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Arithmetic shift right.

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 1968 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVConst() [1/2]

BitVecExpr MkBVConst ( string  name, uint  size  )

inline

Creates a bit-vector constant.

Definition at line 992 of file Context.cs.

        {
            using var sort = MkBitVecSort(size);
            return (BitVecExpr)MkConst(name, sort);
        }

MkBVConst() [2/2]

BitVecExpr MkBVConst ( Symbol  name, uint  size  )

inline

Creates a bit-vector constant.

Definition at line 981 of file Context.cs.

        {
            Debug.Assert(name != null);
 
            using var sort = MkBitVecSort(size);
            return (BitVecExpr)MkConst(name, sort);
        }

MkBVLSHR()

BitVecExpr MkBVLSHR ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Logical shift right.

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 1944 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVMul()

BitVecExpr MkBVMul ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1591 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVMulNoOverflow()

BoolExpr MkBVMulNoOverflow ( BitVecExpr  t1, BitVecExpr  t2, bool  isSigned  )

inline

Create a predicate that checks that the bit-wise multiplication does not overflow.

The arguments must be of bit-vector sort.

Definition at line 2183 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
        }

MkBVMulNoUnderflow()

BoolExpr MkBVMulNoUnderflow ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Create a predicate that checks that the bit-wise multiplication does not underflow.

The arguments must be of bit-vector sort.

Definition at line 2199 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVNAND()

BitVecExpr MkBVNAND ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1509 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVNeg()

BitVecExpr MkBVNeg ( BitVecExpr  t )

inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1551 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
        }

MkBVNegNoOverflow()

BoolExpr MkBVNegNoOverflow ( BitVecExpr  t )

inline

Create a predicate that checks that the bit-wise negation does not overflow.

The arguments must be of bit-vector sort.

Definition at line 2169 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
        }

MkBVNOR()

BitVecExpr MkBVNOR ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1523 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVNot()

BitVecExpr MkBVNot ( BitVecExpr  t )

inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1431 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
        }

MkBVOR()

BitVecExpr MkBVOR ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1481 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVRedAND()

BitVecExpr MkBVRedAND ( BitVecExpr  t )

inline

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

The argument must have a bit-vector sort.

Definition at line 1443 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
        }

MkBVRedOR()

BitVecExpr MkBVRedOR ( BitVecExpr  t )

inline

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

The argument must have a bit-vector sort.

Definition at line 1455 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
        }

MkBVRotateLeft() [1/2]

BitVecExpr MkBVRotateLeft ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Rotate Left.

Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.

Definition at line 2015 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVRotateLeft() [2/2]

BitVecExpr MkBVRotateLeft ( uint  i, BitVecExpr  t  )

inline

Rotate Left.

Rotate bits of t to the left i times. The argument t must have a bit-vector sort.

Definition at line 1985 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
        }

MkBVRotateRight() [1/2]

BitVecExpr MkBVRotateRight ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Rotate Right.

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

Definition at line 2032 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVRotateRight() [2/2]

BitVecExpr MkBVRotateRight ( uint  i, BitVecExpr  t  )

inline

Rotate Right.

Rotate bits of t to the right i times. The argument t must have a bit-vector sort.

Definition at line 2000 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
        }

MkBVSDiv()

BitVecExpr MkBVSDiv ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Signed division.

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 1633 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSDivNoOverflow()

BoolExpr MkBVSDivNoOverflow ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Create a predicate that checks that the bit-wise signed division does not overflow.

The arguments must be of bit-vector sort.

Definition at line 2153 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSGE()

BoolExpr MkBVSGE ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement signed greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1784 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSGT()

BoolExpr MkBVSGT ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement signed greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1816 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSHL()

BitVecExpr MkBVSHL ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Shift left.

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 1922 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSLE()

BoolExpr MkBVSLE ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement signed less-than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1752 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSLT()

BoolExpr MkBVSLT ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement signed less-than.

The arguments must have the same bit-vector sort.

Definition at line 1720 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSMod()

BitVecExpr MkBVSMod ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement signed remainder (sign follows divisor).

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

Definition at line 1688 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSRem()

BitVecExpr MkBVSRem ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Signed remainder.

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 1671 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSub()

BitVecExpr MkBVSub ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1577 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSubNoOverflow()

BoolExpr MkBVSubNoOverflow ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Create a predicate that checks that the bit-wise subtraction does not overflow.

The arguments must be of bit-vector sort.

Definition at line 2121 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVSubNoUnderflow()

BoolExpr MkBVSubNoUnderflow ( BitVecExpr  t1, BitVecExpr  t2, bool  isSigned  )

inline

Create a predicate that checks that the bit-wise subtraction does not underflow.

The arguments must be of bit-vector sort.

Definition at line 2137 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
        }

MkBVUDiv()

BitVecExpr MkBVUDiv ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Unsigned division.

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 1610 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVUGE()

BoolExpr MkBVUGE ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Unsigned greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1768 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVUGT()

BoolExpr MkBVUGT ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1800 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVULE()

BoolExpr MkBVULE ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Unsigned less-than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1736 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVULT()

BoolExpr MkBVULT ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Unsigned less-than.

The arguments must have the same bit-vector sort.

Definition at line 1704 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVURem()

BitVecExpr MkBVURem ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Unsigned remainder.

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 1651 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVXNOR()

BitVecExpr MkBVXNOR ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1537 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkBVXOR()

BitVecExpr MkBVXOR ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1495 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkCharLe()

BoolExpr MkCharLe ( Expr  ch1, Expr  ch2  )

inline

Create less than or equal to between two characters.

Definition at line 3139 of file Context.cs.

        {
            Debug.Assert(ch1 != null);
            Debug.Assert(ch2 != null);
            return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject));
        }

MkComplement()

ReExpr MkComplement ( ReExpr  re )

inline

Create the complement regular expression.

Definition at line 3051 of file Context.cs.

        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
        }

MkComplex()

ComplexExpr MkComplex ( ArithExpr  real, ArithExpr  imag  )

inline

Constructs a Complex expression from Int or Real components.

Definition at line 958 of file Context.cs.

        {
            CheckContextMatch(real, imag);
            return new ComplexExpr(this, Native.Z3_mk_complex(nCtx, real.NativeObject, imag.NativeObject));
        }

MkComplexConst() [1/2]

ComplexExpr MkComplexConst ( string  name )

inline

Creates a Complex constant.

Definition at line 952 of file Context.cs.

        {
            return (ComplexExpr)MkConst(name, ComplexSort);
        }

MkComplexConst() [2/2]

ComplexExpr MkComplexConst ( Symbol  name )

inline

Creates a Complex constant.

Definition at line 946 of file Context.cs.

        {
            return (ComplexExpr)MkConst(name, ComplexSort);
        }

MkComplexSort()

ComplexSort MkComplexSort ( )

inline

Creates the Complex sort.

Definition at line 259 of file Context.cs.

        {
            return new ComplexSort(this);
        }

MkConcat() [1/3]

BitVecExpr MkConcat ( BitVecExpr  t1, BitVecExpr  t2  )

inline

Bit-vector concatenation.

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 1836 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkConcat() [2/3]

ReExpr MkConcat ( params ReExpr[]  t )

inline

Create the concatenation of regular languages.

Definition at line 3060 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<ReExpr>(t);
            return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }

MkConcat() [3/3]

SeqExpr MkConcat ( params SeqExpr[]  t )

inline

Concatenate sequences.

Definition at line 2799 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<SeqExpr>(t);
            return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }

MkConst() [1/3]

Expr MkConst ( FuncDecl  f )

inline

Creates a fresh constant from the FuncDecl f .

Parameters

f	A decl of a 0-arity function

Definition at line 880 of file Context.cs.

        {
            Debug.Assert(f != null);
 
            return MkApp(f);
        }

MkConst() [2/3]

Expr MkConst ( string  name, Sort  range  )

inline

Creates a new Constant of sort range and named name .

Definition at line 856 of file Context.cs.

        {
            Debug.Assert(range != null);
 
            using var symbol = MkSymbol(name);
            return MkConst(symbol, range);
        }

MkConst() [3/3]

Expr MkConst ( Symbol  name, Sort  range  )

inline

Creates a new Constant of sort range and named name .

Definition at line 842 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(name);
            CheckContextMatch(range);
 
            return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
        }

Referenced by Context.MkArrayConst(), Context.MkArrayConst(), Context.MkBoolConst(), Context.MkBoolConst(), Context.MkBVConst(), Context.MkBVConst(), Context.MkComplexConst(), Context.MkComplexConst(), Context.MkConst(), Context.MkIntConst(), Context.MkIntConst(), Context.MkRealConst(), and Context.MkRealConst().

MkConstArray()

ArrayExpr MkConstArray ( Sort  domain, Expr  v  )

inline

Create a constant array.

The resulting term is an array, such that a selecton an arbitrary index produces the value v.

See also

MkArraySort(Sort, Sort), MkSelect(ArrayExpr, Expr)

Definition at line 2354 of file Context.cs.

        {
            Debug.Assert(domain != null);
            Debug.Assert(v != null);
 
            CheckContextMatch(domain);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
        }

MkConstDecl() [1/2]

FuncDecl MkConstDecl ( string  name, Sort  range  )

inline

Creates a new constant function declaration.

Definition at line 776 of file Context.cs.

        {
            Debug.Assert(range != null);
 
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            return new FuncDecl(this, symbol, null, range);
        }

MkConstDecl() [2/2]

FuncDecl MkConstDecl ( Symbol  name, Sort  range  )

inline

Creates a new constant function declaration.

Definition at line 763 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(name);
            CheckContextMatch(range);
            return new FuncDecl(this, name, null, range);
        }

MkConstructor() [1/2]

Constructor MkConstructor ( string  name, string  recognizer, string[]  fieldNames = null, Sort[]  sorts = null, uint[]  sortRefs = null  )

inline

Create a datatype constructor.

Parameters

name
recognizer
fieldNames
sorts
sortRefs

Returns

Definition at line 449 of file Context.cs.

        {
 
            using var nameSymbol = MkSymbol(name);
            using var recognizerSymbol = MkSymbol(recognizer);
            var fieldSymbols = MkSymbols(fieldNames);
            try
            {
                return new Constructor(this, nameSymbol, recognizerSymbol, fieldSymbols, sorts, sortRefs);
            }
            finally
            {
                foreach (var fieldSymbol in fieldSymbols)
                    fieldSymbol.Dispose();
            }
        }

MkConstructor() [2/2]

Constructor MkConstructor ( Symbol  name, Symbol  recognizer, Symbol[]  fieldNames = null, Sort[]  sorts = null, uint[]  sortRefs = null  )

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 432 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(recognizer != null);
 
            return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
        }

MkContains()

BoolExpr MkContains ( SeqExpr  s1, SeqExpr  s2  )

inline

Check for sequence containment of s2 in s1.

Definition at line 2854 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkDatatypeSort() [1/2]

DatatypeSort MkDatatypeSort ( string  name, Constructor[]  constructors  )

inline

Create a new datatype sort.

Definition at line 484 of file Context.cs.

        {
            Debug.Assert(constructors != null);
            Debug.Assert(constructors.All(c => c != null));
 
            CheckContextMatch<Constructor>(constructors);
            using var symbol = MkSymbol(name);
            return new DatatypeSort(this, symbol, constructors);
        }

MkDatatypeSort() [2/2]

DatatypeSort MkDatatypeSort ( Symbol  name, Constructor[]  constructors  )

inline

Create a new datatype sort.

Definition at line 469 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(constructors != null);
            Debug.Assert(constructors.All(c => c != null));
 
 
            CheckContextMatch(name);
            CheckContextMatch<Constructor>(constructors);
            return new DatatypeSort(this, name, constructors);
        }

MkDatatypeSortRef() [1/2]

DatatypeSort MkDatatypeSortRef ( string  name, Sort[]  parameters = null  )

inline

Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or parametric datatypes.

Parameters

name	name of the datatype sort
parameters	optional array of sort parameters for parametric datatypes

Definition at line 518 of file Context.cs.

        {
            using var symbol = MkSymbol(name);
            return MkDatatypeSortRef(symbol, parameters);
        }

MkDatatypeSortRef() [2/2]

DatatypeSort MkDatatypeSortRef ( Symbol  name, Sort[]  parameters = null  )

inline

Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or parametric datatypes.

Parameters

name	name of the datatype sort
parameters	optional array of sort parameters for parametric datatypes

Definition at line 500 of file Context.cs.

        {
            Debug.Assert(name != null);
            CheckContextMatch(name);
            if (parameters != null)
                CheckContextMatch<Sort>(parameters);
            
            var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
            var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
            return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
        }

Referenced by Context.MkDatatypeSortRef().

MkDatatypeSorts() [1/2]

DatatypeSort[] MkDatatypeSorts ( string[]  names, Constructor  c[][]  )

inline

Create mutually recursive data-types.

Parameters

names
c

Returns

Definition at line 562 of file Context.cs.

        {
            Debug.Assert(names != null);
            Debug.Assert(c != null);
            Debug.Assert(names.Length == c.Length);
            //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
            //Debug.Assert(names.All(name => name != null));
 
            var symbols = MkSymbols(names);
            try
            {
                return MkDatatypeSorts(symbols, c);
            }
            finally
            {
                foreach (var symbol in symbols)
                    symbol.Dispose();
            }
        }

MkDatatypeSorts() [2/2]

DatatypeSort[] MkDatatypeSorts ( Symbol[]  names, Constructor  c[][]  )

inline

Create mutually recursive datatypes.

Parameters

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

Definition at line 529 of file Context.cs.

        {
            Debug.Assert(names != null);
            Debug.Assert(c != null);
            Debug.Assert(names.Length == c.Length);
            //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
            Debug.Assert(names.All(name => name != null));
 
            CheckContextMatch<Symbol>(names);
            uint n = (uint)names.Length;
            ConstructorList[] cla = new ConstructorList[n];
            IntPtr[] n_constr = new IntPtr[n];
            for (uint i = 0; i < n; i++)
            {
                Constructor[] constructor = c[i];
                CheckContextMatch<Constructor>(constructor);
                cla[i] = new ConstructorList(this, constructor);
                n_constr[i] = cla[i].NativeObject;
            }
            IntPtr[] n_res = new IntPtr[n];
            Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
            DatatypeSort[] res = new DatatypeSort[n];
            for (uint i = 0; i < n; i++)
                res[i] = new DatatypeSort(this, n_res[i]);
            return res;
        }

Referenced by Context.MkDatatypeSorts().

MkDiff()

ReExpr MkDiff ( ReExpr  a, ReExpr  b  )

inline

Create a difference regular expression.

Definition at line 3096 of file Context.cs.

        {
            Debug.Assert(a != null);
            Debug.Assert(b != null);
            CheckContextMatch(a, b);
            return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
        }

MkDistinct() [1/2]

BoolExpr MkDistinct ( IEnumerable< Expr >  args )

inline

Creates a distinct term.

Definition at line 1074 of file Context.cs.

        {
            Debug.Assert(args != null);
            return MkDistinct(args.ToArray());
        }

MkDistinct() [2/2]

BoolExpr MkDistinct ( params Expr[]  args )

inline

Creates a distinct term.

Definition at line 1062 of file Context.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            CheckContextMatch<Expr>(args);
            return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }

Referenced by Context.MkDistinct().

MkDiv()

ArithExpr MkDiv ( ArithExpr  t1, ArithExpr  t2  )

inline

Create an expression representing t1 / t2.

Definition at line 1278 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by ArithExpr.operator/().

MkEmptyRe()

ReExpr MkEmptyRe ( Sort  s )

inline

Create the empty regular expression. The sort s should be a regular expression.

Definition at line 3108 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
        }

MkEmptySeq()

SeqExpr MkEmptySeq ( Sort  s )

inline

Create the empty sequence.

Definition at line 2731 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
        }

MkEmptySet()

ArrayExpr MkEmptySet ( Sort  domain )

inline

Create an empty set.

Definition at line 2430 of file Context.cs.

        {
            Debug.Assert(domain != null);
 
            CheckContextMatch(domain);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
        }

MkEnumSort() [1/2]

EnumSort MkEnumSort ( string  name, params string[]  enumNames  )

inline

Create a new enumeration sort.

Definition at line 350 of file Context.cs.

        {
            Debug.Assert(enumNames != null);
 
            var enumSymbols = MkSymbols(enumNames);
            try
            {
                using var symbol = MkSymbol(name);
                return new EnumSort(this, symbol, enumSymbols);
            }
            finally
            {
                foreach (var enumSymbol in enumSymbols)
                    enumSymbol.Dispose();
            }
        }

MkEnumSort() [2/2]

EnumSort MkEnumSort ( Symbol  name, params Symbol[]  enumNames  )

inline

Create a new enumeration sort.

Definition at line 335 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(enumNames != null);
            Debug.Assert(enumNames.All(f => f != null));
 
 
            CheckContextMatch(name);
            CheckContextMatch<Symbol>(enumNames);
            return new EnumSort(this, name, enumNames);
        }

MkEq()

BoolExpr MkEq ( Expr  x, Expr  y  )

inline

Creates the equality x = y .

Definition at line 1049 of file Context.cs.

        {
            Debug.Assert(x != null);
            Debug.Assert(y != null);
 
            CheckContextMatch(x);
            CheckContextMatch(y);
            return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
        }

MkExists() [1/2]

Quantifier MkExists ( Expr[]  boundConstants, Expr  body, uint  weight = 1, Pattern[]  patterns = null, Expr[]  noPatterns = null, Symbol  quantifierID = null, Symbol  skolemID = null  )

inline

Create an existential Quantifier.

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

See also

MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)

Definition at line 3619 of file Context.cs.

        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
            return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }

MkExists() [2/2]

Quantifier MkExists ( Sort[]  sorts, Symbol[]  names, Expr  body, uint  weight = 1, Pattern[]  patterns = null, Expr[]  noPatterns = null, Symbol  quantifierID = null, Symbol  skolemID = null  )

inline

Create an existential Quantifier.

Creates an existential quantifier using de-Bruijn indexed variables. (MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)).

Definition at line 3597 of file Context.cs.

        {
            Debug.Assert(sorts != null);
            Debug.Assert(names != null);
            Debug.Assert(body != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
            return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }

Referenced by Context.MkQuantifier(), and Context.MkQuantifier().

MkExtract() [1/2]

SeqExpr MkExtract ( SeqExpr  s, IntExpr  offset, IntExpr  length  )

inline

Extract subsequence.

Definition at line 2909 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(offset != null);
            Debug.Assert(length != null);
            CheckContextMatch(s, offset, length);
            return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
        }

MkExtract() [2/2]

BitVecExpr MkExtract ( uint  high, uint  low, BitVecExpr  t  )

inline

Bit-vector extraction.

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 1855 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
        }

MkFalse()

BoolExpr MkFalse ( )

inline

The false Term.

Definition at line 1033 of file Context.cs.

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

Referenced by Context.MkBool(), and Context.MkXor().

MkFiniteDomainSort() [1/2]

FiniteDomainSort MkFiniteDomainSort ( string  name, ulong  size  )

inline

Create a new finite domain sort.

Returns

The result is a sort

Elements of the sort are created using

See also

MkNumeral(ulong, Sort)

, and the elements range from 0 to size-1.

Parameters

name	The name used to identify the sort
size	The size of the sort

Definition at line 414 of file Context.cs.

        {
            using var symbol = MkSymbol(name);
            return new FiniteDomainSort(this, symbol, size);
        }

MkFiniteDomainSort() [2/2]

FiniteDomainSort MkFiniteDomainSort ( Symbol  name, ulong  size  )

inline

Create a new finite domain sort.

Returns

The result is a sort

Parameters

name	The name used to identify the sort
size	The size of the sort

Definition at line 398 of file Context.cs.

        {
            Debug.Assert(name != null);
 
            CheckContextMatch(name);
            return new FiniteDomainSort(this, name, size);
        }

MkFiniteSetDifference()

Expr MkFiniteSetDifference ( Expr  s1, Expr  s2  )

inline

Create the difference of two finite sets.

Definition at line 2638 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return Expr.Create(this, Native.Z3_mk_finite_set_difference(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkFiniteSetEmpty()

Expr MkFiniteSetEmpty ( Sort  setSort )

inline

Create an empty finite set.

Definition at line 2590 of file Context.cs.

        {
            Debug.Assert(setSort != null);
 
            CheckContextMatch(setSort);
            return Expr.Create(this, Native.Z3_mk_finite_set_empty(nCtx, setSort.NativeObject));
        }

MkFiniteSetFilter()

Expr MkFiniteSetFilter ( Expr  f, Expr  set  )

inline

Filter a finite set with a predicate.

Definition at line 2701 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(f);
            CheckContextMatch(set);
            return Expr.Create(this, Native.Z3_mk_finite_set_filter(nCtx, f.NativeObject, set.NativeObject));
        }

MkFiniteSetIntersect()

Expr MkFiniteSetIntersect ( Expr  s1, Expr  s2  )

inline

Create the intersection of two finite sets.

Definition at line 2625 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return Expr.Create(this, Native.Z3_mk_finite_set_intersect(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkFiniteSetMap()

Expr MkFiniteSetMap ( Expr  f, Expr  set  )

inline

Map a function over all elements in a finite set.

Definition at line 2688 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(f);
            CheckContextMatch(set);
            return Expr.Create(this, Native.Z3_mk_finite_set_map(nCtx, f.NativeObject, set.NativeObject));
        }

MkFiniteSetMember()

BoolExpr MkFiniteSetMember ( Expr  elem, Expr  set  )

inline

Check for membership in a finite set.

Definition at line 2651 of file Context.cs.

        {
            Debug.Assert(elem != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(elem);
            CheckContextMatch(set);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_member(nCtx, elem.NativeObject, set.NativeObject));
        }

MkFiniteSetRange()

Expr MkFiniteSetRange ( Expr  low, Expr  high  )

inline

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

Definition at line 2714 of file Context.cs.

        {
            Debug.Assert(low != null);
            Debug.Assert(high != null);
 
            CheckContextMatch(low);
            CheckContextMatch(high);
            return Expr.Create(this, Native.Z3_mk_finite_set_range(nCtx, low.NativeObject, high.NativeObject));
        }

MkFiniteSetSingleton()

Expr MkFiniteSetSingleton ( Expr  elem )

inline

Create a singleton finite set.

Definition at line 2601 of file Context.cs.

        {
            Debug.Assert(elem != null);
 
            CheckContextMatch(elem);
            return Expr.Create(this, Native.Z3_mk_finite_set_singleton(nCtx, elem.NativeObject));
        }

MkFiniteSetSize()

Expr MkFiniteSetSize ( Expr  set )

inline

Get the cardinality of a finite set.

Definition at line 2664 of file Context.cs.

        {
            Debug.Assert(set != null);
 
            CheckContextMatch(set);
            return Expr.Create(this, Native.Z3_mk_finite_set_size(nCtx, set.NativeObject));
        }

MkFiniteSetSort()

FiniteSetSort MkFiniteSetSort ( Sort  elemSort )

inline

Create a finite set sort over the given element sort.

Definition at line 2557 of file Context.cs.

        {
            Debug.Assert(elemSort != null);
 
            CheckContextMatch(elemSort);
            return new FiniteSetSort(this, elemSort);
        }

MkFiniteSetSubset()

BoolExpr MkFiniteSetSubset ( Expr  s1, Expr  s2  )

inline

Check if one finite set is a subset of another.

Definition at line 2675 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_subset(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkFiniteSetUnion()

Expr MkFiniteSetUnion ( Expr  s1, Expr  s2  )

inline

Create the union of two finite sets.

Definition at line 2612 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
 
            CheckContextMatch(s1);
            CheckContextMatch(s2);
            return Expr.Create(this, Native.Z3_mk_finite_set_union(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkFixedpoint()

Fixedpoint MkFixedpoint ( )

inline

Create a Fixedpoint context.

Definition at line 4499 of file Context.cs.

        {
 
            return new Fixedpoint(this);
        }

MkForall() [1/2]

Quantifier MkForall ( Expr[]  boundConstants, Expr  body, uint  weight = 1, Pattern[]  patterns = null, Expr[]  noPatterns = null, Symbol  quantifierID = null, Symbol  skolemID = null  )

inline

Create a universal Quantifier.

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

See also

MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)

Definition at line 3579 of file Context.cs.

        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }

MkForall() [2/2]

Quantifier MkForall ( Sort[]  sorts, Symbol[]  names, Expr  body, uint  weight = 1, Pattern[]  patterns = null, Expr[]  noPatterns = null, Symbol  quantifierID = null, Symbol  skolemID = null  )

inline

Create a universal Quantifier.

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.

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.

Definition at line 3555 of file Context.cs.

        {
            Debug.Assert(sorts != null);
            Debug.Assert(names != null);
            Debug.Assert(body != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }

Referenced by Context.MkQuantifier(), and Context.MkQuantifier().

MkFP() [1/6]

FPExpr MkFP ( BitVecExpr  sgn, BitVecExpr  sig, BitVecExpr  exp  )

inline

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

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.

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.

Definition at line 5089 of file Context.cs.

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

MkFP() [2/6]

FPNum MkFP ( bool  sgn, int  exp, uint  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.

Definition at line 4810 of file Context.cs.

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

MkFP() [3/6]

FPNum MkFP ( bool  sgn, Int64  exp, UInt64  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.

Definition at line 4822 of file Context.cs.

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

MkFP() [4/6]

FPNum MkFP ( double  v, FPSort  s  )

inline

Create a numeral of FloatingPoint sort from a float.

Parameters

v	numeral value.
s	FloatingPoint sort.

Definition at line 4788 of file Context.cs.

        {
            return MkFPNumeral(v, s);
        }

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.

Definition at line 4778 of file Context.cs.

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

Definition at line 4798 of file Context.cs.

        {
            return MkFPNumeral(v, s);
        }

MkFPAbs()

FPExpr MkFPAbs ( FPExpr  t )

inline

Floating-point absolute value.

Parameters

t	floating-point term

Definition at line 4834 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
        }

MkFPAdd()

FPExpr MkFPAdd ( FPRMExpr  rm, FPExpr  t1, FPExpr  t2  )

inline

Floating-point addition.

Parameters

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

Definition at line 4854 of file Context.cs.

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

MkFPDiv()

FPExpr MkFPDiv ( FPRMExpr  rm, FPExpr  t1, FPExpr  t2  )

inline

Floating-point division.

Parameters

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

Definition at line 4887 of file Context.cs.

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

MkFPEq()

BoolExpr MkFPEq ( FPExpr  t1, FPExpr  t2  )

inline

Floating-point equality.

Note that this is IEEE 754 equality (as opposed to standard =).

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 5006 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPFMA()

FPExpr MkFPFMA ( FPRMExpr  rm, FPExpr  t1, FPExpr  t2, FPExpr  t3  )

inline

Floating-point fused multiply-add.

The result is round((t1 * t2) + t3)

Parameters

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

Definition at line 4902 of file Context.cs.

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

MkFPGEq()

BoolExpr MkFPGEq ( FPExpr  t1, FPExpr  t2  )

inline

Floating-point greater than or equal.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4983 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPGt()

BoolExpr MkFPGt ( FPExpr  t1, FPExpr  t2  )

inline

Floating-point greater than.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4993 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPInf()

FPNum MkFPInf ( FPSort  s, bool  negative  )

inline

Create a floating-point infinity of sort s.

Parameters

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

Definition at line 4704 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
        }

MkFPIsInfinite()

BoolExpr MkFPIsInfinite ( FPExpr  t )

inline

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

Parameters

t	floating-point term

Definition at line 5042 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
        }

MkFPIsNaN()

BoolExpr MkFPIsNaN ( FPExpr  t )

inline

Predicate indicating whether t is a NaN.

Parameters

t	floating-point term

Definition at line 5051 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
        }

MkFPIsNegative()

BoolExpr MkFPIsNegative ( FPExpr  t )

inline

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

Parameters

t	floating-point term

Definition at line 5060 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
        }

MkFPIsNormal()

BoolExpr MkFPIsNormal ( FPExpr  t )

inline

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

Parameters

t	floating-point term

Definition at line 5015 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
        }

MkFPIsPositive()

BoolExpr MkFPIsPositive ( FPExpr  t )

inline

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

Parameters

t	floating-point term

Definition at line 5069 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
        }

MkFPIsSubnormal()

BoolExpr MkFPIsSubnormal ( FPExpr  t )

inline

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

Parameters

t	floating-point term

Definition at line 5024 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
        }

MkFPIsZero()

BoolExpr MkFPIsZero ( FPExpr  t )

inline

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

Parameters

t	floating-point term

Definition at line 5033 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
        }

MkFPLEq()

BoolExpr MkFPLEq ( FPExpr  t1, FPExpr  t2  )

inline

Floating-point less than or equal.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4963 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPLt()

BoolExpr MkFPLt ( FPExpr  t1, FPExpr  t2  )

inline

Floating-point less than.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4973 of file Context.cs.

        {
            return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPMax()

FPExpr MkFPMax ( FPExpr  t1, FPExpr  t2  )

inline

Maximum of floating-point numbers.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4953 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPMin()

FPExpr MkFPMin ( FPExpr  t1, FPExpr  t2  )

inline

Minimum of floating-point numbers.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4943 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPMul()

FPExpr MkFPMul ( FPRMExpr  rm, FPExpr  t1, FPExpr  t2  )

inline

Floating-point multiplication.

Parameters

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

Definition at line 4876 of file Context.cs.

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

MkFPNaN()

FPNum MkFPNaN ( FPSort  s )

inline

Create a NaN of sort s.

Parameters

s	FloatingPoint sort.

Definition at line 4694 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
        }

MkFPNeg()

FPExpr MkFPNeg ( FPExpr  t )

inline

Floating-point negation.

Parameters

t	floating-point term

Definition at line 4843 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
        }

MkFPNumeral() [1/5]

FPNum MkFPNumeral ( bool  sgn, Int64  exp, UInt64  sig, FPSort  s  )

inline

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

Parameters

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

Definition at line 4768 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
        }

MkFPNumeral() [2/5]

FPNum MkFPNumeral ( bool  sgn, uint  sig, int  exp, FPSort  s  )

inline

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

Parameters

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

Definition at line 4756 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject));
        }

MkFPNumeral() [3/5]

FPNum MkFPNumeral ( double  v, FPSort  s  )

inline

Create a numeral of FloatingPoint sort from a float.

Parameters

v	numeral value.
s	FloatingPoint sort.

Definition at line 4734 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
        }

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.

Definition at line 4724 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
        }

Referenced by Context.MkFP(), Context.MkFP(), Context.MkFP(), Context.MkFP(), and Context.MkFP().

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.

Definition at line 4744 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
        }

MkFPRem()

FPExpr MkFPRem ( FPExpr  t1, FPExpr  t2  )

inline

Floating-point remainder.

Parameters

t1	floating-point term
t2	floating-point term

Definition at line 4922 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
        }

MkFPRNA()

FPRMNum MkFPRNA ( )

inline

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

Definition at line 4558 of file Context.cs.

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

MkFPRNE()

FPRMNum MkFPRNE ( )

inline

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

Definition at line 4542 of file Context.cs.

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

MkFPRoundingModeSort()

FPRMSort MkFPRoundingModeSort ( )

inline

Create the floating-point RoundingMode sort.

Definition at line 4524 of file Context.cs.

        {
            return new FPRMSort(this);
        }

MkFPRoundNearestTiesToAway()

FPRMNum MkFPRoundNearestTiesToAway ( )

inline

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

Definition at line 4550 of file Context.cs.

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

MkFPRoundNearestTiesToEven()

FPRMExpr MkFPRoundNearestTiesToEven ( )

inline

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

Definition at line 4534 of file Context.cs.

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

MkFPRoundToIntegral()

FPExpr MkFPRoundToIntegral ( FPRMExpr  rm, FPExpr  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

Definition at line 4933 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
        }

MkFPRoundTowardNegative()

FPRMNum MkFPRoundTowardNegative ( )

inline

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

Definition at line 4582 of file Context.cs.

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

MkFPRoundTowardPositive()

FPRMNum MkFPRoundTowardPositive ( )

inline

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

Definition at line 4566 of file Context.cs.

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

MkFPRoundTowardZero()

FPRMNum MkFPRoundTowardZero ( )

inline

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

Definition at line 4598 of file Context.cs.

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

MkFPRTN()

FPRMNum MkFPRTN ( )

inline

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

Definition at line 4590 of file Context.cs.

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

MkFPRTP()

FPRMNum MkFPRTP ( )

inline

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

Definition at line 4574 of file Context.cs.

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

MkFPRTZ()

FPRMNum MkFPRTZ ( )

inline

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

Definition at line 4606 of file Context.cs.

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

MkFPSort()

FPSort MkFPSort ( uint  ebits, uint  sbits  )

inline

Create a FloatingPoint sort.

Parameters

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

Definition at line 4619 of file Context.cs.

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

MkFPSort128()

FPSort MkFPSort128 ( )

inline

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

Definition at line 4683 of file Context.cs.

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

MkFPSort16()

FPSort MkFPSort16 ( )

inline

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

Definition at line 4635 of file Context.cs.

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

MkFPSort32()

FPSort MkFPSort32 ( )

inline

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

Definition at line 4651 of file Context.cs.

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

MkFPSort64()

FPSort MkFPSort64 ( )

inline

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

Definition at line 4667 of file Context.cs.

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

MkFPSortDouble()

FPSort MkFPSortDouble ( )

inline

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

Definition at line 4659 of file Context.cs.

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

MkFPSortHalf()

FPSort MkFPSortHalf ( )

inline

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

Definition at line 4627 of file Context.cs.

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

MkFPSortQuadruple()

FPSort MkFPSortQuadruple ( )

inline

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

Definition at line 4675 of file Context.cs.

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

MkFPSortSingle()

FPSort MkFPSortSingle ( )

inline

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

Definition at line 4643 of file Context.cs.

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

MkFPSqrt()

FPExpr MkFPSqrt ( FPRMExpr  rm, FPExpr  t  )

inline

Floating-point square root.

Parameters

rm	rounding mode term
t	floating-point term

Definition at line 4912 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
        }

MkFPSub()

FPExpr MkFPSub ( FPRMExpr  rm, FPExpr  t1, FPExpr  t2  )

inline

Floating-point subtraction.

Parameters

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

Definition at line 4865 of file Context.cs.

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

MkFPToBV()

BitVecExpr MkFPToBV ( FPRMExpr  rm, FPExpr  t, uint  sz, bool  sign  )

inline

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

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 sign==true). If necessary, the result will be rounded according to rounding mode rm.

Parameters

rm	RoundingMode term.
t	FloatingPoint term
sz	Size of the resulting bit-vector.
sign	Indicates whether the result is a signed or unsigned bit-vector.

Definition at line 5192 of file Context.cs.

        {
            if (sign)
                return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
            else
                return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
        }

MkFPToFP() [1/6]

FPExpr MkFPToFP ( BitVecExpr  bv, FPSort  s  )

inline

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

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.

Parameters

bv	bit-vector value (of size m).
s	FloatingPoint sort (ebits+sbits == m)

Definition at line 5105 of file Context.cs.

        {
            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
        }

MkFPToFP() [2/6]

FPExpr MkFPToFP ( FPRMExpr  rm, BitVecExpr  t, FPSort  s, bool signed    )

inline

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

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.

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.

Definition at line 5155 of file Context.cs.

        {
            if (signed)
                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
            else
                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
        }

MkFPToFP() [3/6]

FPExpr MkFPToFP ( FPRMExpr  rm, FPExpr  t, FPSort  s  )

inline

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

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.

Parameters

rm	RoundingMode term.
t	FloatingPoint term.
s	FloatingPoint sort.

Definition at line 5121 of file Context.cs.

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

MkFPToFP() [4/6]

BitVecExpr MkFPToFP ( FPRMExpr  rm, IntExpr  exp, RealExpr  sig, FPSort  s  )

inline

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

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.

Parameters

rm	RoundingMode term.
exp	Exponent term of Int sort.
sig	Significand term of Real sort.
s	FloatingPoint sort.

Definition at line 5243 of file Context.cs.

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

MkFPToFP() [5/6]

FPExpr MkFPToFP ( FPRMExpr  rm, RealExpr  t, FPSort  s  )

inline

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

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.

Parameters

rm	RoundingMode term.
t	term of Real sort.
s	FloatingPoint sort.

Definition at line 5137 of file Context.cs.

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

MkFPToFP() [6/6]

FPExpr MkFPToFP ( FPSort  s, FPRMExpr  rm, FPExpr  t  )

inline

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

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.

Parameters

s	FloatingPoint sort
rm	floating-point rounding mode term
t	floating-point term

Definition at line 5173 of file Context.cs.

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

MkFPToIEEEBV()

BitVecExpr MkFPToIEEEBV ( FPExpr  t )

inline

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

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.

Parameters

t	FloatingPoint term.

Definition at line 5226 of file Context.cs.

        {
            return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
        }

MkFPToReal()

RealExpr MkFPToReal ( FPExpr  t )

inline

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

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.

Parameters

t	FloatingPoint term

Definition at line 5209 of file Context.cs.

        {
            return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
        }

MkFPZero()

FPNum MkFPZero ( FPSort  s, bool  negative  )

inline

Create a floating-point zero of sort s.

Parameters

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

Definition at line 4714 of file Context.cs.

        {
            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0)));
        }

MkFreshConst()

Expr MkFreshConst ( string  prefix, Sort  range  )

inline

Creates a fresh Constant of sort range and a name prefixed with prefix .

Definition at line 868 of file Context.cs.

        {
            Debug.Assert(range != null);
 
            CheckContextMatch(range);
            return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
        }

MkFreshConstDecl()

FuncDecl MkFreshConstDecl ( string  prefix, Sort  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 790 of file Context.cs.

        {
            Debug.Assert(range != null);
 
            CheckContextMatch(range);
            return new FuncDecl(this, prefix, null, range);
        }

MkFreshFuncDecl()

FuncDecl MkFreshFuncDecl ( string  prefix, Sort[]  domain, Sort  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 750 of file Context.cs.

        {
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            return new FuncDecl(this, prefix, domain, range);
        }

MkFullRe()

ReExpr MkFullRe ( Sort  s )

inline

Create the full regular expression. The sort s should be a regular expression.

Definition at line 3118 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
        }

MkFullSet()

ArrayExpr MkFullSet ( Sort  domain )

inline

Create the full set.

Definition at line 2441 of file Context.cs.

        {
            Debug.Assert(domain != null);
 
            CheckContextMatch(domain);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
        }

MkFuncDecl() [1/4]

FuncDecl MkFuncDecl ( string  name, Sort  domain, Sort  range  )

inline

Creates a new function declaration.

Definition at line 733 of file Context.cs.

        {
            Debug.Assert(range != null);
            Debug.Assert(domain != null);
 
            CheckContextMatch(domain);
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            Sort[] q = new Sort[] { domain };
            return new FuncDecl(this, symbol, q, range);
        }

MkFuncDecl() [2/4]

FuncDecl MkFuncDecl ( string  name, Sort[]  domain, Sort  range  )

inline

Creates a new function declaration.

Definition at line 690 of file Context.cs.

        {
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            return new FuncDecl(this, symbol, domain, range);
        }

MkFuncDecl() [3/4]

FuncDecl MkFuncDecl ( Symbol  name, Sort  domain, Sort  range  )

inline

Creates a new function declaration.

Definition at line 674 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(domain != null);
            Debug.Assert(range != null);
 
            CheckContextMatch(name);
            CheckContextMatch(domain);
            CheckContextMatch(range);
            Sort[] q = new Sort[] { domain };
            return new FuncDecl(this, name, q, range);
        }

MkFuncDecl() [4/4]

FuncDecl MkFuncDecl ( Symbol  name, Sort[]  domain, Sort  range  )

inline

Creates a new function declaration.

Definition at line 659 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch(name);
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            return new FuncDecl(this, name, domain, range);
        }

MkGe()

BoolExpr MkGe ( ArithExpr  t1, ArithExpr  t2  )

inline

Create an expression representing t1 >= t2

Definition at line 1371 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by ArithExpr.operator>=().

MkGoal()

Goal MkGoal ( bool  models = true, bool  unsatCores = false, bool  proofs = false  )

inline

Creates a new Goal.

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 3826 of file Context.cs.

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

MkGt()

BoolExpr MkGt ( ArithExpr  t1, ArithExpr  t2  )

inline

Create an expression representing t1 > t2

Definition at line 1358 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by ArithExpr.operator>().

MkIff()

BoolExpr MkIff ( BoolExpr  t1, BoolExpr  t2  )

inline

Create an expression representing t1 iff t2.

Definition at line 1111 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkImagPart()

RealExpr MkImagPart ( ArithExpr  value )

inline

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

Definition at line 972 of file Context.cs.

        {
            CheckContextMatch(value);
            return new RealExpr(this, Native.Z3_mk_imag_part(nCtx, value.NativeObject));
        }

MkImplies()

BoolExpr MkImplies ( BoolExpr  t1, BoolExpr  t2  )

inline

Create an expression representing t1 -> t2.

Definition at line 1124 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkIndexOf()

IntExpr MkIndexOf ( SeqExpr  s, SeqExpr  substr, ArithExpr  offset  )

inline

Extract index of sub-string starting at offset.

Definition at line 2921 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(offset != null);
            Debug.Assert(substr != null);
            CheckContextMatch(s, substr, offset);
            return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
        }

MkInRe()

BoolExpr MkInRe ( SeqExpr  s, ReExpr  re  )

inline

Check for regular expression membership.

Definition at line 3004 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(re != null);
            CheckContextMatch(s, re);
            return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
        }

MkInt() [1/5]

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 3418 of file Context.cs.

        {
 
            return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
        }

MkInt() [2/5]

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 3440 of file Context.cs.

        {
 
            return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
        }

MkInt() [3/5]

IntNum MkInt ( string  v )

inline

Create an integer numeral.

Parameters

v	A string representing the Term value in decimal notation.

Definition at line 3407 of file Context.cs.

        {
 
            return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
        }

MkInt() [4/5]

IntNum MkInt ( uint  v )

inline

Create an integer numeral.

Parameters

v	value of the numeral.

Returns

A Term with value v and sort Integer

Definition at line 3429 of file Context.cs.

        {
 
            return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
        }

MkInt() [5/5]

IntNum MkInt ( ulong  v )

inline

Create an integer numeral.

Parameters

v	value of the numeral.

Returns

A Term with value v and sort Integer

Definition at line 3451 of file Context.cs.

        {
 
            return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
        }

MkInt2BV()

BitVecExpr MkInt2BV ( uint  n, IntExpr  t  )

inline

Create an n bit bit-vector from the integer argument t .

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 2052 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
        }

MkInt2Real()

RealExpr MkInt2Real ( IntExpr  t )

inline

Coerce an integer to a real.

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

Definition at line 1391 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
        }

MkIntConst() [1/2]

IntExpr MkIntConst ( string  name )

inline

Creates an integer constant.

Definition at line 919 of file Context.cs.

        {
            Debug.Assert(name != null);
 
            return (IntExpr)MkConst(name, IntSort);
        }

MkIntConst() [2/2]

IntExpr MkIntConst ( Symbol  name )

inline

Creates an integer constant.

Definition at line 909 of file Context.cs.

        {
            Debug.Assert(name != null);
 
            return (IntExpr)MkConst(name, IntSort);
        }

MkIntersect()

ReExpr MkIntersect ( params ReExpr[]  t )

inline

Create the intersection of regular languages.

Definition at line 3084 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<ReExpr>(t);
            return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }

MkIntSort()

IntSort MkIntSort ( )

inline

Create a new integer sort.

Definition at line 244 of file Context.cs.

        {
 
            return new IntSort(this);
        }

MkIsDigit()

BoolExpr MkIsDigit ( Expr  ch )

inline

Create a check if the character is a digit.

Definition at line 3176 of file Context.cs.

        {
            Debug.Assert(ch != null);
            return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject));
        }

MkIsInteger()

BoolExpr MkIsInteger ( RealExpr  t )

inline

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

Definition at line 1417 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
        }

MkITE()

Expr MkITE ( BoolExpr  t1, Expr  t2, Expr  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 1096 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            Debug.Assert(t3 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch(t3);
            return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
        }

MkLambda() [1/2]

Lambda MkLambda ( Expr[]  boundConstants, Expr  body  )

inline

Create a lambda expression.

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

See also

MkLambda(Sort[], Symbol[], Expr)

Definition at line 3708 of file Context.cs.

        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
            return new Lambda(this, boundConstants, body);
        }

MkLambda() [2/2]

Lambda MkLambda ( Sort[]  sorts, Symbol[]  names, Expr  body  )

inline

Create a lambda expression.

Creates 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 3689 of file Context.cs.

        {
            Debug.Assert(sorts != null);
            Debug.Assert(names != null);
            Debug.Assert(body != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            return new Lambda(this, sorts, names, body);
        }

MkLe()

BoolExpr MkLe ( ArithExpr  t1, ArithExpr  t2  )

inline

Create an expression representing t1 <= t2

Definition at line 1345 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by ArithExpr.operator<=().

MkLength()

IntExpr MkLength ( SeqExpr  s )

inline

Retrieve the length of a given sequence.

Definition at line 2812 of file Context.cs.

        {
            Debug.Assert(s != null);
            return (IntExpr)Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
        }

MkListSort() [1/2]

ListSort MkListSort ( string  name, Sort  elemSort  )

inline

Create a new list sort.

Definition at line 383 of file Context.cs.

        {
            Debug.Assert(elemSort != null);
 
            CheckContextMatch(elemSort);
            using var symbol = MkSymbol(name);
            return new ListSort(this, symbol, elemSort);
        }

MkListSort() [2/2]

ListSort MkListSort ( Symbol  name, Sort  elemSort  )

inline

Create a new list sort.

Definition at line 370 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(elemSort != null);
 
            CheckContextMatch(name);
            CheckContextMatch(elemSort);
            return new ListSort(this, name, elemSort);
        }

MkLoop()

ReExpr MkLoop ( ReExpr  re, uint  lo, uint  hi = 0  )

inline

Take the bounded Kleene star of a regular expression.

Definition at line 3024 of file Context.cs.

        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
        }

MkLt()

BoolExpr MkLt ( ArithExpr  t1, ArithExpr  t2  )

inline

Create an expression representing t1 < t2

Definition at line 1332 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by ArithExpr.operator<().

MkMap()

ArrayExpr MkMap ( FuncDecl  f, params ArrayExpr[]  args  )

inline

Maps f on the argument arrays.

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, Sort), MkSelect(ArrayExpr, Expr), MkStore(ArrayExpr, Expr, Expr)

Definition at line 2375 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(args == null || args.All(a => a != null));
 
            CheckContextMatch(f);
            CheckContextMatch<ArrayExpr>(args);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
        }

MkMod()

IntExpr MkMod ( IntExpr  t1, IntExpr  t2  )

inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 1292 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkMul() [1/2]

ArithExpr MkMul ( IEnumerable< ArithExpr >  ts )

inline

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

Definition at line 1246 of file Context.cs.

        {
            Debug.Assert(ts != null);
            return MkMul(ts.ToArray());
        }

MkMul() [2/2]

ArithExpr MkMul ( params ArithExpr[]  ts )

inline

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

Definition at line 1234 of file Context.cs.

        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<ArithExpr>(ts);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }

Referenced by Context.MkMul(), and ArithExpr.operator*().

MkNot()

BoolExpr MkNot ( BoolExpr  a )

inline

Mk an expression representing not(a).

Definition at line 1083 of file Context.cs.

        {
            Debug.Assert(a != null);
            CheckContextMatch(a);
            return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
        }

Referenced by BoolExpr.operator!().

MkNth()

Expr MkNth ( SeqExpr  s, Expr  index  )

inline

Retrieve element at index.

Definition at line 2898 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(index != null);
            CheckContextMatch(s, index);
            return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
        }

MkNumeral() [1/5]

Expr MkNumeral ( int  v, Sort  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 3276 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
        }

MkNumeral() [2/5]

Expr MkNumeral ( long  v, Sort  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 3306 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
        }

MkNumeral() [3/5]

Expr MkNumeral ( string  v, Sort  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 3261 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
        }

Referenced by Context.MkBV(), Context.MkBV(), Context.MkBV(), Context.MkBV(), and Context.MkBV().

MkNumeral() [4/5]

Expr MkNumeral ( uint  v, Sort  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 3291 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
        }

MkNumeral() [5/5]

Expr MkNumeral ( ulong  v, Sort  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 3321 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
        }

MkOptimize()

Optimize MkOptimize ( )

inline

Create an Optimization context.

Definition at line 4510 of file Context.cs.

        {
 
            return new Optimize(this);
        }

MkOption()

ReExpr MkOption ( ReExpr  re )

inline

Create the optional regular expression.

Definition at line 3042 of file Context.cs.

        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
        }

MkOr() [1/2]

BoolExpr MkOr ( IEnumerable< BoolExpr >  ts )

inline

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

Definition at line 1201 of file Context.cs.

        {
            Debug.Assert(ts != null);
            return MkOr(ts.ToArray());
        }

MkOr() [2/2]

BoolExpr MkOr ( params BoolExpr[]  ts )

inline

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

Definition at line 1188 of file Context.cs.

        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<BoolExpr>(ts);
            return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }

Referenced by Context.MkOr(), and BoolExpr.operator|().

MkParams()

Params MkParams ( )

inline

Creates a new ParameterSet.

Definition at line 3837 of file Context.cs.

        {
 
            return new Params(this);
        }

Referenced by Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), Solver.Set(), Optimize.Set(), and Solver.Set().

MkPartialOrder()

FuncDecl MkPartialOrder ( Sort  a, uint  index  )

inline

Create a partial order relation over a sort.

Parameters

a	The sort of the relation.
index	The index of the relation.

Definition at line 5287 of file Context.cs.

        {
            return new FuncDecl(this, Native.Z3_mk_partial_order(this.nCtx, a.NativeObject, index));
        }

MkPattern()

Pattern MkPattern ( params Expr[]  terms )

inline

Create a quantifier pattern.

Definition at line 827 of file Context.cs.

        {
            Debug.Assert(terms != null);
            if (terms.Length == 0)
                throw new Z3Exception("Cannot create a pattern from zero terms");
 
            IntPtr[] termsNative = AST.ArrayToNative(terms);
            return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
        }

MkPBEq()

BoolExpr MkPBEq ( int[]  coeffs, BoolExpr[]  args, int  k  )

inline

Create a pseudo-Boolean equal constraint.

Definition at line 3240 of file Context.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(coeffs != null);
            Debug.Assert(args.Length == coeffs.Length);
            CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
        }

MkPBGe()

BoolExpr MkPBGe ( int[]  coeffs, BoolExpr[]  args, int  k  )

inline

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

Definition at line 3227 of file Context.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(coeffs != null);
            Debug.Assert(args.Length == coeffs.Length);
            CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
        }

MkPBLe()

BoolExpr MkPBLe ( int[]  coeffs, BoolExpr[]  args, int  k  )

inline

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

Definition at line 3213 of file Context.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(coeffs != null);
            Debug.Assert(args.Length == coeffs.Length);
            CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
        }

MkPlus()

ReExpr MkPlus ( ReExpr  re )

inline

Take the Kleene plus of a regular expression.

Definition at line 3033 of file Context.cs.

        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
        }

MkPolymorphicDatatypeSort() [1/2]

DatatypeSort MkPolymorphicDatatypeSort ( string  name, Sort[]  typeParams, Constructor[]  constructors  )

inline

Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts created with MkTypeVariable(string).

Parameters

name	name of the datatype sort
typeParams	array of type variable sorts
constructors	array of constructors

Definition at line 633 of file Context.cs.

        {
            using var symbol = MkSymbol(name);
            return MkPolymorphicDatatypeSort(symbol, typeParams, constructors);
        }

MkPolymorphicDatatypeSort() [2/2]

DatatypeSort MkPolymorphicDatatypeSort ( Symbol  name, Sort[]  typeParams, Constructor[]  constructors  )

inline

Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts created with MkTypeVariable(string).

Parameters

name	name of the datatype sort
typeParams	array of type variable sorts
constructors	array of constructors

Definition at line 610 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(typeParams != null);
            Debug.Assert(constructors != null);
            Debug.Assert(constructors.All(c => c != null));
 
            CheckContextMatch(name);
            CheckContextMatch<Sort>(typeParams);
            CheckContextMatch<Constructor>(constructors);
            return new DatatypeSort(this,
                Native.Z3_mk_polymorphic_datatype(nCtx, name.NativeObject,
                    (uint)typeParams.Length, AST.ArrayToNative(typeParams),
                    (uint)constructors.Length, Z3Object.ArrayToNative(constructors)));
        }

Referenced by Context.MkPolymorphicDatatypeSort().

MkPower()

ArithExpr MkPower ( ArithExpr  t1, ArithExpr  t2  )

inline

Create an expression representing t1 ^ t2.

Definition at line 1319 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkPrefixOf()

BoolExpr MkPrefixOf ( SeqExpr  s1, SeqExpr  s2  )

inline

Check for sequence prefix.

Definition at line 2832 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkProbe()

Probe MkProbe ( string  name )

inline

Creates a new Probe.

Definition at line 4305 of file Context.cs.

        {
 
            return new Probe(this, name);
        }

MkQuantifier() [1/2]

Quantifier MkQuantifier ( bool  universal, Expr[]  boundConstants, Expr  body, uint  weight = 1, Pattern[]  patterns = null, Expr[]  noPatterns = null, Symbol  quantifierID = null, Symbol  skolemID = null  )

inline

Create a Quantifier.

MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)

Definition at line 3657 of file Context.cs.

        {
            Debug.Assert(body != null);
            Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            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 ( bool  universal, Sort[]  sorts, Symbol[]  names, Expr  body, uint  weight = 1, Pattern[]  patterns = null, Expr[]  noPatterns = null, Symbol  quantifierID = null, Symbol  skolemID = null  )

inline

Create a Quantifier.

MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)

Definition at line 3634 of file Context.cs.

        {
            Debug.Assert(body != null);
            Debug.Assert(names != null);
            Debug.Assert(sorts != null);
            Debug.Assert(sorts.Length == names.Length);
            Debug.Assert(sorts.All(s => s != null));
            Debug.Assert(names.All(n => n != null));
            Debug.Assert(patterns == null || patterns.All(p => p != null));
            Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
 
 
            if (universal)
                return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
            else
                return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }

MkRange()

ReExpr MkRange ( SeqExpr  lo, SeqExpr  hi  )

inline

Create a range expression.

Definition at line 3128 of file Context.cs.

        {
            Debug.Assert(lo != null);
            Debug.Assert(hi != null);
            CheckContextMatch(lo, hi);
            return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
        }

MkReal() [1/6]

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, Sort)

Definition at line 3338 of file Context.cs.

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

MkReal() [2/6]

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 3362 of file Context.cs.

        {
 
            return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
        }

MkReal() [3/6]

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 3384 of file Context.cs.

        {
 
            return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
        }

MkReal() [4/6]

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 3351 of file Context.cs.

        {
 
            return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
        }

MkReal() [5/6]

RatNum MkReal ( uint  v )

inline

Create a real numeral.

Parameters

v	value of the numeral.

Returns

A Term with value v and sort Real

Definition at line 3373 of file Context.cs.

        {
 
            return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
        }

MkReal() [6/6]

RatNum MkReal ( ulong  v )

inline

Create a real numeral.

Parameters

v	value of the numeral.

Returns

A Term with value v and sort Real

Definition at line 3395 of file Context.cs.

        {
 
            return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
        }

MkReal2Int()

IntExpr MkReal2Int ( RealExpr  t )

inline

Coerce a real to an integer.

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 1406 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
        }

MkRealConst() [1/2]

RealExpr MkRealConst ( string  name )

inline

Creates a real constant.

Definition at line 939 of file Context.cs.

        {
 
            return (RealExpr)MkConst(name, RealSort);
        }

MkRealConst() [2/2]

RealExpr MkRealConst ( Symbol  name )

inline

Creates a real constant.

Definition at line 929 of file Context.cs.

        {
            Debug.Assert(name != null);
 
            return (RealExpr)MkConst(name, RealSort);
        }

MkRealPart()

RealExpr MkRealPart ( ArithExpr  value )

inline

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

Definition at line 965 of file Context.cs.

        {
            CheckContextMatch(value);
            return new RealExpr(this, Native.Z3_mk_real_part(nCtx, value.NativeObject));
        }

MkRealSort()

RealSort MkRealSort ( )

inline

Create a real sort.

Definition at line 253 of file Context.cs.

        {
            return new RealSort(this);
        }

MkRecFuncDecl()

FuncDecl MkRecFuncDecl ( string  name, Sort[]  domain, Sort  range  )

inline

Creates a new recursive function declaration.

Definition at line 704 of file Context.cs.

        {
            Debug.Assert(range != null);
            Debug.Assert(domain.All(d => d != null));
 
            CheckContextMatch<Sort>(domain);
            CheckContextMatch(range);
            using var symbol = MkSymbol(name);
            return new FuncDecl(this, symbol, domain, range, true);
        }

MkRem()

IntExpr MkRem ( IntExpr  t1, IntExpr  t2  )

inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 1306 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
        }

MkRepeat()

BitVecExpr MkRepeat ( uint  i, BitVecExpr  t  )

inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1902 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
        }

MkReplace()

SeqExpr MkReplace ( SeqExpr  s, SeqExpr  src, SeqExpr  dst  )

inline

Replace the first occurrence of src by dst in s.

Definition at line 2933 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(src != null);
            Debug.Assert(dst != null);
            CheckContextMatch(s, src, dst);
            return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
        }

MkReSort()

ReSort MkReSort ( SeqSort  s )

inline

Create a new regular expression sort.

Definition at line 284 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
        }

MkSelect() [1/2]

Expr MkSelect ( ArrayExpr  a, Expr  i  )

inline

Array read.

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, Sort), MkStore(ArrayExpr, Expr, Expr)

Definition at line 2251 of file Context.cs.

        {
            Debug.Assert(a != null);
            Debug.Assert(i != null);
 
            CheckContextMatch(a);
            CheckContextMatch(i);
            return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
        }

MkSelect() [2/2]

Expr MkSelect ( ArrayExpr  a, params Expr[]  args  )

inline

Array read.

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 [domain1,..,domaink -> range], and args must have the sort domain1,..,domaink. The sort of the result is range.

See also

MkArraySort(Sort, Sort), MkStore(ArrayExpr, Expr, Expr)

Definition at line 2274 of file Context.cs.

        {
            Debug.Assert(a != null);
            Debug.Assert(args != null && args.All(n => n != null));
 
            CheckContextMatch(a);
            CheckContextMatch<Expr>(args);
            return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
        }

MkSeqFoldLeft()

Expr MkSeqFoldLeft ( Expr  f, Expr  a, SeqExpr  s  )

inline

Fold left the function f over the sequence s with initial value a.

Definition at line 2968 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(a != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, a, s);
            return Expr.Create(this, Native.Z3_mk_seq_foldl(nCtx, f.NativeObject, a.NativeObject, s.NativeObject));
        }

MkSeqFoldLeftI()

Expr MkSeqFoldLeftI ( Expr  f, Expr  i, Expr  a, SeqExpr  s  )

inline

Fold left with index the function f over the sequence s with initial value a starting at index i.

Definition at line 2980 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(i != null);
            Debug.Assert(a != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, i, a);
            CheckContextMatch(s, a);
            return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
        }

MkSeqMap()

Expr MkSeqMap ( Expr  f, SeqExpr  s  )

inline

Map function f over the sequence s.

Definition at line 2945 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, s);
            return Expr.Create(this, Native.Z3_mk_seq_map(nCtx, f.NativeObject, s.NativeObject));
        }

MkSeqMapi()

Expr MkSeqMapi ( Expr  f, Expr  i, SeqExpr  s  )

inline

Map function f over the sequence s at index i.

Definition at line 2956 of file Context.cs.

        {
            Debug.Assert(f != null);
            Debug.Assert(i != null);
            Debug.Assert(s != null);
            CheckContextMatch(f, i, s);
            return Expr.Create(this, Native.Z3_mk_seq_mapi(nCtx, f.NativeObject, i.NativeObject, s.NativeObject));
        }

MkSeqPower()

SeqExpr MkSeqPower ( SeqExpr  s, Expr  n  )

inline

Retrieve the sequence s concatenated n times with itself.

Definition at line 2821 of file Context.cs.

        {
            Debug.Assert(s != null);
            Debug.Assert(n != null);
            CheckContextMatch(s, n);
            return new SeqExpr(this, Native.Z3_mk_seq_power(nCtx, s.NativeObject, n.NativeObject));
        }

MkSeqSort()

SeqSort MkSeqSort ( Sort  s )

inline

Create a new sequence sort.

Definition at line 275 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
        }

MkSetAdd()

ArrayExpr MkSetAdd ( ArrayExpr  set, Expr  element  )

inline

Add an element to the set.

Definition at line 2452 of file Context.cs.

        {
            Debug.Assert(set != null);
            Debug.Assert(element != null);
 
            CheckContextMatch(set);
            CheckContextMatch(element);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
        }

MkSetComplement()

ArrayExpr MkSetComplement ( ArrayExpr  arg )

inline

Take the complement of a set.

Definition at line 2516 of file Context.cs.

        {
            Debug.Assert(arg != null);
 
            CheckContextMatch(arg);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
        }

MkSetDel()

ArrayExpr MkSetDel ( ArrayExpr  set, Expr  element  )

inline

Remove an element from a set.

Definition at line 2466 of file Context.cs.

        {
            Debug.Assert(set != null);
            Debug.Assert(element != null);
 
            CheckContextMatch(set);
            CheckContextMatch(element);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
        }

MkSetDifference()

ArrayExpr MkSetDifference ( ArrayExpr  arg1, ArrayExpr  arg2  )

inline

Take the difference between two sets.

Definition at line 2503 of file Context.cs.

        {
            Debug.Assert(arg1 != null);
            Debug.Assert(arg2 != null);
 
            CheckContextMatch(arg1);
            CheckContextMatch(arg2);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
        }

MkSetIntersection()

ArrayExpr MkSetIntersection ( params ArrayExpr[]  args )

inline

Take the intersection of a list of sets.

Definition at line 2491 of file Context.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            CheckContextMatch<ArrayExpr>(args);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }

MkSetMembership()

BoolExpr MkSetMembership ( Expr  elem, ArrayExpr  set  )

inline

Check for set membership.

Definition at line 2527 of file Context.cs.

        {
            Debug.Assert(elem != null);
            Debug.Assert(set != null);
 
            CheckContextMatch(elem);
            CheckContextMatch(set);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
        }

MkSetSort()

SetSort MkSetSort ( Sort  ty )

inline

Create a set type.

Definition at line 2419 of file Context.cs.

        {
            Debug.Assert(ty != null);
 
            CheckContextMatch(ty);
            return new SetSort(this, ty);
        }

MkSetSubset()

BoolExpr MkSetSubset ( ArrayExpr  arg1, ArrayExpr  arg2  )

inline

Check for subsetness of sets.

Definition at line 2540 of file Context.cs.

        {
            Debug.Assert(arg1 != null);
            Debug.Assert(arg2 != null);
 
            CheckContextMatch(arg1);
            CheckContextMatch(arg2);
            return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
        }

MkSetUnion()

ArrayExpr MkSetUnion ( params ArrayExpr[]  args )

inline

Take the union of a list of sets.

Definition at line 2479 of file Context.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            CheckContextMatch<ArrayExpr>(args);
            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }

MkSignExt()

BitVecExpr MkSignExt ( uint  i, BitVecExpr  t  )

inline

Bit-vector sign extension.

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 1871 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
        }

MkSimpleSolver()

Solver MkSimpleSolver ( )

inline

Creates a new (incremental) solver.

Definition at line 4462 of file Context.cs.

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

MkSimplifier()

Simplifier MkSimplifier ( string  name )

inline

Creates a new Tactic.

Definition at line 4201 of file Context.cs.

        {
 
            return new Simplifier(this, name);
        }

MkSolver() [1/4]

Solver MkSolver ( Solver  s, Simplifier  t  )

inline

Creates a solver that uses an incremental simplifier.

Definition at line 4471 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(s != null);
            return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
        }

MkSolver() [2/4]

Solver MkSolver ( string  logic )

inline

Creates a new (incremental) solver.

See also

MkSolver(Symbol)

Definition at line 4453 of file Context.cs.

        {
            using var symbol = MkSymbol(logic);
            return MkSolver(symbol);
        }

MkSolver() [3/4]

Solver MkSolver ( Symbol  logic = null )

inline

Creates a new (incremental) solver.

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 4440 of file Context.cs.

        {
 
            if (logic == null)
                return new Solver(this, Native.Z3_mk_solver(nCtx));
            else
                return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
        }

Referenced by Context.MkSolver().

MkSolver() [4/4]

Solver MkSolver ( Tactic  t )

inline

Creates a solver that is implemented using the given tactic.

The solver supports the commands Push and Pop, but it will always solve each check from scratch.

Definition at line 4485 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
        }

MkStar()

ReExpr MkStar ( ReExpr  re )

inline

Take the Kleene star of a regular expression.

Definition at line 3015 of file Context.cs.

        {
            Debug.Assert(re != null);
            return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
        }

MkStore() [1/2]

ArrayExpr MkStore ( ArrayExpr  a, Expr  i, Expr  v  )

inline

Array update.

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

See also

MkArraySort(Sort, Sort), MkSelect(ArrayExpr, Expr), MkSelect(ArrayExpr, Expr[])

Definition at line 2303 of file Context.cs.

        {
            Debug.Assert(a != null);
            Debug.Assert(i != null);
            Debug.Assert(v != null);
 
            CheckContextMatch(a);
            CheckContextMatch(i);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
        }

MkStore() [2/2]

ArrayExpr MkStore ( ArrayExpr  a, Expr[]  args, Expr  v  )

inline

Array update.

The node a must have an array sort [domain1,..,domaink -> range], args must have sort domain1,..,domaink, 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 args, where it maps to v (and the select of a with respect to args may be a different value).

See also

MkArraySort(Sort, Sort), MkSelect(ArrayExpr, Expr), MkSelect(ArrayExpr, Expr[])

Definition at line 2333 of file Context.cs.

        {
            Debug.Assert(a != null);
            Debug.Assert(args != null);
            Debug.Assert(v != null);
 
            CheckContextMatch<Expr>(args);
            CheckContextMatch(a);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
        }

MkString()

SeqExpr MkString ( string  s )

inline

Create a string constant.

Definition at line 2749 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
        }

MkStringLe()

BoolExpr MkStringLe ( SeqExpr  s1, SeqExpr  s2  )

inline

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

Definition at line 2876 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkStringLt()

BoolExpr MkStringLt ( SeqExpr  s1, SeqExpr  s2  )

inline

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

Definition at line 2865 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkSub()

ArithExpr MkSub ( params ArithExpr[]  ts )

inline

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

Definition at line 1255 of file Context.cs.

        {
            Debug.Assert(ts != null);
            Debug.Assert(ts.All(a => a != null));
 
            CheckContextMatch<ArithExpr>(ts);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
        }

Referenced by ArithExpr.operator-().

MkSuffixOf()

BoolExpr MkSuffixOf ( SeqExpr  s1, SeqExpr  s2  )

inline

Check for sequence suffix.

Definition at line 2843 of file Context.cs.

        {
            Debug.Assert(s1 != null);
            Debug.Assert(s2 != null);
            CheckContextMatch(s1, s2);
            return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
        }

MkSymbol() [1/2]

IntSymbol MkSymbol ( int  i )

inline

Creates a new symbol using an integer.

Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

Definition at line 111 of file Context.cs.

        {
            return new IntSymbol(this, i);
        }

Referenced by Params.Add(), Params.Add(), Params.Add(), Params.Add(), Params.Add(), Params.Add(), Optimize.AssertSoft(), Context.MkArrayConst(), Context.MkBoolConst(), Context.MkConst(), Context.MkConstDecl(), Context.MkConstructor(), Context.MkDatatypeSort(), Context.MkDatatypeSortRef(), Context.MkEnumSort(), Context.MkFiniteDomainSort(), Context.MkFuncDecl(), Context.MkFuncDecl(), Context.MkListSort(), Context.MkPolymorphicDatatypeSort(), Context.MkRecFuncDecl(), Context.MkSolver(), Context.MkTypeVariable(), Context.MkUninterpretedSort(), and Context.MkUserPropagatorFuncDecl().

MkSymbol() [2/2]

StringSymbol MkSymbol ( string  name )

inline

Create a symbol using a string.

Definition at line 119 of file Context.cs.

        {
            return new StringSymbol(this, name);
        }

MkTactic()

Tactic MkTactic ( string  name )

inline

Creates a new Tactic.

Definition at line 3881 of file Context.cs.

        {
 
            return new Tactic(this, name);
        }

Referenced by Goal.Simplify().

MkTermArray()

Expr MkTermArray ( ArrayExpr  array )

inline

Access the array default value.

Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Definition at line 2392 of file Context.cs.

        {
            Debug.Assert(array != null);
 
            CheckContextMatch(array);
            return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
        }

MkToRe()

ReExpr MkToRe ( SeqExpr  s )

inline

Convert a regular expression that accepts sequence s.

Definition at line 2994 of file Context.cs.

        {
            Debug.Assert(s != null);
            return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
        }

MkTransitiveClosure()

FuncDecl MkTransitiveClosure ( FuncDecl  f )

inline

Create the transitive closure of a binary relation.

The resulting relation is recursive.

Parameters

f	A binary relation represented as a function declaration.

Definition at line 5297 of file Context.cs.

        {
            return new FuncDecl(this, Native.Z3_mk_transitive_closure(this.nCtx, f.NativeObject));
        }

MkTrue()

BoolExpr MkTrue ( )

inline

The true Term.

Definition at line 1025 of file Context.cs.

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

Referenced by Goal.AsBoolExpr(), Context.MkBool(), and Solver.ToSmt2().

MkTupleSort()

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

inline

Create a new tuple sort.

Definition at line 319 of file Context.cs.

        {
            Debug.Assert(name != null);
            Debug.Assert(fieldNames != null);
            Debug.Assert(fieldNames.All(fn => fn != null));
            Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null));
 
            CheckContextMatch(name);
            CheckContextMatch<Symbol>(fieldNames);
            CheckContextMatch<Sort>(fieldSorts);
            return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
        }

MkTypeVariable() [1/2]

Sort MkTypeVariable ( string  name )

inline

Create a type variable sort for use as a parameter in polymorphic datatypes.

Parameters

name	name of the type variable

Definition at line 597 of file Context.cs.

        {
            using var symbol = MkSymbol(name);
            return MkTypeVariable(symbol);
        }

MkTypeVariable() [2/2]

Sort MkTypeVariable ( Symbol  name )

inline

Create a type variable sort for use as a parameter in polymorphic datatypes.

Parameters

name	name of the type variable

Definition at line 586 of file Context.cs.

        {
            Debug.Assert(name != null);
            CheckContextMatch(name);
            return new Sort(this, Native.Z3_mk_type_variable(nCtx, name.NativeObject));
        }

Referenced by Context.MkTypeVariable().

MkUnaryMinus()

ArithExpr MkUnaryMinus ( ArithExpr  t )

inline

Create an expression representing -t.

Definition at line 1267 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
        }

Referenced by ArithExpr.operator-().

MkUninterpretedSort() [1/2]

UninterpretedSort MkUninterpretedSort ( string  str )

inline

Create a new uninterpreted sort.

Definition at line 235 of file Context.cs.

        {
            using var sym = MkSymbol(str);
            return MkUninterpretedSort(sym);
        }

MkUninterpretedSort() [2/2]

UninterpretedSort MkUninterpretedSort ( Symbol  s )

inline

Create a new uninterpreted sort.

Definition at line 224 of file Context.cs.

        {
            Debug.Assert(s != null);
 
            CheckContextMatch(s);
            return new UninterpretedSort(this, s);
        }

Referenced by Context.MkUninterpretedSort().

MkUnion()

ReExpr MkUnion ( params ReExpr[]  t )

inline

Create the union of regular languages.

Definition at line 3072 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(t.All(a => a != null));
 
            CheckContextMatch<ReExpr>(t);
            return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }

MkUnit()

SeqExpr MkUnit ( Expr  elem )

inline

Create the singleton sequence.

Definition at line 2740 of file Context.cs.

        {
            Debug.Assert(elem != null);
            return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
        }

MkUpdateField()

Expr MkUpdateField ( FuncDecl  field, Expr  t, Expr  v  )

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 645 of file Context.cs.

        {
            return Expr.Create(this, Native.Z3_datatype_update_field(
                                        nCtx, field.NativeObject,
                                        t.NativeObject, v.NativeObject));
        }

MkUserPropagatorFuncDecl()

FuncDecl MkUserPropagatorFuncDecl ( string  name, Sort[]  domain, Sort  range  )

inline

Declare a function to be processed by the user propagator plugin.

Definition at line 801 of file Context.cs.

        {
             using var _name = MkSymbol(name);
             var fn = Native.Z3_solver_propagate_declare(nCtx, _name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject);
             return new FuncDecl(this, fn);
        }

MkXor() [1/2]

BoolExpr MkXor ( BoolExpr  t1, BoolExpr  t2  )

inline

Create an expression representing t1 xor t2.

Definition at line 1137 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
        }

Referenced by Context.MkXor(), and BoolExpr.operator^().

MkXor() [2/2]

BoolExpr MkXor ( IEnumerable< BoolExpr >  args )

inline

Create an expression representing t1 xor t2 xor t3 ... .

Definition at line 1150 of file Context.cs.

        {
            Debug.Assert(args != null);
            var ts = args.ToArray();
            Debug.Assert(ts.All(a => a != null));
            CheckContextMatch<BoolExpr>(ts);
 
            return ts.Aggregate(MkFalse(), (r, t) =>
                    {
                        using (r)
                            return MkXor(r, t);
                    });
        }

MkZeroExt()

BitVecExpr MkZeroExt ( uint  i, BitVecExpr  t  )

inline

Bit-vector zero extension.

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 1888 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
        }

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 4422 of file Context.cs.

        {
            Debug.Assert(p != null);
 
            CheckContextMatch(p);
            return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
        }

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 4408 of file Context.cs.

        {
            Debug.Assert(p1 != null);
            Debug.Assert(p2 != null);
 
            CheckContextMatch(p1);
            CheckContextMatch(p2);
            return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
        }

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 3938 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
        }

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 4086 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
 
            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
        }

ParOr()

Tactic ParOr ( params 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 4074 of file Context.cs.

        {
            Debug.Assert(t == null || t.All(tactic => tactic != null));
 
            CheckContextMatch<Tactic>(t);
            return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
        }

ParseSMTLIB2File()

BoolExpr[] ParseSMTLIB2File ( string  fileName, Symbol[]  sortNames = null, Sort[]  sorts = null, Symbol[]  declNames = null, FuncDecl[]  decls = null  )

inline

Parse the given file using the SMT-LIB2 parser.

See also

ParseSMTLIB2String

Definition at line 3773 of file Context.cs.

        {
 
            uint csn = Symbol.ArrayLength(sortNames);
            uint cs = Sort.ArrayLength(sorts);
            uint cdn = Symbol.ArrayLength(declNames);
            uint cd = AST.ArrayLength(decls);
            if (csn != cs || cdn != cd)
                throw new Z3Exception("Argument size mismatch");
            using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
                AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
                AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
            return assertions.ToBoolExprArray();
        }

ParseSMTLIB2String()

BoolExpr[] ParseSMTLIB2String ( string  str, Symbol[]  sortNames = null, Sort[]  sorts = null, Symbol[]  declNames = null, FuncDecl[]  decls = null  )

inline

Parse the given string using the SMT-LIB2 parser.

Returns

A conjunction of assertions in the scope (up to push/pop) at the end of the string.

Definition at line 3754 of file Context.cs.

        {
 
            uint csn = Symbol.ArrayLength(sortNames);
            uint cs = Sort.ArrayLength(sorts);
            uint cdn = Symbol.ArrayLength(declNames);
            uint cd = AST.ArrayLength(decls);
            if (csn != cs || cdn != cd)
                throw new Z3Exception("Argument size mismatch");
            using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
                AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
                AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
            return assertions.ToBoolExprArray();
        }

PolynomialSubresultants()

ASTVector PolynomialSubresultants ( Expr  p, Expr  q, Expr  x  )

inline

Return the nonzero subresultants of p and q with respect to the "variable" x.

p, q and x are Z3 expressions where p and q are arithmetic terms. Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable.

Parameters

p	First arithmetic term.
q	Second arithmetic term.
x	The variable with respect to which subresultants are computed.

Definition at line 5312 of file Context.cs.

        {
            CheckContextMatch(p);
            CheckContextMatch(q);
            CheckContextMatch(x);
            return new ASTVector(this, Native.Z3_polynomial_subresultants(this.nCtx, p.NativeObject, q.NativeObject, x.NativeObject));
        }

ProbeDescription()

string ProbeDescription ( string  name )

inline

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

Definition at line 4296 of file Context.cs.

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

QeLite()

Expr QeLite ( ASTVector  vars, Expr  body  )

inline

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

Definition at line 4118 of file Context.cs.

        {
            CheckContextMatch(vars);
            CheckContextMatch(body);
            return Expr.Create(this, Native.Z3_qe_lite(nCtx, vars.NativeObject, body.NativeObject));
        }

QeModelProject()

Expr QeModelProject ( Model  model, Expr[]  bounds, Expr  body  )

inline

Projects the bound applications from body using model .

Definition at line 4128 of file Context.cs.

        {
            CheckContextMatch(model);
            CheckContextMatch<Expr>(bounds);
            CheckContextMatch(body);
            return Expr.Create(this, Native.Z3_qe_model_project(nCtx, model.NativeObject,
                (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject));
        }

QeModelProjectSkolem()

Expr QeModelProjectSkolem ( Model  model, Expr[]  bounds, Expr  body, ASTMap  map  )

inline

Projects bound applications and records Skolem terms in map .

Definition at line 4140 of file Context.cs.

        {
            CheckContextMatch(model);
            CheckContextMatch<Expr>(bounds);
            CheckContextMatch(body);
            CheckContextMatch(map);
            return Expr.Create(this, Native.Z3_qe_model_project_skolem(nCtx, model.NativeObject,
                (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject, map.NativeObject));
        }

QeModelProjectWithWitness()

Expr QeModelProjectWithWitness ( Model  model, Expr[]  bounds, Expr  body, ASTMap  map  )

inline

Projects bound applications and records witnesses in map .

Definition at line 4153 of file Context.cs.

        {
            CheckContextMatch(model);
            CheckContextMatch<Expr>(bounds);
            CheckContextMatch(body);
            CheckContextMatch(map);
            return Expr.Create(this, Native.Z3_qe_model_project_with_witness(nCtx, model.NativeObject,
                (uint)bounds.Length, AST.ArrayToNative(bounds), body.NativeObject, map.NativeObject));
        }

Repeat()

Tactic Repeat ( Tactic  t, uint  max = uint::MaxValue  )

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 3999 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
        }

SbvToString()

SeqExpr SbvToString ( Expr  e )

inline

Convert a bit-vector expression, represented as an signed number, to a string.

Definition at line 2778 of file Context.cs.

        {
            Debug.Assert(e != null);
            Debug.Assert(e is ArithExpr);
            return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
        }

SimplifierDescription()

string SimplifierDescription ( string  name )

inline

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

Definition at line 4192 of file Context.cs.

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

SimplifyHelp()

string SimplifyHelp ( )

inline

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

Definition at line 5323 of file Context.cs.

        {
 
            return Native.Z3_simplify_get_help(nCtx);
        }

Skip()

Tactic Skip ( )

inline

Create a tactic that just returns the given goal.

Definition at line 4010 of file Context.cs.

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

StringToInt()

IntExpr StringToInt ( Expr  e )

inline

Convert an integer expression to a string.

Definition at line 2788 of file Context.cs.

        {
            Debug.Assert(e != null);
            Debug.Assert(e is SeqExpr);
            return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
        }

TacticDescription()

string TacticDescription ( string  name )

inline

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

Definition at line 3872 of file Context.cs.

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

Then() [1/2]

Simplifier Then ( Simplifier  t1, Simplifier  t2, params Simplifier[]  ts  )

inline

Create a simplifier that applies t1 and then then t2 .

Shorthand for AndThen.

Definition at line 4245 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
            return AndThen(t1, t2, ts);
        }

Then() [2/2]

Tactic Then ( Tactic  t1, Tactic  t2, params Tactic[]  ts  )

inline

Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .

Shorthand for AndThen.

Definition at line 3925 of file Context.cs.

        {
            Debug.Assert(t1 != null);
            Debug.Assert(t2 != null);
            //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
            return AndThen(t1, t2, ts);
        }

TryFor()

Tactic TryFor ( Tactic  t, uint  ms  )

inline

Create a tactic that applies t to a goal for ms milliseconds.

If t does not terminate within ms milliseconds, then it fails.

Definition at line 3954 of file Context.cs.

        {
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
        }

UbvToString()

SeqExpr UbvToString ( Expr  e )

inline

Convert a bit-vector expression, represented as an unsigned number, to a string.

Definition at line 2768 of file Context.cs.

        {
            Debug.Assert(e != null);
            Debug.Assert(e is ArithExpr);
            return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
        }

UnwrapAST()

IntPtr UnwrapAST ( AST  a )

inline

Unwraps an AST.

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

).

See also

WrapAST

Parameters

a	The AST to unwrap.

Definition at line 5277 of file Context.cs.

        {
            return a.NativeObject;
        }

UpdateParamValue()

void UpdateParamValue ( string  id, string  value  )

inline

Update a mutable configuration parameter.

The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -p 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 5364 of file Context.cs.

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

UsingParams() [1/2]

Simplifier UsingParams ( Simplifier  t, Params  p  )

inline

Create a tactic that applies t using the given set of parameters p .

Definition at line 4257 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(p != null);
 
            CheckContextMatch(t);
            CheckContextMatch(p);
            return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
        }

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 4049 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(p != null);
 
            CheckContextMatch(t);
            CheckContextMatch(p);
            return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
        }

Referenced by Context.With().

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.

If p evaluates to false, then the new tactic behaves like the skip tactic.

Definition at line 3969 of file Context.cs.

        {
            Debug.Assert(p != null);
            Debug.Assert(t != null);
 
            CheckContextMatch(t);
            CheckContextMatch(p);
            return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
        }

With()

Tactic With ( Tactic  t, Params  p  )

inline

Create a tactic that applies t using the given set of parameters p .

Alias for UsingParams

Definition at line 4063 of file Context.cs.

        {
            Debug.Assert(t != null);
            Debug.Assert(p != null);
 
            return UsingParams(t, p);
        }

WrapAST()

AST WrapAST ( IntPtr  nativeObject )

inline

Wraps an AST.

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

See also

UnwrapAST, Native.Z3_inc_ref

) and that it must have a correct reference count (see e.g., .

See also

UnwrapAST

Parameters

nativeObject

The native pointer to wrap.

Definition at line 5261 of file Context.cs.

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

Property Documentation

BoolSort

BoolSort BoolSort

get

Retrieves the Boolean sort of the context.

Definition at line 147 of file Context.cs.

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

Referenced by Context.MkBoolSort().

CharSort

CharSort CharSort

get

Retrieves the character sort of the context.

Definition at line 191 of file Context.cs.

        {
            get
            {
                if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
            }
        }

ComplexSort

ComplexSort ComplexSort

get

Retrieves the Complex sort of the context.

Definition at line 181 of file Context.cs.

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

Referenced by Context.MkComplexSort().

IntSort

IntSort IntSort

get

Retrieves the Integer sort of the context.

Definition at line 158 of file Context.cs.

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

Referenced by Context.MkIntSort().

NumProbes

uint NumProbes

get

The number of supported Probes.

Definition at line 4272 of file Context.cs.

        {
            get { return Native.Z3_get_num_probes(nCtx); }
        }

NumSimplifiers

uint NumSimplifiers

get

The number of supported simplifiers.

Definition at line 4168 of file Context.cs.

        {
            get { return Native.Z3_get_num_simplifiers(nCtx); }
        }

NumTactics

uint NumTactics

get

The number of supported tactics.

Definition at line 3848 of file Context.cs.

        {
            get { return Native.Z3_get_num_tactics(nCtx); }
        }

PrintMode

Z3_ast_print_mode PrintMode

getset

Selects the format used for pretty-printing expressions.

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 3737 of file Context.cs.

        {
            get { return m_print_mode; }
            set 
            { 
                Native.Z3_set_ast_print_mode(nCtx, (uint)value);
                m_print_mode = value;
            }
        }

ProbeNames

string [] ProbeNames

get

The names of all supported Probes.

Definition at line 4280 of file Context.cs.

        {
            get
            {
 
                uint n = NumProbes;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_get_probe_name(nCtx, i);
                return res;
            }
        }

RealSort

RealSort RealSort

get

Retrieves the Real sort of the context.

Definition at line 170 of file Context.cs.

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

Referenced by Context.MkRealSort().

SimplifierNames

string [] SimplifierNames

get

The names of all supported tactics.

Definition at line 4176 of file Context.cs.

        {
            get
            {
 
                uint n = NumSimplifiers;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_get_simplifier_name(nCtx, i);
                return res;
            }
        }

SimplifyParameterDescriptions

ParamDescrs SimplifyParameterDescriptions

get

Retrieves parameter descriptions for simplifier.

Definition at line 5332 of file Context.cs.

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

StringSort

SeqSort StringSort

get

Retrieves the String sort of the context.

Definition at line 203 of file Context.cs.

        {
            get
            {
                if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
                return m_stringSort;
            }
        }

TacticNames

string [] TacticNames

get

The names of all supported tactics.

Definition at line 3856 of file Context.cs.

        {
            get
            {
 
                uint n = NumTactics;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_get_tactic_name(nCtx, i);
                return res;
            }
        }