Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Properties
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
CharSort CharSort [get]
 Retrieves the String sort of the context.
 
SeqSort StringSort [get]
 Retrieves the String sort of the context.
 
Z3_ast_print_mode PrintMode [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.

40 : base()
41 {
42 lock (creation_lock)
43 {
44 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
45 Native.Z3_enable_concurrent_dec_ref(m_ctx);
46 InitContext();
47 }
48 }

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

69 : base()
70 {
71 Debug.Assert(settings != null);
72
73 lock (creation_lock)
74 {
75 IntPtr cfg = Native.Z3_mk_config();
76 foreach (KeyValuePair<string, string> kv in settings)
77 Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
78 m_ctx = Native.Z3_mk_context_rc(cfg);
79 Native.Z3_enable_concurrent_dec_ref(m_ctx);
80 Native.Z3_del_config(cfg);
81 InitContext();
82 }
83 }

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

648 {
649 CheckContextMatch(f);
650 CheckContextMatch<Expr>(args);
651 CheckContextMatch(body);
652 IntPtr[] argsNative = AST.ArrayToNative(args);
653 Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
654 }

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

3965 {
3966 Debug.Assert(p1 != null);
3967 Debug.Assert(p2 != null);
3968
3969 CheckContextMatch(p1);
3970 CheckContextMatch(p2);
3971 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3972 }

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

3782 {
3783 Debug.Assert(t1 != null);
3784 Debug.Assert(t2 != null);
3785 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3786
3787
3788 CheckContextMatch(t1);
3789 CheckContextMatch(t2);
3790 CheckContextMatch<Simplifier>(ts);
3791
3792 IntPtr last = IntPtr.Zero;
3793 if (ts != null && ts.Length > 0)
3794 {
3795 last = ts[ts.Length - 1].NativeObject;
3796 for (int i = ts.Length - 2; i >= 0; i--)
3797 last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
3798 }
3799 if (last != IntPtr.Zero)
3800 {
3801 last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
3802 return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
3803 }
3804 else
3805 return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3806 }

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

3520 {
3521 Debug.Assert(t1 != null);
3522 Debug.Assert(t2 != null);
3523 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3524
3525
3526 CheckContextMatch(t1);
3527 CheckContextMatch(t2);
3528 CheckContextMatch<Tactic>(ts);
3529
3530 IntPtr last = IntPtr.Zero;
3531 if (ts != null && ts.Length > 0)
3532 {
3533 last = ts[ts.Length - 1].NativeObject;
3534 for (int i = ts.Length - 2; i >= 0; i--)
3535 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3536 }
3537 if (last != IntPtr.Zero)
3538 {
3539 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3540 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3541 }
3542 else
3543 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3544 }

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

◆ CharFromBV()

Expr CharFromBV ( BitVecExpr  bv)
inline

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

Definition at line 2826 of file Context.cs.

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

◆ CharToBV()

BitVecExpr CharToBV ( Expr  ch)
inline

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

Definition at line 2817 of file Context.cs.

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

◆ CharToInt()

IntExpr CharToInt ( Expr  ch)
inline

Create an integer (code point) from character.

Definition at line 2808 of file Context.cs.

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

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

3612 {
3613 Debug.Assert(p != null);
3614 Debug.Assert(t1 != null);
3615 Debug.Assert(t2 != null);
3616
3617 CheckContextMatch(p);
3618 CheckContextMatch(t1);
3619 CheckContextMatch(t2);
3620 return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3621 }

◆ ConstProbe()

Probe ConstProbe ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3884 of file Context.cs.

3885 {
3886
3887 return new Probe(this, Native.Z3_probe_const(nCtx, val));
3888 }

◆ Dispose()

void Dispose ( )
inline

Disposes of the context.

Definition at line 4992 of file Context.cs.

4993 {
4994 // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4995
4996 if (m_boolSort != null) m_boolSort.Dispose();
4997 if (m_intSort != null) m_intSort.Dispose();
4998 if (m_realSort != null) m_realSort.Dispose();
4999 if (m_stringSort != null) m_stringSort.Dispose();
5000 if (m_charSort != null) m_charSort.Dispose();
5001 m_boolSort = null;
5002 m_intSort = null;
5003 m_realSort = null;
5004 m_stringSort = null;
5005 m_charSort = null;
5006 if (m_ctx != IntPtr.Zero)
5007 {
5008 IntPtr ctx = m_ctx;
5009 lock (this)
5010 {
5011 m_n_err_handler = null;
5012 m_ctx = IntPtr.Zero;
5013 }
5014 if (!is_external)
5015 Native.Z3_del_context(ctx);
5016 }
5017
5018 GC.SuppressFinalize(this);
5019 }
Microsoft.Z3.Z3Object.Dispose
void Dispose()
Disposes of the underlying native Z3 object.
Definition Z3Object.cs:45

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

3951 {
3952 Debug.Assert(p1 != null);
3953 Debug.Assert(p2 != null);
3954
3955 CheckContextMatch(p1);
3956 CheckContextMatch(p2);
3957 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3958 }

◆ Fail()

Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3647 of file Context.cs.

3648 {
3649
3650 return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3651 }

◆ FailIf()

Tactic FailIf ( Probe  p)
inline

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

Definition at line 3656 of file Context.cs.

3657 {
3658 Debug.Assert(p != null);
3659
3660 CheckContextMatch(p);
3661 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3662 }

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

3669 {
3670
3671 return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3672 }

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

3937 {
3938 Debug.Assert(p1 != null);
3939 Debug.Assert(p2 != null);
3940
3941 CheckContextMatch(p1);
3942 CheckContextMatch(p2);
3943 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3944 }

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

3909 {
3910 Debug.Assert(p1 != null);
3911 Debug.Assert(p2 != null);
3912
3913 CheckContextMatch(p1);
3914 CheckContextMatch(p2);
3915 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3916 }

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

3729 {
3730 Native.Z3_interrupt(nCtx);
3731 }

◆ IntToString()

SeqExpr IntToString ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 2477 of file Context.cs.

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

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

3923 {
3924 Debug.Assert(p1 != null);
3925 Debug.Assert(p2 != null);
3926
3927 CheckContextMatch(p1);
3928 CheckContextMatch(p2);
3929 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3930 }

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

3895 {
3896 Debug.Assert(p1 != null);
3897 Debug.Assert(p2 != null);
3898
3899 CheckContextMatch(p1);
3900 CheckContextMatch(p2);
3901 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3902 }

◆ MkAdd() [1/2]

ArithExpr MkAdd ( IEnumerable< ArithExpr >  ts)
inline

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

Definition at line 1118 of file Context.cs.

1119 {
1120 Debug.Assert(ts != null);
1121 return MkAdd(ts.ToArray());
1122 }
Microsoft.Z3.Context.MkAdd
ArithExpr MkAdd(params ArithExpr[] ts)
Create an expression representing t[0] + t[1] + ....
Definition Context.cs:1106

◆ MkAdd() [2/2]

ArithExpr MkAdd ( params ArithExpr[]  ts)
inline

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

Definition at line 1106 of file Context.cs.

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

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

1073 {
1074 Debug.Assert(t != null);
1075 return MkAnd(t.ToArray());
1076 }
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(params BoolExpr[] ts)
Create an expression representing t[0] and t[1] and ....
Definition Context.cs:1060

◆ MkAnd() [2/2]

BoolExpr MkAnd ( params BoolExpr[]  ts)
inline

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

Definition at line 1060 of file Context.cs.

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

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

909 {
910 Debug.Assert(f != null);
911 return MkApp(f, args?.ToArray());
912 }
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition Context.cs:896

◆ MkApp() [2/2]

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

Create a new function application.

Definition at line 896 of file Context.cs.

897 {
898 Debug.Assert(f != null);
899 Debug.Assert(args == null || args.All(a => a != null));
900 CheckContextMatch(f);
901 CheckContextMatch<Expr>(args);
902 return Expr.Create(this, f, args);
903 }

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

2121 {
2122 Debug.Assert(domain != null);
2123 Debug.Assert(range != null);
2124
2125 using var symbol = MkSymbol(name);
2126 using var sort = MkArraySort(domain, range);
2127 return (ArrayExpr)MkConst(symbol, sort);
2128 }
Microsoft.Z3.Context.MkConst
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition Context.cs:768
Microsoft.Z3.Context.MkArraySort
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition Context.cs:276
Microsoft.Z3.Context.MkSymbol
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition Context.cs:111

◆ MkArrayConst() [2/2]

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

Create an array constant.

Definition at line 2107 of file Context.cs.

2108 {
2109 Debug.Assert(name != null);
2110 Debug.Assert(domain != null);
2111 Debug.Assert(range != null);
2112
2113 using var sort = MkArraySort(domain, range);
2114 return (ArrayExpr)MkConst(name, sort);
2115 }

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

2297 {
2298 Debug.Assert(arg1 != null);
2299 Debug.Assert(arg2 != null);
2300
2301 CheckContextMatch(arg1);
2302 CheckContextMatch(arg2);
2303 return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2304 }

◆ MkArraySort() [1/2]

ArraySort MkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 276 of file Context.cs.

277 {
278 Debug.Assert(domain != null);
279 Debug.Assert(range != null);
280
281 CheckContextMatch(domain);
282 CheckContextMatch(range);
283 return new ArraySort(this, domain, range);
284 }
z3py.ArraySort
ArraySort(*sig)
Definition z3py.py:4834

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

290 {
291 Debug.Assert(domain != null);
292 Debug.Assert(range != null);
293
294 CheckContextMatch<Sort>(domain);
295 CheckContextMatch(range);
296 return new ArraySort(this, domain, range);
297 }

◆ MkAt()

SeqExpr MkAt ( SeqExpr  s,
Expr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2595 of file Context.cs.

2596 {
2597 Debug.Assert(s != null);
2598 Debug.Assert(index != null);
2599 CheckContextMatch(s, index);
2600 return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2601 }

◆ MkAtLeast()

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

Create an at-least-k constraint.

Definition at line 2860 of file Context.cs.

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

◆ MkAtMost()

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

Create an at-most-k constraint.

Definition at line 2848 of file Context.cs.

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

◆ MkBitVecSort()

BitVecSort MkBitVecSort ( uint  size)
inline

Create a new bit-vector sort.

Definition at line 250 of file Context.cs.

251 {
252 return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
253 }
z3py.BitVecSort
BitVecSort(sz, ctx=None)
Definition z3py.py:4116

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

935 {
936 return value ? MkTrue() : MkFalse();
937 }
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition Context.cs:918
Microsoft.Z3.Context.MkFalse
BoolExpr MkFalse()
The false Term.
Definition Context.cs:926

◆ MkBoolConst() [1/2]

BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 826 of file Context.cs.

827 {
828 using var symbol = MkSymbol(name);
829 return (BoolExpr)MkConst(symbol, BoolSort);
830 }
Microsoft.Z3.Context.BoolSort
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition Context.cs:147

◆ MkBoolConst() [2/2]

BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 816 of file Context.cs.

817 {
818 Debug.Assert(name != null);
819
820 return (BoolExpr)MkConst(name, BoolSort);
821 }

◆ MkBoolSort()

BoolSort MkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 205 of file Context.cs.

206 {
207 return new BoolSort(this);
208 }

◆ MkBound()

Expr MkBound ( uint  index,
Sort  ty 
)
inline

Creates a new bound variable.

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

Definition at line 741 of file Context.cs.

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

◆ MkBV() [1/6]

BitVecNum MkBV ( bool[]  bits)
inline

Create a bit-vector numeral.

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

Definition at line 3177 of file Context.cs.

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

◆ MkBV() [2/6]

BitVecNum MkBV ( int  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3134 of file Context.cs.

3135 {
3136 using var sort = MkBitVecSort(size);
3137 return (BitVecNum)MkNumeral(v, sort);
3138 }
Microsoft.Z3.Context.MkBitVecSort
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition Context.cs:250
Microsoft.Z3.Context.MkNumeral
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition Context.cs:2920

◆ MkBV() [3/6]

BitVecNum MkBV ( long  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3156 of file Context.cs.

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

◆ MkBV() [4/6]

BitVecNum MkBV ( string  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3123 of file Context.cs.

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

◆ MkBV() [5/6]

BitVecNum MkBV ( uint  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3145 of file Context.cs.

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

◆ MkBV() [6/6]

BitVecNum MkBV ( ulong  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3167 of file Context.cs.

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

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

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

◆ MkBVAdd()

BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1456 of file Context.cs.

1457 {
1458 Debug.Assert(t1 != null);
1459 Debug.Assert(t2 != null);
1460
1461 CheckContextMatch(t1);
1462 CheckContextMatch(t2);
1463 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1464 }

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

1983 {
1984 Debug.Assert(t1 != null);
1985 Debug.Assert(t2 != null);
1986
1987 CheckContextMatch(t1);
1988 CheckContextMatch(t2);
1989 return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1990 }

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

1999 {
2000 Debug.Assert(t1 != null);
2001 Debug.Assert(t2 != null);
2002
2003 CheckContextMatch(t1);
2004 CheckContextMatch(t2);
2005 return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2006 }

◆ MkBVAND()

BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1360 of file Context.cs.

1361 {
1362 Debug.Assert(t1 != null);
1363 Debug.Assert(t2 != null);
1364
1365 CheckContextMatch(t1);
1366 CheckContextMatch(t2);
1367 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1368 }

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

1862 {
1863 Debug.Assert(t1 != null);
1864 Debug.Assert(t2 != null);
1865
1866 CheckContextMatch(t1);
1867 CheckContextMatch(t2);
1868 return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1869 }

◆ MkBVConst() [1/2]

BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 885 of file Context.cs.

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

◆ MkBVConst() [2/2]

BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 874 of file Context.cs.

875 {
876 Debug.Assert(name != null);
877
878 using var sort = MkBitVecSort(size);
879 return (BitVecExpr)MkConst(name, sort);
880 }

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

1838 {
1839 Debug.Assert(t1 != null);
1840 Debug.Assert(t2 != null);
1841
1842 CheckContextMatch(t1);
1843 CheckContextMatch(t2);
1844 return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1845 }

◆ MkBVMul()

BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1484 of file Context.cs.

1485 {
1486 Debug.Assert(t1 != null);
1487 Debug.Assert(t2 != null);
1488
1489 CheckContextMatch(t1);
1490 CheckContextMatch(t2);
1491 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1492 }

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

2077 {
2078 Debug.Assert(t1 != null);
2079 Debug.Assert(t2 != null);
2080
2081 CheckContextMatch(t1);
2082 CheckContextMatch(t2);
2083 return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2084 }

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

2093 {
2094 Debug.Assert(t1 != null);
2095 Debug.Assert(t2 != null);
2096
2097 CheckContextMatch(t1);
2098 CheckContextMatch(t2);
2099 return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2100 }

◆ MkBVNAND()

BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1402 of file Context.cs.

1403 {
1404 Debug.Assert(t1 != null);
1405 Debug.Assert(t2 != null);
1406
1407 CheckContextMatch(t1);
1408 CheckContextMatch(t2);
1409 return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1410 }

◆ MkBVNeg()

BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1444 of file Context.cs.

1445 {
1446 Debug.Assert(t != null);
1447
1448 CheckContextMatch(t);
1449 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1450 }

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

2063 {
2064 Debug.Assert(t != null);
2065
2066 CheckContextMatch(t);
2067 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2068 }

◆ MkBVNOR()

BitVecExpr MkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1416 of file Context.cs.

1417 {
1418 Debug.Assert(t1 != null);
1419 Debug.Assert(t2 != null);
1420
1421 CheckContextMatch(t1);
1422 CheckContextMatch(t2);
1423 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1424 }

◆ MkBVNot()

BitVecExpr MkBVNot ( BitVecExpr  t)
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1324 of file Context.cs.

1325 {
1326 Debug.Assert(t != null);
1327
1328 CheckContextMatch(t);
1329 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1330 }

◆ MkBVOR()

BitVecExpr MkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1374 of file Context.cs.

1375 {
1376 Debug.Assert(t1 != null);
1377 Debug.Assert(t2 != null);
1378
1379 CheckContextMatch(t1);
1380 CheckContextMatch(t2);
1381 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1382 }

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

1337 {
1338 Debug.Assert(t != null);
1339
1340 CheckContextMatch(t);
1341 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1342 }

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

1349 {
1350 Debug.Assert(t != null);
1351
1352 CheckContextMatch(t);
1353 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1354 }

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

1909 {
1910 Debug.Assert(t1 != null);
1911 Debug.Assert(t2 != null);
1912
1913 CheckContextMatch(t1);
1914 CheckContextMatch(t2);
1915 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1916 }

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

1879 {
1880 Debug.Assert(t != null);
1881
1882 CheckContextMatch(t);
1883 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1884 }

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

1926 {
1927 Debug.Assert(t1 != null);
1928 Debug.Assert(t2 != null);
1929
1930 CheckContextMatch(t1);
1931 CheckContextMatch(t2);
1932 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1933 }

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

1894 {
1895 Debug.Assert(t != null);
1896
1897 CheckContextMatch(t);
1898 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1899 }

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

1527 {
1528 Debug.Assert(t1 != null);
1529 Debug.Assert(t2 != null);
1530
1531 CheckContextMatch(t1);
1532 CheckContextMatch(t2);
1533 return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1534 }

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

2047 {
2048 Debug.Assert(t1 != null);
2049 Debug.Assert(t2 != null);
2050
2051 CheckContextMatch(t1);
2052 CheckContextMatch(t2);
2053 return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2054 }

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

1678 {
1679 Debug.Assert(t1 != null);
1680 Debug.Assert(t2 != null);
1681
1682 CheckContextMatch(t1);
1683 CheckContextMatch(t2);
1684 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1685 }

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

1710 {
1711 Debug.Assert(t1 != null);
1712 Debug.Assert(t2 != null);
1713
1714 CheckContextMatch(t1);
1715 CheckContextMatch(t2);
1716 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1717 }

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

1816 {
1817 Debug.Assert(t1 != null);
1818 Debug.Assert(t2 != null);
1819
1820 CheckContextMatch(t1);
1821 CheckContextMatch(t2);
1822 return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1823 }

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

1646 {
1647 Debug.Assert(t1 != null);
1648 Debug.Assert(t2 != null);
1649
1650 CheckContextMatch(t1);
1651 CheckContextMatch(t2);
1652 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1653 }

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

1614 {
1615 Debug.Assert(t1 != null);
1616 Debug.Assert(t2 != null);
1617
1618 CheckContextMatch(t1);
1619 CheckContextMatch(t2);
1620 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1621 }

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

1582 {
1583 Debug.Assert(t1 != null);
1584 Debug.Assert(t2 != null);
1585
1586 CheckContextMatch(t1);
1587 CheckContextMatch(t2);
1588 return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1589 }

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

1565 {
1566 Debug.Assert(t1 != null);
1567 Debug.Assert(t2 != null);
1568
1569 CheckContextMatch(t1);
1570 CheckContextMatch(t2);
1571 return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1572 }

◆ MkBVSub()

BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1470 of file Context.cs.

1471 {
1472 Debug.Assert(t1 != null);
1473 Debug.Assert(t2 != null);
1474
1475 CheckContextMatch(t1);
1476 CheckContextMatch(t2);
1477 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1478 }

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

2015 {
2016 Debug.Assert(t1 != null);
2017 Debug.Assert(t2 != null);
2018
2019 CheckContextMatch(t1);
2020 CheckContextMatch(t2);
2021 return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2022 }

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

2031 {
2032 Debug.Assert(t1 != null);
2033 Debug.Assert(t2 != null);
2034
2035 CheckContextMatch(t1);
2036 CheckContextMatch(t2);
2037 return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2038 }

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

1504 {
1505 Debug.Assert(t1 != null);
1506 Debug.Assert(t2 != null);
1507
1508 CheckContextMatch(t1);
1509 CheckContextMatch(t2);
1510 return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1511 }

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

1662 {
1663 Debug.Assert(t1 != null);
1664 Debug.Assert(t2 != null);
1665
1666 CheckContextMatch(t1);
1667 CheckContextMatch(t2);
1668 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1669 }

◆ MkBVUGT()

BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1693 of file Context.cs.

1694 {
1695 Debug.Assert(t1 != null);
1696 Debug.Assert(t2 != null);
1697
1698 CheckContextMatch(t1);
1699 CheckContextMatch(t2);
1700 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1701 }

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

1630 {
1631 Debug.Assert(t1 != null);
1632 Debug.Assert(t2 != null);
1633
1634 CheckContextMatch(t1);
1635 CheckContextMatch(t2);
1636 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1637 }

◆ MkBVULT()

BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than.

The arguments must have the same bit-vector sort.

Definition at line 1597 of file Context.cs.

1598 {
1599 Debug.Assert(t1 != null);
1600 Debug.Assert(t2 != null);
1601
1602 CheckContextMatch(t1);
1603 CheckContextMatch(t2);
1604 return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1605 }

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

1545 {
1546 Debug.Assert(t1 != null);
1547 Debug.Assert(t2 != null);
1548
1549 CheckContextMatch(t1);
1550 CheckContextMatch(t2);
1551 return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1552 }

◆ MkBVXNOR()

BitVecExpr MkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1430 of file Context.cs.

1431 {
1432 Debug.Assert(t1 != null);
1433 Debug.Assert(t2 != null);
1434
1435 CheckContextMatch(t1);
1436 CheckContextMatch(t2);
1437 return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1438 }

◆ MkBVXOR()

BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1388 of file Context.cs.

1389 {
1390 Debug.Assert(t1 != null);
1391 Debug.Assert(t2 != null);
1392
1393 CheckContextMatch(t1);
1394 CheckContextMatch(t2);
1395 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1396 }

◆ MkCharLe()

BoolExpr MkCharLe ( Expr  ch1,
Expr  ch2 
)
inline

Create less than or equal to between two characters.

Definition at line 2798 of file Context.cs.

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

◆ MkComplement()

ReExpr MkComplement ( ReExpr  re)
inline

Create the complement regular expression.

Definition at line 2710 of file Context.cs.

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

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

1730 {
1731 Debug.Assert(t1 != null);
1732 Debug.Assert(t2 != null);
1733
1734 CheckContextMatch(t1);
1735 CheckContextMatch(t2);
1736 return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1737 }

◆ MkConcat() [2/3]

ReExpr MkConcat ( params ReExpr[]  t)
inline

Create the concatenation of regular languages.

Definition at line 2719 of file Context.cs.

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

◆ MkConcat() [3/3]

SeqExpr MkConcat ( params SeqExpr[]  t)
inline

Concatenate sequences.

Definition at line 2518 of file Context.cs.

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

◆ MkConst() [1/3]

Expr MkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 806 of file Context.cs.

807 {
808 Debug.Assert(f != null);
809
810 return MkApp(f);
811 }

◆ MkConst() [2/3]

Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 782 of file Context.cs.

783 {
784 Debug.Assert(range != null);
785
786 using var symbol = MkSymbol(name);
787 return MkConst(symbol, range);
788 }

◆ MkConst() [3/3]

Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 768 of file Context.cs.

769 {
770 Debug.Assert(name != null);
771 Debug.Assert(range != null);
772
773 CheckContextMatch(name);
774 CheckContextMatch(range);
775
776 return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
777 }
z3::range
expr range(expr const &lo, expr const &hi)
Definition z3++.h:4185

Referenced by Context.MkArrayConst(), Context.MkArrayConst(), Context.MkBoolConst(), Context.MkBoolConst(), Context.MkBVConst(), Context.MkBVConst(), 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 2247 of file Context.cs.

2248 {
2249 Debug.Assert(domain != null);
2250 Debug.Assert(v != null);
2251
2252 CheckContextMatch(domain);
2253 CheckContextMatch(v);
2254 return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2255 }

◆ MkConstDecl() [1/2]

FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 702 of file Context.cs.

703 {
704 Debug.Assert(range != null);
705
706 CheckContextMatch(range);
707 using var symbol = MkSymbol(name);
708 return new FuncDecl(this, symbol, null, range);
709 }

◆ MkConstDecl() [2/2]

FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 689 of file Context.cs.

690 {
691 Debug.Assert(name != null);
692 Debug.Assert(range != null);
693
694 CheckContextMatch(name);
695 CheckContextMatch(range);
696 return new FuncDecl(this, name, null, range);
697 }

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

433 {
434
435 using var nameSymbol = MkSymbol(name);
436 using var recognizerSymbol = MkSymbol(recognizer);
437 var fieldSymbols = MkSymbols(fieldNames);
438 try
439 {
440 return new Constructor(this, nameSymbol, recognizerSymbol, fieldSymbols, sorts, sortRefs);
441 }
442 finally
443 {
444 foreach (var fieldSymbol in fieldSymbols)
445 fieldSymbol.Dispose();
446 }
447 }

◆ MkConstructor() [2/2]

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

Create a datatype constructor.

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

Definition at line 415 of file Context.cs.

416 {
417 Debug.Assert(name != null);
418 Debug.Assert(recognizer != null);
419
420 return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
421 }

◆ MkContains()

BoolExpr MkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2562 of file Context.cs.

2563 {
2564 Debug.Assert(s1 != null);
2565 Debug.Assert(s2 != null);
2566 CheckContextMatch(s1, s2);
2567 return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2568 }

◆ MkDatatypeSort() [1/2]

DatatypeSort MkDatatypeSort ( string  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 467 of file Context.cs.

468 {
469 Debug.Assert(constructors != null);
470 Debug.Assert(constructors.All(c => c != null));
471
472 CheckContextMatch<Constructor>(constructors);
473 using var symbol = MkSymbol(name);
474 return new DatatypeSort(this, symbol, constructors);
475 }
z3py.DatatypeSort
DatatypeSort(name, params=None, ctx=None)
Definition z3py.py:5485

◆ MkDatatypeSort() [2/2]

DatatypeSort MkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 452 of file Context.cs.

453 {
454 Debug.Assert(name != null);
455 Debug.Assert(constructors != null);
456 Debug.Assert(constructors.All(c => c != null));
457
458
459 CheckContextMatch(name);
460 CheckContextMatch<Constructor>(constructors);
461 return new DatatypeSort(this, name, constructors);
462 }

◆ 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
namename of the datatype sort
parametersoptional array of sort parameters for parametric datatypes

Definition at line 501 of file Context.cs.

502 {
503 using var symbol = MkSymbol(name);
504 return MkDatatypeSortRef(symbol, parameters);
505 }
Microsoft.Z3.Context.MkDatatypeSortRef
DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters=null)
Create a forward reference to a datatype sort. This is useful for creating recursive datatypes or par...
Definition Context.cs:483

◆ 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
namename of the datatype sort
parametersoptional array of sort parameters for parametric datatypes

Definition at line 483 of file Context.cs.

484 {
485 Debug.Assert(name != null);
486 CheckContextMatch(name);
487 if (parameters != null)
488 CheckContextMatch<Sort>(parameters);
489
490 var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
491 var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
492 return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
493 }
z3py.Length
Length(s)
Definition z3py.py:11406

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

546 {
547 Debug.Assert(names != null);
548 Debug.Assert(c != null);
549 Debug.Assert(names.Length == c.Length);
550 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
551 //Debug.Assert(names.All(name => name != null));
552
553 var symbols = MkSymbols(names);
554 try
555 {
556 return MkDatatypeSorts(symbols, c);
557 }
558 finally
559 {
560 foreach (var symbol in symbols)
561 symbol.Dispose();
562 }
563 }
Microsoft.Z3.Context.MkDatatypeSorts
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition Context.cs:512

◆ MkDatatypeSorts() [2/2]

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

Create mutually recursive datatypes.

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

Definition at line 512 of file Context.cs.

513 {
514 Debug.Assert(names != null);
515 Debug.Assert(c != null);
516 Debug.Assert(names.Length == c.Length);
517 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
518 Debug.Assert(names.All(name => name != null));
519
520 CheckContextMatch<Symbol>(names);
521 uint n = (uint)names.Length;
522 ConstructorList[] cla = new ConstructorList[n];
523 IntPtr[] n_constr = new IntPtr[n];
524 for (uint i = 0; i < n; i++)
525 {
526 Constructor[] constructor = c[i];
527 CheckContextMatch<Constructor>(constructor);
528 cla[i] = new ConstructorList(this, constructor);
529 n_constr[i] = cla[i].NativeObject;
530 }
531 IntPtr[] n_res = new IntPtr[n];
532 Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
533 DatatypeSort[] res = new DatatypeSort[n];
534 for (uint i = 0; i < n; i++)
535 res[i] = new DatatypeSort(this, n_res[i]);
536 return res;
537 }

Referenced by Context.MkDatatypeSorts().

◆ MkDiff()

ReExpr MkDiff ( ReExpr  a,
ReExpr  b 
)
inline

Create a difference regular expression.

Definition at line 2755 of file Context.cs.

2756 {
2757 Debug.Assert(a != null);
2758 Debug.Assert(b != null);
2759 CheckContextMatch(a, b);
2760 return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
2761 }

◆ MkDistinct() [1/2]

BoolExpr MkDistinct ( IEnumerable< Expr >  args)
inline

Creates a distinct term.

Definition at line 967 of file Context.cs.

968 {
969 Debug.Assert(args != null);
970 return MkDistinct(args.ToArray());
971 }
Microsoft.Z3.Context.MkDistinct
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition Context.cs:955

◆ MkDistinct() [2/2]

BoolExpr MkDistinct ( params Expr[]  args)
inline

Creates a distinct term.

Definition at line 955 of file Context.cs.

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

Referenced by Context.MkDistinct().

◆ MkDiv()

ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 1171 of file Context.cs.

1172 {
1173 Debug.Assert(t1 != null);
1174 Debug.Assert(t2 != null);
1175
1176 CheckContextMatch(t1);
1177 CheckContextMatch(t2);
1178 return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1179 }

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

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

◆ MkEmptySeq()

SeqExpr MkEmptySeq ( Sort  s)
inline

Create the empty sequence.

Definition at line 2450 of file Context.cs.

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

◆ MkEmptySet()

ArrayExpr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2323 of file Context.cs.

2324 {
2325 Debug.Assert(domain != null);
2326
2327 CheckContextMatch(domain);
2328 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2329 }

◆ MkEnumSort() [1/2]

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

Create a new enumeration sort.

Definition at line 333 of file Context.cs.

334 {
335 Debug.Assert(enumNames != null);
336
337 var enumSymbols = MkSymbols(enumNames);
338 try
339 {
340 using var symbol = MkSymbol(name);
341 return new EnumSort(this, symbol, enumSymbols);
342 }
343 finally
344 {
345 foreach (var enumSymbol in enumSymbols)
346 enumSymbol.Dispose();
347 }
348 }
z3py.EnumSort
EnumSort(name, values, ctx=None)
Definition z3py.py:5534

◆ MkEnumSort() [2/2]

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

Create a new enumeration sort.

Definition at line 318 of file Context.cs.

319 {
320 Debug.Assert(name != null);
321 Debug.Assert(enumNames != null);
322 Debug.Assert(enumNames.All(f => f != null));
323
324
325 CheckContextMatch(name);
326 CheckContextMatch<Symbol>(enumNames);
327 return new EnumSort(this, name, enumNames);
328 }

◆ MkEq()

BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 942 of file Context.cs.

943 {
944 Debug.Assert(x != null);
945 Debug.Assert(y != null);
946
947 CheckContextMatch(x);
948 CheckContextMatch(y);
949 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
950 }

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

3279 {
3280 Debug.Assert(body != null);
3281 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3282 Debug.Assert(patterns == null || patterns.All(p => p != null));
3283 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3284
3285 return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3286 }

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

3257 {
3258 Debug.Assert(sorts != null);
3259 Debug.Assert(names != null);
3260 Debug.Assert(body != null);
3261 Debug.Assert(sorts.Length == names.Length);
3262 Debug.Assert(sorts.All(s => s != null));
3263 Debug.Assert(names.All(n => n != null));
3264 Debug.Assert(patterns == null || patterns.All(p => p != null));
3265 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3266
3267 return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3268 }

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

◆ MkExtract() [1/2]

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

Extract subsequence.

Definition at line 2617 of file Context.cs.

2618 {
2619 Debug.Assert(s != null);
2620 Debug.Assert(offset != null);
2621 Debug.Assert(length != null);
2622 CheckContextMatch(s, offset, length);
2623 return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2624 }

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

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

◆ MkFalse()

BoolExpr MkFalse ( )
inline

The false Term.

Definition at line 926 of file Context.cs.

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

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
nameThe name used to identify the sort
sizeThe size of the sort

Definition at line 397 of file Context.cs.

398 {
399 using var symbol = MkSymbol(name);
400 return new FiniteDomainSort(this, symbol, size);
401 }
z3py.FiniteDomainSort
FiniteDomainSort(name, sz, ctx=None)
Definition z3py.py:7930

◆ MkFiniteDomainSort() [2/2]

FiniteDomainSort MkFiniteDomainSort ( Symbol  name,
ulong  size 
)
inline

Create a new finite domain sort.

Returns
The result is a sort

Parameters
nameThe name used to identify the sort
sizeThe size of the sort

Definition at line 381 of file Context.cs.

382 {
383 Debug.Assert(name != null);
384
385 CheckContextMatch(name);
386 return new FiniteDomainSort(this, name, size);
387 }

◆ MkFixedpoint()

Fixedpoint MkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 4069 of file Context.cs.

4070 {
4071
4072 return new Fixedpoint(this);
4073 }

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

3239 {
3240 Debug.Assert(body != null);
3241 Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
3242 Debug.Assert(patterns == null || patterns.All(p => p != null));
3243 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3244
3245
3246 return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3247 }

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

Definition at line 3214 of file Context.cs.

3215 {
3216 Debug.Assert(sorts != null);
3217 Debug.Assert(names != null);
3218 Debug.Assert(body != null);
3219 Debug.Assert(sorts.Length == names.Length);
3220 Debug.Assert(sorts.All(s => s != null));
3221 Debug.Assert(names.All(n => n != null));
3222 Debug.Assert(patterns == null || patterns.All(p => p != null));
3223 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3224
3225
3226 return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3227 }

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

Definition at line 4659 of file Context.cs.

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

◆ 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
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.

Definition at line 4380 of file Context.cs.

4381 {
4382 return MkFPNumeral(sgn, exp, sig, s);
4383 }
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition Context.cs:4294

◆ 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
sgnthe sign.
expthe exponent.
sigthe significand.
sFloatingPoint sort.

Definition at line 4392 of file Context.cs.

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

◆ MkFP() [4/6]

FPNum MkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4358 of file Context.cs.

4359 {
4360 return MkFPNumeral(v, s);
4361 }

◆ MkFP() [5/6]

FPNum MkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4348 of file Context.cs.

4349 {
4350 return MkFPNumeral(v, s);
4351 }

◆ MkFP() [6/6]

FPNum MkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4368 of file Context.cs.

4369 {
4370 return MkFPNumeral(v, s);
4371 }

◆ MkFPAbs()

FPExpr MkFPAbs ( FPExpr  t)
inline

Floating-point absolute value.

Parameters
tfloating-point term

Definition at line 4404 of file Context.cs.

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

◆ MkFPAdd()

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

Floating-point addition.

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

Definition at line 4424 of file Context.cs.

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

◆ MkFPDiv()

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

Floating-point division.

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

Definition at line 4457 of file Context.cs.

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

◆ MkFPEq()

BoolExpr MkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

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

Parameters
t1floating-point term
t2floating-point term

Definition at line 4576 of file Context.cs.

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

◆ 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
rmrounding mode term
t1floating-point term
t2floating-point term
t3floating-point term

Definition at line 4472 of file Context.cs.

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

◆ MkFPGEq()

BoolExpr MkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4553 of file Context.cs.

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

◆ MkFPGt()

BoolExpr MkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4563 of file Context.cs.

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

◆ MkFPInf()

FPNum MkFPInf ( FPSort  s,
bool  negative 
)
inline

Create a floating-point infinity of sort s.

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

Definition at line 4274 of file Context.cs.

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

◆ MkFPIsInfinite()

BoolExpr MkFPIsInfinite ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4612 of file Context.cs.

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

◆ MkFPIsNaN()

BoolExpr MkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term

Definition at line 4621 of file Context.cs.

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

◆ MkFPIsNegative()

BoolExpr MkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4630 of file Context.cs.

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

◆ MkFPIsNormal()

BoolExpr MkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4585 of file Context.cs.

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

◆ MkFPIsPositive()

BoolExpr MkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4639 of file Context.cs.

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

◆ MkFPIsSubnormal()

BoolExpr MkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4594 of file Context.cs.

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

◆ MkFPIsZero()

BoolExpr MkFPIsZero ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4603 of file Context.cs.

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

◆ MkFPLEq()

BoolExpr MkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4533 of file Context.cs.

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

◆ MkFPLt()

BoolExpr MkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4543 of file Context.cs.

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

◆ MkFPMax()

FPExpr MkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4523 of file Context.cs.

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

◆ MkFPMin()

FPExpr MkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4513 of file Context.cs.

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

◆ MkFPMul()

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

Floating-point multiplication.

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

Definition at line 4446 of file Context.cs.

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

◆ MkFPNaN()

FPNum MkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.

Definition at line 4264 of file Context.cs.

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

◆ MkFPNeg()

FPExpr MkFPNeg ( FPExpr  t)
inline

Floating-point negation.

Parameters
tfloating-point term

Definition at line 4413 of file Context.cs.

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

◆ 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
sgnthe sign.
sigthe significand.
expthe exponent.
sFloatingPoint sort.

Definition at line 4338 of file Context.cs.

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

◆ 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
sgnthe sign.
sigthe significand.
expthe exponent.
sFloatingPoint sort.

Definition at line 4326 of file Context.cs.

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

◆ MkFPNumeral() [3/5]

FPNum MkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4304 of file Context.cs.

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

◆ MkFPNumeral() [4/5]

FPNum MkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4294 of file Context.cs.

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

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
vnumeral value.
sFloatingPoint sort.

Definition at line 4314 of file Context.cs.

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

◆ MkFPRem()

FPExpr MkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4492 of file Context.cs.

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

◆ MkFPRNA()

FPRMNum MkFPRNA ( )
inline

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

Definition at line 4128 of file Context.cs.

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

◆ MkFPRNE()

FPRMNum MkFPRNE ( )
inline

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

Definition at line 4112 of file Context.cs.

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

◆ MkFPRoundingModeSort()

FPRMSort MkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Definition at line 4094 of file Context.cs.

4095 {
4096 return new FPRMSort(this);
4097 }

◆ MkFPRoundNearestTiesToAway()

FPRMNum MkFPRoundNearestTiesToAway ( )
inline

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

Definition at line 4120 of file Context.cs.

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

◆ MkFPRoundNearestTiesToEven()

FPRMExpr MkFPRoundNearestTiesToEven ( )
inline

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

Definition at line 4104 of file Context.cs.

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

◆ 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
rmterm of RoundingMode sort
tfloating-point term

Definition at line 4503 of file Context.cs.

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

◆ MkFPRoundTowardNegative()

FPRMNum MkFPRoundTowardNegative ( )
inline

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

Definition at line 4152 of file Context.cs.

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

◆ MkFPRoundTowardPositive()

FPRMNum MkFPRoundTowardPositive ( )
inline

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

Definition at line 4136 of file Context.cs.

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

◆ MkFPRoundTowardZero()

FPRMNum MkFPRoundTowardZero ( )
inline

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

Definition at line 4168 of file Context.cs.

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

◆ MkFPRTN()

FPRMNum MkFPRTN ( )
inline

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

Definition at line 4160 of file Context.cs.

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

◆ MkFPRTP()

FPRMNum MkFPRTP ( )
inline

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

Definition at line 4144 of file Context.cs.

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

◆ MkFPRTZ()

FPRMNum MkFPRTZ ( )
inline

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

Definition at line 4176 of file Context.cs.

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

◆ MkFPSort()

FPSort MkFPSort ( uint  ebits,
uint  sbits 
)
inline

Create a FloatingPoint sort.

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

Definition at line 4189 of file Context.cs.

4190 {
4191 return new FPSort(this, ebits, sbits);
4192 }
z3py.FPSort
FPSort(ebits, sbits, ctx=None)
Definition z3py.py:10198

◆ MkFPSort128()

FPSort MkFPSort128 ( )
inline

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

Definition at line 4253 of file Context.cs.

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

◆ MkFPSort16()

FPSort MkFPSort16 ( )
inline

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

Definition at line 4205 of file Context.cs.

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

◆ MkFPSort32()

FPSort MkFPSort32 ( )
inline

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

Definition at line 4221 of file Context.cs.

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

◆ MkFPSort64()

FPSort MkFPSort64 ( )
inline

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

Definition at line 4237 of file Context.cs.

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

◆ MkFPSortDouble()

FPSort MkFPSortDouble ( )
inline

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

Definition at line 4229 of file Context.cs.

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

◆ MkFPSortHalf()

FPSort MkFPSortHalf ( )
inline

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

Definition at line 4197 of file Context.cs.

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

◆ MkFPSortQuadruple()

FPSort MkFPSortQuadruple ( )
inline

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

Definition at line 4245 of file Context.cs.

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

◆ MkFPSortSingle()

FPSort MkFPSortSingle ( )
inline

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

Definition at line 4213 of file Context.cs.

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

◆ MkFPSqrt()

FPExpr MkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root.

Parameters
rmrounding mode term
tfloating-point term

Definition at line 4482 of file Context.cs.

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

◆ MkFPSub()

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

Floating-point subtraction.

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

Definition at line 4435 of file Context.cs.

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

◆ 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
rmRoundingMode term.
tFloatingPoint term
szSize of the resulting bit-vector.
signIndicates whether the result is a signed or unsigned bit-vector.

Definition at line 4762 of file Context.cs.

4763 {
4764 if (sign)
4765 return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4766 else
4767 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4768 }

◆ 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
bvbit-vector value (of size m).
sFloatingPoint sort (ebits+sbits == m)

Definition at line 4675 of file Context.cs.

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

◆ 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
rmRoundingMode term.
tterm of bit-vector sort.
sFloatingPoint sort.
signedflag indicating whether t is interpreted as signed or unsigned bit-vector.

Definition at line 4725 of file Context.cs.

4726 {
4727 if (signed)
4728 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4729 else
4730 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4731 }

◆ 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
rmRoundingMode term.
tFloatingPoint term.
sFloatingPoint sort.

Definition at line 4691 of file Context.cs.

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

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

Definition at line 4813 of file Context.cs.

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

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

Definition at line 4707 of file Context.cs.

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

◆ 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
sFloatingPoint sort
rmfloating-point rounding mode term
tfloating-point term

Definition at line 4743 of file Context.cs.

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

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

Definition at line 4796 of file Context.cs.

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

◆ 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
tFloatingPoint term

Definition at line 4779 of file Context.cs.

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

◆ MkFPZero()

FPNum MkFPZero ( FPSort  s,
bool  negative 
)
inline

Create a floating-point zero of sort s.

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

Definition at line 4284 of file Context.cs.

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

◆ MkFreshConst()

Expr MkFreshConst ( string  prefix,
Sort  range 
)
inline

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

Definition at line 794 of file Context.cs.

795 {
796 Debug.Assert(range != null);
797
798 CheckContextMatch(range);
799 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
800 }

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

717 {
718 Debug.Assert(range != null);
719
720 CheckContextMatch(range);
721 return new FuncDecl(this, prefix, null, range);
722 }

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

677 {
678 Debug.Assert(range != null);
679 Debug.Assert(domain.All(d => d != null));
680
681 CheckContextMatch<Sort>(domain);
682 CheckContextMatch(range);
683 return new FuncDecl(this, prefix, domain, range);
684 }

◆ MkFullRe()

ReExpr MkFullRe ( Sort  s)
inline

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

Definition at line 2777 of file Context.cs.

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

◆ MkFullSet()

ArrayExpr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2334 of file Context.cs.

2335 {
2336 Debug.Assert(domain != null);
2337
2338 CheckContextMatch(domain);
2339 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2340 }

◆ MkFuncDecl() [1/4]

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

Creates a new function declaration.

Definition at line 659 of file Context.cs.

660 {
661 Debug.Assert(range != null);
662 Debug.Assert(domain != null);
663
664 CheckContextMatch(domain);
665 CheckContextMatch(range);
666 using var symbol = MkSymbol(name);
667 Sort[] q = new Sort[] { domain };
668 return new FuncDecl(this, symbol, q, range);
669 }

◆ MkFuncDecl() [2/4]

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

Creates a new function declaration.

Definition at line 616 of file Context.cs.

617 {
618 Debug.Assert(range != null);
619 Debug.Assert(domain.All(d => d != null));
620
621 CheckContextMatch<Sort>(domain);
622 CheckContextMatch(range);
623 using var symbol = MkSymbol(name);
624 return new FuncDecl(this, symbol, domain, range);
625 }

◆ MkFuncDecl() [3/4]

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

Creates a new function declaration.

Definition at line 600 of file Context.cs.

601 {
602 Debug.Assert(name != null);
603 Debug.Assert(domain != null);
604 Debug.Assert(range != null);
605
606 CheckContextMatch(name);
607 CheckContextMatch(domain);
608 CheckContextMatch(range);
609 Sort[] q = new Sort[] { domain };
610 return new FuncDecl(this, name, q, range);
611 }

◆ MkFuncDecl() [4/4]

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

Creates a new function declaration.

Definition at line 585 of file Context.cs.

586 {
587 Debug.Assert(name != null);
588 Debug.Assert(range != null);
589 Debug.Assert(domain.All(d => d != null));
590
591 CheckContextMatch(name);
592 CheckContextMatch<Sort>(domain);
593 CheckContextMatch(range);
594 return new FuncDecl(this, name, domain, range);
595 }

◆ MkGe()

BoolExpr MkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 >= t2

Definition at line 1264 of file Context.cs.

1265 {
1266 Debug.Assert(t1 != null);
1267 Debug.Assert(t2 != null);
1268
1269 CheckContextMatch(t1);
1270 CheckContextMatch(t2);
1271 return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1272 }

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

Definition at line 3454 of file Context.cs.

3455 {
3456
3457 return new Goal(this, models, unsatCores, proofs);
3458 }

◆ MkGt()

BoolExpr MkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 > t2

Definition at line 1251 of file Context.cs.

1252 {
1253 Debug.Assert(t1 != null);
1254 Debug.Assert(t2 != null);
1255
1256 CheckContextMatch(t1);
1257 CheckContextMatch(t2);
1258 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1259 }

Referenced by ArithExpr.operator>().

◆ MkIff()

BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 1004 of file Context.cs.

1005 {
1006 Debug.Assert(t1 != null);
1007 Debug.Assert(t2 != null);
1008
1009 CheckContextMatch(t1);
1010 CheckContextMatch(t2);
1011 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
1012 }

◆ MkImplies()

BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 1017 of file Context.cs.

1018 {
1019 Debug.Assert(t1 != null);
1020 Debug.Assert(t2 != null);
1021
1022 CheckContextMatch(t1);
1023 CheckContextMatch(t2);
1024 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
1025 }

◆ MkIndexOf()

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

Extract index of sub-string starting at offset.

Definition at line 2629 of file Context.cs.

2630 {
2631 Debug.Assert(s != null);
2632 Debug.Assert(offset != null);
2633 Debug.Assert(substr != null);
2634 CheckContextMatch(s, substr, offset);
2635 return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2636 }

◆ MkInRe()

BoolExpr MkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2663 of file Context.cs.

2664 {
2665 Debug.Assert(s != null);
2666 Debug.Assert(re != null);
2667 CheckContextMatch(s, re);
2668 return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2669 }

◆ MkInt() [1/5]

IntNum MkInt ( int  v)
inline

Create an integer numeral.

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

Definition at line 3077 of file Context.cs.

3078 {
3079
3080 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
3081 }
Microsoft.Z3.Context.IntSort
IntSort IntSort
Retrieves the Integer sort of the context.
Definition Context.cs:158

◆ MkInt() [2/5]

IntNum MkInt ( long  v)
inline

Create an integer numeral.

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

Definition at line 3099 of file Context.cs.

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

◆ MkInt() [3/5]

IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 3066 of file Context.cs.

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

◆ MkInt() [4/5]

IntNum MkInt ( uint  v)
inline

Create an integer numeral.

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

Definition at line 3088 of file Context.cs.

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

◆ MkInt() [5/5]

IntNum MkInt ( ulong  v)
inline

Create an integer numeral.

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

Definition at line 3110 of file Context.cs.

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

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

1946 {
1947 Debug.Assert(t != null);
1948
1949 CheckContextMatch(t);
1950 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1951 }

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

1285 {
1286 Debug.Assert(t != null);
1287
1288 CheckContextMatch(t);
1289 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1290 }

◆ MkIntConst() [1/2]

IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 845 of file Context.cs.

846 {
847 Debug.Assert(name != null);
848
849 return (IntExpr)MkConst(name, IntSort);
850 }

◆ MkIntConst() [2/2]

IntExpr MkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 835 of file Context.cs.

836 {
837 Debug.Assert(name != null);
838
839 return (IntExpr)MkConst(name, IntSort);
840 }

◆ MkIntersect()

ReExpr MkIntersect ( params ReExpr[]  t)
inline

Create the intersection of regular languages.

Definition at line 2743 of file Context.cs.

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

◆ MkIntSort()

IntSort MkIntSort ( )
inline

Create a new integer sort.

Definition at line 233 of file Context.cs.

234 {
235
236 return new IntSort(this);
237 }

◆ MkIsDigit()

BoolExpr MkIsDigit ( Expr  ch)
inline

Create a check if the character is a digit.

Definition at line 2835 of file Context.cs.

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

◆ MkIsInteger()

BoolExpr MkIsInteger ( RealExpr  t)
inline

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

Definition at line 1310 of file Context.cs.

1311 {
1312 Debug.Assert(t != null);
1313
1314 CheckContextMatch(t);
1315 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1316 }

◆ MkITE()

Expr MkITE ( BoolExpr  t1,
Expr  t2,
Expr  t3 
)
inline

Create an expression representing an if-then-else: ite(t1, t2, t3).

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

Definition at line 989 of file Context.cs.

990 {
991 Debug.Assert(t1 != null);
992 Debug.Assert(t2 != null);
993 Debug.Assert(t3 != null);
994
995 CheckContextMatch(t1);
996 CheckContextMatch(t2);
997 CheckContextMatch(t3);
998 return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
999 }

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

3368 {
3369 Debug.Assert(body != null);
3370 Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
3371 return new Lambda(this, boundConstants, body);
3372 }
z3py.Lambda
Lambda(vs, body)
Definition z3py.py:2363

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

Definition at line 3348 of file Context.cs.

3349 {
3350 Debug.Assert(sorts != null);
3351 Debug.Assert(names != null);
3352 Debug.Assert(body != null);
3353 Debug.Assert(sorts.Length == names.Length);
3354 Debug.Assert(sorts.All(s => s != null));
3355 Debug.Assert(names.All(n => n != null));
3356 return new Lambda(this, sorts, names, body);
3357 }

◆ MkLe()

BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1238 of file Context.cs.

1239 {
1240 Debug.Assert(t1 != null);
1241 Debug.Assert(t2 != null);
1242
1243 CheckContextMatch(t1);
1244 CheckContextMatch(t2);
1245 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1246 }

Referenced by ArithExpr.operator<=().

◆ MkLength()

IntExpr MkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 2531 of file Context.cs.

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

◆ MkListSort() [1/2]

ListSort MkListSort ( string  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 366 of file Context.cs.

367 {
368 Debug.Assert(elemSort != null);
369
370 CheckContextMatch(elemSort);
371 using var symbol = MkSymbol(name);
372 return new ListSort(this, symbol, elemSort);
373 }

◆ MkListSort() [2/2]

ListSort MkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 353 of file Context.cs.

354 {
355 Debug.Assert(name != null);
356 Debug.Assert(elemSort != null);
357
358 CheckContextMatch(name);
359 CheckContextMatch(elemSort);
360 return new ListSort(this, name, elemSort);
361 }

◆ MkLoop()

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

Take the bounded Kleene star of a regular expression.

Definition at line 2683 of file Context.cs.

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

◆ MkLt()

BoolExpr MkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 < t2

Definition at line 1225 of file Context.cs.

1226 {
1227 Debug.Assert(t1 != null);
1228 Debug.Assert(t2 != null);
1229
1230 CheckContextMatch(t1);
1231 CheckContextMatch(t2);
1232 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1233 }

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

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

◆ MkMod()

IntExpr MkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 1185 of file Context.cs.

1186 {
1187 Debug.Assert(t1 != null);
1188 Debug.Assert(t2 != null);
1189
1190 CheckContextMatch(t1);
1191 CheckContextMatch(t2);
1192 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1193 }

◆ MkMul() [1/2]

ArithExpr MkMul ( IEnumerable< ArithExpr >  ts)
inline

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

Definition at line 1139 of file Context.cs.

1140 {
1141 Debug.Assert(ts != null);
1142 return MkMul(ts.ToArray());
1143 }
Microsoft.Z3.Context.MkMul
ArithExpr MkMul(params ArithExpr[] ts)
Create an expression representing t[0] * t[1] * ....
Definition Context.cs:1127

◆ MkMul() [2/2]

ArithExpr MkMul ( params ArithExpr[]  ts)
inline

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

Definition at line 1127 of file Context.cs.

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

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

◆ MkNot()

BoolExpr MkNot ( BoolExpr  a)
inline

Mk an expression representing not(a).

Definition at line 976 of file Context.cs.

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

Referenced by BoolExpr.operator!().

◆ MkNth()

Expr MkNth ( SeqExpr  s,
Expr  index 
)
inline

Retrieve element at index.

Definition at line 2606 of file Context.cs.

2607 {
2608 Debug.Assert(s != null);
2609 Debug.Assert(index != null);
2610 CheckContextMatch(s, index);
2611 return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2612 }

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

Definition at line 2935 of file Context.cs.

2936 {
2937 Debug.Assert(ty != null);
2938
2939 CheckContextMatch(ty);
2940 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2941 }

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

Definition at line 2965 of file Context.cs.

2966 {
2967 Debug.Assert(ty != null);
2968
2969 CheckContextMatch(ty);
2970 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2971 }

◆ MkNumeral() [3/5]

Expr MkNumeral ( string  v,
Sort  ty 
)
inline

Create a Term of a given sort.

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

Definition at line 2920 of file Context.cs.

2921 {
2922 Debug.Assert(ty != null);
2923
2924 CheckContextMatch(ty);
2925 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2926 }

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

Definition at line 2950 of file Context.cs.

2951 {
2952 Debug.Assert(ty != null);
2953
2954 CheckContextMatch(ty);
2955 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2956 }

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

Definition at line 2980 of file Context.cs.

2981 {
2982 Debug.Assert(ty != null);
2983
2984 CheckContextMatch(ty);
2985 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2986 }

◆ MkOptimize()

Optimize MkOptimize ( )
inline

Create an Optimization context.

Definition at line 4080 of file Context.cs.

4081 {
4082
4083 return new Optimize(this);
4084 }

◆ MkOption()

ReExpr MkOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2701 of file Context.cs.

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

◆ MkOr() [1/2]

BoolExpr MkOr ( IEnumerable< BoolExpr >  ts)
inline

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

Definition at line 1094 of file Context.cs.

1095 {
1096 Debug.Assert(ts != null);
1097 return MkOr(ts.ToArray());
1098 }
Microsoft.Z3.Context.MkOr
BoolExpr MkOr(params BoolExpr[] ts)
Create an expression representing t[0] or t[1] or ....
Definition Context.cs:1081

◆ MkOr() [2/2]

BoolExpr MkOr ( params BoolExpr[]  ts)
inline

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

Definition at line 1081 of file Context.cs.

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

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

◆ MkParams()

Params MkParams ( )
inline

Creates a new ParameterSet.

Definition at line 3465 of file Context.cs.

3466 {
3467
3468 return new Params(this);
3469 }

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

◆ MkPattern()

Pattern MkPattern ( params Expr[]  terms)
inline

Create a quantifier pattern.

Definition at line 753 of file Context.cs.

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

◆ MkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2899 of file Context.cs.

2900 {
2901 Debug.Assert(args != null);
2902 Debug.Assert(coeffs != null);
2903 Debug.Assert(args.Length == coeffs.Length);
2904 CheckContextMatch<BoolExpr>(args);
2905 return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
2906 AST.ArrayToNative(args),
2907 coeffs, k));
2908 }

◆ MkPBGe()

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

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

Definition at line 2886 of file Context.cs.

2887 {
2888 Debug.Assert(args != null);
2889 Debug.Assert(coeffs != null);
2890 Debug.Assert(args.Length == coeffs.Length);
2891 CheckContextMatch<BoolExpr>(args);
2892 return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
2893 AST.ArrayToNative(args),
2894 coeffs, k));
2895 }

◆ MkPBLe()

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

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

Definition at line 2872 of file Context.cs.

2873 {
2874 Debug.Assert(args != null);
2875 Debug.Assert(coeffs != null);
2876 Debug.Assert(args.Length == coeffs.Length);
2877 CheckContextMatch<BoolExpr>(args);
2878 return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
2879 AST.ArrayToNative(args),
2880 coeffs, k));
2881 }

◆ MkPlus()

ReExpr MkPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2692 of file Context.cs.

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

◆ MkPower()

ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 1212 of file Context.cs.

1213 {
1214 Debug.Assert(t1 != null);
1215 Debug.Assert(t2 != null);
1216
1217 CheckContextMatch(t1);
1218 CheckContextMatch(t2);
1219 return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1220 }

◆ MkPrefixOf()

BoolExpr MkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 2540 of file Context.cs.

2541 {
2542 Debug.Assert(s1 != null);
2543 Debug.Assert(s2 != null);
2544 CheckContextMatch(s1, s2);
2545 return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2546 }

◆ MkProbe()

Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3875 of file Context.cs.

3876 {
3877
3878 return new Probe(this, name);
3879 }

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

3317 {
3318 Debug.Assert(body != null);
3319 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3320 Debug.Assert(patterns == null || patterns.All(p => p != null));
3321 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3322
3323
3324 if (universal)
3325 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3326 else
3327 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3328 }
Microsoft.Z3.Context.MkExists
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.
Definition Context.cs:3256
Microsoft.Z3.Context.MkForall
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.
Definition Context.cs:3214

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

3294 {
3295 Debug.Assert(body != null);
3296 Debug.Assert(names != null);
3297 Debug.Assert(sorts != null);
3298 Debug.Assert(sorts.Length == names.Length);
3299 Debug.Assert(sorts.All(s => s != null));
3300 Debug.Assert(names.All(n => n != null));
3301 Debug.Assert(patterns == null || patterns.All(p => p != null));
3302 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3303
3304
3305 if (universal)
3306 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3307 else
3308 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3309 }

◆ MkRange()

ReExpr MkRange ( SeqExpr  lo,
SeqExpr  hi 
)
inline

Create a range expression.

Definition at line 2787 of file Context.cs.

2788 {
2789 Debug.Assert(lo != null);
2790 Debug.Assert(hi != null);
2791 CheckContextMatch(lo, hi);
2792 return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
2793 }

◆ MkReal() [1/6]

RatNum MkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

Parameters
numnumerator of rational.
dendenominator of rational.
Returns
A Term with value num /den and sort Real
See also
MkNumeral(string, Sort)

Definition at line 2997 of file Context.cs.

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

◆ MkReal() [2/6]

RatNum MkReal ( int  v)
inline

Create a real numeral.

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

Definition at line 3021 of file Context.cs.

3022 {
3023
3024 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
3025 }
Microsoft.Z3.Context.RealSort
RealSort RealSort
Retrieves the Real sort of the context.
Definition Context.cs:170

◆ MkReal() [3/6]

RatNum MkReal ( long  v)
inline

Create a real numeral.

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

Definition at line 3043 of file Context.cs.

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

◆ MkReal() [4/6]

RatNum MkReal ( string  v)
inline

Create a real numeral.

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

Definition at line 3010 of file Context.cs.

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

◆ MkReal() [5/6]

RatNum MkReal ( uint  v)
inline

Create a real numeral.

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

Definition at line 3032 of file Context.cs.

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

◆ MkReal() [6/6]

RatNum MkReal ( ulong  v)
inline

Create a real numeral.

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

Definition at line 3054 of file Context.cs.

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

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

1300 {
1301 Debug.Assert(t != null);
1302
1303 CheckContextMatch(t);
1304 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1305 }

◆ MkRealConst() [1/2]

RealExpr MkRealConst ( string  name)
inline

Creates a real constant.

Definition at line 865 of file Context.cs.

866 {
867
868 return (RealExpr)MkConst(name, RealSort);
869 }

◆ MkRealConst() [2/2]

RealExpr MkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 855 of file Context.cs.

856 {
857 Debug.Assert(name != null);
858
859 return (RealExpr)MkConst(name, RealSort);
860 }

◆ MkRealSort()

RealSort MkRealSort ( )
inline

Create a real sort.

Definition at line 242 of file Context.cs.

243 {
244 return new RealSort(this);
245 }

◆ MkRecFuncDecl()

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

Creates a new recursive function declaration.

Definition at line 630 of file Context.cs.

631 {
632 Debug.Assert(range != null);
633 Debug.Assert(domain.All(d => d != null));
634
635 CheckContextMatch<Sort>(domain);
636 CheckContextMatch(range);
637 using var symbol = MkSymbol(name);
638 return new FuncDecl(this, symbol, domain, range, true);
639 }

◆ MkRem()

IntExpr MkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 1199 of file Context.cs.

1200 {
1201 Debug.Assert(t1 != null);
1202 Debug.Assert(t2 != null);
1203
1204 CheckContextMatch(t1);
1205 CheckContextMatch(t2);
1206 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1207 }

◆ MkRepeat()

BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1795 of file Context.cs.

1796 {
1797 Debug.Assert(t != null);
1798
1799 CheckContextMatch(t);
1800 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1801 }

◆ MkReplace()

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

Replace the first occurrence of src by dst in s.

Definition at line 2641 of file Context.cs.

2642 {
2643 Debug.Assert(s != null);
2644 Debug.Assert(src != null);
2645 Debug.Assert(dst != null);
2646 CheckContextMatch(s, src, dst);
2647 return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2648 }

◆ MkReSort()

ReSort MkReSort ( SeqSort  s)
inline

Create a new regular expression sort.

Definition at line 267 of file Context.cs.

268 {
269 Debug.Assert(s != null);
270 return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
271 }
z3py.ReSort
ReSort(s)
Definition z3py.py:11496

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

2145 {
2146 Debug.Assert(a != null);
2147 Debug.Assert(i != null);
2148
2149 CheckContextMatch(a);
2150 CheckContextMatch(i);
2151 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2152 }

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

2168 {
2169 Debug.Assert(a != null);
2170 Debug.Assert(args != null && args.All(n => n != null));
2171
2172 CheckContextMatch(a);
2173 CheckContextMatch<Expr>(args);
2174 return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2175 }

◆ MkSeqSort()

SeqSort MkSeqSort ( Sort  s)
inline

Create a new sequence sort.

Definition at line 258 of file Context.cs.

259 {
260 Debug.Assert(s != null);
261 return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
262 }
z3py.SeqSort
SeqSort(s)
Definition z3py.py:11062

◆ MkSetAdd()

ArrayExpr MkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2345 of file Context.cs.

2346 {
2347 Debug.Assert(set != null);
2348 Debug.Assert(element != null);
2349
2350 CheckContextMatch(set);
2351 CheckContextMatch(element);
2352 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2353 }

◆ MkSetComplement()

ArrayExpr MkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 2409 of file Context.cs.

2410 {
2411 Debug.Assert(arg != null);
2412
2413 CheckContextMatch(arg);
2414 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2415 }

◆ MkSetDel()

ArrayExpr MkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 2359 of file Context.cs.

2360 {
2361 Debug.Assert(set != null);
2362 Debug.Assert(element != null);
2363
2364 CheckContextMatch(set);
2365 CheckContextMatch(element);
2366 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2367 }

◆ MkSetDifference()

ArrayExpr MkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2396 of file Context.cs.

2397 {
2398 Debug.Assert(arg1 != null);
2399 Debug.Assert(arg2 != null);
2400
2401 CheckContextMatch(arg1);
2402 CheckContextMatch(arg2);
2403 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2404 }

◆ MkSetIntersection()

ArrayExpr MkSetIntersection ( params ArrayExpr[]  args)
inline

Take the intersection of a list of sets.

Definition at line 2384 of file Context.cs.

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

◆ MkSetMembership()

BoolExpr MkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 2420 of file Context.cs.

2421 {
2422 Debug.Assert(elem != null);
2423 Debug.Assert(set != null);
2424
2425 CheckContextMatch(elem);
2426 CheckContextMatch(set);
2427 return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2428 }

◆ MkSetSort()

SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2312 of file Context.cs.

2313 {
2314 Debug.Assert(ty != null);
2315
2316 CheckContextMatch(ty);
2317 return new SetSort(this, ty);
2318 }
z3py.SetSort
SetSort(s)
Sets.
Definition z3py.py:5044

◆ MkSetSubset()

BoolExpr MkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2433 of file Context.cs.

2434 {
2435 Debug.Assert(arg1 != null);
2436 Debug.Assert(arg2 != null);
2437
2438 CheckContextMatch(arg1);
2439 CheckContextMatch(arg2);
2440 return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2441 }

◆ MkSetUnion()

ArrayExpr MkSetUnion ( params ArrayExpr[]  args)
inline

Take the union of a list of sets.

Definition at line 2372 of file Context.cs.

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

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

1765 {
1766 Debug.Assert(t != null);
1767
1768 CheckContextMatch(t);
1769 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1770 }

◆ MkSimpleSolver()

Solver MkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 4032 of file Context.cs.

4033 {
4034
4035 return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
4036 }

◆ MkSimplifier()

Simplifier MkSimplifier ( string  name)
inline

Creates a new Tactic.

Definition at line 3771 of file Context.cs.

3772 {
3773
3774 return new Simplifier(this, name);
3775 }

◆ MkSolver() [1/4]

Solver MkSolver ( Solver  s,
Simplifier  t 
)
inline

Creates a solver that uses an incremental simplifier.

Definition at line 4041 of file Context.cs.

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

◆ MkSolver() [2/4]

Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 4023 of file Context.cs.

4024 {
4025 using var symbol = MkSymbol(logic);
4026 return MkSolver(symbol);
4027 }
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition Context.cs:4010

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

4011 {
4012
4013 if (logic == null)
4014 return new Solver(this, Native.Z3_mk_solver(nCtx));
4015 else
4016 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
4017 }

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

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

◆ MkStar()

ReExpr MkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2674 of file Context.cs.

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

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

2197 {
2198 Debug.Assert(a != null);
2199 Debug.Assert(i != null);
2200 Debug.Assert(v != null);
2201
2202 CheckContextMatch(a);
2203 CheckContextMatch(i);
2204 CheckContextMatch(v);
2205 return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2206 }

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

2227 {
2228 Debug.Assert(a != null);
2229 Debug.Assert(args != null);
2230 Debug.Assert(v != null);
2231
2232 CheckContextMatch<Expr>(args);
2233 CheckContextMatch(a);
2234 CheckContextMatch(v);
2235 return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
2236 }

◆ MkString()

SeqExpr MkString ( string  s)
inline

Create a string constant.

Definition at line 2468 of file Context.cs.

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

◆ MkStringLe()

BoolExpr MkStringLe ( SeqExpr  s1,
SeqExpr  s2 
)
inline

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

Definition at line 2584 of file Context.cs.

2585 {
2586 Debug.Assert(s1 != null);
2587 Debug.Assert(s2 != null);
2588 CheckContextMatch(s1, s2);
2589 return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2590 }

◆ MkStringLt()

BoolExpr MkStringLt ( SeqExpr  s1,
SeqExpr  s2 
)
inline

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

Definition at line 2573 of file Context.cs.

2574 {
2575 Debug.Assert(s1 != null);
2576 Debug.Assert(s2 != null);
2577 CheckContextMatch(s1, s2);
2578 return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2579 }

◆ MkSub()

ArithExpr MkSub ( params ArithExpr[]  ts)
inline

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

Definition at line 1148 of file Context.cs.

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

Referenced by ArithExpr.operator-().

◆ MkSuffixOf()

BoolExpr MkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 2551 of file Context.cs.

2552 {
2553 Debug.Assert(s1 != null);
2554 Debug.Assert(s2 != null);
2555 CheckContextMatch(s1, s2);
2556 return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2557 }

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

112 {
113 return new IntSymbol(this, i);
114 }

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.MkRecFuncDecl(), Context.MkSolver(), 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.

120 {
121 return new StringSymbol(this, name);
122 }

◆ MkTactic()

Tactic MkTactic ( string  name)
inline

Creates a new Tactic.

Definition at line 3509 of file Context.cs.

3510 {
3511
3512 return new Tactic(this, name);
3513 }

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

2286 {
2287 Debug.Assert(array != null);
2288
2289 CheckContextMatch(array);
2290 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2291 }

◆ MkToRe()

ReExpr MkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2653 of file Context.cs.

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

◆ MkTrue()

BoolExpr MkTrue ( )
inline

The true Term.

Definition at line 918 of file Context.cs.

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

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

◆ MkTupleSort()

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

Create a new tuple sort.

Definition at line 302 of file Context.cs.

303 {
304 Debug.Assert(name != null);
305 Debug.Assert(fieldNames != null);
306 Debug.Assert(fieldNames.All(fn => fn != null));
307 Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null));
308
309 CheckContextMatch(name);
310 CheckContextMatch<Symbol>(fieldNames);
311 CheckContextMatch<Sort>(fieldSorts);
312 return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
313 }
z3py.TupleSort
TupleSort(name, sorts, ctx=None)
Definition z3py.py:5510

