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...
 
FuncDecl MkUserPropagatorFuncDecl (string name, Sort[] domain, Sort range)
 Declare a function to be processed by the user propagator plugin. 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 MkDistinct (IEnumerable< 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...
 
SeqExpr UbvToString (Expr e)
 Convert a bit-vector expression, represented as an unsigned number, to a string. More...
 
SeqExpr SbvToString (Expr e)
 Convert a bit-vector expression, represented as an signed number, 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 less or equal to 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 MkDiff (ReExpr a, ReExpr b)
 Create a difference regular expression. 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 MkCharLe (Expr ch1, Expr ch2)
 Create less than or equal to between two characters. More...
 
IntExpr CharToInt (Expr ch)
 Create an integer (code point) from character. More...
 
BitVecExpr CharToBV (Expr ch)
 Create a bit-vector (code point) from character. More...
 
Expr CharFromBV (BitVecExpr bv)
 Create a character from a bit-vector (code point). More...
 
BoolExpr MkIsDigit (Expr ch)
 Create a check if the character is a digit. 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 sign)
 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...
 
CharSort CharSort [get]
 Retrieves the String 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...
 

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 33 of file Context.cs.

Constructor & Destructor Documentation

◆ Context() [1/2]

Context ( )
inline

Constructor.

Definition at line 39 of file Context.cs.

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

◆ Context() [2/2]

Context ( Dictionary< string, string >  settings)
inline

Constructor.

The following parameters can be set:

  • proof (Boolean) Enable proof generation
  • debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
  • trace (Boolean) Tracing support for VCC
  • trace_file_name (String) Trace out file for VCC traces
  • timeout (unsigned) default timeout (in milliseconds) used for solvers
  • well_sorted_check type checker
  • auto_config use heuristics to automatically select solver and configure it
  • model model generation for solvers, this parameter can be overwritten when creating a solver
  • model_validate validate models produced by solvers
  • unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver Note that in previous versions of Z3, this constructor was also used to set global and module parameters. For this purpose we should now use Global.SetParameter

Definition at line 68 of file Context.cs.

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

Member Function Documentation

◆ AddRecDef()

void AddRecDef ( FuncDecl  f,
Expr[]  args,
Expr  body 
)
inline

Bind a definition to a recursive function declaration. The function must have previously been created using MkRecFuncDecl. The body may contain recursive uses of the function or other mutually recursive functions.

Definition at line 617 of file Context.cs.

618  {
619  CheckContextMatch(f);
620  CheckContextMatch<Expr>(args);
621  CheckContextMatch(body);
622  IntPtr[] argsNative = AST.ArrayToNative(args);
623  Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
624  }

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

3856  {
3857  Debug.Assert(p1 != null);
3858  Debug.Assert(p2 != null);
3859 
3860  CheckContextMatch(p1);
3861  CheckContextMatch(p2);
3862  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3863  }

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

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

Referenced by Context.Then().

◆ CharFromBV()

Expr CharFromBV ( BitVecExpr  bv)
inline

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

Definition at line 2821 of file Context.cs.

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

◆ CharToBV()

BitVecExpr CharToBV ( Expr  ch)
inline

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

Definition at line 2812 of file Context.cs.

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

◆ CharToInt()

IntExpr CharToInt ( Expr  ch)
inline

Create an integer (code point) from character.

Definition at line 2803 of file Context.cs.

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

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

3607  {
3608  Debug.Assert(p != null);
3609  Debug.Assert(t1 != null);
3610  Debug.Assert(t2 != null);
3611 
3612  CheckContextMatch(p);
3613  CheckContextMatch(t1);
3614  CheckContextMatch(t2);
3615  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3616  }

◆ ConstProbe()

Probe ConstProbe ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3775 of file Context.cs.

3776  {
3777 
3778  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3779  }

◆ Dispose()

void Dispose ( )
inline

Disposes of the context.

Definition at line 4871 of file Context.cs.

4872  {
4873  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4874 
4875  if (m_boolSort != null) m_boolSort.Dispose();
4876  if (m_intSort != null) m_intSort.Dispose();
4877  if (m_realSort != null) m_realSort.Dispose();
4878  if (m_stringSort != null) m_stringSort.Dispose();
4879  if (m_charSort != null) m_charSort.Dispose();
4880  m_boolSort = null;
4881  m_intSort = null;
4882  m_realSort = null;
4883  m_stringSort = null;
4884  m_charSort = null;
4885  if (m_ctx != IntPtr.Zero)
4886  {
4887  IntPtr ctx = m_ctx;
4888  lock (this)
4889  {
4890  m_n_err_handler = null;
4891  m_ctx = IntPtr.Zero;
4892  }
4893  if (!is_external)
4894  Native.Z3_del_context(ctx);
4895  }
4896 
4897  GC.SuppressFinalize(this);
4898  }
void Dispose()
Disposes of the underlying native Z3 object.
Definition: Z3Object.cs:45

◆ Eq()

Probe Eq ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2

Definition at line 3841 of file Context.cs.

3842  {
3843  Debug.Assert(p1 != null);
3844  Debug.Assert(p2 != null);
3845 
3846  CheckContextMatch(p1);
3847  CheckContextMatch(p2);
3848  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3849  }

◆ Fail()

Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3642 of file Context.cs.

3643  {
3644 
3645  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3646  }

◆ FailIf()

Tactic FailIf ( Probe  p)
inline

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

Definition at line 3651 of file Context.cs.

3652  {
3653  Debug.Assert(p != null);
3654 
3655  CheckContextMatch(p);
3656  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3657  }

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

3664  {
3665 
3666  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3667  }

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

3828  {
3829  Debug.Assert(p1 != null);
3830  Debug.Assert(p2 != null);
3831 
3832  CheckContextMatch(p1);
3833  CheckContextMatch(p2);
3834  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3835  }

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

3800  {
3801  Debug.Assert(p1 != null);
3802  Debug.Assert(p2 != null);
3803 
3804  CheckContextMatch(p1);
3805  CheckContextMatch(p2);
3806  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3807  }

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

3724  {
3725  Native.Z3_interrupt(nCtx);
3726  }

◆ IntToString()

SeqExpr IntToString ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 2472 of file Context.cs.

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

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

3814  {
3815  Debug.Assert(p1 != null);
3816  Debug.Assert(p2 != null);
3817 
3818  CheckContextMatch(p1);
3819  CheckContextMatch(p2);
3820  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3821  }

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

3786  {
3787  Debug.Assert(p1 != null);
3788  Debug.Assert(p2 != null);
3789 
3790  CheckContextMatch(p1);
3791  CheckContextMatch(p2);
3792  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3793  }

◆ MkAdd() [1/2]

ArithExpr MkAdd ( IEnumerable< ArithExpr t)
inline

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

Definition at line 1104 of file Context.cs.

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

◆ MkAdd() [2/2]

ArithExpr MkAdd ( params ArithExpr[]  t)
inline

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

Definition at line 1092 of file Context.cs.

1093  {
1094  Debug.Assert(t != null);
1095  Debug.Assert(t.All(a => a != null));
1096 
1097  CheckContextMatch<ArithExpr>(t);
1098  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1099  }

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

1052  {
1053  Debug.Assert(t != null);
1054  Debug.Assert(t.All(a => a != null));
1055  CheckContextMatch<BoolExpr>(t);
1056  var ands = t.ToArray();
1057  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands)));
1058  }

◆ MkAnd() [2/2]

BoolExpr MkAnd ( params BoolExpr[]  t)
inline

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

Definition at line 1039 of file Context.cs.

1040  {
1041  Debug.Assert(t != null);
1042  Debug.Assert(t.All(a => a != null));
1043 
1044  CheckContextMatch<BoolExpr>(t);
1045  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1046  }

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

880  {
881  Debug.Assert(f != null);
882  Debug.Assert(args == null || args.All(a => a != null));
883 
884  CheckContextMatch(f);
885  CheckContextMatch(args);
886  return Expr.Create(this, f, args.ToArray());
887  }

◆ MkApp() [2/2]

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

Create a new function application.

Definition at line 866 of file Context.cs.

867  {
868  Debug.Assert(f != null);
869  Debug.Assert(args == null || args.All(a => a != null));
870 
871  CheckContextMatch(f);
872  CheckContextMatch<Expr>(args);
873  return Expr.Create(this, f, args);
874  }

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

