Z3 |

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. More...
| Context (Dictionary< string, string > settings)
| Constructor. More...
IntSymbol | MkSymbol (int i)
| Creates a new symbol using an integer. More...
StringSymbol | MkSymbol (string name)
| Create a symbol using a string. More...
BoolSort | MkBoolSort ()
| Create a new Boolean sort. More...
UninterpretedSort | MkUninterpretedSort (Symbol s)
| Create a new uninterpreted sort. More...
UninterpretedSort | MkUninterpretedSort (string str)
| Create a new uninterpreted sort. More...
IntSort | MkIntSort ()
| Create a new integer sort. More...
RealSort | MkRealSort ()
| Create a real sort. More...
BitVecSort | MkBitVecSort (uint size)
| Create a new bit-vector sort. More...
SeqSort | MkSeqSort (Sort s)
| Create a new sequence sort. More...
ReSort | MkReSort (SeqSort s)
| Create a new regular expression sort. More...
ArraySort | MkArraySort (Sort domain, Sort range)
| Create a new array sort. More...
ArraySort | MkArraySort (Sort[] domain, Sort range)
| Create a new n-ary array sort. More...
TupleSort | MkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
| Create a new tuple sort. More...
EnumSort | MkEnumSort (Symbol name, params Symbol[] enumNames)
| Create a new enumeration sort. More...
EnumSort | MkEnumSort (string name, params string[] enumNames)
| Create a new enumeration sort. More...
ListSort | MkListSort (Symbol name, Sort elemSort)
| Create a new list sort. More...
ListSort | MkListSort (string name, Sort elemSort)
| Create a new list sort. More...
FiniteDomainSort | MkFiniteDomainSort (Symbol name, ulong size)
| Create a new finite domain sort. Returns The result is a sort More...
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`. More...
Constructor | MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
| Create a datatype constructor. More...
Constructor | MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
| Create a datatype constructor. More...
DatatypeSort | MkDatatypeSort (Symbol name, Constructor[] constructors)
| Create a new datatype sort. More...
DatatypeSort | MkDatatypeSort (string name, Constructor[] constructors)
| Create a new datatype sort. More...
DatatypeSort[] | MkDatatypeSorts (Symbol[] names, Constructor[][] c)
| Create mutually recursive datatypes. More...
DatatypeSort[] | MkDatatypeSorts (string[] names, Constructor[][] c)
| Create mutually recursive data-types. More...
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. More...
FuncDecl | MkFuncDecl (Symbol name, Sort[] domain, Sort range)
| Creates a new function declaration. More...
FuncDecl | MkFuncDecl (Symbol name, Sort domain, Sort range)
| Creates a new function declaration. More...
FuncDecl | MkFuncDecl (string name, Sort[] domain, Sort range)
| Creates a new function declaration. More...
FuncDecl | MkRecFuncDecl (string name, Sort[] domain, Sort range)
| Creates a new recursive function declaration. More...
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. More...
FuncDecl | MkFuncDecl (string name, Sort domain, Sort range)
| Creates a new function declaration. More...
FuncDecl | MkFreshFuncDecl (string prefix, Sort[] domain, Sort range)
| Creates a fresh function declaration with a name prefixed with prefix . More...
FuncDecl | MkConstDecl (Symbol name, Sort range)
| Creates a new constant function declaration. More...
FuncDecl | MkConstDecl (string name, Sort range)
| Creates a new constant function declaration. More...
FuncDecl | MkFreshConstDecl (string prefix, Sort range)
| Creates a fresh constant function declaration with a name prefixed with prefix . More...
Expr | MkBound (uint index, Sort ty)
| Creates a new bound variable. More...
Pattern | MkPattern (params Expr[] terms)
| Create a quantifier pattern. More...
Expr | MkConst (Symbol name, Sort range)
| Creates a new Constant of sort range and named name . More...
Expr | MkConst (string name, Sort range)
| Creates a new Constant of sort range and named name . More...
Expr | MkFreshConst (string prefix, Sort range)
| Creates a fresh Constant of sort range and a name prefixed with prefix . More...
Expr | MkConst (FuncDecl f)
| Creates a fresh constant from the FuncDecl f . More...
BoolExpr | MkBoolConst (Symbol name)
| Create a Boolean constant. More...
BoolExpr | MkBoolConst (string name)
| Create a Boolean constant. More...
IntExpr | MkIntConst (Symbol name)
| Creates an integer constant. More...
IntExpr | MkIntConst (string name)
| Creates an integer constant. More...
RealExpr | MkRealConst (Symbol name)
| Creates a real constant. More...
RealExpr | MkRealConst (string name)
| Creates a real constant. More...
BitVecExpr | MkBVConst (Symbol name, uint size)
| Creates a bit-vector constant. More...
BitVecExpr | MkBVConst (string name, uint size)
| Creates a bit-vector constant. More...
Expr | MkApp (FuncDecl f, params Expr[] args)
| Create a new function application. More...
Expr | MkApp (FuncDecl f, IEnumerable< Expr > args)
| Create a new function application. More...
BoolExpr | MkTrue ()
| The true Term. More...
BoolExpr | MkFalse ()
| The false Term. More...
BoolExpr | MkBool (bool value)
| Creates a Boolean value. More...
BoolExpr | MkEq (Expr x, Expr y)
| Creates the equality x = y . More...
BoolExpr | MkDistinct (params Expr[] args)
| Creates a `distinct` term. More...
BoolExpr | MkNot (BoolExpr a)
| Mk an expression representing `not(a)`. More...
Expr | MkITE (BoolExpr t1, Expr t2, Expr t3)
| Create an expression representing an if-then-else: `ite(t1, t2, t3)`. More...
BoolExpr | MkIff (BoolExpr t1, BoolExpr t2)
| Create an expression representing `t1 iff t2`. More...
BoolExpr | MkImplies (BoolExpr t1, BoolExpr t2)
| Create an expression representing `t1 -> t2`. More...
BoolExpr | MkXor (BoolExpr t1, BoolExpr t2)
| Create an expression representing `t1 xor t2`. More...
BoolExpr | MkXor (IEnumerable< BoolExpr > ts)
| Create an expression representing `t1 xor t2 xor t3 ...` . More...
BoolExpr | MkAnd (params BoolExpr[] t)
| Create an expression representing `t[0] and t[1] and ...`. More...
BoolExpr | MkAnd (IEnumerable< BoolExpr > t)
| Create an expression representing `t[0] and t[1] and ...`. More...
BoolExpr | MkOr (params BoolExpr[] t)
| Create an expression representing `t[0] or t[1] or ...`. More...
BoolExpr | MkOr (IEnumerable< BoolExpr > t)
| Create an expression representing `t[0] or t[1] or ...`. More...
ArithExpr | MkAdd (params ArithExpr[] t)
| Create an expression representing `t[0] + t[1] + ...`. More...
ArithExpr | MkAdd (IEnumerable< ArithExpr > t)
| Create an expression representing `t[0] + t[1] + ...`. More...
ArithExpr | MkMul (params ArithExpr[] t)
| Create an expression representing `t[0] * t[1] * ...`. More...
ArithExpr | MkMul (IEnumerable< ArithExpr > t)
| Create an expression representing `t[0] * t[1] * ...`. More...
ArithExpr | MkSub (params ArithExpr[] t)
| Create an expression representing `t[0] - t[1] - ...`. More...
ArithExpr | MkUnaryMinus (ArithExpr t)
| Create an expression representing `-t`. More...
ArithExpr | MkDiv (ArithExpr t1, ArithExpr t2)
| Create an expression representing `t1 / t2`. More...
IntExpr | MkMod (IntExpr t1, IntExpr t2)
| Create an expression representing `t1 mod t2`. More...
IntExpr | MkRem (IntExpr t1, IntExpr t2)
| Create an expression representing `t1 rem t2`. More...
ArithExpr | MkPower (ArithExpr t1, ArithExpr t2)
| Create an expression representing `t1 ^ t2`. More...
BoolExpr | MkLt (ArithExpr t1, ArithExpr t2)
| Create an expression representing `t1 < t2` More...
BoolExpr | MkLe (ArithExpr t1, ArithExpr t2)
| Create an expression representing `t1 <= t2` More...
BoolExpr | MkGt (ArithExpr t1, ArithExpr t2)
| Create an expression representing `t1 > t2` More...
BoolExpr | MkGe (ArithExpr t1, ArithExpr t2)
| Create an expression representing `t1 >= t2` More...
RealExpr | MkInt2Real (IntExpr t)
| Coerce an integer to a real. More...
IntExpr | MkReal2Int (RealExpr t)
| Coerce a real to an integer. More...
BoolExpr | MkIsInteger (RealExpr t)
| Creates an expression that checks whether a real number is an integer. More...
BitVecExpr | MkBVNot (BitVecExpr t)
| Bitwise negation. More...
BitVecExpr | MkBVRedAND (BitVecExpr t)
| Take conjunction of bits in a vector, return vector of length 1. More...
BitVecExpr | MkBVRedOR (BitVecExpr t)
| Take disjunction of bits in a vector, return vector of length 1. More...
BitVecExpr | MkBVAND (BitVecExpr t1, BitVecExpr t2)
| Bitwise conjunction. More...
BitVecExpr | MkBVOR (BitVecExpr t1, BitVecExpr t2)
| Bitwise disjunction. More...
BitVecExpr | MkBVXOR (BitVecExpr t1, BitVecExpr t2)
| Bitwise XOR. More...
BitVecExpr | MkBVNAND (BitVecExpr t1, BitVecExpr t2)
| Bitwise NAND. More...
BitVecExpr | MkBVNOR (BitVecExpr t1, BitVecExpr t2)
| Bitwise NOR. More...
BitVecExpr | MkBVXNOR (BitVecExpr t1, BitVecExpr t2)
| Bitwise XNOR. More...
BitVecExpr | MkBVNeg (BitVecExpr t)
| Standard two's complement unary minus. More...
BitVecExpr | MkBVAdd (BitVecExpr t1, BitVecExpr t2)
| Two's complement addition. More...
BitVecExpr | MkBVSub (BitVecExpr t1, BitVecExpr t2)
| Two's complement subtraction. More...
BitVecExpr | MkBVMul (BitVecExpr t1, BitVecExpr t2)
| Two's complement multiplication. More...
BitVecExpr | MkBVUDiv (BitVecExpr t1, BitVecExpr t2)
| Unsigned division. More...
BitVecExpr | MkBVSDiv (BitVecExpr t1, BitVecExpr t2)
| Signed division. More...
BitVecExpr | MkBVURem (BitVecExpr t1, BitVecExpr t2)
| Unsigned remainder. More...
BitVecExpr | MkBVSRem (BitVecExpr t1, BitVecExpr t2)
| Signed remainder. More...
BitVecExpr | MkBVSMod (BitVecExpr t1, BitVecExpr t2)
| Two's complement signed remainder (sign follows divisor). More...
BoolExpr | MkBVULT (BitVecExpr t1, BitVecExpr t2)
| Unsigned less-than More...
BoolExpr | MkBVSLT (BitVecExpr t1, BitVecExpr t2)
| Two's complement signed less-than More...
BoolExpr | MkBVULE (BitVecExpr t1, BitVecExpr t2)
| Unsigned less-than or equal to. More...
BoolExpr | MkBVSLE (BitVecExpr t1, BitVecExpr t2)
| Two's complement signed less-than or equal to. More...
BoolExpr | MkBVUGE (BitVecExpr t1, BitVecExpr t2)
| Unsigned greater than or equal to. More...
BoolExpr | MkBVSGE (BitVecExpr t1, BitVecExpr t2)
| Two's complement signed greater than or equal to. More...
BoolExpr | MkBVUGT (BitVecExpr t1, BitVecExpr t2)
| Unsigned greater-than. More...
BoolExpr | MkBVSGT (BitVecExpr t1, BitVecExpr t2)
| Two's complement signed greater-than. More...
BitVecExpr | MkConcat (BitVecExpr t1, BitVecExpr t2)
| Bit-vector concatenation. More...
BitVecExpr | MkExtract (uint high, uint low, BitVecExpr t)
| Bit-vector extraction. More...
BitVecExpr | MkSignExt (uint i, BitVecExpr t)
| Bit-vector sign extension. More...
BitVecExpr | MkZeroExt (uint i, BitVecExpr t)
| Bit-vector zero extension. More...
BitVecExpr | MkRepeat (uint i, BitVecExpr t)
| Bit-vector repetition. More...
BitVecExpr | MkBVSHL (BitVecExpr t1, BitVecExpr t2)
| Shift left. More...
BitVecExpr | MkBVLSHR (BitVecExpr t1, BitVecExpr t2)
| Logical shift right More...
BitVecExpr | MkBVASHR (BitVecExpr t1, BitVecExpr t2)
| Arithmetic shift right More...
BitVecExpr | MkBVRotateLeft (uint i, BitVecExpr t)
| Rotate Left. More...
BitVecExpr | MkBVRotateRight (uint i, BitVecExpr t)
| Rotate Right. More...
BitVecExpr | MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
| Rotate Left. More...
BitVecExpr | MkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
| Rotate Right. More...
BitVecExpr | MkInt2BV (uint n, IntExpr t)
| Create an n bit bit-vector from the integer argument t . More...
IntExpr | MkBV2Int (BitVecExpr t, bool signed)
| Create an integer from the bit-vector argument t . More...
BoolExpr | MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
| Create a predicate that checks that the bit-wise addition does not overflow. More...
BoolExpr | MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
| Create a predicate that checks that the bit-wise addition does not underflow. More...
BoolExpr | MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
| Create a predicate that checks that the bit-wise subtraction does not overflow. More...
BoolExpr | MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
| Create a predicate that checks that the bit-wise subtraction does not underflow. More...
BoolExpr | MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
| Create a predicate that checks that the bit-wise signed division does not overflow. More...
BoolExpr | MkBVNegNoOverflow (BitVecExpr t)
| Create a predicate that checks that the bit-wise negation does not overflow. More...
BoolExpr | MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
| Create a predicate that checks that the bit-wise multiplication does not overflow. More...
BoolExpr | MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
| Create a predicate that checks that the bit-wise multiplication does not underflow. More...
ArrayExpr | MkArrayConst (Symbol name, Sort domain, Sort range)
| Create an array constant. More...
ArrayExpr | MkArrayConst (string name, Sort domain, Sort range)
| Create an array constant. More...
Expr | MkSelect (ArrayExpr a, Expr i)
| Array read. More...
Expr | MkSelect (ArrayExpr a, params Expr[] args)
| Array read. More...
ArrayExpr | MkStore (ArrayExpr a, Expr i, Expr v)
| Array update. More...
ArrayExpr | MkStore (ArrayExpr a, Expr[] args, Expr v)
| Array update. More...
ArrayExpr | MkConstArray (Sort domain, Expr v)
| Create a constant array. More...
ArrayExpr | MkMap (FuncDecl f, params ArrayExpr[] args)
| Maps f on the argument arrays. More...
Expr | MkTermArray (ArrayExpr array)
| Access the array default value. More...
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. More...
SetSort | MkSetSort (Sort ty)
| Create a set type. More...
ArrayExpr | MkEmptySet (Sort domain)
| Create an empty set. More...
ArrayExpr | MkFullSet (Sort domain)
| Create the full set. More...
ArrayExpr | MkSetAdd (ArrayExpr set, Expr element)
| Add an element to the set. More...
ArrayExpr | MkSetDel (ArrayExpr set, Expr element)
| Remove an element from a set. More...
ArrayExpr | MkSetUnion (params ArrayExpr[] args)
| Take the union of a list of sets. More...
ArrayExpr | MkSetIntersection (params ArrayExpr[] args)
| Take the intersection of a list of sets. More...
ArrayExpr | MkSetDifference (ArrayExpr arg1, ArrayExpr arg2)
| Take the difference between two sets. More...
ArrayExpr | MkSetComplement (ArrayExpr arg)
| Take the complement of a set. More...
BoolExpr | MkSetMembership (Expr elem, ArrayExpr set)
| Check for set membership. More...
BoolExpr | MkSetSubset (ArrayExpr arg1, ArrayExpr arg2)
| Check for subsetness of sets. More...
SeqExpr | MkEmptySeq (Sort s)
| Create the empty sequence. More...
SeqExpr | MkUnit (Expr elem)
| Create the singleton sequence. More...
SeqExpr | MkString (string s)
| Create a string constant. More...
SeqExpr | IntToString (Expr e)
| Convert an integer expression to a string. More...
IntExpr | StringToInt (Expr e)
| Convert an integer expression to a string. More...
SeqExpr | MkConcat (params SeqExpr[] t)
| Concatenate sequences. More...
IntExpr | MkLength (SeqExpr s)
| Retrieve the length of a given sequence. More...
BoolExpr | MkPrefixOf (SeqExpr s1, SeqExpr s2)
| Check for sequence prefix. More...
BoolExpr | MkSuffixOf (SeqExpr s1, SeqExpr s2)
| Check for sequence suffix. More...
BoolExpr | MkContains (SeqExpr s1, SeqExpr s2)
| Check for sequence containment of s2 in s1. More...
BoolExpr | MkStringLt (SeqExpr s1, SeqExpr s2)
| Check if the string s1 is lexicographically strictly less than s2. More...
BoolExpr | MkStringLe (SeqExpr s1, SeqExpr s2)
| Check if the string s1 is lexicographically strictly less than s2. More...
SeqExpr | MkAt (SeqExpr s, Expr index)
| Retrieve sequence of length one at index. More...
Expr | MkNth (SeqExpr s, Expr index)
| Retrieve element at index. More...
SeqExpr | MkExtract (SeqExpr s, IntExpr offset, IntExpr length)
| Extract subsequence. More...
IntExpr | MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset)
| Extract index of sub-string starting at offset. More...
SeqExpr | MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst)
| Replace the first occurrence of src by dst in s. More...
ReExpr | MkToRe (SeqExpr s)
| Convert a regular expression that accepts sequence s. More...
BoolExpr | MkInRe (SeqExpr s, ReExpr re)
| Check for regular expression membership. More...
ReExpr | MkStar (ReExpr re)
| Take the Kleene star of a regular expression. More...
ReExpr | MkLoop (ReExpr re, uint lo, uint hi=0)
| Take the bounded Kleene star of a regular expression. More...
ReExpr | MkPlus (ReExpr re)
| Take the Kleene plus of a regular expression. More...
ReExpr | MkOption (ReExpr re)
| Create the optional regular expression. More...
ReExpr | MkComplement (ReExpr re)
| Create the complement regular expression. More...
ReExpr | MkConcat (params ReExpr[] t)
| Create the concatenation of regular languages. More...
ReExpr | MkUnion (params ReExpr[] t)
| Create the union of regular languages. More...
ReExpr | MkIntersect (params ReExpr[] t)
| Create the intersection of regular languages. More...
ReExpr | MkEmptyRe (Sort s)
| Create the empty regular expression. The sort s should be a regular expression. More...
ReExpr | MkFullRe (Sort s)
| Create the full regular expression. The sort s should be a regular expression. More...
ReExpr | MkRange (SeqExpr lo, SeqExpr hi)
| Create a range expression. More...
BoolExpr | MkAtMost (IEnumerable< BoolExpr > args, uint k)
| Create an at-most-k constraint. More...
BoolExpr | MkAtLeast (IEnumerable< BoolExpr > args, uint k)
| Create an at-least-k constraint. More...
BoolExpr | MkPBLe (int[] coeffs, BoolExpr[] args, int k)
| Create a pseudo-Boolean less-or-equal constraint. More...
BoolExpr | MkPBGe (int[] coeffs, BoolExpr[] args, int k)
| Create a pseudo-Boolean greater-or-equal constraint. More...
BoolExpr | MkPBEq (int[] coeffs, BoolExpr[] args, int k)
| Create a pseudo-Boolean equal constraint. More...
Expr | MkNumeral (string v, Sort ty)
| Create a Term of a given sort. More...
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. More...
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. More...
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. More...
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. More...
RatNum | MkReal (int num, int den)
| Create a real from a fraction. More...
RatNum | MkReal (string v)
| Create a real numeral. More...
RatNum | MkReal (int v)
| Create a real numeral. More...
RatNum | MkReal (uint v)
| Create a real numeral. More...
RatNum | MkReal (long v)
| Create a real numeral. More...
RatNum | MkReal (ulong v)
| Create a real numeral. More...
IntNum | MkInt (string v)
| Create an integer numeral. More...
IntNum | MkInt (int v)
| Create an integer numeral. More...
IntNum | MkInt (uint v)
| Create an integer numeral. More...
IntNum | MkInt (long v)
| Create an integer numeral. More...
IntNum | MkInt (ulong v)
| Create an integer numeral. More...
BitVecNum | MkBV (string v, uint size)
| Create a bit-vector numeral. More...
BitVecNum | MkBV (int v, uint size)
| Create a bit-vector numeral. More...
BitVecNum | MkBV (uint v, uint size)
| Create a bit-vector numeral. More...
BitVecNum | MkBV (long v, uint size)
| Create a bit-vector numeral. More...
BitVecNum | MkBV (ulong v, uint size)
| Create a bit-vector numeral. More...
BitVecNum | MkBV (bool[] bits)
| Create a bit-vector numeral. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
Lambda | MkLambda (Sort[] sorts, Symbol[] names, Expr body)
| Create a lambda expression. More...
Lambda | MkLambda (Expr[] boundConstants, Expr body)
| Create a lambda expression. More...
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. More...
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. More...
Goal | MkGoal (bool models=true, bool unsatCores=false, bool proofs=false)
| Creates a new Goal. More...
Params | MkParams ()
| Creates a new ParameterSet. More...
string | TacticDescription (string name)
| Returns a string containing a description of the tactic with the given name. More...
Tactic | MkTactic (string name)
| Creates a new Tactic. More...
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 . More...
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 . More...
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. More...
Tactic | TryFor (Tactic t, uint ms)
| Create a tactic that applies t to a goal for ms milliseconds. More...
Tactic | When (Probe p, Tactic t)
| Create a tactic that applies t to a given goal if the probe p evaluates to true. More...
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. More...
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. More...
Tactic | Skip ()
| Create a tactic that just returns the given goal. More...
Tactic | Fail ()
| Create a tactic always fails. More...
Tactic | FailIf (Probe p)
| Create a tactic that fails if the probe p evaluates to false. More...
Tactic | FailIfNotDecided ()
| Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’). More...
Tactic | UsingParams (Tactic t, Params p)
| Create a tactic that applies t using the given set of parameters p . More...
Tactic | With (Tactic t, Params p)
| Create a tactic that applies t using the given set of parameters p . More...
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). More...
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. More...
void | Interrupt ()
| Interrupt the execution of a Z3 procedure. More...
string | ProbeDescription (string name)
| Returns a string containing a description of the probe with the given name. More...
Probe | MkProbe (string name)
| Creates a new Probe. More...
Probe | ConstProbe (double val)
| Create a probe that always evaluates to val . More...
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 More...
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 More...
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 More...
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 More...
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 More...
Probe | And (Probe p1, Probe p2)
| Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true". More...
Probe | Or (Probe p1, Probe p2)
| Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true". More...
Probe | Not (Probe p)
| Create a probe that evaluates to "true" when the value p does not evaluate to "true". More...
Solver | MkSolver (Symbol logic=null)
| Creates a new (incremental) solver. More...
Solver | MkSolver (string logic)
| Creates a new (incremental) solver. More...
Solver | MkSimpleSolver ()
| Creates a new (incremental) solver. More...
Solver | MkSolver (Tactic t)
| Creates a solver that is implemented using the given tactic. More...
Fixedpoint | MkFixedpoint ()
| Create a Fixedpoint context. More...
Optimize | MkOptimize ()
| Create an Optimization context. More...
FPRMSort | MkFPRoundingModeSort ()
| Create the floating-point RoundingMode sort. More...
FPRMExpr | MkFPRoundNearestTiesToEven ()
| Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More...
FPRMNum | MkFPRNE ()
| Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More...
FPRMNum | MkFPRoundNearestTiesToAway ()
| Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More...
FPRMNum | MkFPRNA ()
| Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More...
FPRMNum | MkFPRoundTowardPositive ()
| Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More...
FPRMNum | MkFPRTP ()
| Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More...
FPRMNum | MkFPRoundTowardNegative ()
| Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More...
FPRMNum | MkFPRTN ()
| Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More...
FPRMNum | MkFPRoundTowardZero ()
| Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More...
FPRMNum | MkFPRTZ ()
| Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More...
FPSort | MkFPSort (uint ebits, uint sbits)
| Create a FloatingPoint sort. More...
FPSort | MkFPSortHalf ()
| Create the half-precision (16-bit) FloatingPoint sort. More...
FPSort | MkFPSort16 ()
| Create the half-precision (16-bit) FloatingPoint sort. More...
FPSort | MkFPSortSingle ()
| Create the single-precision (32-bit) FloatingPoint sort. More...
FPSort | MkFPSort32 ()
| Create the single-precision (32-bit) FloatingPoint sort. More...
FPSort | MkFPSortDouble ()
| Create the double-precision (64-bit) FloatingPoint sort. More...
FPSort | MkFPSort64 ()
| Create the double-precision (64-bit) FloatingPoint sort. More...
FPSort | MkFPSortQuadruple ()
| Create the quadruple-precision (128-bit) FloatingPoint sort. More...
FPSort | MkFPSort128 ()
| Create the quadruple-precision (128-bit) FloatingPoint sort. More...
FPNum | MkFPNaN (FPSort s)
| Create a NaN of sort s. More...
FPNum | MkFPInf (FPSort s, bool negative)
| Create a floating-point infinity of sort s. More...
FPNum | MkFPZero (FPSort s, bool negative)
| Create a floating-point zero of sort s. More...
FPNum | MkFPNumeral (float v, FPSort s)
| Create a numeral of FloatingPoint sort from a float. More...
FPNum | MkFPNumeral (double v, FPSort s)
| Create a numeral of FloatingPoint sort from a float. More...
FPNum | MkFPNumeral (int v, FPSort s)
| Create a numeral of FloatingPoint sort from an int. More...
FPNum | MkFPNumeral (bool sgn, uint sig, int exp, FPSort s)
| Create a numeral of FloatingPoint sort from a sign bit and two integers. More...
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. More...
FPNum | MkFP (float v, FPSort s)
| Create a numeral of FloatingPoint sort from a float. More...
FPNum | MkFP (double v, FPSort s)
| Create a numeral of FloatingPoint sort from a float. More...
FPNum | MkFP (int v, FPSort s)
| Create a numeral of FloatingPoint sort from an int. More...
FPNum | MkFP (bool sgn, int exp, uint sig, FPSort s)
| Create a numeral of FloatingPoint sort from a sign bit and two integers. More...
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. More...
FPExpr | MkFPAbs (FPExpr t)
| Floating-point absolute value More...
FPExpr | MkFPNeg (FPExpr t)
| Floating-point negation More...
FPExpr | MkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
| Floating-point addition More...
FPExpr | MkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
| Floating-point subtraction More...
FPExpr | MkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
| Floating-point multiplication More...
FPExpr | MkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
| Floating-point division More...
FPExpr | MkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
| Floating-point fused multiply-add More...
FPExpr | MkFPSqrt (FPRMExpr rm, FPExpr t)
| Floating-point square root More...
FPExpr | MkFPRem (FPExpr t1, FPExpr t2)
| Floating-point remainder More...
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. More...
FPExpr | MkFPMin (FPExpr t1, FPExpr t2)
| Minimum of floating-point numbers. More...
FPExpr | MkFPMax (FPExpr t1, FPExpr t2)
| Maximum of floating-point numbers. More...
BoolExpr | MkFPLEq (FPExpr t1, FPExpr t2)
| Floating-point less than or equal. More...
BoolExpr | MkFPLt (FPExpr t1, FPExpr t2)
| Floating-point less than. More...
BoolExpr | MkFPGEq (FPExpr t1, FPExpr t2)
| Floating-point greater than or equal. More...
BoolExpr | MkFPGt (FPExpr t1, FPExpr t2)
| Floating-point greater than. More...
BoolExpr | MkFPEq (FPExpr t1, FPExpr t2)
| Floating-point equality. More...
BoolExpr | MkFPIsNormal (FPExpr t)
| Predicate indicating whether t is a normal floating-point number. More...
BoolExpr | MkFPIsSubnormal (FPExpr t)
| Predicate indicating whether t is a subnormal floating-point number. More...
BoolExpr | MkFPIsZero (FPExpr t)
| Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0. More...
BoolExpr | MkFPIsInfinite (FPExpr t)
| Predicate indicating whether t is a floating-point number representing +oo or -oo. More...
BoolExpr | MkFPIsNaN (FPExpr t)
| Predicate indicating whether t is a NaN. More...
BoolExpr | MkFPIsNegative (FPExpr t)
| Predicate indicating whether t is a negative floating-point number. More...
BoolExpr | MkFPIsPositive (FPExpr t)
| Predicate indicating whether t is a positive floating-point number. More...
FPExpr | MkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
| Create an expression of FloatingPoint sort from three bit-vector expressions. More...
FPExpr | MkFPToFP (BitVecExpr bv, FPSort s)
| Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. More...
FPExpr | MkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
| Conversion of a FloatingPoint term into another term of different FloatingPoint sort. More...
FPExpr | MkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
| Conversion of a term of real sort into a term of FloatingPoint sort. More...
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. More...
FPExpr | MkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
| Conversion of a floating-point number to another FloatingPoint sort s. More...
BitVecExpr | MkFPToBV (FPRMExpr rm, FPExpr t, uint sz, bool signed)
| Conversion of a floating-point term into a bit-vector. More...
RealExpr | MkFPToReal (FPExpr t)
| Conversion of a floating-point term into a real-numbered term. More...
BitVecExpr | MkFPToIEEEBV (FPExpr t)
| Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. More...
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. More...
AST | WrapAST (IntPtr nativeObject)
| Wraps an AST. More...
IntPtr | UnwrapAST (AST a)
| Unwraps an AST. More...
string | SimplifyHelp ()
| Return a string describing all available parameters to `Expr.Simplify`. More...
void | UpdateParamValue (string id, string value)
| Update a mutable configuration parameter. More...
void | Dispose ()
| Disposes of the context. More...

## Properties
BoolSort | BoolSort`[get]`
| Retrieves the Boolean sort of the context. More...
IntSort | IntSort`[get]`
| Retrieves the Integer sort of the context. More...
RealSort | RealSort`[get]`
| Retrieves the Real sort of the context. More...
SeqSort | StringSort`[get]`
| Retrieves the String sort of the context. More...
Z3_ast_print_mode | PrintMode`[set]`
| Selects the format used for pretty-printing expressions. More...
uint | NumTactics`[get]`
| The number of supported tactics. More...
string[] | TacticNames`[get]`
| The names of all supported tactics. More...
uint | NumProbes`[get]`
| The number of supported Probes. More...
string[] | ProbeNames`[get]`
| The names of all supported Probes. More...
ParamDescrs | SimplifyParameterDescriptions`[get]`
| Retrieves parameter descriptions for simplifier. More...
IDecRefQueue | AST_DRQ`[get]`
| AST DRQ More...
IDecRefQueue | ASTMap_DRQ`[get]`
| ASTMap DRQ More...
IDecRefQueue | ASTVector_DRQ`[get]`
| ASTVector DRQ More...
IDecRefQueue | ApplyResult_DRQ`[get]`
| ApplyResult DRQ More...
IDecRefQueue | FuncEntry_DRQ`[get]`
| FuncEntry DRQ More...
IDecRefQueue | FuncInterp_DRQ`[get]`
| FuncInterp DRQ More...
IDecRefQueue | Goal_DRQ`[get]`
| Goal DRQ More...
IDecRefQueue | Model_DRQ`[get]`
| Model DRQ More...
IDecRefQueue | Params_DRQ`[get]`
| Params DRQ More...
IDecRefQueue | ParamDescrs_DRQ`[get]`
| ParamDescrs DRQ More...
IDecRefQueue | Probe_DRQ`[get]`
| Probe DRQ More...
IDecRefQueue | Solver_DRQ`[get]`
| Solver DRQ More...
IDecRefQueue | Statistics_DRQ`[get]`
| Statistics DRQ More...
IDecRefQueue | Tactic_DRQ`[get]`
| Tactic DRQ More...
IDecRefQueue | Fixedpoint_DRQ`[get]`
| FixedPoint DRQ More...
IDecRefQueue | Optimize_DRQ`[get]`
| Optimize DRQ More...

## Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 31 of file Context.cs.

## Constructor & Destructor Documentation

## ◆ Context() [1/2]

Context | ( |  | ) |
| inline

Constructor.

Definition at line 37 of file Context.cs.

38 : base()
39 {
40 lock (creation_lock)
41 {
42 m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
43 InitContext();
44 }
45 }

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

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

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

554 {
555 CheckContextMatch(f);
556 CheckContextMatch<Expr>(args);
557 CheckContextMatch(body);
558 IntPtr[] argsNative = AST.ArrayToNative(args);
559 Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
560 }

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

3686 {
3687 Debug.Assert(p1 != null);
3688 Debug.Assert(p2 != null);
3689
3690 CheckContextMatch(p1);
3691 CheckContextMatch(p2);
3692 return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3693 }

## ◆ AndThen()

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

3345 {
3346 Debug.Assert(t1 != null);
3347 Debug.Assert(t2 != null);
3348 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3349
3350
3351 CheckContextMatch(t1);
3352 CheckContextMatch(t2);
3353 CheckContextMatch<Tactic>(ts);
3354
3355 IntPtr last = IntPtr.Zero;
3356 if (ts != null && ts.Length > 0)
3357 {
3358 last = ts[ts.Length - 1].NativeObject;
3359 for (int i = ts.Length - 2; i >= 0; i--)
3360 last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3361 }
3362 if (last != IntPtr.Zero)
3363 {
3364 last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3365 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3366 }
3367 else
3368 return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3369 }

Referenced by Context.Then().

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

3437 {
3438 Debug.Assert(p != null);
3439 Debug.Assert(t1 != null);
3440 Debug.Assert(t2 != null);
3441
3442 CheckContextMatch(p);
3443 CheckContextMatch(t1);
3444 CheckContextMatch(t2);
3445 return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3446 }

## ◆ ConstProbe()

Probe ConstProbe | ( | double | val | ) |
| inline

Create a probe that always evaluates to val .

Definition at line 3605 of file Context.cs.

3606 {
3607
3608 return new Probe(this, Native.Z3_probe_const(nCtx, val));
3609 }

## ◆ Dispose()

void Dispose | ( |  | ) |
| inline

Disposes of the context.

Definition at line 4816 of file Context.cs.

4817 {
4818 // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4819 AST_DRQ.Clear(this);
4820 ASTMap_DRQ.Clear(this);
4821 ASTVector_DRQ.Clear(this);
4822 ApplyResult_DRQ.Clear(this);
4823 FuncEntry_DRQ.Clear(this);
4824 FuncInterp_DRQ.Clear(this);
4825 Goal_DRQ.Clear(this);
4826 Model_DRQ.Clear(this);
4827 Params_DRQ.Clear(this);
4828 ParamDescrs_DRQ.Clear(this);
4829 Probe_DRQ.Clear(this);
4830 Solver_DRQ.Clear(this);
4831 Statistics_DRQ.Clear(this);
4832 Tactic_DRQ.Clear(this);
4833 Fixedpoint_DRQ.Clear(this);
4834 Optimize_DRQ.Clear(this);
4835
4836 m_boolSort = null;
4837 m_intSort = null;
4838 m_realSort = null;
4839 m_stringSort = null;
4840 if (refCount == 0 && m_ctx != IntPtr.Zero)
4841 {
4842 m_n_err_handler = null;
4843 IntPtr ctx = m_ctx;
4844 m_ctx = IntPtr.Zero;
4845 Native.Z3_del_context(ctx);
4846 }
4847 else
4848 GC.ReRegisterForFinalize(this);
4849 }
Microsoft.Z3.Context.ParamDescrs_DRQ
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Definition: Context.cs:4770
Microsoft.Z3.Context.Params_DRQ
IDecRefQueue Params_DRQ
Params DRQ
Definition: Context.cs:4765
Microsoft.Z3.Context.Model_DRQ
IDecRefQueue Model_DRQ
Model DRQ
Definition: Context.cs:4760
Microsoft.Z3.Context.Optimize_DRQ
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4800
Microsoft.Z3.Context.ApplyResult_DRQ
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
Definition: Context.cs:4740
Microsoft.Z3.Context.ASTVector_DRQ
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
Definition: Context.cs:4735
Microsoft.Z3.Context.Goal_DRQ
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4755
Microsoft.Z3.Context.Statistics_DRQ
IDecRefQueue Statistics_DRQ
Statistics DRQ
Definition: Context.cs:4785
Microsoft.Z3.Context.FuncEntry_DRQ
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
Definition: Context.cs:4745
Microsoft.Z3.Context.Solver_DRQ
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4780
Microsoft.Z3.Context.FuncInterp_DRQ
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Definition: Context.cs:4750
Microsoft.Z3.Context.AST_DRQ
IDecRefQueue AST_DRQ
AST DRQ
Definition: Context.cs:4725
Microsoft.Z3.Context.Fixedpoint_DRQ
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Definition: Context.cs:4795
Microsoft.Z3.Context.Tactic_DRQ
IDecRefQueue Tactic_DRQ
Tactic DRQ
Definition: Context.cs:4790
Microsoft.Z3.Context.Probe_DRQ
IDecRefQueue Probe_DRQ
Probe DRQ
Definition: Context.cs:4775
Microsoft.Z3.Context.ASTMap_DRQ
IDecRefQueue ASTMap_DRQ
ASTMap DRQ
Definition: Context.cs:4730

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

3672 {
3673 Debug.Assert(p1 != null);
3674 Debug.Assert(p2 != null);
3675
3676 CheckContextMatch(p1);
3677 CheckContextMatch(p2);
3678 return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3679 }

## ◆ Fail()

Tactic Fail | ( |  | ) |
| inline

Create a tactic always fails.

Definition at line 3472 of file Context.cs.

3473 {
3474
3475 return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3476 }

## ◆ FailIf()

Tactic FailIf | ( | Probe | p | ) |
| inline

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

Definition at line 3481 of file Context.cs.

3482 {
3483 Debug.Assert(p != null);
3484
3485 CheckContextMatch(p);
3486 return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3487 }

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

3494 {
3495
3496 return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3497 }

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

3658 {
3659 Debug.Assert(p1 != null);
3660 Debug.Assert(p2 != null);
3661
3662 CheckContextMatch(p1);
3663 CheckContextMatch(p2);
3664 return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3665 }

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

3630 {
3631 Debug.Assert(p1 != null);
3632 Debug.Assert(p2 != null);
3633
3634 CheckContextMatch(p1);
3635 CheckContextMatch(p2);
3636 return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3637 }

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

3554 {
3555 Native.Z3_interrupt(nCtx);
3556 }

## ◆ IntToString()

SeqExpr IntToString | ( | Expr | e | ) |
| inline

Convert an integer expression to a string.

Definition at line 2381 of file Context.cs.

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

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

3644 {
3645 Debug.Assert(p1 != null);
3646 Debug.Assert(p2 != null);
3647
3648 CheckContextMatch(p1);
3649 CheckContextMatch(p2);
3650 return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3651 }

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

3616 {
3617 Debug.Assert(p1 != null);
3618 Debug.Assert(p2 != null);
3619
3620 CheckContextMatch(p1);
3621 CheckContextMatch(p2);
3622 return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3623 }

## ◆ MkAdd() [1/2]

ArithExpr MkAdd | ( | IEnumerable< ArithExpr > | t | ) |
| inline

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

Definition at line 1019 of file Context.cs.

1020 {
1021 Debug.Assert(t != null);
1022 Debug.Assert(t.All(a => a != null));
1023
1024 CheckContextMatch(t);
1025 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1026 }

## ◆ MkAdd() [2/2]

ArithExpr MkAdd | ( | params ArithExpr[] | t | ) |
| inline

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

Definition at line 1007 of file Context.cs.

1008 {
1009 Debug.Assert(t != null);
1010 Debug.Assert(t.All(a => a != null));
1011
1012 CheckContextMatch<ArithExpr>(t);
1013 return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1014 }

Referenced by ArithExpr.operator+().

## ◆ MkAnd() [1/2]

BoolExpr MkAnd | ( | IEnumerable< BoolExpr > | t | ) |
| inline

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

Definition at line 968 of file Context.cs.

969 {
970 Debug.Assert(t != null);
971 Debug.Assert(t.All(a => a != null));
972 CheckContextMatch<BoolExpr>(t);
973 return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
974 }

## ◆ MkAnd() [2/2]

BoolExpr MkAnd | ( | params BoolExpr[] | t | ) |
| inline

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

Definition at line 956 of file Context.cs.

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

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

## ◆ MkApp() [1/2]

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

Create a new function application.

Definition at line 801 of file Context.cs.

802 {
803 Debug.Assert(f != null);
804 Debug.Assert(args == null || args.All( a => a != null));
805
806 CheckContextMatch(f);
807 CheckContextMatch(args);
808 return Expr.Create(this, f, args.ToArray());
809 }

## ◆ MkApp() [2/2]

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

Create a new function application.

Definition at line 788 of file Context.cs.

789 {
790 Debug.Assert(f != null);
791 Debug.Assert(args == null || args.All(a => a != null));
792
793 CheckContextMatch(f);
794 CheckContextMatch<Expr>(args);
795 return Expr.Create(this, f, args);
796 }

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

## ◆ MkArrayConst() [1/2]

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

Create an array constant.

Definition at line 2026 of file Context.cs.

2027 {
2028 Debug.Assert(domain != null);
2029 Debug.Assert(range != null);
2030
2031 return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2032 }
Microsoft.Z3.Context.MkConst
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:662
Microsoft.Z3.Context.MkArraySort
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:246
Microsoft.Z3.Context.MkSymbol
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:90
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725

## ◆ MkArrayConst() [2/2]

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

Create an array constant.

Definition at line 2014 of file Context.cs.

2015 {
2016 Debug.Assert(name != null);
2017 Debug.Assert(domain != null);
2018 Debug.Assert(range != null);
2019
2020 return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
2021 }

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

2201 {
2202 Debug.Assert(arg1 != null);
2203 Debug.Assert(arg2 != null);
2204
2205 CheckContextMatch(arg1);
2206 CheckContextMatch(arg2);
2207 return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2208 }

## ◆ MkArraySort() [1/2]

ArraySort MkArraySort | ( | Sort | domain,
|  | Sort | range
| ) |  |
| inline

Create a new array sort.

Definition at line 246 of file Context.cs.

247 {
248 Debug.Assert(domain != null);
249 Debug.Assert(range != null);
250
251 CheckContextMatch(domain);
252 CheckContextMatch(range);
253 return new ArraySort(this, domain, range);
254 }
z3py.ArraySort
def ArraySort(*sig)
Definition: z3py.py:4645

Referenced by Context.MkArrayConst().

## ◆ MkArraySort() [2/2]

ArraySort MkArraySort | ( | Sort[] | domain,
|  | Sort | range
| ) |  |
| inline

Create a new n-ary array sort.

Definition at line 259 of file Context.cs.

260 {
261 Debug.Assert(domain != null);
262 Debug.Assert(range != null);
263
264 CheckContextMatch<Sort>(domain);
265 CheckContextMatch(range);
266 return new ArraySort(this, domain, range);
267 }

## ◆ MkAt()

SeqExpr MkAt | ( | SeqExpr | s,
|  | Expr | index
| ) |  |
| inline

Retrieve sequence of length one at index.

Definition at line 2479 of file Context.cs.

2480 {
2481 Debug.Assert(s != null);
2482 Debug.Assert(index != null);
2483 CheckContextMatch(s, index);
2484 return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2485 }

## ◆ MkAtLeast()

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

Create an at-least-k constraint.

Definition at line 2686 of file Context.cs.

2687 {
2688 Debug.Assert(args != null);
2689 CheckContextMatch<BoolExpr>(args);
2690 return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(),
2691 AST.EnumToNative(args), k));
2692 }

## ◆ MkAtMost()

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

Create an at-most-k constraint.

Definition at line 2675 of file Context.cs.

2676 {
2677 Debug.Assert(args != null);
2678 CheckContextMatch<BoolExpr>(args);
2679 return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(),
2680 AST.EnumToNative(args), k));
2681 }

## ◆ MkBitVecSort()

BitVecSort MkBitVecSort | ( | uint | size | ) |
| inline

Create a new bit-vector sort.

Definition at line 219 of file Context.cs.

220 {
221 return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
222 }
z3py.BitVecSort
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967

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

## ◆ MkBool()

BoolExpr MkBool | ( | bool | value | ) |
| inline

Creates a Boolean value.

Definition at line 833 of file Context.cs.

834 {
835
836 return value ? MkTrue() : MkFalse();
837 }
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
Microsoft.Z3.Context.MkFalse
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:824

## ◆ MkBoolConst() [1/2]

BoolExpr MkBoolConst | ( | string | name | ) |
| inline

Create a Boolean constant.

Definition at line 719 of file Context.cs.

720 {
721
722 return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
723 }
Microsoft.Z3.Context.BoolSort
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:128

## ◆ MkBoolConst() [2/2]

BoolExpr MkBoolConst | ( | Symbol | name | ) |
| inline

Create a Boolean constant.

Definition at line 709 of file Context.cs.

710 {
711 Debug.Assert(name != null);
712
713 return (BoolExpr)MkConst(name, BoolSort);
714 }

## ◆ MkBoolSort()

BoolSort MkBoolSort | ( |  | ) |
| inline

Create a new Boolean sort.

Definition at line 174 of file Context.cs.

175 {
176 return new BoolSort(this);
177 }

## ◆ MkBound()

Expr MkBound | ( | uint | index,
|  | Sort | ty
| ) |  |
| inline

Creates a new bound variable.

Parameters

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

Definition at line 635 of file Context.cs.

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

## ◆ MkBV() [1/6]

BitVecNum MkBV | ( | bool[] | bits | ) |
| inline

Create a bit-vector numeral.

Parameters

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

Definition at line 3002 of file Context.cs.

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

## ◆ MkBV() [2/6]

BitVecNum MkBV | ( | int | v,
|  | uint | size
| ) |  |
| inline

Create a bit-vector numeral.

Parameters

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

Definition at line 2959 of file Context.cs.

2960 {
2961
2962 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2963 }
Microsoft.Z3.Context.MkBitVecSort
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:219
Microsoft.Z3.Context.MkNumeral
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2745

## ◆ MkBV() [3/6]

BitVecNum MkBV | ( | long | v,
|  | uint | size
| ) |  |
| inline

Create a bit-vector numeral.

Parameters

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

Definition at line 2981 of file Context.cs.

2982 {
2983
2984 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2985 }

## ◆ MkBV() [4/6]

BitVecNum MkBV | ( | string | v,
|  | uint | size
| ) |  |
| inline

Create a bit-vector numeral.

Parameters

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

Definition at line 2948 of file Context.cs.

2949 {
2950
2951 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2952 }

## ◆ MkBV() [5/6]

BitVecNum MkBV | ( | uint | v,
|  | uint | size
| ) |  |
| inline

Create a bit-vector numeral.

Parameters

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

Definition at line 2970 of file Context.cs.

2971 {
2972
2973 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2974 }

## ◆ MkBV() [6/6]

BitVecNum MkBV | ( | ulong | v,
|  | uint | size
| ) |  |
| inline

Create a bit-vector numeral.

Parameters

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

Definition at line 2992 of file Context.cs.

2993 {
2994
2995 return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2996 }

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

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

## ◆ MkBVAdd()

BitVecExpr MkBVAdd | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1363 of file Context.cs.

1364 {
1365 Debug.Assert(t1 != null);
1366 Debug.Assert(t2 != null);
1367
1368 CheckContextMatch(t1);
1369 CheckContextMatch(t2);
1370 return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1371 }

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

1890 {
1891 Debug.Assert(t1 != null);
1892 Debug.Assert(t2 != null);
1893
1894 CheckContextMatch(t1);
1895 CheckContextMatch(t2);
1896 return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1897 }

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

1906 {
1907 Debug.Assert(t1 != null);
1908 Debug.Assert(t2 != null);
1909
1910 CheckContextMatch(t1);
1911 CheckContextMatch(t2);
1912 return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1913 }

## ◆ MkBVAND()

BitVecExpr MkBVAND | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1267 of file Context.cs.

1268 {
1269 Debug.Assert(t1 != null);
1270 Debug.Assert(t2 != null);
1271
1272 CheckContextMatch(t1);
1273 CheckContextMatch(t2);
1274 return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1275 }

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

1769 {
1770 Debug.Assert(t1 != null);
1771 Debug.Assert(t2 != null);
1772
1773 CheckContextMatch(t1);
1774 CheckContextMatch(t2);
1775 return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1776 }

## ◆ MkBVConst() [1/2]

BitVecExpr MkBVConst | ( | string | name,
|  | uint | size
| ) |  |
| inline

Creates a bit-vector constant.

Definition at line 777 of file Context.cs.

778 {
779
780 return (BitVecExpr)MkConst(name, MkBitVecSort(size));
781 }

## ◆ MkBVConst() [2/2]

BitVecExpr MkBVConst | ( | Symbol | name,
|  | uint | size
| ) |  |
| inline

Creates a bit-vector constant.

Definition at line 767 of file Context.cs.

768 {
769 Debug.Assert(name != null);
770
771 return (BitVecExpr)MkConst(name, MkBitVecSort(size));
772 }

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

1745 {
1746 Debug.Assert(t1 != null);
1747 Debug.Assert(t2 != null);
1748
1749 CheckContextMatch(t1);
1750 CheckContextMatch(t2);
1751 return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1752 }

## ◆ MkBVMul()

BitVecExpr MkBVMul | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1391 of file Context.cs.

1392 {
1393 Debug.Assert(t1 != null);
1394 Debug.Assert(t2 != null);
1395
1396 CheckContextMatch(t1);
1397 CheckContextMatch(t2);
1398 return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1399 }

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

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

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

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

## ◆ MkBVNAND()

BitVecExpr MkBVNAND | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1309 of file Context.cs.

1310 {
1311 Debug.Assert(t1 != null);
1312 Debug.Assert(t2 != null);
1313
1314 CheckContextMatch(t1);
1315 CheckContextMatch(t2);
1316 return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1317 }

## ◆ MkBVNeg()

BitVecExpr MkBVNeg | ( | BitVecExpr | t | ) |
| inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1351 of file Context.cs.

1352 {
1353 Debug.Assert(t != null);
1354
1355 CheckContextMatch(t);
1356 return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1357 }

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

1970 {
1971 Debug.Assert(t != null);
1972
1973 CheckContextMatch(t);
1974 return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1975 }

## ◆ MkBVNOR()

BitVecExpr MkBVNOR | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1323 of file Context.cs.

1324 {
1325 Debug.Assert(t1 != null);
1326 Debug.Assert(t2 != null);
1327
1328 CheckContextMatch(t1);
1329 CheckContextMatch(t2);
1330 return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1331 }

## ◆ MkBVNot()

BitVecExpr MkBVNot | ( | BitVecExpr | t | ) |
| inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1231 of file Context.cs.

1232 {
1233 Debug.Assert(t != null);
1234
1235 CheckContextMatch(t);
1236 return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1237 }

## ◆ MkBVOR()

BitVecExpr MkBVOR | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1281 of file Context.cs.

1282 {
1283 Debug.Assert(t1 != null);
1284 Debug.Assert(t2 != null);
1285
1286 CheckContextMatch(t1);
1287 CheckContextMatch(t2);
1288 return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1289 }

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

1244 {
1245 Debug.Assert(t != null);
1246
1247 CheckContextMatch(t);
1248 return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1249 }

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

1256 {
1257 Debug.Assert(t != null);
1258
1259 CheckContextMatch(t);
1260 return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1261 }

## ◆ 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 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_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1823 }

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

1786 {
1787 Debug.Assert(t != null);
1788
1789 CheckContextMatch(t);
1790 return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1791 }

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

1833 {
1834 Debug.Assert(t1 != null);
1835 Debug.Assert(t2 != null);
1836
1837 CheckContextMatch(t1);
1838 CheckContextMatch(t2);
1839 return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1840 }

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

1801 {
1802 Debug.Assert(t != null);
1803
1804 CheckContextMatch(t);
1805 return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1806 }

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

1434 {
1435 Debug.Assert(t1 != null);
1436 Debug.Assert(t2 != null);
1437
1438 CheckContextMatch(t1);
1439 CheckContextMatch(t2);
1440 return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1441 }

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

1954 {
1955 Debug.Assert(t1 != null);
1956 Debug.Assert(t2 != null);
1957
1958 CheckContextMatch(t1);
1959 CheckContextMatch(t2);
1960 return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1961 }

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

1585 {
1586 Debug.Assert(t1 != null);
1587 Debug.Assert(t2 != null);
1588
1589 CheckContextMatch(t1);
1590 CheckContextMatch(t2);
1591 return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1592 }

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

1617 {
1618 Debug.Assert(t1 != null);
1619 Debug.Assert(t2 != null);
1620
1621 CheckContextMatch(t1);
1622 CheckContextMatch(t2);
1623 return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1624 }

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

1723 {
1724 Debug.Assert(t1 != null);
1725 Debug.Assert(t2 != null);
1726
1727 CheckContextMatch(t1);
1728 CheckContextMatch(t2);
1729 return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1730 }

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

1553 {
1554 Debug.Assert(t1 != null);
1555 Debug.Assert(t2 != null);
1556
1557 CheckContextMatch(t1);
1558 CheckContextMatch(t2);
1559 return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1560 }

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

1521 {
1522 Debug.Assert(t1 != null);
1523 Debug.Assert(t2 != null);
1524
1525 CheckContextMatch(t1);
1526 CheckContextMatch(t2);
1527 return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1528 }

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

1489 {
1490 Debug.Assert(t1 != null);
1491 Debug.Assert(t2 != null);
1492
1493 CheckContextMatch(t1);
1494 CheckContextMatch(t2);
1495 return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1496 }

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

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

## ◆ MkBVSub()

BitVecExpr MkBVSub | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1377 of file Context.cs.

1378 {
1379 Debug.Assert(t1 != null);
1380 Debug.Assert(t2 != null);
1381
1382 CheckContextMatch(t1);
1383 CheckContextMatch(t2);
1384 return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1385 }

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

1922 {
1923 Debug.Assert(t1 != null);
1924 Debug.Assert(t2 != null);
1925
1926 CheckContextMatch(t1);
1927 CheckContextMatch(t2);
1928 return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1929 }

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

1938 {
1939 Debug.Assert(t1 != null);
1940 Debug.Assert(t2 != null);
1941
1942 CheckContextMatch(t1);
1943 CheckContextMatch(t2);
1944 return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1945 }

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

1411 {
1412 Debug.Assert(t1 != null);
1413 Debug.Assert(t2 != null);
1414
1415 CheckContextMatch(t1);
1416 CheckContextMatch(t2);
1417 return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1418 }

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

1569 {
1570 Debug.Assert(t1 != null);
1571 Debug.Assert(t2 != null);
1572
1573 CheckContextMatch(t1);
1574 CheckContextMatch(t2);
1575 return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1576 }

## ◆ MkBVUGT()

BoolExpr MkBVUGT | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1600 of file Context.cs.

1601 {
1602 Debug.Assert(t1 != null);
1603 Debug.Assert(t2 != null);
1604
1605 CheckContextMatch(t1);
1606 CheckContextMatch(t2);
1607 return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1608 }

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

1537 {
1538 Debug.Assert(t1 != null);
1539 Debug.Assert(t2 != null);
1540
1541 CheckContextMatch(t1);
1542 CheckContextMatch(t2);
1543 return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1544 }

## ◆ MkBVULT()

BoolExpr MkBVULT | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1504 of file Context.cs.

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

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

1452 {
1453 Debug.Assert(t1 != null);
1454 Debug.Assert(t2 != null);
1455
1456 CheckContextMatch(t1);
1457 CheckContextMatch(t2);
1458 return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1459 }

## ◆ MkBVXNOR()

BitVecExpr MkBVXNOR | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1337 of file Context.cs.

1338 {
1339 Debug.Assert(t1 != null);
1340 Debug.Assert(t2 != null);
1341
1342 CheckContextMatch(t1);
1343 CheckContextMatch(t2);
1344 return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1345 }

## ◆ MkBVXOR()

BitVecExpr MkBVXOR | ( | BitVecExpr | t1,
|  | BitVecExpr | t2
| ) |  |
| inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1295 of file Context.cs.

1296 {
1297 Debug.Assert(t1 != null);
1298 Debug.Assert(t2 != null);
1299
1300 CheckContextMatch(t1);
1301 CheckContextMatch(t2);
1302 return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1303 }

## ◆ MkComplement()

ReExpr MkComplement | ( | ReExpr | re | ) |
| inline

Create the complement regular expression.

Definition at line 2594 of file Context.cs.

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

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

1637 {
1638 Debug.Assert(t1 != null);
1639 Debug.Assert(t2 != null);
1640
1641 CheckContextMatch(t1);
1642 CheckContextMatch(t2);
1643 return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1644 }

## ◆ MkConcat() [2/3]

ReExpr MkConcat | ( | params ReExpr[] | t | ) |
| inline

Create the concatenation of regular languages.

Definition at line 2603 of file Context.cs.

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

## ◆ MkConcat() [3/3]

SeqExpr MkConcat | ( | params SeqExpr[] | t | ) |
| inline

Concatenate sequences.

Definition at line 2402 of file Context.cs.

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

## ◆ MkConst() [1/3]

Expr MkConst | ( | FuncDecl | f | ) |
| inline

Creates a fresh constant from the FuncDecl f .

Parameters

  f | A decl of a 0-arity function

Definition at line 699 of file Context.cs.

700 {
701 Debug.Assert(f != null);
702
703 return MkApp(f);
704 }
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788

## ◆ MkConst() [2/3]

Expr MkConst | ( | string | name,
|  | Sort | range
| ) |  |
| inline

Creates a new Constant of sort range and named name .

Definition at line 676 of file Context.cs.

677 {
678 Debug.Assert(range != null);
679
680 return MkConst(MkSymbol(name), range);
681 }

## ◆ MkConst() [3/3]

Expr MkConst | ( | Symbol | name,
|  | Sort | range
| ) |  |
| inline

Creates a new Constant of sort range and named name .

Definition at line 662 of file Context.cs.

663 {
664 Debug.Assert(name != null);
665 Debug.Assert(range != null);
666
667 CheckContextMatch(name);
668 CheckContextMatch(range);
669
670 return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
671 }

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

## ◆ MkConstArray()

ArrayExpr MkConstArray | ( | Sort | domain,
|  | Expr | v
| ) |  |
| inline

Create a constant array.

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

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

Definition at line 2151 of file Context.cs.

2152 {
2153 Debug.Assert(domain != null);
2154 Debug.Assert(v != null);
2155
2156 CheckContextMatch(domain);
2157 CheckContextMatch(v);
2158 return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2159 }

## ◆ MkConstDecl() [1/2]

FuncDecl MkConstDecl | ( | string | name,
|  | Sort | range
| ) |  |
| inline

Creates a new constant function declaration.

Definition at line 607 of file Context.cs.

608 {
609 Debug.Assert(range != null);
610
611 CheckContextMatch(range);
612 return new FuncDecl(this, MkSymbol(name), null, range);
613 }

## ◆ MkConstDecl() [2/2]

FuncDecl MkConstDecl | ( | Symbol | name,
|  | Sort | range
| ) |  |
| inline

Creates a new constant function declaration.

Definition at line 594 of file Context.cs.

595 {
596 Debug.Assert(name != null);
597 Debug.Assert(range != null);
598
599 CheckContextMatch(name);
600 CheckContextMatch(range);
601 return new FuncDecl(this, name, null, range);
602 }

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

392 {
393
394 return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
395 }

## ◆ MkConstructor() [2/2]

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

Create a datatype constructor.

Parameters

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

Definition at line 374 of file Context.cs.

375 {
376 Debug.Assert(name != null);
377 Debug.Assert(recognizer != null);
378
379 return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
380 }

## ◆ MkContains()

BoolExpr MkContains | ( | SeqExpr | s1,
|  | SeqExpr | s2
| ) |  |
| inline

Check for sequence containment of s2 in s1.

Definition at line 2446 of file Context.cs.

2447 {
2448 Debug.Assert(s1 != null);
2449 Debug.Assert(s2 != null);
2450 CheckContextMatch(s1, s2);
2451 return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2452 }

## ◆ MkDatatypeSort() [1/2]

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

Create a new datatype sort.

Definition at line 415 of file Context.cs.

416 {
417 Debug.Assert(constructors != null);
418 Debug.Assert(constructors.All(c => c != null));
419
420 CheckContextMatch<Constructor>(constructors);
421 return new DatatypeSort(this, MkSymbol(name), constructors);
422 }

## ◆ MkDatatypeSort() [2/2]

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

Create a new datatype sort.

Definition at line 400 of file Context.cs.

401 {
402 Debug.Assert(name != null);
403 Debug.Assert(constructors != null);
404 Debug.Assert(constructors.All(c => c != null));
405
406
407 CheckContextMatch(name);
408 CheckContextMatch<Constructor>(constructors);
409 return new DatatypeSort(this, name, constructors);
410 }

## ◆ MkDatatypeSorts() [1/2]

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

Create mutually recursive data-types.

Parameters

  names |
  c |

Returns

Definition at line 462 of file Context.cs.

463 {
464 Debug.Assert(names != null);
465 Debug.Assert(c != null);
466 Debug.Assert(names.Length == c.Length);
467 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
468 //Debug.Assert(names.All(name => name != null));
469
470 return MkDatatypeSorts(MkSymbols(names), c);
471 }
Microsoft.Z3.Context.MkDatatypeSorts
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:429

## ◆ MkDatatypeSorts() [2/2]

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

Create mutually recursive datatypes.

Parameters

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

Definition at line 429 of file Context.cs.

430 {
431 Debug.Assert(names != null);
432 Debug.Assert(c != null);
433 Debug.Assert(names.Length == c.Length);
434 //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
435 Debug.Assert(names.All(name => name != null));
436
437 CheckContextMatch<Symbol>(names);
438 uint n = (uint)names.Length;
439 ConstructorList[] cla = new ConstructorList[n];
440 IntPtr[] n_constr = new IntPtr[n];
441 for (uint i = 0; i < n; i++)
442 {
443 Constructor[] constructor = c[i];
444 CheckContextMatch<Constructor>(constructor);
445 cla[i] = new ConstructorList(this, constructor);
446 n_constr[i] = cla[i].NativeObject;
447 }
448 IntPtr[] n_res = new IntPtr[n];
449 Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
450 DatatypeSort[] res = new DatatypeSort[n];
451 for (uint i = 0; i < n; i++)
452 res[i] = new DatatypeSort(this, n_res[i]);
453 return res;
454 }

Referenced by Context.MkDatatypeSorts().

## ◆ MkDistinct()

BoolExpr MkDistinct | ( | params Expr[] | args | ) |
| inline

Creates a `distinct` term.

Definition at line 855 of file Context.cs.

856 {
857 Debug.Assert(args != null);
858 Debug.Assert(args.All(a => a != null));
859
860
861 CheckContextMatch<Expr>(args);
862 return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
863 }

## ◆ MkDiv()

ArithExpr MkDiv | ( | ArithExpr | t1,
|  | ArithExpr | t2
| ) |  |
| inline

Create an expression representing `t1 / t2`.

Definition at line 1078 of file Context.cs.

1079 {
1080 Debug.Assert(t1 != null);
1081 Debug.Assert(t2 != null);
1082
1083 CheckContextMatch(t1);
1084 CheckContextMatch(t2);
1085 return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1086 }

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

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

## ◆ MkEmptySeq()

SeqExpr MkEmptySeq | ( | Sort | s | ) |
| inline

Create the empty sequence.

Definition at line 2354 of file Context.cs.

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

## ◆ MkEmptySet()

ArrayExpr MkEmptySet | ( | Sort | domain | ) |
| inline

Create an empty set.

Definition at line 2227 of file Context.cs.

2228 {
2229 Debug.Assert(domain != null);
2230
2231 CheckContextMatch(domain);
2232 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2233 }

## ◆ MkEnumSort() [1/2]

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

Create a new enumeration sort.

Definition at line 303 of file Context.cs.

304 {
305 Debug.Assert(enumNames != null);
306
307 return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
308 }
z3py.EnumSort
def EnumSort(name, values, ctx=None)
Definition: z3py.py:5317

## ◆ MkEnumSort() [2/2]

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

Create a new enumeration sort.

Definition at line 288 of file Context.cs.

289 {
290 Debug.Assert(name != null);
291 Debug.Assert(enumNames != null);
292 Debug.Assert(enumNames.All(f => f != null));
293
294
295 CheckContextMatch(name);
296 CheckContextMatch<Symbol>(enumNames);
297 return new EnumSort(this, name, enumNames);
298 }

## ◆ MkEq()

BoolExpr MkEq | ( | Expr | x,
|  | Expr | y
| ) |  |
| inline

Creates the equality x = y .

Definition at line 842 of file Context.cs.

843 {
844 Debug.Assert(x != null);
845 Debug.Assert(y != null);
846
847 CheckContextMatch(x);
848 CheckContextMatch(y);
849 return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
850 }

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

3104 {
3105 Debug.Assert(body != null);
3106 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3107 Debug.Assert(patterns == null || patterns.All(p => p != null));
3108 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3109
3110 return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3111 }

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

3082 {
3083 Debug.Assert(sorts != null);
3084 Debug.Assert(names != null);
3085 Debug.Assert(body != null);
3086 Debug.Assert(sorts.Length == names.Length);
3087 Debug.Assert(sorts.All(s => s != null));
3088 Debug.Assert(names.All(n => n != null));
3089 Debug.Assert(patterns == null || patterns.All(p => p != null));
3090 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3091
3092 return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3093 }

Referenced by Context.MkQuantifier().

## ◆ MkExtract() [1/2]

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

Extract subsequence.

Definition at line 2501 of file Context.cs.

2502 {
2503 Debug.Assert(s != null);
2504 Debug.Assert(offset != null);
2505 Debug.Assert(length != null);
2506 CheckContextMatch(s, offset, length);
2507 return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2508 }

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

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

## ◆ MkFalse()

BoolExpr MkFalse | ( |  | ) |
| inline

The false Term.

Definition at line 824 of file Context.cs.

825 {
826
827 return new BoolExpr(this, Native.Z3_mk_false(nCtx));
828 }

Referenced by Context.MkBool().

## ◆ MkFiniteDomainSort() [1/2]

FiniteDomainSort MkFiniteDomainSort | ( | string | name,
|  | ulong | size
| ) |  |
| inline

Create a new finite domain sort.

Returns
  The result is a sort

Elements of the sort are created using

See also
  MkNumeral(ulong, Sort)

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

Parameters

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

Definition at line 356 of file Context.cs.

357 {
358
359 return new FiniteDomainSort(this, MkSymbol(name), size);
360 }
z3py.FiniteDomainSort
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7590

## ◆ MkFiniteDomainSort() [2/2]

FiniteDomainSort MkFiniteDomainSort | ( | Symbol | name,
|  | ulong | size
| ) |  |
| inline

Create a new finite domain sort.

Returns
  The result is a sort

Parameters

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

Definition at line 340 of file Context.cs.

341 {
342 Debug.Assert(name != null);
343
344 CheckContextMatch(name);
345 return new FiniteDomainSort(this, name, size);
346 }

## ◆ MkFixedpoint()

Fixedpoint MkFixedpoint | ( |  | ) |
| inline

Create a Fixedpoint context.

Definition at line 3778 of file Context.cs.

3779 {
3780
3781 return new Fixedpoint(this);
3782 }

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

3064 {
3065 Debug.Assert(body != null);
3066 Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
3067 Debug.Assert(patterns == null || patterns.All(p => p != null));
3068 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3069
3070
3071 return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3072 }

## ◆ MkForall() [2/2]

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

Create a universal Quantifier.

Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. Note that the bound variables are de-Bruijn indices created using MkBound. Z3 applies the convention that the last element in names and sorts refers to the variable with index 0, the second to last element of names and sorts refers to the variable with index 1, etc.

Parameters

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

Definition at line 3039 of file Context.cs.

3040 {
3041 Debug.Assert(sorts != null);
3042 Debug.Assert(names != null);
3043 Debug.Assert(body != null);
3044 Debug.Assert(sorts.Length == names.Length);
3045 Debug.Assert(sorts.All(s => s != null));
3046 Debug.Assert(names.All(n => n != null));
3047 Debug.Assert(patterns == null || patterns.All(p => p != null));
3048 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3049
3050
3051 return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3052 }

Referenced by Context.MkQuantifier().

## ◆ MkFP() [1/6]

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

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

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

Parameters

  sgn | bit-vector term (of size 1) representing the sign.
  sig | bit-vector term representing the significand.
  exp | bit-vector term representing the exponent.

Definition at line 4368 of file Context.cs.

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

## ◆ MkFP() [2/6]

FPNum MkFP | ( | bool | sgn,
|  | int | exp,
|  | uint | sig,
|  | FPSort | s
| ) |  |
| inline

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

Parameters

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

Definition at line 4089 of file Context.cs.

4090 {
4091 return MkFPNumeral(sgn, exp, sig, s);
4092 }
Microsoft.Z3.Context.MkFPNumeral
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4003

## ◆ MkFP() [3/6]

FPNum MkFP | ( | bool | sgn,
|  | Int64 | exp,
|  | UInt64 | sig,
|  | FPSort | s
| ) |  |
| inline

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

Parameters

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

Definition at line 4101 of file Context.cs.

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

## ◆ MkFP() [4/6]

FPNum MkFP | ( | double | v,
|  | FPSort | s
| ) |  |
| inline

Create a numeral of FloatingPoint sort from a float.

Parameters

  v | numeral value.
  s | FloatingPoint sort.

Definition at line 4067 of file Context.cs.

4068 {
4069 return MkFPNumeral(v, s);
4070 }

## ◆ MkFP() [5/6]

FPNum MkFP | ( | float | v,
|  | FPSort | s
| ) |  |
| inline

Create a numeral of FloatingPoint sort from a float.

Parameters

  v | numeral value.
  s | FloatingPoint sort.

Definition at line 4057 of file Context.cs.

4058 {
4059 return MkFPNumeral(v, s);
4060 }

## ◆ MkFP() [6/6]

FPNum MkFP | ( | int | v,
|  | FPSort | s
| ) |  |
| inline

Create a numeral of FloatingPoint sort from an int.

Parameters

  v | numeral value.
  s | FloatingPoint sort.

Definition at line 4077 of file Context.cs.

4078 {
4079 return MkFPNumeral(v, s);
4080 }

## ◆ MkFPAbs()

FPExpr MkFPAbs | ( | FPExpr | t | ) |
| inline

Floating-point absolute value

Parameters

  t | floating-point term

Definition at line 4113 of file Context.cs.

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

## ◆ MkFPAdd()

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

Floating-point addition

Parameters

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

Definition at line 4133 of file Context.cs.

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

## ◆ MkFPDiv()

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

Floating-point division

Parameters

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

Definition at line 4166 of file Context.cs.

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

## ◆ MkFPEq()

BoolExpr MkFPEq | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Floating-point equality.

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

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4285 of file Context.cs.

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

## ◆ MkFPFMA()

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

Floating-point fused multiply-add

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

Parameters

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

Definition at line 4181 of file Context.cs.

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

## ◆ MkFPGEq()

BoolExpr MkFPGEq | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Floating-point greater than or equal.

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4262 of file Context.cs.

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

## ◆ MkFPGt()

BoolExpr MkFPGt | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Floating-point greater than.

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4272 of file Context.cs.

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

## ◆ MkFPInf()

FPNum MkFPInf | ( | FPSort | s,
|  | bool | negative
| ) |  |
| inline

Create a floating-point infinity of sort s.

Parameters

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

Definition at line 3983 of file Context.cs.

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

## ◆ MkFPIsInfinite()

BoolExpr MkFPIsInfinite | ( | FPExpr | t | ) |
| inline

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

Parameters

  t | floating-point term

Definition at line 4321 of file Context.cs.

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

## ◆ MkFPIsNaN()

BoolExpr MkFPIsNaN | ( | FPExpr | t | ) |
| inline

Predicate indicating whether t is a NaN.

Parameters

  t | floating-point term

Definition at line 4330 of file Context.cs.

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

## ◆ MkFPIsNegative()

BoolExpr MkFPIsNegative | ( | FPExpr | t | ) |
| inline

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

Parameters

  t | floating-point term

Definition at line 4339 of file Context.cs.

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

## ◆ MkFPIsNormal()

BoolExpr MkFPIsNormal | ( | FPExpr | t | ) |
| inline

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

Parameters

  t | floating-point term

Definition at line 4294 of file Context.cs.

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

## ◆ MkFPIsPositive()

BoolExpr MkFPIsPositive | ( | FPExpr | t | ) |
| inline

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

Parameters

  t | floating-point term

Definition at line 4348 of file Context.cs.

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

## ◆ MkFPIsSubnormal()

BoolExpr MkFPIsSubnormal | ( | FPExpr | t | ) |
| inline

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

Parameters

  t | floating-point term

Definition at line 4303 of file Context.cs.

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

## ◆ MkFPIsZero()

BoolExpr MkFPIsZero | ( | FPExpr | t | ) |
| inline

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

Parameters

  t | floating-point term

Definition at line 4312 of file Context.cs.

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

## ◆ MkFPLEq()

BoolExpr MkFPLEq | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Floating-point less than or equal.

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4242 of file Context.cs.

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

## ◆ MkFPLt()

BoolExpr MkFPLt | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Floating-point less than.

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4252 of file Context.cs.

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

## ◆ MkFPMax()

FPExpr MkFPMax | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Maximum of floating-point numbers.

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4232 of file Context.cs.

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

## ◆ MkFPMin()

FPExpr MkFPMin | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Minimum of floating-point numbers.

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4222 of file Context.cs.

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

## ◆ MkFPMul()

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

Floating-point multiplication

Parameters

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

Definition at line 4155 of file Context.cs.

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

## ◆ MkFPNaN()

FPNum MkFPNaN | ( | FPSort | s | ) |
| inline

Create a NaN of sort s.

Parameters

  s | FloatingPoint sort.

Definition at line 3973 of file Context.cs.

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

## ◆ MkFPNeg()

FPExpr MkFPNeg | ( | FPExpr | t | ) |
| inline

Floating-point negation

Parameters

  t | floating-point term

Definition at line 4122 of file Context.cs.

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

## ◆ MkFPNumeral() [1/5]

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

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

Parameters

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

Definition at line 4047 of file Context.cs.

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

## ◆ MkFPNumeral() [2/5]

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

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

Parameters

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

Definition at line 4035 of file Context.cs.

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

## ◆ MkFPNumeral() [3/5]

FPNum MkFPNumeral | ( | double | v,
|  | FPSort | s
| ) |  |
| inline

Create a numeral of FloatingPoint sort from a float.

Parameters

  v | numeral value.
  s | FloatingPoint sort.

Definition at line 4013 of file Context.cs.

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

## ◆ MkFPNumeral() [4/5]

FPNum MkFPNumeral | ( | float | v,
|  | FPSort | s
| ) |  |
| inline

Create a numeral of FloatingPoint sort from a float.

Parameters

  v | numeral value.
  s | FloatingPoint sort.

Definition at line 4003 of file Context.cs.

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

Referenced by Context.MkFP().

## ◆ MkFPNumeral() [5/5]

FPNum MkFPNumeral | ( | int | v,
|  | FPSort | s
| ) |  |
| inline

Create a numeral of FloatingPoint sort from an int.

Parameters

  v | numeral value.
  s | FloatingPoint sort.

Definition at line 4023 of file Context.cs.

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

## ◆ MkFPRem()

FPExpr MkFPRem | ( | FPExpr | t1,
|  | FPExpr | t2
| ) |  |
| inline

Floating-point remainder

Parameters

  t1 | floating-point term
  t2 | floating-point term

Definition at line 4201 of file Context.cs.

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

## ◆ MkFPRNA()

FPRMNum MkFPRNA | ( |  | ) |
| inline

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

Definition at line 3837 of file Context.cs.

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

## ◆ MkFPRNE()

FPRMNum MkFPRNE | ( |  | ) |
| inline

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

Definition at line 3821 of file Context.cs.

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

## ◆ MkFPRoundingModeSort()

FPRMSort MkFPRoundingModeSort | ( |  | ) |
| inline

Create the floating-point RoundingMode sort.

Definition at line 3803 of file Context.cs.

3804 {
3805 return new FPRMSort(this);
3806 }

## ◆ MkFPRoundNearestTiesToAway()

FPRMNum MkFPRoundNearestTiesToAway | ( |  | ) |
| inline

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

Definition at line 3829 of file Context.cs.

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

## ◆ MkFPRoundNearestTiesToEven()

FPRMExpr MkFPRoundNearestTiesToEven | ( |  | ) |
| inline

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

Definition at line 3813 of file Context.cs.

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

## ◆ MkFPRoundToIntegral()

FPExpr MkFPRoundToIntegral | ( | FPRMExpr | rm,
|  | FPExpr | t
| ) |  |
| inline

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

Parameters

  rm | term of RoundingMode sort
  t | floating-point term

Definition at line 4212 of file Context.cs.

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

## ◆ MkFPRoundTowardNegative()

FPRMNum MkFPRoundTowardNegative | ( |  | ) |
| inline

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

Definition at line 3861 of file Context.cs.

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

## ◆ MkFPRoundTowardPositive()

FPRMNum MkFPRoundTowardPositive | ( |  | ) |
| inline

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

Definition at line 3845 of file Context.cs.

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

## ◆ MkFPRoundTowardZero()

FPRMNum MkFPRoundTowardZero | ( |  | ) |
| inline

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

Definition at line 3877 of file Context.cs.

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

## ◆ MkFPRTN()

FPRMNum MkFPRTN | ( |  | ) |
| inline

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

Definition at line 3869 of file Context.cs.

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

## ◆ MkFPRTP()

FPRMNum MkFPRTP | ( |  | ) |
| inline

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

Definition at line 3853 of file Context.cs.

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

## ◆ MkFPRTZ()

FPRMNum MkFPRTZ | ( |  | ) |
| inline

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

Definition at line 3885 of file Context.cs.

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

## ◆ MkFPSort()

FPSort MkFPSort | ( | uint | ebits,
|  | uint | sbits
| ) |  |
| inline

Create a FloatingPoint sort.

Parameters

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

Definition at line 3898 of file Context.cs.

3899 {
3900 return new FPSort(this, ebits, sbits);
3901 }
z3py.FPSort
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727

## ◆ MkFPSort128()

FPSort MkFPSort128 | ( |  | ) |
| inline

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

Definition at line 3962 of file Context.cs.

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

## ◆ MkFPSort16()

FPSort MkFPSort16 | ( |  | ) |
| inline

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

Definition at line 3914 of file Context.cs.

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

## ◆ MkFPSort32()

FPSort MkFPSort32 | ( |  | ) |
| inline

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

Definition at line 3930 of file Context.cs.

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

## ◆ MkFPSort64()

FPSort MkFPSort64 | ( |  | ) |
| inline

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

Definition at line 3946 of file Context.cs.

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

## ◆ MkFPSortDouble()

FPSort MkFPSortDouble | ( |  | ) |
| inline

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

Definition at line 3938 of file Context.cs.

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

## ◆ MkFPSortHalf()

FPSort MkFPSortHalf | ( |  | ) |
| inline

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

Definition at line 3906 of file Context.cs.

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

## ◆ MkFPSortQuadruple()

FPSort MkFPSortQuadruple | ( |  | ) |
| inline

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

Definition at line 3954 of file Context.cs.

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

## ◆ MkFPSortSingle()

FPSort MkFPSortSingle | ( |  | ) |
| inline

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

Definition at line 3922 of file Context.cs.

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

## ◆ MkFPSqrt()

FPExpr MkFPSqrt | ( | FPRMExpr | rm,
|  | FPExpr | t
| ) |  |
| inline

Floating-point square root

Parameters

  rm | rounding mode term
  t | floating-point term

Definition at line 4191 of file Context.cs.

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

## ◆ MkFPSub()

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

Floating-point subtraction

Parameters

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

Definition at line 4144 of file Context.cs.

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

## ◆ MkFPToBV()

BitVecExpr MkFPToBV | ( | FPRMExpr | rm,
|  | FPExpr | t,
|  | uint | sz,
|  | bool signed |
| ) |  |
| 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 signed==true). If necessary, the result will be rounded according to rounding mode rm.

Parameters

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

Definition at line 4471 of file Context.cs.

4472 {
4473 if (signed)
4474 return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4475 else
4476 return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4477 }

## ◆ MkFPToFP() [1/6]

FPExpr MkFPToFP | ( | BitVecExpr | bv,
|  | FPSort | s
| ) |  |
| inline

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

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

Parameters

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

Definition at line 4384 of file Context.cs.

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

## ◆ MkFPToFP() [2/6]

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

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

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

Parameters

  rm | RoundingMode term.
  t | term of bit-vector sort.
  s | FloatingPoint sort.
  signed | flag indicating whether t is interpreted as signed or unsigned bit-vector.

Definition at line 4434 of file Context.cs.

4435 {
4436 if (signed)
4437 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4438 else
4439 return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4440 }

## ◆ MkFPToFP() [3/6]

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

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

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

Parameters

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

Definition at line 4400 of file Context.cs.

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

## ◆ MkFPToFP() [4/6]

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

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

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

Parameters

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

Definition at line 4522 of file Context.cs.

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

## ◆ MkFPToFP() [5/6]

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

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

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

Parameters

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

Definition at line 4416 of file Context.cs.

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

## ◆ MkFPToFP() [6/6]

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

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

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

Parameters

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

Definition at line 4452 of file Context.cs.

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

## ◆ MkFPToIEEEBV()

BitVecExpr MkFPToIEEEBV | ( | FPExpr | t | ) |
| inline

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

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

Parameters

  t | FloatingPoint term.

Definition at line 4505 of file Context.cs.

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

## ◆ MkFPToReal()

RealExpr MkFPToReal | ( | FPExpr | t | ) |
| inline

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

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

Parameters

  t | FloatingPoint term

Definition at line 4488 of file Context.cs.

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

## ◆ MkFPZero()

FPNum MkFPZero | ( | FPSort | s,
|  | bool | negative
| ) |  |
| inline

Create a floating-point zero of sort s.

Parameters

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

Definition at line 3993 of file Context.cs.

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

## ◆ MkFreshConst()

Expr MkFreshConst | ( | string | prefix,
|  | Sort | range
| ) |  |
| inline

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

Definition at line 687 of file Context.cs.

688 {
689 Debug.Assert(range != null);
690
691 CheckContextMatch(range);
692 return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
693 }

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

621 {
622 Debug.Assert(range != null);
623
624 CheckContextMatch(range);
625 return new FuncDecl(this, prefix, null, range);
626 }

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

582 {
583 Debug.Assert(range != null);
584 Debug.Assert(domain.All(d => d != null));
585
586 CheckContextMatch<Sort>(domain);
587 CheckContextMatch(range);
588 return new FuncDecl(this, prefix, domain, range);
589 }

## ◆ MkFullRe()

ReExpr MkFullRe | ( | Sort | s | ) |
| inline

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

Definition at line 2650 of file Context.cs.

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

## ◆ MkFullSet()

ArrayExpr MkFullSet | ( | Sort | domain | ) |
| inline

Create the full set.

Definition at line 2238 of file Context.cs.

2239 {
2240 Debug.Assert(domain != null);
2241
2242 CheckContextMatch(domain);
2243 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2244 }

## ◆ MkFuncDecl() [1/4]

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

Creates a new function declaration.

Definition at line 565 of file Context.cs.

566 {
567 Debug.Assert(range != null);
568 Debug.Assert(domain != null);
569
570 CheckContextMatch(domain);
571 CheckContextMatch(range);
572 Sort[] q = new Sort[] { domain };
573 return new FuncDecl(this, MkSymbol(name), q, range);
574 }

## ◆ MkFuncDecl() [2/4]

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

Creates a new function declaration.

Definition at line 524 of file Context.cs.

525 {
526 Debug.Assert(range != null);
527 Debug.Assert(domain.All(d => d != null));
528
529 CheckContextMatch<Sort>(domain);
530 CheckContextMatch(range);
531 return new FuncDecl(this, MkSymbol(name), domain, range);
532 }

## ◆ MkFuncDecl() [3/4]

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

Creates a new function declaration.

Definition at line 508 of file Context.cs.

509 {
510 Debug.Assert(name != null);
511 Debug.Assert(domain != null);
512 Debug.Assert(range != null);
513
514 CheckContextMatch(name);
515 CheckContextMatch(domain);
516 CheckContextMatch(range);
517 Sort[] q = new Sort[] { domain };
518 return new FuncDecl(this, name, q, range);
519 }

## ◆ MkFuncDecl() [4/4]

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

Creates a new function declaration.

Definition at line 493 of file Context.cs.

494 {
495 Debug.Assert(name != null);
496 Debug.Assert(range != null);
497 Debug.Assert(domain.All(d => d != null));
498
499 CheckContextMatch(name);
500 CheckContextMatch<Sort>(domain);
501 CheckContextMatch(range);
502 return new FuncDecl(this, name, domain, range);
503 }

## ◆ MkGe()

BoolExpr MkGe | ( | 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 new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1179 }

Referenced by ArithExpr.operator>=().

## ◆ MkGoal()

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

Creates a new Goal.

Note that the Context must have been created with proof generation support if proofs is set to true here.

Parameters

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

Definition at line 3279 of file Context.cs.

3280 {
3281
3282 return new Goal(this, models, unsatCores, proofs);
3283 }

## ◆ MkGt()

BoolExpr MkGt | ( | ArithExpr | t1,
|  | ArithExpr | t2
| ) |  |
| inline

Create an expression representing `t1 > t2`

Definition at line 1158 of file Context.cs.

1159 {
1160 Debug.Assert(t1 != null);
1161 Debug.Assert(t2 != null);
1162
1163 CheckContextMatch(t1);
1164 CheckContextMatch(t2);
1165 return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1166 }

Referenced by ArithExpr.operator>().

## ◆ MkIff()

BoolExpr MkIff | ( | BoolExpr | t1,
|  | BoolExpr | t2
| ) |  |
| inline

Create an expression representing `t1 iff t2`.

Definition at line 897 of file Context.cs.

898 {
899 Debug.Assert(t1 != null);
900 Debug.Assert(t2 != null);
901
902 CheckContextMatch(t1);
903 CheckContextMatch(t2);
904 return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
905 }

## ◆ MkImplies()

BoolExpr MkImplies | ( | BoolExpr | t1,
|  | BoolExpr | t2
| ) |  |
| inline

Create an expression representing `t1 -> t2`.

Definition at line 910 of file Context.cs.

911 {
912 Debug.Assert(t1 != null);
913 Debug.Assert(t2 != null);
914
915 CheckContextMatch(t1);
916 CheckContextMatch(t2);
917 return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
918 }

## ◆ MkIndexOf()

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

Extract index of sub-string starting at offset.

Definition at line 2513 of file Context.cs.

2514 {
2515 Debug.Assert(s != null);
2516 Debug.Assert(offset != null);
2517 Debug.Assert(substr != null);
2518 CheckContextMatch(s, substr, offset);
2519 return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2520 }

## ◆ MkInRe()

BoolExpr MkInRe | ( | SeqExpr | s,
|  | ReExpr | re
| ) |  |
| inline

Check for regular expression membership.

Definition at line 2547 of file Context.cs.

2548 {
2549 Debug.Assert(s != null);
2550 Debug.Assert(re != null);
2551 CheckContextMatch(s, re);
2552 return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2553 }

## ◆ MkInt() [1/5]

IntNum MkInt | ( | int | v | ) |
| inline

Create an integer numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Integer

Definition at line 2902 of file Context.cs.

2903 {
2904
2905 return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2906 }
Microsoft.Z3.Context.IntSort
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139

## ◆ MkInt() [2/5]

IntNum MkInt | ( | long | v | ) |
| inline

Create an integer numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Integer

Definition at line 2924 of file Context.cs.

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

## ◆ MkInt() [3/5]

IntNum MkInt | ( | string | v | ) |
| inline

Create an integer numeral.

Parameters

  v | A string representing the Term value in decimal notation.

Definition at line 2891 of file Context.cs.

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

## ◆ MkInt() [4/5]

IntNum MkInt | ( | uint | v | ) |
| inline

Create an integer numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Integer

Definition at line 2913 of file Context.cs.

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

## ◆ MkInt() [5/5]

IntNum MkInt | ( | ulong | v | ) |
| inline

Create an integer numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Integer

Definition at line 2935 of file Context.cs.

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

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

1853 {
1854 Debug.Assert(t != null);
1855
1856 CheckContextMatch(t);
1857 return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1858 }

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

1192 {
1193 Debug.Assert(t != null);
1194
1195 CheckContextMatch(t);
1196 return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1197 }

## ◆ MkIntConst() [1/2]

IntExpr MkIntConst | ( | string | name | ) |
| inline

Creates an integer constant.

Definition at line 738 of file Context.cs.

739 {
740 Debug.Assert(name != null);
741
742 return (IntExpr)MkConst(name, IntSort);
743 }

## ◆ MkIntConst() [2/2]

IntExpr MkIntConst | ( | Symbol | name | ) |
| inline

Creates an integer constant.

Definition at line 728 of file Context.cs.

729 {
730 Debug.Assert(name != null);
731
732 return (IntExpr)MkConst(name, IntSort);
733 }

## ◆ MkIntersect()

ReExpr MkIntersect | ( | params ReExpr[] | t | ) |
| inline

Create the intersection of regular languages.

Definition at line 2627 of file Context.cs.

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

## ◆ MkIntSort()

IntSort MkIntSort | ( |  | ) |
| inline

Create a new integer sort.

Definition at line 202 of file Context.cs.

203 {
204
205 return new IntSort(this);
206 }

## ◆ MkIsInteger()

BoolExpr MkIsInteger | ( | RealExpr | t | ) |
| inline

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

Definition at line 1217 of file Context.cs.

1218 {
1219 Debug.Assert(t != null);
1220
1221 CheckContextMatch(t);
1222 return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1223 }

## ◆ MkITE()

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

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

Parameters

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

Definition at line 882 of file Context.cs.

883 {
884 Debug.Assert(t1 != null);
885 Debug.Assert(t2 != null);
886 Debug.Assert(t3 != null);
887
888 CheckContextMatch(t1);
889 CheckContextMatch(t2);
890 CheckContextMatch(t3);
891 return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
892 }

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

3193 {
3194 Debug.Assert(body != null);
3195 Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
3196 return new Lambda(this, boundConstants, body);
3197 }
z3py.Lambda
def Lambda(vs, body)
Definition: z3py.py:2226

## ◆ MkLambda() [2/2]

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

Create a lambda expression.

Creates a lambda expression. sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the lambda. Note that the bound variables are de-Bruijn indices created using MkBound. Z3 applies the convention that the last element in names and sorts refers to the variable with index 0, the second to last element of names and sorts refers to the variable with index 1, etc.

Parameters

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

Definition at line 3173 of file Context.cs.

3174 {
3175 Debug.Assert(sorts != null);
3176 Debug.Assert(names != null);
3177 Debug.Assert(body != null);
3178 Debug.Assert(sorts.Length == names.Length);
3179 Debug.Assert(sorts.All(s => s != null));
3180 Debug.Assert(names.All(n => n != null));
3181 return new Lambda(this, sorts, names, body);
3182 }

## ◆ MkLe()

BoolExpr MkLe | ( | ArithExpr | t1,
|  | ArithExpr | t2
| ) |  |
| inline

Create an expression representing `t1 <= t2`

Definition at line 1145 of file Context.cs.

1146 {
1147 Debug.Assert(t1 != null);
1148 Debug.Assert(t2 != null);
1149
1150 CheckContextMatch(t1);
1151 CheckContextMatch(t2);
1152 return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1153 }

Referenced by ArithExpr.operator<=().

## ◆ MkLength()

IntExpr MkLength | ( | SeqExpr | s | ) |
| inline

Retrieve the length of a given sequence.

Definition at line 2415 of file Context.cs.

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

## ◆ MkListSort() [1/2]

ListSort MkListSort | ( | string | name,
|  | Sort | elemSort
| ) |  |
| inline

Create a new list sort.

Definition at line 326 of file Context.cs.

327 {
328 Debug.Assert(elemSort != null);
329
330 CheckContextMatch(elemSort);
331 return new ListSort(this, MkSymbol(name), elemSort);
332 }

## ◆ MkListSort() [2/2]

ListSort MkListSort | ( | Symbol | name,
|  | Sort | elemSort
| ) |  |
| inline

Create a new list sort.

Definition at line 313 of file Context.cs.

314 {
315 Debug.Assert(name != null);
316 Debug.Assert(elemSort != null);
317
318 CheckContextMatch(name);
319 CheckContextMatch(elemSort);
320 return new ListSort(this, name, elemSort);
321 }

## ◆ MkLoop()

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

Take the bounded Kleene star of a regular expression.

Definition at line 2567 of file Context.cs.

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

## ◆ MkLt()

BoolExpr MkLt | ( | ArithExpr | t1,
|  | ArithExpr | t2
| ) |  |
| inline

Create an expression representing `t1 < t2`

Definition at line 1132 of file Context.cs.

1133 {
1134 Debug.Assert(t1 != null);
1135 Debug.Assert(t2 != null);
1136
1137 CheckContextMatch(t1);
1138 CheckContextMatch(t2);
1139 return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1140 }

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

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

## ◆ MkMod()

IntExpr MkMod | ( | IntExpr | t1,
|  | IntExpr | t2
| ) |  |
| inline

Create an expression representing `t1 mod t2`.

The arguments must have int type.

Definition at line 1092 of file Context.cs.

1093 {
1094 Debug.Assert(t1 != null);
1095 Debug.Assert(t2 != null);
1096
1097 CheckContextMatch(t1);
1098 CheckContextMatch(t2);
1099 return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1100 }

## ◆ MkMul() [1/2]

ArithExpr MkMul | ( | IEnumerable< ArithExpr > | t | ) |
| inline

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

Definition at line 1043 of file Context.cs.

1044 {
1045 Debug.Assert(t != null);
1046 Debug.Assert(t.All(a => a != null));
1047
1048 CheckContextMatch<ArithExpr>(t);
1049 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1050 }

## ◆ MkMul() [2/2]

ArithExpr MkMul | ( | params ArithExpr[] | t | ) |
| inline

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

Definition at line 1031 of file Context.cs.

1032 {
1033 Debug.Assert(t != null);
1034 Debug.Assert(t.All(a => a != null));
1035
1036 CheckContextMatch<ArithExpr>(t);
1037 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1038 }

Referenced by ArithExpr.operator*().

## ◆ MkNot()

BoolExpr MkNot | ( | BoolExpr | a | ) |
| inline

Mk an expression representing `not(a)`.

Definition at line 868 of file Context.cs.

869 {
870 Debug.Assert(a != null);
871
872 CheckContextMatch(a);
873 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
874 }

Referenced by BoolExpr.operator!().

## ◆ MkNth()

Expr MkNth | ( | SeqExpr | s,
|  | Expr | index
| ) |  |
| inline

Retrieve element at index.

Definition at line 2490 of file Context.cs.

2491 {
2492 Debug.Assert(s != null);
2493 Debug.Assert(index != null);
2494 CheckContextMatch(s, index);
2495 return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2496 }

## ◆ MkNumeral() [1/5]

Expr MkNumeral | ( | int | v,
|  | Sort | ty
| ) |  |
| inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than `MakeNumeral` since it is not necessary to parse a string.

Parameters

  v | Value of the numeral
  ty | Sort of the numeral

Returns
  A Term with value v and type ty

Definition at line 2760 of file Context.cs.

2761 {
2762 Debug.Assert(ty != null);
2763
2764 CheckContextMatch(ty);
2765 return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2766 }

## ◆ MkNumeral() [2/5]

Expr MkNumeral | ( | long | v,
|  | Sort | ty
| ) |  |
| inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than `MakeNumeral` since it is not necessary to parse a string.

Parameters

  v | Value of the numeral
  ty | Sort of the numeral

Returns
  A Term with value v and type ty

Definition at line 2790 of file Context.cs.

2791 {
2792 Debug.Assert(ty != null);
2793
2794 CheckContextMatch(ty);
2795 return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2796 }

## ◆ MkNumeral() [3/5]

Expr MkNumeral | ( | string | v,
|  | Sort | ty
| ) |  |
| inline

Create a Term of a given sort.

Parameters

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

Returns
  A Term with value v and sort ty

Definition at line 2745 of file Context.cs.

2746 {
2747 Debug.Assert(ty != null);
2748
2749 CheckContextMatch(ty);
2750 return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2751 }

Referenced by Context.MkBV().

## ◆ MkNumeral() [4/5]

Expr MkNumeral | ( | uint | v,
|  | Sort | ty
| ) |  |
| inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than `MakeNumeral` since it is not necessary to parse a string.

Parameters

  v | Value of the numeral
  ty | Sort of the numeral

Returns
  A Term with value v and type ty

Definition at line 2775 of file Context.cs.

2776 {
2777 Debug.Assert(ty != null);
2778
2779 CheckContextMatch(ty);
2780 return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2781 }

## ◆ MkNumeral() [5/5]

Expr MkNumeral | ( | ulong | v,
|  | Sort | ty
| ) |  |
| inline

Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than `MakeNumeral` since it is not necessary to parse a string.

Parameters

  v | Value of the numeral
  ty | Sort of the numeral

Returns
  A Term with value v and type ty

Definition at line 2805 of file Context.cs.

2806 {
2807 Debug.Assert(ty != null);
2808
2809 CheckContextMatch(ty);
2810 return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2811 }

## ◆ MkOptimize()

Optimize MkOptimize | ( |  | ) |
| inline

Create an Optimization context.

Definition at line 3789 of file Context.cs.

3790 {
3791
3792 return new Optimize(this);
3793 }

## ◆ MkOption()

ReExpr MkOption | ( | ReExpr | re | ) |
| inline

Create the optional regular expression.

Definition at line 2585 of file Context.cs.

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

## ◆ MkOr() [1/2]

BoolExpr MkOr | ( | IEnumerable< BoolExpr > | t | ) |
| inline

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

Definition at line 992 of file Context.cs.

993 {
994 Debug.Assert(t != null);
995 Debug.Assert(t.All(a => a != null));
996
997 CheckContextMatch(t);
998 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
999 }

## ◆ MkOr() [2/2]

BoolExpr MkOr | ( | params BoolExpr[] | t | ) |
| inline

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

Definition at line 979 of file Context.cs.

980 {
981 Debug.Assert(t != null);
982 Debug.Assert(t.All(a => a != null));
983
984 CheckContextMatch<BoolExpr>(t);
985 return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
986 }

Referenced by BoolExpr.operator|().

## ◆ MkParams()

Params MkParams | ( |  | ) |
| inline

Creates a new ParameterSet.

Definition at line 3290 of file Context.cs.

3291 {
3292
3293 return new Params(this);
3294 }

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

## ◆ MkPattern()

Pattern MkPattern | ( | params Expr[] | terms | ) |
| inline

Create a quantifier pattern.

Definition at line 647 of file Context.cs.

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

## ◆ MkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2724 of file Context.cs.

2725 {
2726 Debug.Assert(args != null);
2727 Debug.Assert(coeffs != null);
2728 Debug.Assert(args.Length == coeffs.Length);
2729 CheckContextMatch<BoolExpr>(args);
2730 return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
2731 AST.ArrayToNative(args),
2732 coeffs, k));
2733 }

## ◆ MkPBGe()

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

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

Definition at line 2711 of file Context.cs.

2712 {
2713 Debug.Assert(args != null);
2714 Debug.Assert(coeffs != null);
2715 Debug.Assert(args.Length == coeffs.Length);
2716 CheckContextMatch<BoolExpr>(args);
2717 return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length,
2718 AST.ArrayToNative(args),
2719 coeffs, k));
2720 }

## ◆ MkPBLe()

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

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

Definition at line 2697 of file Context.cs.

2698 {
2699 Debug.Assert(args != null);
2700 Debug.Assert(coeffs != null);
2701 Debug.Assert(args.Length == coeffs.Length);
2702 CheckContextMatch<BoolExpr>(args);
2703 return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2704 AST.ArrayToNative(args),
2705 coeffs, k));
2706 }

## ◆ MkPlus()

ReExpr MkPlus | ( | ReExpr | re | ) |
| inline

Take the Kleene plus of a regular expression.

Definition at line 2576 of file Context.cs.

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

## ◆ MkPower()

ArithExpr MkPower | ( | ArithExpr | t1,
|  | ArithExpr | t2
| ) |  |
| inline

Create an expression representing `t1 ^ t2`.

Definition at line 1119 of file Context.cs.

1120 {
1121 Debug.Assert(t1 != null);
1122 Debug.Assert(t2 != null);
1123
1124 CheckContextMatch(t1);
1125 CheckContextMatch(t2);
1126 return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1127 }

## ◆ MkPrefixOf()

BoolExpr MkPrefixOf | ( | SeqExpr | s1,
|  | SeqExpr | s2
| ) |  |
| inline

Check for sequence prefix.

Definition at line 2424 of file Context.cs.

2425 {
2426 Debug.Assert(s1 != null);
2427 Debug.Assert(s2 != null);
2428 CheckContextMatch(s1, s2);
2429 return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2430 }

## ◆ MkProbe()

Probe MkProbe | ( | string | name | ) |
| inline

Creates a new Probe.

Definition at line 3596 of file Context.cs.

3597 {
3598
3599 return new Probe(this, name);
3600 }

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

3142 {
3143 Debug.Assert(body != null);
3144 Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3145 Debug.Assert(patterns == null || patterns.All(p => p != null));
3146 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3147
3148
3149 if (universal)
3150 return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3151 else
3152 return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3153 }
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:3081
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:3039

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

3119 {
3120 Debug.Assert(body != null);
3121 Debug.Assert(names != null);
3122 Debug.Assert(sorts != null);
3123 Debug.Assert(sorts.Length == names.Length);
3124 Debug.Assert(sorts.All(s => s != null));
3125 Debug.Assert(names.All(n => n != null));
3126 Debug.Assert(patterns == null || patterns.All(p => p != null));
3127 Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3128
3129
3130 if (universal)
3131 return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3132 else
3133 return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3134 }

## ◆ MkRange()

ReExpr MkRange | ( | SeqExpr | lo,
|  | SeqExpr | hi
| ) |  |
| inline

Create a range expression.

Definition at line 2660 of file Context.cs.

2661 {
2662 Debug.Assert(lo != null);
2663 Debug.Assert(hi != null);
2664 CheckContextMatch(lo, hi);
2665 return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
2666 }

## ◆ MkReal() [1/6]

RatNum MkReal | ( | int | num,
|  | int | den
| ) |  |
| inline

Create a real from a fraction.

Parameters

  num | numerator of rational.
  den | denominator of rational.

Returns
  A Term with value num /den and sort Real

See also
  MkNumeral(string, Sort)

Definition at line 2822 of file Context.cs.

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

## ◆ MkReal() [2/6]

RatNum MkReal | ( | int | v | ) |
| inline

Create a real numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Real

Definition at line 2846 of file Context.cs.

2847 {
2848
2849 return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2850 }
Microsoft.Z3.Context.RealSort
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:151

## ◆ MkReal() [3/6]

RatNum MkReal | ( | long | v | ) |
| inline

Create a real numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Real

Definition at line 2868 of file Context.cs.

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

## ◆ MkReal() [4/6]

RatNum MkReal | ( | string | v | ) |
| inline

Create a real numeral.

Parameters

  v | A string representing the Term value in decimal notation.

Returns
  A Term with value v and sort Real

Definition at line 2835 of file Context.cs.

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

## ◆ MkReal() [5/6]

RatNum MkReal | ( | uint | v | ) |
| inline

Create a real numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Real

Definition at line 2857 of file Context.cs.

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

## ◆ MkReal() [6/6]

RatNum MkReal | ( | ulong | v | ) |
| inline

Create a real numeral.

Parameters

  v | value of the numeral.

Returns
  A Term with value v and sort Real

Definition at line 2879 of file Context.cs.

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

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

1207 {
1208 Debug.Assert(t != null);
1209
1210 CheckContextMatch(t);
1211 return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1212 }

## ◆ MkRealConst() [1/2]

RealExpr MkRealConst | ( | string | name | ) |
| inline

Creates a real constant.

Definition at line 758 of file Context.cs.

759 {
760
761 return (RealExpr)MkConst(name, RealSort);
762 }

## ◆ MkRealConst() [2/2]

RealExpr MkRealConst | ( | Symbol | name | ) |
| inline

Creates a real constant.

Definition at line 748 of file Context.cs.

749 {
750 Debug.Assert(name != null);
751
752 return (RealExpr)MkConst(name, RealSort);
753 }

## ◆ MkRealSort()

RealSort MkRealSort | ( |  | ) |
| inline

Create a real sort.

Definition at line 211 of file Context.cs.

212 {
213 return new RealSort(this);
214 }

## ◆ MkRecFuncDecl()

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

Creates a new recursive function declaration.

Definition at line 537 of file Context.cs.

538 {
539 Debug.Assert(range != null);
540 Debug.Assert(domain.All(d => d != null));
541
542 CheckContextMatch<Sort>(domain);
543 CheckContextMatch(range);
544 return new FuncDecl(this, MkSymbol(name), domain, range, true);
545 }

## ◆ MkRem()

IntExpr MkRem | ( | IntExpr | t1,
|  | IntExpr | t2
| ) |  |
| inline

Create an expression representing `t1 rem t2`.

The arguments must have int type.

Definition at line 1106 of file Context.cs.

1107 {
1108 Debug.Assert(t1 != null);
1109 Debug.Assert(t2 != null);
1110
1111 CheckContextMatch(t1);
1112 CheckContextMatch(t2);
1113 return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1114 }

## ◆ MkRepeat()

BitVecExpr MkRepeat | ( | uint | i,
|  | BitVecExpr | t
| ) |  |
| inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1702 of file Context.cs.

1703 {
1704 Debug.Assert(t != null);
1705
1706 CheckContextMatch(t);
1707 return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1708 }

## ◆ MkReplace()

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

Replace the first occurrence of src by dst in s.

Definition at line 2525 of file Context.cs.

2526 {
2527 Debug.Assert(s != null);
2528 Debug.Assert(src != null);
2529 Debug.Assert(dst != null);
2530 CheckContextMatch(s, src, dst);
2531 return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2532 }

## ◆ MkReSort()

ReSort MkReSort | ( | SeqSort | s | ) |
| inline

Create a new regular expression sort.

Definition at line 237 of file Context.cs.

238 {
239 Debug.Assert(s != null);
240 return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
241 }
z3py.ReSort
def ReSort(s)
Definition: z3py.py:10904

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

2049 {
2050 Debug.Assert(a != null);
2051 Debug.Assert(i != null);
2052
2053 CheckContextMatch(a);
2054 CheckContextMatch(i);
2055 return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2056 }

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

2072 {
2073 Debug.Assert(a != null);
2074 Debug.Assert(args != null && args.All(n => n != null));
2075
2076 CheckContextMatch(a);
2077 CheckContextMatch<Expr>(args);
2078 return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2079 }

## ◆ MkSeqSort()

SeqSort MkSeqSort | ( | Sort | s | ) |
| inline

Create a new sequence sort.

Definition at line 228 of file Context.cs.

229 {
230 Debug.Assert(s != null);
231 return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
232 }
z3py.SeqSort
def SeqSort(s)
Definition: z3py.py:10579

## ◆ MkSetAdd()

ArrayExpr MkSetAdd | ( | ArrayExpr | set,
|  | Expr | element
| ) |  |
| inline

Add an element to the set.

Definition at line 2249 of file Context.cs.

2250 {
2251 Debug.Assert(set != null);
2252 Debug.Assert(element != null);
2253
2254 CheckContextMatch(set);
2255 CheckContextMatch(element);
2256 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2257 }

## ◆ MkSetComplement()

ArrayExpr MkSetComplement | ( | ArrayExpr | arg | ) |
| inline

Take the complement of a set.

Definition at line 2313 of file Context.cs.

2314 {
2315 Debug.Assert(arg != null);
2316
2317 CheckContextMatch(arg);
2318 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2319 }

## ◆ MkSetDel()

ArrayExpr MkSetDel | ( | ArrayExpr | set,
|  | Expr | element
| ) |  |
| inline

Remove an element from a set.

Definition at line 2263 of file Context.cs.

2264 {
2265 Debug.Assert(set != null);
2266 Debug.Assert(element != null);
2267
2268 CheckContextMatch(set);
2269 CheckContextMatch(element);
2270 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2271 }

## ◆ MkSetDifference()

ArrayExpr MkSetDifference | ( | ArrayExpr | arg1,
|  | ArrayExpr | arg2
| ) |  |
| inline

Take the difference between two sets.

Definition at line 2300 of file Context.cs.

2301 {
2302 Debug.Assert(arg1 != null);
2303 Debug.Assert(arg2 != null);
2304
2305 CheckContextMatch(arg1);
2306 CheckContextMatch(arg2);
2307 return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2308 }

## ◆ MkSetIntersection()

ArrayExpr MkSetIntersection | ( | params ArrayExpr[] | args | ) |
| inline

Take the intersection of a list of sets.

Definition at line 2288 of file Context.cs.

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

## ◆ MkSetMembership()

BoolExpr MkSetMembership | ( | Expr | elem,
|  | ArrayExpr | set
| ) |  |
| inline

Check for set membership.

Definition at line 2324 of file Context.cs.

2325 {
2326 Debug.Assert(elem != null);
2327 Debug.Assert(set != null);
2328
2329 CheckContextMatch(elem);
2330 CheckContextMatch(set);
2331 return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2332 }

## ◆ MkSetSort()

SetSort MkSetSort | ( | Sort | ty | ) |
| inline

Create a set type.

Definition at line 2216 of file Context.cs.

2217 {
2218 Debug.Assert(ty != null);
2219
2220 CheckContextMatch(ty);
2221 return new SetSort(this, ty);
2222 }
z3py.SetSort
def SetSort(s)
Sets.
Definition: z3py.py:4851

## ◆ MkSetSubset()

BoolExpr MkSetSubset | ( | ArrayExpr | arg1,
|  | ArrayExpr | arg2
| ) |  |
| inline

Check for subsetness of sets.

Definition at line 2337 of file Context.cs.

2338 {
2339 Debug.Assert(arg1 != null);
2340 Debug.Assert(arg2 != null);
2341
2342 CheckContextMatch(arg1);
2343 CheckContextMatch(arg2);
2344 return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2345 }

## ◆ MkSetUnion()

ArrayExpr MkSetUnion | ( | params ArrayExpr[] | args | ) |
| inline

Take the union of a list of sets.

Definition at line 2276 of file Context.cs.

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

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

1672 {
1673 Debug.Assert(t != null);
1674
1675 CheckContextMatch(t);
1676 return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1677 }

## ◆ MkSimpleSolver()

Solver MkSimpleSolver | ( |  | ) |
| inline

Creates a new (incremental) solver.

Definition at line 3753 of file Context.cs.

3754 {
3755
3756 return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3757 }

## ◆ MkSolver() [1/3]

Solver MkSolver | ( | string | logic | ) |
| inline

Creates a new (incremental) solver.

See also
  MkSolver(Symbol)

Definition at line 3744 of file Context.cs.

3745 {
3746
3747 return MkSolver(MkSymbol(logic));
3748 }
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3731

## ◆ MkSolver() [2/3]

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

3732 {
3733
3734 if (logic == null)
3735 return new Solver(this, Native.Z3_mk_solver(nCtx));
3736 else
3737 return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3738 }

Referenced by Context.MkSolver().

## ◆ MkSolver() [3/3]

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

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

## ◆ MkStar()

ReExpr MkStar | ( | ReExpr | re | ) |
| inline

Take the Kleene star of a regular expression.

Definition at line 2558 of file Context.cs.

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

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

2101 {
2102 Debug.Assert(a != null);
2103 Debug.Assert(i != null);
2104 Debug.Assert(v != null);
2105
2106 CheckContextMatch(a);
2107 CheckContextMatch(i);
2108 CheckContextMatch(v);
2109 return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2110 }

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

2131 {
2132 Debug.Assert(a != null);
2133 Debug.Assert(args != null);
2134 Debug.Assert(v != null);
2135
2136 CheckContextMatch<Expr>(args);
2137 CheckContextMatch(a);
2138 CheckContextMatch(v);
2139 return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
2140 }

## ◆ MkString()

SeqExpr MkString | ( | string | s | ) |
| inline

Create a string constant.

Definition at line 2372 of file Context.cs.

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

## ◆ MkStringLe()

BoolExpr MkStringLe | ( | SeqExpr | s1,
|  | SeqExpr | s2
| ) |  |
| inline

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

Definition at line 2468 of file Context.cs.

2469 {
2470 Debug.Assert(s1 != null);
2471 Debug.Assert(s2 != null);
2472 CheckContextMatch(s1, s2);
2473 return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2474 }

## ◆ MkStringLt()

BoolExpr MkStringLt | ( | SeqExpr | s1,
|  | SeqExpr | s2
| ) |  |
| inline

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

Definition at line 2457 of file Context.cs.

2458 {
2459 Debug.Assert(s1 != null);
2460 Debug.Assert(s2 != null);
2461 CheckContextMatch(s1, s2);
2462 return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2463 }

## ◆ MkSub()

ArithExpr MkSub | ( | params ArithExpr[] | t | ) |
| inline

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

Definition at line 1055 of file Context.cs.

1056 {
1057 Debug.Assert(t != null);
1058 Debug.Assert(t.All(a => a != null));
1059
1060 CheckContextMatch<ArithExpr>(t);
1061 return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1062 }

Referenced by ArithExpr.operator-().

## ◆ MkSuffixOf()

BoolExpr MkSuffixOf | ( | SeqExpr | s1,
|  | SeqExpr | s2
| ) |  |
| inline

Check for sequence suffix.

Definition at line 2435 of file Context.cs.

2436 {
2437 Debug.Assert(s1 != null);
2438 Debug.Assert(s2 != null);
2439 CheckContextMatch(s1, s2);
2440 return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2441 }

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

91 {
92
93 return new IntSymbol(this, i);
94 }

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

## ◆ MkSymbol() [2/2]

StringSymbol MkSymbol | ( | string | name | ) |
| inline

Create a symbol using a string.

Definition at line 99 of file Context.cs.

100 {
101
102 return new StringSymbol(this, name);
103 }

## ◆ MkTactic()

Tactic MkTactic | ( | string | name | ) |
| inline

Creates a new Tactic.

Definition at line 3334 of file Context.cs.

3335 {
3336
3337 return new Tactic(this, name);
3338 }

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

2190 {
2191 Debug.Assert(array != null);
2192
2193 CheckContextMatch(array);
2194 return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2195 }

## ◆ MkToRe()

ReExpr MkToRe | ( | SeqExpr | s | ) |
| inline

Convert a regular expression that accepts sequence s.

Definition at line 2537 of file Context.cs.

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

## ◆ MkTrue()

BoolExpr MkTrue | ( |  | ) |
| inline

The true Term.

Definition at line 815 of file Context.cs.

816 {
817
818 return new BoolExpr(this, Native.Z3_mk_true(nCtx));
819 }

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

## ◆ MkTupleSort()

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

Create a new tuple sort.

Definition at line 272 of file Context.cs.

273 {
274 Debug.Assert(name != null);
275 Debug.Assert(fieldNames != null);
276 Debug.Assert(fieldNames.All(fn => fn != null));
277 Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null));
278
279 CheckContextMatch(name);
280 CheckContextMatch<Symbol>(fieldNames);
281 CheckContextMatch<Sort>(fieldSorts);
282 return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
283 }
z3py.TupleSort
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5293

## ◆ MkUnaryMinus()

ArithExpr MkUnaryMinus | ( | ArithExpr | t | ) |
| inline

Create an expression representing `-t`.

Definition at line 1067 of file Context.cs.

1068 {
1069 Debug.Assert(t != null);
1070
1071 CheckContextMatch(t);
1072 return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1073 }

Referenced by ArithExpr.operator-().

## ◆ MkUninterpretedSort() [1/2]

UninterpretedSort MkUninterpretedSort | ( | string | str | ) |
| inline

Create a new uninterpreted sort.

Definition at line 193 of file Context.cs.

194 {
195
196 return MkUninterpretedSort(MkSymbol(str));
197 }
Microsoft.Z3.Context.MkUninterpretedSort
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:182

## ◆ MkUninterpretedSort() [2/2]

UninterpretedSort MkUninterpretedSort | ( | Symbol | s | ) |
| inline

Create a new uninterpreted sort.

Definition at line 182 of file Context.cs.

183 {
184 Debug.Assert(s != null);
185
186 CheckContextMatch(s);
187 return new UninterpretedSort(this, s);
188 }

Referenced by Context.MkUninterpretedSort().

## ◆ MkUnion()

ReExpr MkUnion | ( | params ReExpr[] | t | ) |
| inline

Create the union of regular languages.

Definition at line 2615 of file Context.cs.

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

## ◆ MkUnit()

SeqExpr MkUnit | ( | Expr | elem | ) |
| inline

Create the singleton sequence.

Definition at line 2363 of file Context.cs.

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

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

480 {
481 return Expr.Create(this, Native.Z3_datatype_update_field(
482 nCtx, field.NativeObject,
483 t.NativeObject, v.NativeObject));
484 }

## ◆ MkXor() [1/2]

BoolExpr MkXor | ( | BoolExpr | t1,
|  | BoolExpr | t2
| ) |  |
| inline

Create an expression representing `t1 xor t2`.

Definition at line 923 of file Context.cs.

924 {
925 Debug.Assert(t1 != null);
926 Debug.Assert(t2 != null);
927
928 CheckContextMatch(t1);
929 CheckContextMatch(t2);
930 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
931 }

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

## ◆ MkXor() [2/2]

BoolExpr MkXor | ( | IEnumerable< BoolExpr > | ts | ) |
| inline

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

Definition at line 936 of file Context.cs.

937 {
938 Debug.Assert(ts != null);
939 Debug.Assert(ts.All(a => a != null));
940 CheckContextMatch<BoolExpr>(ts);
941 BoolExpr r = null;
942 foreach (var t in ts) {
943 if (r == null)
944 r = t;
945 else
946 r = MkXor(r, t);
947 }
948 if (r == null)
949 r = MkTrue();
950 return r;
951 }
Microsoft.Z3.Context.MkXor
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:923

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

1689 {
1690 Debug.Assert(t != null);
1691
1692 CheckContextMatch(t);
1693 return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1694 }

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

3714 {
3715 Debug.Assert(p != null);
3716
3717 CheckContextMatch(p);
3718 return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3719 }

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

3700 {
3701 Debug.Assert(p1 != null);
3702 Debug.Assert(p2 != null);
3703
3704 CheckContextMatch(p1);
3705 CheckContextMatch(p2);
3706 return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3707 }

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

3392 {
3393 Debug.Assert(t1 != null);
3394 Debug.Assert(t2 != null);
3395
3396 CheckContextMatch(t1);
3397 CheckContextMatch(t2);
3398 return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3399 }

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

3540 {
3541 Debug.Assert(t1 != null);
3542 Debug.Assert(t2 != null);
3543
3544 CheckContextMatch(t1);
3545 CheckContextMatch(t2);
3546 return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3547 }

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

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

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

3253 {
3254
3255 uint csn = Symbol.ArrayLength(sortNames);
3256 uint cs = Sort.ArrayLength(sorts);
3257 uint cdn = Symbol.ArrayLength(declNames);
3258 uint cd = AST.ArrayLength(decls);
3259 if (csn != cs || cdn != cd)
3260 throw new Z3Exception("Argument size mismatch");
3261 ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3262 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3263 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3264 return assertions.ToBoolExprArray();
3265 }

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

3234 {
3235
3236 uint csn = Symbol.ArrayLength(sortNames);
3237 uint cs = Sort.ArrayLength(sorts);
3238 uint cdn = Symbol.ArrayLength(declNames);
3239 uint cd = AST.ArrayLength(decls);
3240 if (csn != cs || cdn != cd)
3241 throw new Z3Exception("Argument size mismatch");
3242 ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3243 AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3244 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3245 return assertions.ToBoolExprArray();
3246 }

## ◆ ProbeDescription()

string ProbeDescription | ( | string | name | ) |
| inline

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

Definition at line 3587 of file Context.cs.

3588 {
3589
3590 return Native.Z3_probe_get_descr(nCtx, name);
3591 }

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

3453 {
3454 Debug.Assert(t != null);
3455
3456 CheckContextMatch(t);
3457 return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3458 }
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836

## ◆ SimplifyHelp()

string SimplifyHelp | ( |  | ) |
| inline

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

Definition at line 4564 of file Context.cs.

4565 {
4566
4567 return Native.Z3_simplify_get_help(nCtx);
4568 }

## ◆ Skip()

Tactic Skip | ( |  | ) |
| inline

Create a tactic that just returns the given goal.

Definition at line 3463 of file Context.cs.

3464 {
3465
3466 return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3467 }

## ◆ StringToInt()

IntExpr StringToInt | ( | Expr | e | ) |
| inline

Convert an integer expression to a string.

Definition at line 2391 of file Context.cs.

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

## ◆ TacticDescription()

string TacticDescription | ( | string | name | ) |
| inline

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

Definition at line 3325 of file Context.cs.

3326 {
3327
3328 return Native.Z3_tactic_get_descr(nCtx, name);
3329 }

## ◆ Then()

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

3379 {
3380 Debug.Assert(t1 != null);
3381 Debug.Assert(t2 != null);
3382 // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3383
3384 return AndThen(t1, t2, ts);
3385 }
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:3344

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

3408 {
3409 Debug.Assert(t != null);
3410
3411 CheckContextMatch(t);
3412 return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3413 }

## ◆ UnwrapAST()

IntPtr UnwrapAST | ( | AST | a | ) |
| inline

Unwraps an AST.

This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,

See also
  Native.Z3_inc_ref

).

See also
  WrapAST

Parameters

  a | The AST to unwrap.

Definition at line 4556 of file Context.cs.

4557 {
4558 return a.NativeObject;
4559 }

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

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

## ◆ UsingParams()

Tactic UsingParams | ( | Tactic | t,
|  | Params | p
| ) |  |
| inline

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

Definition at line 3502 of file Context.cs.

3503 {
3504 Debug.Assert(t != null);
3505 Debug.Assert(p != null);
3506
3507 CheckContextMatch(t);
3508 CheckContextMatch(p);
3509 return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3510 }

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

3423 {
3424 Debug.Assert(p != null);
3425 Debug.Assert(t != null);
3426
3427 CheckContextMatch(t);
3428 CheckContextMatch(p);
3429 return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3430 }

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

3517 {
3518 Debug.Assert(t != null);
3519 Debug.Assert(p != null);
3520
3521 return UsingParams(t, p);
3522 }
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:3502

## ◆ WrapAST()

AST WrapAST | ( | IntPtr | nativeObject | ) |
| inline

Wraps an AST.

This function is used for transitions between native and managed objects. Note that nativeObject must be a native object obtained from Z3 (e.g., through

See also
  UnwrapAST, Native.Z3_inc_ref

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

See also
  UnwrapAST

Parameters

  nativeObject | The native pointer to wrap.

Definition at line 4540 of file Context.cs.

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

## Property Documentation

## ◆ ApplyResult_DRQ

IDecRefQueue ApplyResult_DRQ
| get

ApplyResult DRQ

Definition at line 4740 of file Context.cs.

4740{ get { return m_ApplyResult_DRQ; } }

Referenced by Context.Dispose().

## ◆ AST_DRQ

IDecRefQueue AST_DRQ
| get

AST DRQ

Definition at line 4725 of file Context.cs.

4725{ get { return m_AST_DRQ; } }

Referenced by Context.Dispose().

## ◆ ASTMap_DRQ

IDecRefQueue ASTMap_DRQ
| get

ASTMap DRQ

Definition at line 4730 of file Context.cs.

4730{ get { return m_ASTMap_DRQ; } }

Referenced by Context.Dispose().

## ◆ ASTVector_DRQ

IDecRefQueue ASTVector_DRQ
| get

ASTVector DRQ

Definition at line 4735 of file Context.cs.

4735{ get { return m_ASTVector_DRQ; } }

Referenced by Context.Dispose().

## ◆ BoolSort

BoolSort BoolSort
| get

Retrieves the Boolean sort of the context.

Definition at line 127 of file Context.cs.

128 {
129 get
130 {
131 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
132 }
133 }

Referenced by Context.MkBoolSort().

## ◆ Fixedpoint_DRQ

IDecRefQueue Fixedpoint_DRQ
| get

FixedPoint DRQ

Definition at line 4795 of file Context.cs.

4795{ get { return m_Fixedpoint_DRQ; } }

Referenced by Context.Dispose().

## ◆ FuncEntry_DRQ

IDecRefQueue FuncEntry_DRQ
| get

FuncEntry DRQ

Definition at line 4745 of file Context.cs.

4745{ get { return m_FuncEntry_DRQ; } }

Referenced by Context.Dispose().

## ◆ FuncInterp_DRQ

IDecRefQueue FuncInterp_DRQ
| get

FuncInterp DRQ

Definition at line 4750 of file Context.cs.

4750{ get { return m_FuncInterp_DRQ; } }

Referenced by Context.Dispose().

## ◆ Goal_DRQ

IDecRefQueue Goal_DRQ
| get

Goal DRQ

Definition at line 4755 of file Context.cs.

4755{ get { return m_Goal_DRQ; } }

Referenced by Context.Dispose().

## ◆ IntSort

IntSort IntSort
| get

Retrieves the Integer sort of the context.

Definition at line 138 of file Context.cs.

139 {
140 get
141 {
142 if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
143 }
144 }

Referenced by Context.MkIntSort().

## ◆ Model_DRQ

IDecRefQueue Model_DRQ
| get

Model DRQ

Definition at line 4760 of file Context.cs.

4760{ get { return m_Model_DRQ; } }

Referenced by Context.Dispose().

## ◆ NumProbes

uint NumProbes
| get

The number of supported Probes.

Definition at line 3563 of file Context.cs.

3564 {
3565 get { return Native.Z3_get_num_probes(nCtx); }
3566 }

## ◆ NumTactics

uint NumTactics
| get

The number of supported tactics.

Definition at line 3301 of file Context.cs.

3302 {
3303 get { return Native.Z3_get_num_tactics(nCtx); }
3304 }

## ◆ Optimize_DRQ

IDecRefQueue Optimize_DRQ
| get

Optimize DRQ

Definition at line 4800 of file Context.cs.

4800{ get { return m_Fixedpoint_DRQ; } }

Referenced by Context.Dispose().

## ◆ ParamDescrs_DRQ

IDecRefQueue ParamDescrs_DRQ
| get

ParamDescrs DRQ

Definition at line 4770 of file Context.cs.

4770{ get { return m_ParamDescrs_DRQ; } }

Referenced by Context.Dispose().

## ◆ Params_DRQ

IDecRefQueue Params_DRQ
| get

Params DRQ

Definition at line 4765 of file Context.cs.

4765{ get { return m_Params_DRQ; } }

Referenced by Context.Dispose().

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

3222 {
3223 set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3224 }

## ◆ Probe_DRQ

IDecRefQueue Probe_DRQ
| get

Probe DRQ

Definition at line 4775 of file Context.cs.

4775{ get { return m_Probe_DRQ; } }

Referenced by Context.Dispose().

## ◆ ProbeNames

string [] ProbeNames
| get

The names of all supported Probes.

Definition at line 3571 of file Context.cs.

3572 {
3573 get
3574 {
3575
3576 uint n = NumProbes;
3577 string[] res = new string[n];
3578 for (uint i = 0; i < n; i++)
3579 res[i] = Native.Z3_get_probe_name(nCtx, i);
3580 return res;
3581 }
3582 }
Microsoft.Z3.Context.NumProbes
uint NumProbes
The number of supported Probes.
Definition: Context.cs:3564

## ◆ RealSort

RealSort RealSort
| get

Retrieves the Real sort of the context.

Definition at line 150 of file Context.cs.

151 {
152 get
153 {
154 if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
155 }
156 }

Referenced by Context.MkRealSort().

## ◆ SimplifyParameterDescriptions

ParamDescrs SimplifyParameterDescriptions
| get

Retrieves parameter descriptions for simplifier.

Definition at line 4573 of file Context.cs.

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

## ◆ Solver_DRQ

IDecRefQueue Solver_DRQ
| get

Solver DRQ

Definition at line 4780 of file Context.cs.

4780{ get { return m_Solver_DRQ; } }

Referenced by Context.Dispose().

## ◆ Statistics_DRQ

IDecRefQueue Statistics_DRQ
| get

Statistics DRQ

Definition at line 4785 of file Context.cs.

4785{ get { return m_Statistics_DRQ; } }

Referenced by Context.Dispose().

## ◆ StringSort

SeqSort StringSort
| get

Retrieves the String sort of the context.

Definition at line 161 of file Context.cs.

162 {
163 get
164 {
165 if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
166 return m_stringSort;
167 }
168 }

## ◆ Tactic_DRQ

IDecRefQueue Tactic_DRQ
| get

Tactic DRQ

Definition at line 4790 of file Context.cs.

4790{ get { return m_Tactic_DRQ; } }

Referenced by Context.Dispose().

## ◆ TacticNames

string [] TacticNames
| get

The names of all supported tactics.

Definition at line 3309 of file Context.cs.

3310 {
3311 get
3312 {
3313
3314 uint n = NumTactics;
3315 string[] res = new string[n];
3316 for (uint i = 0; i < n; i++)
3317 res[i] = Native.Z3_get_tactic_name(nCtx, i);
3318 return res;
3319 }
3320 }
Microsoft.Z3.Context.NumTactics
uint NumTactics
The number of supported tactics.
Definition: Context.cs:3302