◆ MkUnaryMinus()

ArithExpr MkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing -t.

Definition at line 1160 of file Context.cs.

1161 {
1162 Debug.Assert(t != null);
1163
1164 CheckContextMatch(t);
1165 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1166 }

Referenced by ArithExpr.operator-().

◆ MkUninterpretedSort() [1/2]

UninterpretedSort MkUninterpretedSort ( string  str)
inline

Create a new uninterpreted sort.

Definition at line 224 of file Context.cs.

225 {
226 using var sym = MkSymbol(str);
227 return MkUninterpretedSort(sym);
228 }
Microsoft.Z3.Context.MkUninterpretedSort
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition Context.cs:213

◆ MkUninterpretedSort() [2/2]

UninterpretedSort MkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 213 of file Context.cs.

214 {
215 Debug.Assert(s != null);
216
217 CheckContextMatch(s);
218 return new UninterpretedSort(this, s);
219 }

Referenced by Context.MkUninterpretedSort().

◆ MkUnion()

ReExpr MkUnion ( params ReExpr[]  t)
inline

Create the union of regular languages.

Definition at line 2731 of file Context.cs.

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

◆ MkUnit()

SeqExpr MkUnit ( Expr  elem)
inline

Create the singleton sequence.

Definition at line 2459 of file Context.cs.

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

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