2116  {
2117  Debug.Assert(domain != null);
2118  Debug.Assert(range != null);
2119 
2120  using var symbol = MkSymbol(name);
2121  using var sort = MkArraySort(domain, range);
2122  return (ArrayExpr)MkConst(symbol, sort);
2123  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:738
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:276
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:111
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3970

◆ MkArrayConst() [2/2]

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

Create an array constant.

Definition at line 2102 of file Context.cs.

2103  {
2104  Debug.Assert(name != null);
2105  Debug.Assert(domain != null);
2106  Debug.Assert(range != null);
2107 
2108  using var sort = MkArraySort(domain, range);
2109  return (ArrayExpr)MkConst(name, sort);
2110  }

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

2292  {
2293  Debug.Assert(arg1 != null);
2294  Debug.Assert(arg2 != null);
2295 
2296  CheckContextMatch(arg1);
2297  CheckContextMatch(arg2);
2298  return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2299  }

◆ MkArraySort() [1/2]

ArraySort MkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 276 of file Context.cs.

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

Referenced by Context.MkArrayConst().

◆ MkArraySort() [2/2]

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

Create a new n-ary array sort.

Definition at line 289 of file Context.cs.

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

◆ MkAt()

SeqExpr MkAt ( SeqExpr  s,
Expr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2590 of file Context.cs.

2591  {
2592  Debug.Assert(s != null);
2593  Debug.Assert(index != null);
2594  CheckContextMatch(s, index);
2595  return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2596  }

◆ MkAtLeast()

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

Create an at-least-k constraint.

Definition at line 2855 of file Context.cs.

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

◆ MkAtMost()

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

Create an at-most-k constraint.

Definition at line 2843 of file Context.cs.

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

◆ MkBitVecSort()

BitVecSort MkBitVecSort ( uint  size)
inline

Create a new bit-vector sort.

Definition at line 250 of file Context.cs.

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

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

◆ MkBool()

BoolExpr MkBool ( bool  value)
inline

Creates a Boolean value.

Definition at line 911 of file Context.cs.

912  {
913 
914  return value ? MkTrue() : MkFalse();
915  }
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:893
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:902

◆ MkBoolConst() [1/2]

BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 796 of file Context.cs.

797  {
798  using var symbol = MkSymbol(name);
799  return (BoolExpr)MkConst(symbol, BoolSort);
800  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:147

◆ MkBoolConst() [2/2]

BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 786 of file Context.cs.

787  {
788  Debug.Assert(name != null);
789 
790  return (BoolExpr)MkConst(name, BoolSort);
791  }

◆ MkBoolSort()

BoolSort MkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 205 of file Context.cs.

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

◆ MkBound()

Expr MkBound ( uint  index,
Sort  ty 
)
inline

Creates a new bound variable.

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

Definition at line 711 of file Context.cs.

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

◆ MkBV() [1/6]

BitVecNum MkBV ( bool[]  bits)
inline

Create a bit-vector numeral.

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

Definition at line 3172 of file Context.cs.

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

◆ MkBV() [2/6]

BitVecNum MkBV ( int  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3129 of file Context.cs.

3130  {
3131  using var sort = MkBitVecSort(size);
3132  return (BitVecNum)MkNumeral(v, sort);
3133  }
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:250
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2915

◆ MkBV() [3/6]

BitVecNum MkBV ( long  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3151 of file Context.cs.

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

◆ MkBV() [4/6]

BitVecNum MkBV ( string  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3118 of file Context.cs.

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

◆ MkBV() [5/6]

BitVecNum MkBV ( uint  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3140 of file Context.cs.

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

◆ MkBV() [6/6]

BitVecNum MkBV ( ulong  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 3162 of file Context.cs.

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

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

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

◆ MkBVAdd()

BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition.

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_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1459  }

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

1978  {
1979  Debug.Assert(t1 != null);
1980  Debug.Assert(t2 != null);
1981 
1982  CheckContextMatch(t1);
1983  CheckContextMatch(t2);
1984  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
1985  }

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

1994  {
1995  Debug.Assert(t1 != null);
1996  Debug.Assert(t2 != null);
1997 
1998  CheckContextMatch(t1);
1999  CheckContextMatch(t2);
2000  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2001  }

◆ MkBVAND()

BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1355 of file Context.cs.

1356  {
1357  Debug.Assert(t1 != null);
1358  Debug.Assert(t2 != null);
1359 
1360  CheckContextMatch(t1);
1361  CheckContextMatch(t2);
1362  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1363  }

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

1857  {
1858  Debug.Assert(t1 != null);
1859  Debug.Assert(t2 != null);
1860 
1861  CheckContextMatch(t1);
1862  CheckContextMatch(t2);
1863  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1864  }

◆ MkBVConst() [1/2]

BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 855 of file Context.cs.

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

◆ MkBVConst() [2/2]

BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 844 of file Context.cs.

845  {
846  Debug.Assert(name != null);
847 
848  using var sort = MkBitVecSort(size);
849  return (BitVecExpr)MkConst(name, sort);
850  }

◆ 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 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_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1840  }

◆ MkBVMul()

BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1479 of file Context.cs.

1480  {
1481  Debug.Assert(t1 != null);
1482  Debug.Assert(t2 != null);
1483 
1484  CheckContextMatch(t1);
1485  CheckContextMatch(t2);
1486  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1487  }

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

2072  {
2073  Debug.Assert(t1 != null);
2074  Debug.Assert(t2 != null);
2075 
2076  CheckContextMatch(t1);
2077  CheckContextMatch(t2);
2078  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2079  }

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

2088  {
2089  Debug.Assert(t1 != null);
2090  Debug.Assert(t2 != null);
2091 
2092  CheckContextMatch(t1);
2093  CheckContextMatch(t2);
2094  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2095  }

◆ MkBVNAND()

BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1397 of file Context.cs.

1398  {
1399  Debug.Assert(t1 != null);
1400  Debug.Assert(t2 != null);
1401 
1402  CheckContextMatch(t1);
1403  CheckContextMatch(t2);
1404  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1405  }

◆ MkBVNeg()

BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1439 of file Context.cs.

1440  {
1441  Debug.Assert(t != null);
1442 
1443  CheckContextMatch(t);
1444  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1445  }

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

2058  {
2059  Debug.Assert(t != null);
2060 
2061  CheckContextMatch(t);
2062  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2063  }

◆ MkBVNOR()

BitVecExpr MkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1411 of file Context.cs.

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

◆ MkBVNot()

BitVecExpr MkBVNot ( BitVecExpr  t)
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1319 of file Context.cs.

1320  {
1321  Debug.Assert(t != null);
1322 
1323  CheckContextMatch(t);
1324  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1325  }

◆ MkBVOR()

BitVecExpr MkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1369 of file Context.cs.

1370  {
1371  Debug.Assert(t1 != null);
1372  Debug.Assert(t2 != null);
1373 
1374  CheckContextMatch(t1);
1375  CheckContextMatch(t2);
1376  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1377  }

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

1332  {
1333  Debug.Assert(t != null);
1334 
1335  CheckContextMatch(t);
1336  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1337  }

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

1344  {
1345  Debug.Assert(t != null);
1346 
1347  CheckContextMatch(t);
1348  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1349  }

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

1904  {
1905  Debug.Assert(t1 != null);
1906  Debug.Assert(t2 != null);
1907 
1908  CheckContextMatch(t1);
1909  CheckContextMatch(t2);
1910  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1911  }

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

1874  {
1875  Debug.Assert(t != null);
1876 
1877  CheckContextMatch(t);
1878  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1879  }

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

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

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

1889  {
1890  Debug.Assert(t != null);
1891 
1892  CheckContextMatch(t);
1893  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1894  }

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

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

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

2042  {
2043  Debug.Assert(t1 != null);
2044  Debug.Assert(t2 != null);
2045 
2046  CheckContextMatch(t1);
2047  CheckContextMatch(t2);
2048  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2049  }

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

1673  {
1674  Debug.Assert(t1 != null);
1675  Debug.Assert(t2 != null);
1676 
1677  CheckContextMatch(t1);
1678  CheckContextMatch(t2);
1679  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1680  }

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

1705  {
1706  Debug.Assert(t1 != null);
1707  Debug.Assert(t2 != null);
1708 
1709  CheckContextMatch(t1);
1710  CheckContextMatch(t2);
1711  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1712  }

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

1811  {
1812  Debug.Assert(t1 != null);
1813  Debug.Assert(t2 != null);
1814 
1815  CheckContextMatch(t1);
1816  CheckContextMatch(t2);
1817  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1818  }

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

1641  {
1642  Debug.Assert(t1 != null);
1643  Debug.Assert(t2 != null);
1644 
1645  CheckContextMatch(t1);
1646  CheckContextMatch(t2);
1647  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1648  }

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

1609  {
1610  Debug.Assert(t1 != null);
1611  Debug.Assert(t2 != null);
1612 
1613  CheckContextMatch(t1);
1614  CheckContextMatch(t2);
1615  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1616  }

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

1577  {
1578  Debug.Assert(t1 != null);
1579  Debug.Assert(t2 != null);
1580 
1581  CheckContextMatch(t1);
1582  CheckContextMatch(t2);
1583  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1584  }

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

1560  {
1561  Debug.Assert(t1 != null);
1562  Debug.Assert(t2 != null);
1563 
1564  CheckContextMatch(t1);
1565  CheckContextMatch(t2);
1566  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1567  }

◆ MkBVSub()

BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1465 of file Context.cs.

1466  {
1467  Debug.Assert(t1 != null);
1468  Debug.Assert(t2 != null);
1469 
1470  CheckContextMatch(t1);
1471  CheckContextMatch(t2);
1472  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1473  }

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

2010  {
2011  Debug.Assert(t1 != null);
2012  Debug.Assert(t2 != null);
2013 
2014  CheckContextMatch(t1);
2015  CheckContextMatch(t2);
2016  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2017  }

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

2026  {
2027  Debug.Assert(t1 != null);
2028  Debug.Assert(t2 != null);
2029 
2030  CheckContextMatch(t1);
2031  CheckContextMatch(t2);
2032  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (byte)(isSigned ? 1 : 0)));
2033  }

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

1499  {
1500  Debug.Assert(t1 != null);
1501  Debug.Assert(t2 != null);
1502 
1503  CheckContextMatch(t1);
1504  CheckContextMatch(t2);
1505  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1506  }

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

1657  {
1658  Debug.Assert(t1 != null);
1659  Debug.Assert(t2 != null);
1660 
1661  CheckContextMatch(t1);
1662  CheckContextMatch(t2);
1663  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1664  }

◆ MkBVUGT()

BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1688 of file Context.cs.

1689  {
1690  Debug.Assert(t1 != null);
1691  Debug.Assert(t2 != null);
1692 
1693  CheckContextMatch(t1);
1694  CheckContextMatch(t2);
1695  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1696  }

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

1625  {
1626  Debug.Assert(t1 != null);
1627  Debug.Assert(t2 != null);
1628 
1629  CheckContextMatch(t1);
1630  CheckContextMatch(t2);
1631  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1632  }

◆ MkBVULT()

BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1592 of file Context.cs.

1593  {
1594  Debug.Assert(t1 != null);
1595  Debug.Assert(t2 != null);
1596 
1597  CheckContextMatch(t1);
1598  CheckContextMatch(t2);
1599  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1600  }

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

1540  {
1541  Debug.Assert(t1 != null);
1542  Debug.Assert(t2 != null);
1543 
1544  CheckContextMatch(t1);
1545  CheckContextMatch(t2);
1546  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1547  }

◆ MkBVXNOR()

BitVecExpr MkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1425 of file Context.cs.

1426  {
1427  Debug.Assert(t1 != null);
1428  Debug.Assert(t2 != null);
1429 
1430  CheckContextMatch(t1);
1431  CheckContextMatch(t2);
1432  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1433  }

◆ MkBVXOR()

BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1383 of file Context.cs.

1384  {
1385  Debug.Assert(t1 != null);
1386  Debug.Assert(t2 != null);
1387 
1388  CheckContextMatch(t1);
1389  CheckContextMatch(t2);
1390  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1391  }

◆ MkCharLe()

BoolExpr MkCharLe ( Expr  ch1,
Expr  ch2 
)
inline

Create less than or equal to between two characters.

Definition at line 2793 of file Context.cs.

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

◆ MkComplement()

ReExpr MkComplement ( ReExpr  re)
inline

Create the complement regular expression.

Definition at line 2705 of file Context.cs.

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

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

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

◆ MkConcat() [2/3]

ReExpr MkConcat ( params ReExpr[]  t)
inline

Create the concatenation of regular languages.

Definition at line 2714 of file Context.cs.

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

◆ MkConcat() [3/3]

SeqExpr MkConcat ( params SeqExpr[]  t)
inline

Concatenate sequences.

Definition at line 2513 of file Context.cs.

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

◆ MkConst() [1/3]

Expr MkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 776 of file Context.cs.

777  {
778  Debug.Assert(f != null);
779 
780  return MkApp(f);
781  }
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:866

◆ MkConst() [2/3]

Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 752 of file Context.cs.

753  {
754  Debug.Assert(range != null);
755 
756  using var symbol = MkSymbol(name);
757  return MkConst(symbol, range);
758  }

◆ MkConst() [3/3]

Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 738 of file Context.cs.

739  {
740  Debug.Assert(name != null);
741  Debug.Assert(range != null);
742 
743  CheckContextMatch(name);
744  CheckContextMatch(range);
745 
746  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
747  }

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 selecton an arbitrary index produces the value v.

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

Definition at line 2242 of file Context.cs.

2243  {
2244  Debug.Assert(domain != null);
2245  Debug.Assert(v != null);
2246 
2247  CheckContextMatch(domain);
2248  CheckContextMatch(v);
2249  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2250  }

◆ MkConstDecl() [1/2]

FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 672 of file Context.cs.

673  {
674  Debug.Assert(range != null);
675 
676  CheckContextMatch(range);
677  using var symbol = MkSymbol(name);
678  return new FuncDecl(this, symbol, null, range);
679  }

◆ MkConstDecl() [2/2]

FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 659 of file Context.cs.

660  {
661  Debug.Assert(name != null);
662  Debug.Assert(range != null);
663 
664  CheckContextMatch(name);
665  CheckContextMatch(range);
666  return new FuncDecl(this, name, null, range);
667  }

◆ MkConstructor() [1/2]

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

Create a datatype constructor.

Parameters
name
recognizer
fieldNames
sorts
sortRefs
Returns

Definition at line 432 of file Context.cs.

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

◆ MkConstructor() [2/2]

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

Create a datatype constructor.

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

Definition at line 415 of file Context.cs.

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

◆ MkContains()

BoolExpr MkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2557 of file Context.cs.

2558  {
2559  Debug.Assert(s1 != null);
2560  Debug.Assert(s2 != null);
2561  CheckContextMatch(s1, s2);
2562  return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2563  }

◆ MkDatatypeSort() [1/2]

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

Create a new datatype sort.

Definition at line 467 of file Context.cs.

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

◆ MkDatatypeSort() [2/2]

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

Create a new datatype sort.

Definition at line 452 of file Context.cs.

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

◆ MkDatatypeSorts() [1/2]

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

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 515 of file Context.cs.

516  {
517  Debug.Assert(names != null);
518  Debug.Assert(c != null);
519  Debug.Assert(names.Length == c.Length);
520  //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
521  //Debug.Assert(names.All(name => name != null));
522 
523  var symbols = MkSymbols(names);
524  try
525  {
526  return MkDatatypeSorts(symbols, c);
527  }
528  finally
529  {
530  foreach (var symbol in symbols)
531  symbol.Dispose();
532  }
533  }
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:482

◆ MkDatatypeSorts() [2/2]

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

Create mutually recursive datatypes.

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

Definition at line 482 of file Context.cs.

483  {
484  Debug.Assert(names != null);
485  Debug.Assert(c != null);
486  Debug.Assert(names.Length == c.Length);
487  //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
488  Debug.Assert(names.All(name => name != null));
489 
490  CheckContextMatch<Symbol>(names);
491  uint n = (uint)names.Length;
492  ConstructorList[] cla = new ConstructorList[n];
493  IntPtr[] n_constr = new IntPtr[n];
494  for (uint i = 0; i < n; i++)
495  {
496  Constructor[] constructor = c[i];
497  CheckContextMatch<Constructor>(constructor);
498  cla[i] = new ConstructorList(this, constructor);
499  n_constr[i] = cla[i].NativeObject;
500  }
501  IntPtr[] n_res = new IntPtr[n];
502  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
503  DatatypeSort[] res = new DatatypeSort[n];
504  for (uint i = 0; i < n; i++)
505  res[i] = new DatatypeSort(this, n_res[i]);
506  return res;
507  }

Referenced by Context.MkDatatypeSorts().

◆ MkDiff()

ReExpr MkDiff ( ReExpr  a,
ReExpr  b 
)
inline

Create a difference regular expression.

Definition at line 2750 of file Context.cs.

2751  {
2752  Debug.Assert(a != null);
2753  Debug.Assert(b != null);
2754  CheckContextMatch(a, b);
2755  return new ReExpr(this, Native.Z3_mk_re_diff(nCtx, a.NativeObject, b.NativeObject));
2756  }

◆ MkDistinct() [1/2]

BoolExpr MkDistinct ( IEnumerable< Expr args)
inline

Creates a distinct term.

Definition at line 946 of file Context.cs.

947  {
948  Debug.Assert(args != null);
949  return MkDistinct(args.ToArray());
950  }
BoolExpr MkDistinct(params Expr[] args)
Creates a distinct term.
Definition: Context.cs:933

◆ MkDistinct() [2/2]

BoolExpr MkDistinct ( params Expr[]  args)
inline

Creates a distinct term.

Definition at line 933 of file Context.cs.

934  {
935  Debug.Assert(args != null);
936  Debug.Assert(args.All(a => a != null));
937 
938 
939  CheckContextMatch<Expr>(args);
940  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
941  }

Referenced by Context.MkDistinct().

◆ MkDiv()

ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 1166 of file Context.cs.

1167  {
1168  Debug.Assert(t1 != null);
1169  Debug.Assert(t2 != null);
1170 
1171  CheckContextMatch(t1);
1172  CheckContextMatch(t2);
1173  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1174  }

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

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

◆ MkEmptySeq()

SeqExpr MkEmptySeq ( Sort  s)
inline

Create the empty sequence.

Definition at line 2445 of file Context.cs.

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

◆ MkEmptySet()

ArrayExpr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2318 of file Context.cs.

2319  {
2320  Debug.Assert(domain != null);
2321 
2322  CheckContextMatch(domain);
2323  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2324  }

◆ MkEnumSort() [1/2]

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

Create a new enumeration sort.

Definition at line 333 of file Context.cs.

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

◆ MkEnumSort() [2/2]

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

Create a new enumeration sort.

Definition at line 318 of file Context.cs.

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

◆ MkEq()

BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 920 of file Context.cs.

921  {
922  Debug.Assert(x != null);
923  Debug.Assert(y != null);
924 
925  CheckContextMatch(x);
926  CheckContextMatch(y);
927  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
928  }

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

3274  {
3275  Debug.Assert(body != null);
3276  Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3277  Debug.Assert(patterns == null || patterns.All(p => p != null));
3278  Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3279 
3280  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3281  }

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

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

Referenced by Context.MkQuantifier().

◆ MkExtract() [1/2]

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

Extract subsequence.

Definition at line 2612 of file Context.cs.

2613  {
2614  Debug.Assert(s != null);
2615  Debug.Assert(offset != null);
2616  Debug.Assert(length != null);
2617  CheckContextMatch(s, offset, length);
2618  return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2619  }

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

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

◆ MkFalse()

BoolExpr MkFalse ( )
inline

The false Term.

Definition at line 902 of file Context.cs.

903  {
904 
905  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
906  }

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

◆ MkFiniteDomainSort() [1/2]

FiniteDomainSort MkFiniteDomainSort ( string  name,
ulong  size 
)
inline

Create a new finite domain sort.

Returns
The result is a sort

Elements of the sort are created using

See also
MkNumeral(ulong, Sort)

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

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

Definition at line 397 of file Context.cs.

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

◆ MkFiniteDomainSort() [2/2]

FiniteDomainSort MkFiniteDomainSort ( Symbol  name,
ulong  size 
)
inline

Create a new finite domain sort.

Returns
The result is a sort

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

Definition at line 381 of file Context.cs.

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

◆ MkFixedpoint()

Fixedpoint MkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3948 of file Context.cs.

3949  {
3950 
3951  return new Fixedpoint(this);
3952  }

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

3234  {
3235  Debug.Assert(body != null);
3236  Debug.Assert(boundConstants == null || boundConstants.All(b => b != null));
3237  Debug.Assert(patterns == null || patterns.All(p => p != null));
3238  Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3239 
3240 
3241  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3242  }

◆ MkForall() [2/2]

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

Create a universal Quantifier.

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

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

Definition at line 3209 of file Context.cs.

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

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

Definition at line 4538 of file Context.cs.

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

◆ MkFP() [2/6]

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

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

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

Definition at line 4259 of file Context.cs.

4260  {
4261  return MkFPNumeral(sgn, exp, sig, s);
4262  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4173

◆ MkFP() [3/6]

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

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

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

Definition at line 4271 of file Context.cs.

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

◆ MkFP() [4/6]

FPNum MkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4237 of file Context.cs.

4238  {
4239  return MkFPNumeral(v, s);
4240  }

◆ MkFP() [5/6]

FPNum MkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4227 of file Context.cs.

4228  {
4229  return MkFPNumeral(v, s);
4230  }

◆ MkFP() [6/6]

FPNum MkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4247 of file Context.cs.

4248  {
4249  return MkFPNumeral(v, s);
4250  }

◆ MkFPAbs()

FPExpr MkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term

Definition at line 4283 of file Context.cs.

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

◆ MkFPAdd()

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

Floating-point addition

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

Definition at line 4303 of file Context.cs.

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

◆ MkFPDiv()

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

Floating-point division

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

Definition at line 4336 of file Context.cs.

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

◆ MkFPEq()

BoolExpr MkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

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

Parameters
t1floating-point term
t2floating-point term

Definition at line 4455 of file Context.cs.

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

◆ MkFPFMA()

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

Floating-point fused multiply-add

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

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

Definition at line 4351 of file Context.cs.

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

◆ MkFPGEq()

BoolExpr MkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4432 of file Context.cs.

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

◆ MkFPGt()

BoolExpr MkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4442 of file Context.cs.

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

◆ MkFPInf()

FPNum MkFPInf ( FPSort  s,
bool  negative 
)
inline

Create a floating-point infinity of sort s.

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

Definition at line 4153 of file Context.cs.

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

◆ MkFPIsInfinite()

BoolExpr MkFPIsInfinite ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4491 of file Context.cs.

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

◆ MkFPIsNaN()

BoolExpr MkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term

Definition at line 4500 of file Context.cs.

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

◆ MkFPIsNegative()

BoolExpr MkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4509 of file Context.cs.

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

◆ MkFPIsNormal()

BoolExpr MkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4464 of file Context.cs.

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

◆ MkFPIsPositive()

BoolExpr MkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4518 of file Context.cs.

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

◆ MkFPIsSubnormal()

BoolExpr MkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4473 of file Context.cs.

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

◆ MkFPIsZero()

BoolExpr MkFPIsZero ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4482 of file Context.cs.

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

◆ MkFPLEq()

BoolExpr MkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4412 of file Context.cs.

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

◆ MkFPLt()

BoolExpr MkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4422 of file Context.cs.

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

◆ MkFPMax()

FPExpr MkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4402 of file Context.cs.

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

◆ MkFPMin()

FPExpr MkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4392 of file Context.cs.

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

◆ MkFPMul()

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

Floating-point multiplication

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

Definition at line 4325 of file Context.cs.

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

◆ MkFPNaN()

FPNum MkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.

Definition at line 4143 of file Context.cs.

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

◆ MkFPNeg()

FPExpr MkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term

Definition at line 4292 of file Context.cs.

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

◆ MkFPNumeral() [1/5]

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

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

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

Definition at line 4217 of file Context.cs.

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

◆ MkFPNumeral() [2/5]

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

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

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

Definition at line 4205 of file Context.cs.

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

◆ MkFPNumeral() [3/5]

FPNum MkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4183 of file Context.cs.

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

◆ MkFPNumeral() [4/5]

FPNum MkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4173 of file Context.cs.

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

Referenced by Context.MkFP().

◆ MkFPNumeral() [5/5]

FPNum MkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4193 of file Context.cs.

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

◆ MkFPRem()

FPExpr MkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term

Definition at line 4371 of file Context.cs.

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

◆ MkFPRNA()

FPRMNum MkFPRNA ( )
inline

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

Definition at line 4007 of file Context.cs.

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

◆ MkFPRNE()

FPRMNum MkFPRNE ( )
inline

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

Definition at line 3991 of file Context.cs.

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

◆ MkFPRoundingModeSort()

FPRMSort MkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Definition at line 3973 of file Context.cs.

3974  {
3975  return new FPRMSort(this);
3976  }

◆ MkFPRoundNearestTiesToAway()

FPRMNum MkFPRoundNearestTiesToAway ( )
inline

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

Definition at line 3999 of file Context.cs.

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

◆ MkFPRoundNearestTiesToEven()

FPRMExpr MkFPRoundNearestTiesToEven ( )
inline

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

Definition at line 3983 of file Context.cs.

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

◆ MkFPRoundToIntegral()

FPExpr MkFPRoundToIntegral ( FPRMExpr  rm,
FPExpr  t 
)
inline

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

Parameters
rmterm of RoundingMode sort
tfloating-point term

Definition at line 4382 of file Context.cs.

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

◆ MkFPRoundTowardNegative()

FPRMNum MkFPRoundTowardNegative ( )
inline

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

Definition at line 4031 of file Context.cs.

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

◆ MkFPRoundTowardPositive()

FPRMNum MkFPRoundTowardPositive ( )
inline

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

Definition at line 4015 of file Context.cs.

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

◆ MkFPRoundTowardZero()

FPRMNum MkFPRoundTowardZero ( )
inline

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

Definition at line 4047 of file Context.cs.

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

◆ MkFPRTN()

FPRMNum MkFPRTN ( )
inline

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

Definition at line 4039 of file Context.cs.

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

◆ MkFPRTP()

FPRMNum MkFPRTP ( )
inline

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

Definition at line 4023 of file Context.cs.

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

◆ MkFPRTZ()

FPRMNum MkFPRTZ ( )
inline

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

Definition at line 4055 of file Context.cs.

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

◆ MkFPSort()

FPSort MkFPSort ( uint  ebits,
uint  sbits 
)
inline

Create a FloatingPoint sort.

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

Definition at line 4068 of file Context.cs.

4069  {
4070  return new FPSort(this, ebits, sbits);
4071  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9901

◆ MkFPSort128()

FPSort MkFPSort128 ( )
inline

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

Definition at line 4132 of file Context.cs.

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

◆ MkFPSort16()

FPSort MkFPSort16 ( )
inline

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

Definition at line 4084 of file Context.cs.

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

◆ MkFPSort32()

FPSort MkFPSort32 ( )
inline

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

Definition at line 4100 of file Context.cs.

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

◆ MkFPSort64()

FPSort MkFPSort64 ( )
inline

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

Definition at line 4116 of file Context.cs.

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

◆ MkFPSortDouble()

FPSort MkFPSortDouble ( )
inline

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

Definition at line 4108 of file Context.cs.

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

◆ MkFPSortHalf()

FPSort MkFPSortHalf ( )
inline

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

Definition at line 4076 of file Context.cs.

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

◆ MkFPSortQuadruple()

FPSort MkFPSortQuadruple ( )
inline

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

Definition at line 4124 of file Context.cs.

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

◆ MkFPSortSingle()

FPSort MkFPSortSingle ( )
inline

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

Definition at line 4092 of file Context.cs.

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

◆ MkFPSqrt()

FPExpr MkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term

Definition at line 4361 of file Context.cs.

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

◆ MkFPSub()

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

Floating-point subtraction

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

Definition at line 4314 of file Context.cs.

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

◆ MkFPToBV()

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

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

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

Parameters
rmRoundingMode term.
tFloatingPoint term
szSize of the resulting bit-vector.
signIndicates whether the result is a signed or unsigned bit-vector.

Definition at line 4641 of file Context.cs.

4642  {
4643  if (sign)
4644  return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4645  else
4646  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4647  }

◆ MkFPToFP() [1/6]

FPExpr MkFPToFP ( BitVecExpr  bv,
FPSort  s 
)
inline

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

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

Parameters
bvbit-vector value (of size m).
sFloatingPoint sort (ebits+sbits == m)

Definition at line 4554 of file Context.cs.

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

◆ MkFPToFP() [2/6]

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

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

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

Parameters
rmRoundingMode term.
tterm of bit-vector sort.
sFloatingPoint sort.
signedflag indicating whether t is interpreted as signed or unsigned bit-vector.

Definition at line 4604 of file Context.cs.

4605  {
4606  if (signed)
4607  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4608  else
4609  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4610  }

◆ MkFPToFP() [3/6]

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

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

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

Parameters
rmRoundingMode term.
tFloatingPoint term.
sFloatingPoint sort.

Definition at line 4570 of file Context.cs.

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

◆ MkFPToFP() [4/6]

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

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

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

Parameters
rmRoundingMode term.
expExponent term of Int sort.
sigSignificand term of Real sort.
sFloatingPoint sort.

Definition at line 4692 of file Context.cs.

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

◆ MkFPToFP() [5/6]

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

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

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

Parameters
rmRoundingMode term.
tterm of Real sort.
sFloatingPoint sort.

Definition at line 4586 of file Context.cs.

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

◆ MkFPToFP() [6/6]

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

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

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

Parameters
sFloatingPoint sort
rmfloating-point rounding mode term
tfloating-point term

Definition at line 4622 of file Context.cs.

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

◆ MkFPToIEEEBV()

BitVecExpr MkFPToIEEEBV ( FPExpr  t)
inline

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

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

Parameters
tFloatingPoint term.

Definition at line 4675 of file Context.cs.

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

◆ MkFPToReal()

RealExpr MkFPToReal ( FPExpr  t)
inline

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

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

Parameters
tFloatingPoint term

Definition at line 4658 of file Context.cs.

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

◆ MkFPZero()

FPNum MkFPZero ( FPSort  s,
bool  negative 
)
inline

Create a floating-point zero of sort s.

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

Definition at line 4163 of file Context.cs.

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

◆ MkFreshConst()

Expr MkFreshConst ( string  prefix,
Sort  range 
)
inline

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

Definition at line 764 of file Context.cs.

765  {
766  Debug.Assert(range != null);
767 
768  CheckContextMatch(range);
769  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
770  }

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

687  {
688  Debug.Assert(range != null);
689 
690  CheckContextMatch(range);
691  return new FuncDecl(this, prefix, null, range);
692  }

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

647  {
648  Debug.Assert(range != null);
649  Debug.Assert(domain.All(d => d != null));
650 
651  CheckContextMatch<Sort>(domain);
652  CheckContextMatch(range);
653  return new FuncDecl(this, prefix, domain, range);
654  }

◆ MkFullRe()

ReExpr MkFullRe ( Sort  s)
inline

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

Definition at line 2772 of file Context.cs.

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

◆ MkFullSet()

ArrayExpr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2329 of file Context.cs.

2330  {
2331  Debug.Assert(domain != null);
2332 
2333  CheckContextMatch(domain);
2334  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2335  }

◆ MkFuncDecl() [1/4]

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

Creates a new function declaration.

Definition at line 629 of file Context.cs.

630  {
631  Debug.Assert(range != null);
632  Debug.Assert(domain != null);
633 
634  CheckContextMatch(domain);
635  CheckContextMatch(range);
636  using var symbol = MkSymbol(name);
637  Sort[] q = new Sort[] { domain };
638  return new FuncDecl(this, symbol, q, range);
639  }

◆ MkFuncDecl() [2/4]

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

Creates a new function declaration.

Definition at line 586 of file Context.cs.

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

◆ MkFuncDecl() [3/4]

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

Creates a new function declaration.

Definition at line 570 of file Context.cs.

571  {
572  Debug.Assert(name != null);
573  Debug.Assert(domain != null);
574  Debug.Assert(range != null);
575 
576  CheckContextMatch(name);
577  CheckContextMatch(domain);
578  CheckContextMatch(range);
579  Sort[] q = new Sort[] { domain };
580  return new FuncDecl(this, name, q, range);
581  }

◆ MkFuncDecl() [4/4]

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

Creates a new function declaration.

Definition at line 555 of file Context.cs.

556  {
557  Debug.Assert(name != null);
558  Debug.Assert(range != null);
559  Debug.Assert(domain.All(d => d != null));
560 
561  CheckContextMatch(name);
562  CheckContextMatch<Sort>(domain);
563  CheckContextMatch(range);
564  return new FuncDecl(this, name, domain, range);
565  }

◆ MkGe()

BoolExpr MkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 >= t2

Definition at line 1259 of file Context.cs.

1260  {
1261  Debug.Assert(t1 != null);
1262  Debug.Assert(t2 != null);
1263 
1264  CheckContextMatch(t1);
1265  CheckContextMatch(t2);
1266  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1267  }

Referenced by ArithExpr.operator>=().

◆ MkGoal()

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

Creates a new Goal.

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

Parameters
modelsIndicates whether model generation should be enabled.
unsatCoresIndicates whether unsat core generation should be enabled.
proofsIndicates whether proof generation should be enabled.

Definition at line 3449 of file Context.cs.

3450  {
3451 
3452  return new Goal(this, models, unsatCores, proofs);
3453  }

◆ MkGt()

BoolExpr MkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 > t2

Definition at line 1246 of file Context.cs.

1247  {
1248  Debug.Assert(t1 != null);
1249  Debug.Assert(t2 != null);
1250 
1251  CheckContextMatch(t1);
1252  CheckContextMatch(t2);
1253  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1254  }

Referenced by ArithExpr.operator>().

◆ MkIff()

BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 984 of file Context.cs.

985  {
986  Debug.Assert(t1 != null);
987  Debug.Assert(t2 != null);
988 
989  CheckContextMatch(t1);
990  CheckContextMatch(t2);
991  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
992  }

◆ MkImplies()

BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 997 of file Context.cs.

998  {
999  Debug.Assert(t1 != null);
1000  Debug.Assert(t2 != null);
1001 
1002  CheckContextMatch(t1);
1003  CheckContextMatch(t2);
1004  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
1005  }

◆ MkIndexOf()

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

Extract index of sub-string starting at offset.

Definition at line 2624 of file Context.cs.

2625  {
2626  Debug.Assert(s != null);
2627  Debug.Assert(offset != null);
2628  Debug.Assert(substr != null);
2629  CheckContextMatch(s, substr, offset);
2630  return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2631  }

◆ MkInRe()

BoolExpr MkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2658 of file Context.cs.

2659  {
2660  Debug.Assert(s != null);
2661  Debug.Assert(re != null);
2662  CheckContextMatch(s, re);
2663  return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2664  }

◆ MkInt() [1/5]

IntNum MkInt ( int  v)
inline

Create an integer numeral.

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

Definition at line 3072 of file Context.cs.

3073  {
3074 
3075  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
3076  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:158

◆ MkInt() [2/5]

IntNum MkInt ( long  v)
inline

Create an integer numeral.

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

Definition at line 3094 of file Context.cs.

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

◆ MkInt() [3/5]

IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 3061 of file Context.cs.

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

◆ MkInt() [4/5]

IntNum MkInt ( uint  v)
inline

Create an integer numeral.

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

Definition at line 3083 of file Context.cs.

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

◆ MkInt() [5/5]

IntNum MkInt ( ulong  v)
inline

Create an integer numeral.

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

Definition at line 3105 of file Context.cs.

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

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

1941  {
1942  Debug.Assert(t != null);
1943 
1944  CheckContextMatch(t);
1945  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1946  }

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

1280  {
1281  Debug.Assert(t != null);
1282 
1283  CheckContextMatch(t);
1284  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1285  }

◆ MkIntConst() [1/2]

IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 815 of file Context.cs.

816  {
817  Debug.Assert(name != null);
818 
819  return (IntExpr)MkConst(name, IntSort);
820  }

◆ MkIntConst() [2/2]

IntExpr MkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 805 of file Context.cs.

806  {
807  Debug.Assert(name != null);
808 
809  return (IntExpr)MkConst(name, IntSort);
810  }

◆ MkIntersect()

ReExpr MkIntersect ( params ReExpr[]  t)
inline

Create the intersection of regular languages.

Definition at line 2738 of file Context.cs.

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

◆ MkIntSort()

IntSort MkIntSort ( )
inline

Create a new integer sort.

Definition at line 233 of file Context.cs.

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

◆ MkIsDigit()

BoolExpr MkIsDigit ( Expr  ch)
inline

Create a check if the character is a digit.

Definition at line 2830 of file Context.cs.

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

◆ MkIsInteger()

BoolExpr MkIsInteger ( RealExpr  t)
inline

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

Definition at line 1305 of file Context.cs.

1306  {
1307  Debug.Assert(t != null);
1308 
1309  CheckContextMatch(t);
1310  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1311  }

◆ MkITE()

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

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

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

Definition at line 969 of file Context.cs.

970  {
971  Debug.Assert(t1 != null);
972  Debug.Assert(t2 != null);
973  Debug.Assert(t3 != null);
974 
975  CheckContextMatch(t1);
976  CheckContextMatch(t2);
977  CheckContextMatch(t3);
978  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
979  }

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

3363  {
3364  Debug.Assert(body != null);
3365  Debug.Assert(boundConstants != null && boundConstants.All(b => b != null));
3366  return new Lambda(this, boundConstants, body);
3367  }
def Lambda(vs, body)
Definition: z3py.py:2261

◆ MkLambda() [2/2]

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

Create a lambda expression.

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

Parameters
sortsthe sorts of the bound variables.
namesnames of the bound variables
bodythe body of the quantifier.

Definition at line 3343 of file Context.cs.

3344  {
3345  Debug.Assert(sorts != null);
3346  Debug.Assert(names != null);
3347  Debug.Assert(body != null);
3348  Debug.Assert(sorts.Length == names.Length);
3349  Debug.Assert(sorts.All(s => s != null));
3350  Debug.Assert(names.All(n => n != null));
3351  return new Lambda(this, sorts, names, body);
3352  }

◆ MkLe()

BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1233 of file Context.cs.

1234  {
1235  Debug.Assert(t1 != null);
1236  Debug.Assert(t2 != null);
1237 
1238  CheckContextMatch(t1);
1239  CheckContextMatch(t2);
1240  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1241  }

Referenced by ArithExpr.operator<=().

◆ MkLength()

IntExpr MkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 2526 of file Context.cs.

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

◆ MkListSort() [1/2]

ListSort MkListSort ( string  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 366 of file Context.cs.

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

◆ MkListSort() [2/2]

ListSort MkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 353 of file Context.cs.

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

◆ MkLoop()

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

Take the bounded Kleene star of a regular expression.

Definition at line 2678 of file Context.cs.

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

◆ MkLt()

BoolExpr MkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 < t2

Definition at line 1220 of file Context.cs.

1221  {
1222  Debug.Assert(t1 != null);
1223  Debug.Assert(t2 != null);
1224 
1225  CheckContextMatch(t1);
1226  CheckContextMatch(t2);
1227  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1228  }

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

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

◆ MkMod()

IntExpr MkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 1180 of file Context.cs.

1181  {
1182  Debug.Assert(t1 != null);
1183  Debug.Assert(t2 != null);
1184 
1185  CheckContextMatch(t1);
1186  CheckContextMatch(t2);
1187  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1188  }

◆ MkMul() [1/2]

ArithExpr MkMul ( IEnumerable< ArithExpr t)
inline

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

Definition at line 1130 of file Context.cs.

1131  {
1132  Debug.Assert(t != null);
1133  Debug.Assert(t.All(a => a != null));
1134 
1135  CheckContextMatch<ArithExpr>(t);
1136  var ts = t.ToArray();
1137  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1138  }

◆ MkMul() [2/2]

ArithExpr MkMul ( params ArithExpr[]  t)
inline

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

Definition at line 1117 of file Context.cs.

1118  {
1119  Debug.Assert(t != null);
1120  Debug.Assert(t.All(a => a != null));
1121 
1122  CheckContextMatch<ArithExpr>(t);
1123  var ts = t.ToArray();
1124  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1125  }

Referenced by ArithExpr.operator*().

◆ MkNot()

BoolExpr MkNot ( BoolExpr  a)
inline

Mk an expression representing not(a).

Definition at line 955 of file Context.cs.

956  {
957  Debug.Assert(a != null);
958 
959  CheckContextMatch(a);
960  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
961  }

Referenced by BoolExpr.operator!().

◆ MkNth()

Expr MkNth ( SeqExpr  s,
Expr  index 
)
inline

Retrieve element at index.

Definition at line 2601 of file Context.cs.

2602  {
2603  Debug.Assert(s != null);
2604  Debug.Assert(index != null);
2605  CheckContextMatch(s, index);
2606  return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
2607  }

◆ MkNumeral() [1/5]

Expr MkNumeral ( int  v,
Sort  ty 
)
inline

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

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value v and type ty

Definition at line 2930 of file Context.cs.

2931  {
2932  Debug.Assert(ty != null);
2933 
2934  CheckContextMatch(ty);
2935  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2936  }

◆ MkNumeral() [2/5]

Expr MkNumeral ( long  v,
Sort  ty 
)
inline

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

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value v and type ty

Definition at line 2960 of file Context.cs.

2961  {
2962  Debug.Assert(ty != null);
2963 
2964  CheckContextMatch(ty);
2965  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2966  }

◆ MkNumeral() [3/5]

Expr MkNumeral ( string  v,
Sort  ty 
)
inline

Create a Term of a given sort.

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

Definition at line 2915 of file Context.cs.

2916  {
2917  Debug.Assert(ty != null);
2918 
2919  CheckContextMatch(ty);
2920  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2921  }

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

Definition at line 2945 of file Context.cs.

2946  {
2947  Debug.Assert(ty != null);
2948 
2949  CheckContextMatch(ty);
2950  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2951  }

◆ MkNumeral() [5/5]

Expr MkNumeral ( ulong  v,
Sort  ty 
)
inline

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

Parameters
vValue of the numeral
tySort of the numeral
Returns
A Term with value v and type ty

Definition at line 2975 of file Context.cs.

2976  {
2977  Debug.Assert(ty != null);
2978 
2979  CheckContextMatch(ty);
2980  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2981  }

◆ MkOptimize()

Optimize MkOptimize ( )
inline

Create an Optimization context.

Definition at line 3959 of file Context.cs.

3960  {
3961 
3962  return new Optimize(this);
3963  }

◆ MkOption()

ReExpr MkOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2696 of file Context.cs.

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

◆ MkOr() [1/2]

BoolExpr MkOr ( IEnumerable< BoolExpr t)
inline

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

Definition at line 1076 of file Context.cs.

1077  {
1078  Debug.Assert(t != null);
1079  Debug.Assert(t.All(a => a != null));
1080 
1081  CheckContextMatch(t);
1082  var ts = t.ToArray();
1083  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
1084  }

◆ MkOr() [2/2]

BoolExpr MkOr ( params BoolExpr[]  t)
inline

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

Definition at line 1063 of file Context.cs.

1064  {
1065  Debug.Assert(t != null);
1066  Debug.Assert(t.All(a => a != null));
1067 
1068  CheckContextMatch<BoolExpr>(t);
1069  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1070  }

Referenced by BoolExpr.operator|().

◆ MkParams()

Params MkParams ( )
inline

Creates a new ParameterSet.

Definition at line 3460 of file Context.cs.

3461  {
3462 
3463  return new Params(this);
3464  }

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

◆ MkPattern()

Pattern MkPattern ( params Expr[]  terms)
inline

Create a quantifier pattern.

Definition at line 723 of file Context.cs.

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

◆ MkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2894 of file Context.cs.

2895  {
2896  Debug.Assert(args != null);
2897  Debug.Assert(coeffs != null);
2898  Debug.Assert(args.Length == coeffs.Length);
2899  CheckContextMatch<BoolExpr>(args);
2900  return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length,
2901  AST.ArrayToNative(args),
2902  coeffs, k));
2903  }

◆ MkPBGe()

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

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

Definition at line 2881 of file Context.cs.

2882  {
2883  Debug.Assert(args != null);
2884  Debug.Assert(coeffs != null);
2885  Debug.Assert(args.Length == coeffs.Length);
2886  CheckContextMatch<BoolExpr>(args);
2887  return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length,
2888  AST.ArrayToNative(args),
2889  coeffs, k));
2890  }

◆ MkPBLe()

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

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

Definition at line 2867 of file Context.cs.

2868  {
2869  Debug.Assert(args != null);
2870  Debug.Assert(coeffs != null);
2871  Debug.Assert(args.Length == coeffs.Length);
2872  CheckContextMatch<BoolExpr>(args);
2873  return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length,
2874  AST.ArrayToNative(args),
2875  coeffs, k));
2876  }

◆ MkPlus()

ReExpr MkPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2687 of file Context.cs.

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

◆ MkPower()

ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 1207 of file Context.cs.

1208  {
1209  Debug.Assert(t1 != null);
1210  Debug.Assert(t2 != null);
1211 
1212  CheckContextMatch(t1);
1213  CheckContextMatch(t2);
1214  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1215  }

◆ MkPrefixOf()

BoolExpr MkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 2535 of file Context.cs.

2536  {
2537  Debug.Assert(s1 != null);
2538  Debug.Assert(s2 != null);
2539  CheckContextMatch(s1, s2);
2540  return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2541  }

◆ MkProbe()

Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3766 of file Context.cs.

3767  {
3768 
3769  return new Probe(this, name);
3770  }

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

3312  {
3313  Debug.Assert(body != null);
3314  Debug.Assert(boundConstants == null || boundConstants.All(n => n != null));
3315  Debug.Assert(patterns == null || patterns.All(p => p != null));
3316  Debug.Assert(noPatterns == null || noPatterns.All(np => np != null));
3317 
3318 
3319  if (universal)
3320  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3321  else
3322  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3323  }
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:3251
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:3209

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

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

◆ MkRange()

ReExpr MkRange ( SeqExpr  lo,
SeqExpr  hi 
)
inline

Create a range expression.

Definition at line 2782 of file Context.cs.

2783  {
2784  Debug.Assert(lo != null);
2785  Debug.Assert(hi != null);
2786  CheckContextMatch(lo, hi);
2787  return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
2788  }

◆ MkReal() [1/6]

RatNum MkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

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

Definition at line 2992 of file Context.cs.

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

◆ MkReal() [2/6]

RatNum MkReal ( int  v)
inline

Create a real numeral.

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

Definition at line 3016 of file Context.cs.

3017  {
3018 
3019  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
3020  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:170

◆ MkReal() [3/6]

RatNum MkReal ( long  v)
inline

Create a real numeral.

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

Definition at line 3038 of file Context.cs.

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

◆ MkReal() [4/6]

RatNum MkReal ( string  v)
inline

Create a real numeral.

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

Definition at line 3005 of file Context.cs.

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

◆ MkReal() [5/6]

RatNum MkReal ( uint  v)
inline

Create a real numeral.

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

Definition at line 3027 of file Context.cs.

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

◆ MkReal() [6/6]

RatNum MkReal ( ulong  v)
inline

Create a real numeral.

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

Definition at line 3049 of file Context.cs.

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

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

1295  {
1296  Debug.Assert(t != null);
1297 
1298  CheckContextMatch(t);
1299  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1300  }

◆ MkRealConst() [1/2]

RealExpr MkRealConst ( string  name)
inline

Creates a real constant.

Definition at line 835 of file Context.cs.

836  {
837 
838  return (RealExpr)MkConst(name, RealSort);
839  }

◆ MkRealConst() [2/2]

RealExpr MkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 825 of file Context.cs.

826  {
827  Debug.Assert(name != null);
828 
829  return (RealExpr)MkConst(name, RealSort);
830  }

◆ MkRealSort()

RealSort MkRealSort ( )
inline

Create a real sort.

Definition at line 242 of file Context.cs.

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

◆ MkRecFuncDecl()

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

Creates a new recursive function declaration.

Definition at line 600 of file Context.cs.

601  {
602  Debug.Assert(range != null);
603  Debug.Assert(domain.All(d => d != null));
604 
605  CheckContextMatch<Sort>(domain);
606  CheckContextMatch(range);
607  using var symbol = MkSymbol(name);
608  return new FuncDecl(this, symbol, domain, range, true);
609  }

◆ MkRem()

IntExpr MkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 1194 of file Context.cs.

1195  {
1196  Debug.Assert(t1 != null);
1197  Debug.Assert(t2 != null);
1198 
1199  CheckContextMatch(t1);
1200  CheckContextMatch(t2);
1201  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1202  }

◆ MkRepeat()

BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1790 of file Context.cs.

1791  {
1792  Debug.Assert(t != null);
1793 
1794  CheckContextMatch(t);
1795  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1796  }

◆ MkReplace()

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

Replace the first occurrence of src by dst in s.

Definition at line 2636 of file Context.cs.

2637  {
2638  Debug.Assert(s != null);
2639  Debug.Assert(src != null);
2640  Debug.Assert(dst != null);
2641  CheckContextMatch(s, src, dst);
2642  return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2643  }

◆ MkReSort()

ReSort MkReSort ( SeqSort  s)
inline

Create a new regular expression sort.

Definition at line 267 of file Context.cs.

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

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

2140  {
2141  Debug.Assert(a != null);
2142  Debug.Assert(i != null);
2143 
2144  CheckContextMatch(a);
2145  CheckContextMatch(i);
2146  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2147  }

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

2163  {
2164  Debug.Assert(a != null);
2165  Debug.Assert(args != null && args.All(n => n != null));
2166 
2167  CheckContextMatch(a);
2168  CheckContextMatch<Expr>(args);
2169  return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2170  }

◆ MkSeqSort()

SeqSort MkSeqSort ( Sort  s)
inline

Create a new sequence sort.

Definition at line 258 of file Context.cs.

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

◆ MkSetAdd()

ArrayExpr MkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2340 of file Context.cs.

2341  {
2342  Debug.Assert(set != null);
2343  Debug.Assert(element != null);
2344 
2345  CheckContextMatch(set);
2346  CheckContextMatch(element);
2347  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2348  }

◆ MkSetComplement()

ArrayExpr MkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 2404 of file Context.cs.

2405  {
2406  Debug.Assert(arg != null);
2407 
2408  CheckContextMatch(arg);
2409  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2410  }

◆ MkSetDel()

ArrayExpr MkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 2354 of file Context.cs.

2355  {
2356  Debug.Assert(set != null);
2357  Debug.Assert(element != null);
2358 
2359  CheckContextMatch(set);
2360  CheckContextMatch(element);
2361  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2362  }

◆ MkSetDifference()

ArrayExpr MkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2391 of file Context.cs.

2392  {
2393  Debug.Assert(arg1 != null);
2394  Debug.Assert(arg2 != null);
2395 
2396  CheckContextMatch(arg1);
2397  CheckContextMatch(arg2);
2398  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2399  }

◆ MkSetIntersection()

ArrayExpr MkSetIntersection ( params ArrayExpr[]  args)
inline

Take the intersection of a list of sets.

Definition at line 2379 of file Context.cs.

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

◆ MkSetMembership()

BoolExpr MkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 2415 of file Context.cs.

2416  {
2417  Debug.Assert(elem != null);
2418  Debug.Assert(set != null);
2419 
2420  CheckContextMatch(elem);
2421  CheckContextMatch(set);
2422  return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2423  }

◆ MkSetSort()

SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2307 of file Context.cs.

2308  {
2309  Debug.Assert(ty != null);
2310 
2311  CheckContextMatch(ty);
2312  return new SetSort(this, ty);
2313  }
def SetSort(s)
Sets.
Definition: z3py.py:4917

◆ MkSetSubset()

BoolExpr MkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2428 of file Context.cs.

2429  {
2430  Debug.Assert(arg1 != null);
2431  Debug.Assert(arg2 != null);
2432 
2433  CheckContextMatch(arg1);
2434  CheckContextMatch(arg2);
2435  return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2436  }

◆ MkSetUnion()

ArrayExpr MkSetUnion ( params ArrayExpr[]  args)
inline

Take the union of a list of sets.

Definition at line 2367 of file Context.cs.

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

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

1760  {
1761  Debug.Assert(t != null);
1762 
1763  CheckContextMatch(t);
1764  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1765  }

◆ MkSimpleSolver()

Solver MkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3923 of file Context.cs.

3924  {
3925 
3926  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3927  }

◆ MkSolver() [1/3]

Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 3914 of file Context.cs.

3915  {
3916  using var symbol = MkSymbol(logic);
3917  return MkSolver(symbol);
3918  }
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3901

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

3902  {
3903 
3904  if (logic == null)
3905  return new Solver(this, Native.Z3_mk_solver(nCtx));
3906  else
3907  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3908  }

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

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

◆ MkStar()

ReExpr MkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2669 of file Context.cs.

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

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

2192  {
2193  Debug.Assert(a != null);
2194  Debug.Assert(i != null);
2195  Debug.Assert(v != null);
2196 
2197  CheckContextMatch(a);
2198  CheckContextMatch(i);
2199  CheckContextMatch(v);
2200  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2201  }

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

2222  {
2223  Debug.Assert(a != null);
2224  Debug.Assert(args != null);
2225  Debug.Assert(v != null);
2226 
2227  CheckContextMatch<Expr>(args);
2228  CheckContextMatch(a);
2229  CheckContextMatch(v);
2230  return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
2231  }

◆ MkString()

SeqExpr MkString ( string  s)
inline

Create a string constant.

Definition at line 2463 of file Context.cs.

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

◆ MkStringLe()

BoolExpr MkStringLe ( SeqExpr  s1,
SeqExpr  s2 
)
inline

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

Definition at line 2579 of file Context.cs.

2580  {
2581  Debug.Assert(s1 != null);
2582  Debug.Assert(s2 != null);
2583  CheckContextMatch(s1, s2);
2584  return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
2585  }

◆ MkStringLt()

BoolExpr MkStringLt ( SeqExpr  s1,
SeqExpr  s2 
)
inline

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

Definition at line 2568 of file Context.cs.

2569  {
2570  Debug.Assert(s1 != null);
2571  Debug.Assert(s2 != null);
2572  CheckContextMatch(s1, s2);
2573  return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
2574  }

◆ MkSub()

ArithExpr MkSub ( params ArithExpr[]  t)
inline

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

Definition at line 1143 of file Context.cs.

1144  {
1145  Debug.Assert(t != null);
1146  Debug.Assert(t.All(a => a != null));
1147 
1148  CheckContextMatch<ArithExpr>(t);
1149  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1150  }

Referenced by ArithExpr.operator-().

◆ MkSuffixOf()

BoolExpr MkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 2546 of file Context.cs.

2547  {
2548  Debug.Assert(s1 != null);
2549  Debug.Assert(s2 != null);
2550  CheckContextMatch(s1, s2);
2551  return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2552  }

◆ MkSymbol() [1/2]

IntSymbol MkSymbol ( int  i)
inline

Creates a new symbol using an integer.

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

Definition at line 111 of file Context.cs.

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

Referenced by Params.Add(), 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(), Context.MkUninterpretedSort(), and Context.MkUserPropagatorFuncDecl().

◆ MkSymbol() [2/2]

StringSymbol MkSymbol ( string  name)
inline

Create a symbol using a string.

Definition at line 119 of file Context.cs.

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

◆ MkTactic()

Tactic MkTactic ( string  name)
inline

Creates a new Tactic.

Definition at line 3504 of file Context.cs.

3505  {
3506 
3507  return new Tactic(this, name);
3508  }

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

2281  {
2282  Debug.Assert(array != null);
2283 
2284  CheckContextMatch(array);
2285  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2286  }

◆ MkToRe()

ReExpr MkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2648 of file Context.cs.

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

◆ MkTrue()

BoolExpr MkTrue ( )
inline

The true Term.

Definition at line 893 of file Context.cs.

894  {
895 
896  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
897  }

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

◆ MkTupleSort()

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

Create a new tuple sort.

Definition at line 302 of file Context.cs.

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

◆ MkUnaryMinus()

ArithExpr MkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing -t.

Definition at line 1155 of file Context.cs.

1156  {
1157  Debug.Assert(t != null);
1158 
1159  CheckContextMatch(t);
1160  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1161  }

Referenced by ArithExpr.operator-().

◆ MkUninterpretedSort() [1/2]

UninterpretedSort MkUninterpretedSort ( string  str)
inline

Create a new uninterpreted sort.

Definition at line 224 of file Context.cs.

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

◆ MkUninterpretedSort() [2/2]

UninterpretedSort MkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 213 of file Context.cs.

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

Referenced by Context.MkUninterpretedSort().

◆ MkUnion()

ReExpr MkUnion ( params ReExpr[]  t)
inline

Create the union of regular languages.

Definition at line 2726 of file Context.cs.

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

◆ MkUnit()

SeqExpr MkUnit ( Expr  elem)
inline

Create the singleton sequence.

Definition at line 2454 of file Context.cs.

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

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

542  {
543  return Expr.Create(this, Native.Z3_datatype_update_field(
544  nCtx, field.NativeObject,
545  t.NativeObject, v.NativeObject));
546  }

◆ MkUserPropagatorFuncDecl()

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

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


Definition at line 697 of file Context.cs.

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

◆ MkXor() [1/2]

BoolExpr MkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 1010 of file Context.cs.

1011  {
1012  Debug.Assert(t1 != null);
1013  Debug.Assert(t2 != null);
1014 
1015  CheckContextMatch(t1);
1016  CheckContextMatch(t2);
1017  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
1018  }

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

1024  {
1025  Debug.Assert(ts != null);
1026  Debug.Assert(ts.All(a => a != null));
1027  CheckContextMatch<BoolExpr>(ts);
1028 
1029  return ts.Aggregate(MkFalse(), (r, t) =>
1030  {
1031  using (r)
1032  return MkXor(r, t);
1033  });
1034  }
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
Create an expression representing t1 xor t2.
Definition: Context.cs:1010

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

1777  {
1778  Debug.Assert(t != null);
1779 
1780  CheckContextMatch(t);
1781  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1782  }

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

3884  {
3885  Debug.Assert(p != null);
3886 
3887  CheckContextMatch(p);
3888  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3889  }

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

3870  {
3871  Debug.Assert(p1 != null);
3872  Debug.Assert(p2 != null);
3873 
3874  CheckContextMatch(p1);
3875  CheckContextMatch(p2);
3876  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3877  }

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

3562  {
3563  Debug.Assert(t1 != null);
3564  Debug.Assert(t2 != null);
3565 
3566  CheckContextMatch(t1);
3567  CheckContextMatch(t2);
3568  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3569  }

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

3710  {
3711  Debug.Assert(t1 != null);
3712  Debug.Assert(t2 != null);
3713 
3714  CheckContextMatch(t1);
3715  CheckContextMatch(t2);
3716  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3717  }

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

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

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

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

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

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

◆ ProbeDescription()

string ProbeDescription ( string  name)
inline

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

Definition at line 3757 of file Context.cs.

3758  {
3759 
3760  return Native.Z3_probe_get_descr(nCtx, name);
3761  }

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

3623  {
3624  Debug.Assert(t != null);
3625 
3626  CheckContextMatch(t);
3627  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3628  }
expr max(expr const &a, expr const &b)
Definition: z3++.h:1953

◆ SbvToString()

SeqExpr SbvToString ( Expr  e)
inline

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

Definition at line 2492 of file Context.cs.

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

◆ SimplifyHelp()

string SimplifyHelp ( )
inline

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

Definition at line 4734 of file Context.cs.

4735  {
4736 
4737  return Native.Z3_simplify_get_help(nCtx);
4738  }

◆ Skip()

Tactic Skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 3633 of file Context.cs.

3634  {
3635 
3636  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3637  }

◆ StringToInt()

IntExpr StringToInt ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 2502 of file Context.cs.

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

◆ TacticDescription()

string TacticDescription ( string  name)
inline

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

Definition at line 3495 of file Context.cs.

3496  {
3497 
3498  return Native.Z3_tactic_get_descr(nCtx, name);
3499  }

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

3549  {
3550  Debug.Assert(t1 != null);
3551  Debug.Assert(t2 != null);
3552  // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3553 
3554  return AndThen(t1, t2, ts);
3555  }
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:3514

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

3578  {
3579  Debug.Assert(t != null);
3580 
3581  CheckContextMatch(t);
3582  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3583  }

◆ UbvToString()

SeqExpr UbvToString ( Expr  e)
inline

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

Definition at line 2482 of file Context.cs.

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

◆ UnwrapAST()

IntPtr UnwrapAST ( AST  a)
inline

Unwraps an AST.

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

See also
Native.Z3_inc_ref

).

See also
WrapAST
Parameters
aThe AST to unwrap.

Definition at line 4726 of file Context.cs.

4727  {
4728  return a.NativeObject;
4729  }

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

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

◆ UsingParams()

Tactic UsingParams ( Tactic  t,
Params  p 
)
inline

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

Definition at line 3672 of file Context.cs.

3673  {
3674  Debug.Assert(t != null);
3675  Debug.Assert(p != null);
3676 
3677  CheckContextMatch(t);
3678  CheckContextMatch(p);
3679  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3680  }

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

3593  {
3594  Debug.Assert(p != null);
3595  Debug.Assert(t != null);
3596 
3597  CheckContextMatch(t);
3598  CheckContextMatch(p);
3599  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3600  }

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

3687  {
3688  Debug.Assert(t != null);
3689  Debug.Assert(p != null);
3690 
3691  return UsingParams(t, p);
3692  }
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3672

◆ WrapAST()

AST WrapAST ( IntPtr  nativeObject)
inline

Wraps an AST.

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

See also
UnwrapAST, Native.Z3_inc_ref

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

See also
UnwrapAST
Parameters
nativeObjectThe native pointer to wrap.

Definition at line 4710 of file Context.cs.

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

Property Documentation

◆ BoolSort

Retrieves the Boolean sort of the context.

Definition at line 146 of file Context.cs.

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

Referenced by Context.MkBoolSort().

◆ CharSort

Retrieves the String sort of the context.

Definition at line 180 of file Context.cs.

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

◆ IntSort

Retrieves the Integer sort of the context.

Definition at line 157 of file Context.cs.

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

Referenced by Context.MkIntSort().

◆ NumProbes

uint NumProbes
get

The number of supported Probes.

Definition at line 3733 of file Context.cs.

3734  {
3735  get { return Native.Z3_get_num_probes(nCtx); }
3736  }

◆ NumTactics

uint NumTactics
get

The number of supported tactics.

Definition at line 3471 of file Context.cs.

3472  {
3473  get { return Native.Z3_get_num_tactics(nCtx); }
3474  }

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

3392  {
3393  set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
3394  }

◆ ProbeNames

string [] ProbeNames
get

The names of all supported Probes.

Definition at line 3741 of file Context.cs.

3742  {
3743  get
3744  {
3745 
3746  uint n = NumProbes;
3747  string[] res = new string[n];
3748  for (uint i = 0; i < n; i++)
3749  res[i] = Native.Z3_get_probe_name(nCtx, i);
3750  return res;
3751  }
3752  }
uint NumProbes
The number of supported Probes.
Definition: Context.cs:3734

◆ RealSort

Retrieves the Real sort of the context.

Definition at line 169 of file Context.cs.

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

Referenced by Context.MkRealSort().

◆ SimplifyParameterDescriptions

ParamDescrs SimplifyParameterDescriptions
get

Retrieves parameter descriptions for simplifier.

Definition at line 4743 of file Context.cs.

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

◆ StringSort

SeqSort StringSort
get

Retrieves the String sort of the context.

Definition at line 192 of file Context.cs.

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

◆ TacticNames

string [] TacticNames
get

The names of all supported tactics.

Definition at line 3479 of file Context.cs.

3480  {
3481  get
3482  {
3483 
3484  uint n = NumTactics;
3485  string[] res = new string[n];
3486  for (uint i = 0; i < n; i++)
3487  res[i] = Native.Z3_get_tactic_name(nCtx, i);
3488  return res;
3489  }
3490  }
uint NumTactics
The number of supported tactics.
Definition: Context.cs:3472