572 {
573 return Expr.Create(this, Native.Z3_datatype_update_field(
574 nCtx, field.NativeObject,
575 t.NativeObject, v.NativeObject));
576 }

◆ MkUserPropagatorFuncDecl()

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

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


Definition at line 727 of file Context.cs.

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

◆ MkXor() [1/2]

BoolExpr MkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 1030 of file Context.cs.

1031 {
1032 Debug.Assert(t1 != null);
1033 Debug.Assert(t2 != null);
1034
1035 CheckContextMatch(t1);
1036 CheckContextMatch(t2);
1037 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
1038 }

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

1044 {
1045 Debug.Assert(args != null);
1046 var ts = args.ToArray();
1047 Debug.Assert(ts.All(a => a != null));
1048 CheckContextMatch<BoolExpr>(ts);
1049
1050 return ts.Aggregate(MkFalse(), (r, t) =>
1051 {
1052 using (r)
1053 return MkXor(r, t);
1054 });
1055 }
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition Context.cs:1030

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

1782 {
1783 Debug.Assert(t != null);
1784
1785 CheckContextMatch(t);
1786 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1787 }

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

3993 {
3994 Debug.Assert(p != null);
3995
3996 CheckContextMatch(p);
3997 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3998 }

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

3979 {
3980 Debug.Assert(p1 != null);
3981 Debug.Assert(p2 != null);
3982
3983 CheckContextMatch(p1);
3984 CheckContextMatch(p2);
3985 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3986 }

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

3567 {
3568 Debug.Assert(t1 != null);
3569 Debug.Assert(t2 != null);
3570
3571 CheckContextMatch(t1);
3572 CheckContextMatch(t2);
3573 return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3574 }

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

3715 {
3716 Debug.Assert(t1 != null);
3717 Debug.Assert(t2 != null);
3718
3719 CheckContextMatch(t1);
3720 CheckContextMatch(t2);
3721 return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3722 }

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

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

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

3428 {
3429
3430 uint csn = Symbol.ArrayLength(sortNames);
3431 uint cs = Sort.ArrayLength(sorts);
3432 uint cdn = Symbol.ArrayLength(declNames);
3433 uint cd = AST.ArrayLength(decls);
3434 if (csn != cs || cdn != cd)
3435 throw new Z3Exception("Argument size mismatch");
3436 using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3437 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3438 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3439 return assertions.ToBoolExprArray();
3440 }

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

3409 {
3410
3411 uint csn = Symbol.ArrayLength(sortNames);
3412 uint cs = Sort.ArrayLength(sorts);
3413 uint cdn = Symbol.ArrayLength(declNames);
3414 uint cd = AST.ArrayLength(decls);
3415 if (csn != cs || cdn != cd)
3416 throw new Z3Exception("Argument size mismatch");
3417 using ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3418 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3419 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3420 return assertions.ToBoolExprArray();
3421 }

◆ ProbeDescription()

string ProbeDescription ( string  name)
inline

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

Definition at line 3866 of file Context.cs.

3867 {
3868
3869 return Native.Z3_probe_get_descr(nCtx, name);
3870 }

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

3628 {
3629 Debug.Assert(t != null);
3630
3631 CheckContextMatch(t);
3632 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3633 }

◆ SbvToString()

SeqExpr SbvToString ( Expr  e)
inline

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

Definition at line 2497 of file Context.cs.

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

◆ SimplifierDescription()

string SimplifierDescription ( string  name)
inline

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

Definition at line 3762 of file Context.cs.

3763 {
3764
3765 return Native.Z3_simplifier_get_descr(nCtx, name);
3766 }

◆ SimplifyHelp()

string SimplifyHelp ( )
inline

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

Definition at line 4855 of file Context.cs.

4856 {
4857
4858 return Native.Z3_simplify_get_help(nCtx);
4859 }

◆ Skip()

Tactic Skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 3638 of file Context.cs.

3639 {
3640
3641 return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3642 }

◆ StringToInt()

IntExpr StringToInt ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 2507 of file Context.cs.

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

◆ TacticDescription()

string TacticDescription ( string  name)
inline

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

Definition at line 3500 of file Context.cs.

3501 {
3502
3503 return Native.Z3_tactic_get_descr(nCtx, name);
3504 }

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

3816 {
3817 Debug.Assert(t1 != null);
3818 Debug.Assert(t2 != null);
3819 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3820
3821 return AndThen(t1, t2, ts);
3822 }
Microsoft.Z3.Context.AndThen
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 .
Definition Context.cs:3519

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

3554 {
3555 Debug.Assert(t1 != null);
3556 Debug.Assert(t2 != null);
3557 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3558
3559 return AndThen(t1, t2, ts);
3560 }

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

3583 {
3584 Debug.Assert(t != null);
3585
3586 CheckContextMatch(t);
3587 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3588 }

◆ UbvToString()

SeqExpr UbvToString ( Expr  e)
inline

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

Definition at line 2487 of file Context.cs.

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

◆ 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
aThe AST to unwrap.

Definition at line 4847 of file Context.cs.

4848 {
4849 return a.NativeObject;
4850 }

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

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

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

3828 {
3829 Debug.Assert(t != null);
3830 Debug.Assert(p != null);
3831
3832 CheckContextMatch(t);
3833 CheckContextMatch(p);
3834 return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
3835 }

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

3678 {
3679 Debug.Assert(t != null);
3680 Debug.Assert(p != null);
3681
3682 CheckContextMatch(t);
3683 CheckContextMatch(p);
3684 return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3685 }

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

3598 {
3599 Debug.Assert(p != null);
3600 Debug.Assert(t != null);
3601
3602 CheckContextMatch(t);
3603 CheckContextMatch(p);
3604 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3605 }

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

3692 {
3693 Debug.Assert(t != null);
3694 Debug.Assert(p != null);
3695
3696 return UsingParams(t, p);
3697 }
Microsoft.Z3.Context.UsingParams
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition Context.cs:3677

◆ 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
nativeObjectThe native pointer to wrap.

Definition at line 4831 of file Context.cs.

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

Property Documentation

◆ BoolSort

BoolSort BoolSort
get

Retrieves the Boolean sort of the context.

Definition at line 146 of file Context.cs.

147 {
148 get
149 {
150 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
151 }
152 }

Referenced by Context.MkBoolSort().

◆ CharSort

CharSort CharSort
get

Retrieves the String sort of the context.

Definition at line 180 of file Context.cs.

181 {
182 get
183 {
184 if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
185 }
186 }
Microsoft.Z3.Context.CharSort
CharSort CharSort
Retrieves the String sort of the context.
Definition Context.cs:181

◆ IntSort

IntSort IntSort
get

Retrieves the Integer sort of the context.

Definition at line 157 of file Context.cs.

158 {
159 get
160 {
161 if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
162 }
163 }

Referenced by Context.MkIntSort().

◆ NumProbes

uint NumProbes
get

The number of supported Probes.

Definition at line 3842 of file Context.cs.

3843 {
3844 get { return Native.Z3_get_num_probes(nCtx); }
3845 }

◆ NumSimplifiers

uint NumSimplifiers
get

The number of supported simplifiers.

Definition at line 3738 of file Context.cs.

3739 {
3740 get { return Native.Z3_get_num_simplifiers(nCtx); }
3741 }

◆ NumTactics

uint NumTactics
get

The number of supported tactics.

Definition at line 3476 of file Context.cs.

3477 {
3478 get { return Native.Z3_get_num_tactics(nCtx); }
3479 }

◆ PrintMode

Z3_ast_print_mode PrintMode
set

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

3397 {
3398 set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3399 }

◆ ProbeNames

string [] ProbeNames
get

The names of all supported Probes.

Definition at line 3850 of file Context.cs.

3851 {
3852 get
3853 {
3854
3855 uint n = NumProbes;
3856 string[] res = new string[n];
3857 for (uint i = 0; i < n; i++)
3858 res[i] = Native.Z3_get_probe_name(nCtx, i);
3859 return res;
3860 }
3861 }
Microsoft.Z3.Context.NumProbes
uint NumProbes
The number of supported Probes.
Definition Context.cs:3843

◆ RealSort

RealSort RealSort
get

Retrieves the Real sort of the context.

Definition at line 169 of file Context.cs.

170 {
171 get
172 {
173 if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
174 }
175 }

Referenced by Context.MkRealSort().

◆ SimplifierNames

string [] SimplifierNames
get

The names of all supported tactics.

Definition at line 3746 of file Context.cs.

3747 {
3748 get
3749 {
3750
3751 uint n = NumSimplifiers;
3752 string[] res = new string[n];
3753 for (uint i = 0; i < n; i++)
3754 res[i] = Native.Z3_get_simplifier_name(nCtx, i);
3755 return res;
3756 }
3757 }
Microsoft.Z3.Context.NumSimplifiers
uint NumSimplifiers
The number of supported simplifiers.
Definition Context.cs:3739

◆ SimplifyParameterDescriptions

ParamDescrs SimplifyParameterDescriptions
get

Retrieves parameter descriptions for simplifier.

Definition at line 4864 of file Context.cs.

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

◆ StringSort

SeqSort StringSort
get

Retrieves the String sort of the context.

Definition at line 192 of file Context.cs.

193 {
194 get
195 {
196 if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
197 return m_stringSort;
198 }
199 }

◆ TacticNames

string [] TacticNames
get

The names of all supported tactics.

Definition at line 3484 of file Context.cs.

3485 {
3486 get
3487 {
3488
3489 uint n = NumTactics;
3490 string[] res = new string[n];
3491 for (uint i = 0; i < n; i++)
3492 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3493 return res;
3494 }
3495 }
Microsoft.Z3.Context.NumTactics
uint NumTactics
The number of supported tactics.
Definition Context.cs:3477
Generated on Sat Dec 20 2025 19:33:22 for Z3 by doxygen 1.9.8