Z3
Public Member Functions | Properties
Context Class Reference

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

+ Inheritance diagram for Context:

Public Member Functions

 Context ()
 Constructor. More...
 
 Context (Dictionary< string, string > settings)
 Constructor. More...
 
IntSymbol MkSymbol (int i)
 Creates a new symbol using an integer. More...
 
StringSymbol MkSymbol (string name)
 Create a symbol using a string. More...
 
BoolSort MkBoolSort ()
 Create a new Boolean sort. More...
 
UninterpretedSort MkUninterpretedSort (Symbol s)
 Create a new uninterpreted sort. More...
 
UninterpretedSort MkUninterpretedSort (string str)
 Create a new uninterpreted sort. More...
 
IntSort MkIntSort ()
 Create a new integer sort. More...
 
RealSort MkRealSort ()
 Create a real sort. More...
 
BitVecSort MkBitVecSort (uint size)
 Create a new bit-vector sort. More...
 
SeqSort MkSeqSort (Sort s)
 Create a new sequence sort. More...
 
ReSort MkReSort (SeqSort s)
 Create a new regular expression sort. More...
 
ArraySort MkArraySort (Sort domain, Sort range)
 Create a new array sort. More...
 
ArraySort MkArraySort (Sort[] domain, Sort range)
 Create a new n-ary array sort. More...
 
TupleSort MkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 Create a new tuple sort. More...
 
EnumSort MkEnumSort (Symbol name, params Symbol[] enumNames)
 Create a new enumeration sort. More...
 
EnumSort MkEnumSort (string name, params string[] enumNames)
 Create a new enumeration sort. More...
 
ListSort MkListSort (Symbol name, Sort elemSort)
 Create a new list sort. More...
 
ListSort MkListSort (string name, Sort elemSort)
 Create a new list sort. More...
 
FiniteDomainSort MkFiniteDomainSort (Symbol name, ulong size)
 Create a new finite domain sort.

Returns
The result is a sort
More...
 
FiniteDomainSort MkFiniteDomainSort (string name, ulong size)
 Create a new finite domain sort.

Returns
The result is a sort

Elements of the sort are created using

See also
MkNumeral(ulong, Sort)

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

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

Properties

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

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 31 of file Context.cs.

Constructor & Destructor Documentation

◆ Context() [1/2]

Context ( )
inline

Constructor.

Definition at line 37 of file Context.cs.

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

◆ Context() [2/2]

Context ( Dictionary< string, string >  settings)
inline

Constructor.

The following parameters can be set:

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

Definition at line 65 of file Context.cs.

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

Member Function Documentation

◆ AddRecDef()

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

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

Definition at line 553 of file Context.cs.

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

◆ And()

Probe And ( Probe  p1,
Probe  p2 
)
inline

Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".

Definition at line 3685 of file Context.cs.

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

◆ AndThen()

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

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

Definition at line 3344 of file Context.cs.

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

Referenced by Context.Then().

◆ Cond()

Tactic Cond ( Probe  p,
Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.

Definition at line 3436 of file Context.cs.

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

◆ ConstProbe()

Probe ConstProbe ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3605 of file Context.cs.

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

◆ Dispose()

void Dispose ( )
inline

Disposes of the context.

Definition at line 4826 of file Context.cs.

4827  {
4828  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4829  AST_DRQ.Clear(this);
4830  ASTMap_DRQ.Clear(this);
4831  ASTVector_DRQ.Clear(this);
4832  ApplyResult_DRQ.Clear(this);
4833  FuncEntry_DRQ.Clear(this);
4834  FuncInterp_DRQ.Clear(this);
4835  Goal_DRQ.Clear(this);
4836  Model_DRQ.Clear(this);
4837  Params_DRQ.Clear(this);
4838  ParamDescrs_DRQ.Clear(this);
4839  Probe_DRQ.Clear(this);
4840  Solver_DRQ.Clear(this);
4841  Statistics_DRQ.Clear(this);
4842  Tactic_DRQ.Clear(this);
4843  Fixedpoint_DRQ.Clear(this);
4844  Optimize_DRQ.Clear(this);
4845 
4846  m_boolSort = null;
4847  m_intSort = null;
4848  m_realSort = null;
4849  m_stringSort = null;
4850  }

◆ Eq()

Probe Eq ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3671 of file Context.cs.

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

◆ Fail()

Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3472 of file Context.cs.

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

◆ FailIf()

Tactic FailIf ( Probe  p)
inline

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

Definition at line 3481 of file Context.cs.

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

◆ FailIfNotDecided()

Tactic FailIfNotDecided ( )
inline

Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’).

Definition at line 3493 of file Context.cs.

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

◆ Ge()

Probe Ge ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3657 of file Context.cs.

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

◆ Gt()

Probe Gt ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3629 of file Context.cs.

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

◆ Interrupt()

void Interrupt ( )
inline

Interrupt the execution of a Z3 procedure.

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

Definition at line 3553 of file Context.cs.

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

◆ IntToString()

SeqExpr IntToString ( Expr  e)
inline

Convert an integer expression to a string.

Definition at line 2381 of file Context.cs.

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

◆ Le()

Probe Le ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3643 of file Context.cs.

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

◆ Lt()

Probe Lt ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3615 of file Context.cs.

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

◆ MkAdd() [1/2]

ArithExpr MkAdd ( IEnumerable< ArithExpr t)
inline

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

Definition at line 1019 of file Context.cs.

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

◆ MkAdd() [2/2]

ArithExpr MkAdd ( params ArithExpr[]  t)
inline

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

Definition at line 1007 of file Context.cs.

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

Referenced by ArithExpr.operator+().

◆ MkAnd() [1/2]

BoolExpr MkAnd ( IEnumerable< BoolExpr t)
inline

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

Definition at line 968 of file Context.cs.

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

◆ MkAnd() [2/2]

BoolExpr MkAnd ( params BoolExpr[]  t)
inline

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

Definition at line 956 of file Context.cs.

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

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

◆ MkApp() [1/2]

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

Create a new function application.

Definition at line 801 of file Context.cs.

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

◆ MkApp() [2/2]

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

Create a new function application.

Definition at line 788 of file Context.cs.

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

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

◆ MkArrayConst() [1/2]

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

Create an array constant.

Definition at line 2026 of file Context.cs.

2027  {
2028  Debug.Assert(domain != null);
2029  Debug.Assert(range != null);
2030 
2031  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2032  }

◆ MkArrayConst() [2/2]

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

Create an array constant.

Definition at line 2014 of file Context.cs.

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

◆ MkArrayExt()

Expr MkArrayExt ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.

Definition at line 2200 of file Context.cs.

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

◆ MkArraySort() [1/2]

ArraySort MkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 246 of file Context.cs.

247  {
248  Debug.Assert(domain != null);
249  Debug.Assert(range != null);
250 
251  CheckContextMatch(domain);
252  CheckContextMatch(range);
253  return new ArraySort(this, domain, range);
254  }

Referenced by Context.MkArrayConst().

◆ MkArraySort() [2/2]

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

Create a new n-ary array sort.

Definition at line 259 of file Context.cs.

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

◆ MkAt()

SeqExpr MkAt ( SeqExpr  s,
Expr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2479 of file Context.cs.

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

◆ MkAtLeast()

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

Create an at-least-k constraint.

Definition at line 2686 of file Context.cs.

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

◆ MkAtMost()

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

Create an at-most-k constraint.

Definition at line 2675 of file Context.cs.

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

◆ MkBitVecSort()

BitVecSort MkBitVecSort ( uint  size)
inline

Create a new bit-vector sort.

Definition at line 219 of file Context.cs.

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

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

◆ MkBool()

BoolExpr MkBool ( bool  value)
inline

Creates a Boolean value.

Definition at line 833 of file Context.cs.

834  {
835 
836  return value ? MkTrue() : MkFalse();
837  }

◆ MkBoolConst() [1/2]

BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 719 of file Context.cs.

720  {
721 
722  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
723  }

◆ MkBoolConst() [2/2]

BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 709 of file Context.cs.

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

◆ MkBoolSort()

BoolSort MkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 174 of file Context.cs.

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

◆ MkBound()

Expr MkBound ( uint  index,
Sort  ty 
)
inline

Creates a new bound variable.

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

Definition at line 635 of file Context.cs.

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

◆ MkBV() [1/6]

BitVecNum MkBV ( bool[]  bits)
inline

Create a bit-vector numeral.

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

Definition at line 3002 of file Context.cs.

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

◆ MkBV() [2/6]

BitVecNum MkBV ( int  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2959 of file Context.cs.

2960  {
2961 
2962  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2963  }

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

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

◆ MkBV() [4/6]

BitVecNum MkBV ( string  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2948 of file Context.cs.

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

◆ MkBV() [5/6]

BitVecNum MkBV ( uint  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2970 of file Context.cs.

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

◆ MkBV() [6/6]

BitVecNum MkBV ( ulong  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2992 of file Context.cs.

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

◆ MkBV2Int()

IntExpr MkBV2Int ( BitVecExpr  t,
bool signed   
)
inline

Create an integer from the bit-vector argument t .

If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t . If is_signed is true, t1 is treated as a signed bit-vector.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of bit-vector sort.

Definition at line 1875 of file Context.cs.

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

◆ MkBVAdd()

BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1363 of file Context.cs.

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

◆ MkBVAddNoOverflow()

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

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

The arguments must be of bit-vector sort.

Definition at line 1889 of file Context.cs.

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

◆ MkBVAddNoUnderflow()

BoolExpr MkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1905 of file Context.cs.

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

◆ MkBVAND()

BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1267 of file Context.cs.

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

◆ MkBVASHR()

BitVecExpr MkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Arithmetic shift right

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1768 of file Context.cs.

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

◆ MkBVConst() [1/2]

BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 777 of file Context.cs.

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

◆ MkBVConst() [2/2]

BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 767 of file Context.cs.

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

◆ MkBVLSHR()

BitVecExpr MkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Logical shift right

It is equivalent to unsigned division by 2^x where x is the value of t2 .

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1744 of file Context.cs.

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

◆ MkBVMul()

BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1391 of file Context.cs.

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

◆ MkBVMulNoOverflow()

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

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

The arguments must be of bit-vector sort.

Definition at line 1983 of file Context.cs.

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

◆ MkBVMulNoUnderflow()

BoolExpr MkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1999 of file Context.cs.

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

◆ MkBVNAND()

BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1309 of file Context.cs.

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

◆ MkBVNeg()

BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1351 of file Context.cs.

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

◆ MkBVNegNoOverflow()

BoolExpr MkBVNegNoOverflow ( BitVecExpr  t)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1969 of file Context.cs.

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

◆ MkBVNOR()

BitVecExpr MkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1323 of file Context.cs.

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

◆ MkBVNot()

BitVecExpr MkBVNot ( BitVecExpr  t)
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1231 of file Context.cs.

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

◆ MkBVOR()

BitVecExpr MkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1281 of file Context.cs.

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

◆ MkBVRedAND()

BitVecExpr MkBVRedAND ( BitVecExpr  t)
inline

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

The argument must have a bit-vector sort.

Definition at line 1243 of file Context.cs.

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

◆ MkBVRedOR()

BitVecExpr MkBVRedOR ( BitVecExpr  t)
inline

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

The argument must have a bit-vector sort.

Definition at line 1255 of file Context.cs.

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

◆ MkBVRotateLeft() [1/2]

BitVecExpr MkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Left.

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

Definition at line 1815 of file Context.cs.

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

◆ MkBVRotateLeft() [2/2]

BitVecExpr MkBVRotateLeft ( uint  i,
BitVecExpr  t 
)
inline

Rotate Left.

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

Definition at line 1785 of file Context.cs.

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

◆ MkBVRotateRight() [1/2]

BitVecExpr MkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Right.

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

Definition at line 1832 of file Context.cs.

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

◆ MkBVRotateRight() [2/2]

BitVecExpr MkBVRotateRight ( uint  i,
BitVecExpr  t 
)
inline

Rotate Right.

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

Definition at line 1800 of file Context.cs.

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

◆ MkBVSDiv()

BitVecExpr MkBVSDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed division.

It is defined in the following way:

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

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

Definition at line 1433 of file Context.cs.

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

◆ MkBVSDivNoOverflow()

BoolExpr MkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1953 of file Context.cs.

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

◆ MkBVSGE()

BoolExpr MkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1584 of file Context.cs.

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

◆ MkBVSGT()

BoolExpr MkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1616 of file Context.cs.

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

◆ MkBVSHL()

BitVecExpr MkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Shift left.

It is equivalent to multiplication by 2^x where x is the value of t2 .

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The arguments must have a bit-vector sort.

Definition at line 1722 of file Context.cs.

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

◆ MkBVSLE()

BoolExpr MkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must have the same bit-vector sort.

Definition at line 1552 of file Context.cs.

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

◆ MkBVSLT()

BoolExpr MkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed less-than

The arguments must have the same bit-vector sort.

Definition at line 1520 of file Context.cs.

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

◆ MkBVSMod()

BitVecExpr MkBVSMod ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

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

Definition at line 1488 of file Context.cs.

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

◆ MkBVSRem()

BitVecExpr MkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed remainder.

It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

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

Definition at line 1471 of file Context.cs.

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

◆ MkBVSub()

BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1377 of file Context.cs.

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

◆ MkBVSubNoOverflow()

BoolExpr MkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1921 of file Context.cs.

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

◆ MkBVSubNoUnderflow()

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

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

The arguments must be of bit-vector sort.

Definition at line 1937 of file Context.cs.

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

◆ MkBVUDiv()

BitVecExpr MkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned division.

It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1410 of file Context.cs.

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

◆ MkBVUGE()

BoolExpr MkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1568 of file Context.cs.

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

◆ MkBVUGT()

BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1600 of file Context.cs.

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

◆ MkBVULE()

BoolExpr MkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1536 of file Context.cs.

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

◆ MkBVULT()

BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1504 of file Context.cs.

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

◆ MkBVURem()

BitVecExpr MkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

Definition at line 1451 of file Context.cs.

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

◆ MkBVXNOR()

BitVecExpr MkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1337 of file Context.cs.

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

◆ MkBVXOR()

BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1295 of file Context.cs.

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

◆ MkComplement()

ReExpr MkComplement ( ReExpr  re)
inline

Create the complement regular expression.

Definition at line 2594 of file Context.cs.

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

◆ MkConcat() [1/3]

BitVecExpr MkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bit-vector concatenation.

The arguments must have a bit-vector sort.

Returns
The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

Definition at line 1636 of file Context.cs.

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

◆ MkConcat() [2/3]

ReExpr MkConcat ( params ReExpr[]  t)
inline

Create the concatenation of regular languages.

Definition at line 2603 of file Context.cs.

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

◆ MkConcat() [3/3]

SeqExpr MkConcat ( params SeqExpr[]  t)
inline

Concatenate sequences.

Definition at line 2402 of file Context.cs.

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

◆ MkConst() [1/3]

Expr MkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 699 of file Context.cs.

700  {
701  Debug.Assert(f != null);
702 
703  return MkApp(f);
704  }

◆ MkConst() [2/3]

Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 676 of file Context.cs.

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

◆ MkConst() [3/3]

Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 662 of file Context.cs.

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

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

◆ MkConstArray()

ArrayExpr MkConstArray ( Sort  domain,
Expr  v 
)
inline

Create a constant array.

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

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

Definition at line 2151 of file Context.cs.

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

◆ MkConstDecl() [1/2]

FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 607 of file Context.cs.

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

◆ MkConstDecl() [2/2]

FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 594 of file Context.cs.

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

◆ MkConstructor() [1/2]

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

Create a datatype constructor.

Parameters
name
recognizer
fieldNames
sorts
sortRefs
Returns

Definition at line 391 of file Context.cs.

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

◆ MkConstructor() [2/2]

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

Create a datatype constructor.

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

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

◆ MkContains()

BoolExpr MkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2446 of file Context.cs.

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

◆ MkDatatypeSort() [1/2]

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

Create a new datatype sort.

Definition at line 415 of file Context.cs.

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

◆ MkDatatypeSort() [2/2]

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

Create a new datatype sort.

Definition at line 400 of file Context.cs.

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

◆ MkDatatypeSorts() [1/2]

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

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 462 of file Context.cs.

463  {
464  Debug.Assert(names != null);
465  Debug.Assert(c != null);
466  Debug.Assert(names.Length == c.Length);
467  //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null));
468  //Debug.Assert(names.All(name => name != null));
469 
470  return MkDatatypeSorts(MkSymbols(names), c);
471  }

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

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

Referenced by Context.MkDatatypeSorts().

◆ MkDistinct()

BoolExpr MkDistinct ( params Expr[]  args)
inline

Creates a distinct term.

Definition at line 855 of file Context.cs.

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

◆ MkDiv()

ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 1078 of file Context.cs.

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

Referenced by ArithExpr.operator/().

◆ MkEmptyRe()

ReExpr MkEmptyRe ( Sort  s)
inline

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

Definition at line 2640 of file Context.cs.

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

◆ MkEmptySeq()

SeqExpr MkEmptySeq ( Sort  s)
inline

Create the empty sequence.

Definition at line 2354 of file Context.cs.

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

◆ MkEmptySet()

ArrayExpr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2227 of file Context.cs.

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

◆ MkEnumSort() [1/2]

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

Create a new enumeration sort.

Definition at line 303 of file Context.cs.

304  {
305  Debug.Assert(enumNames != null);
306 
307  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
308  }

◆ MkEnumSort() [2/2]

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

Create a new enumeration sort.

Definition at line 288 of file Context.cs.

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

◆ MkEq()

BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 842 of file Context.cs.

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

◆ MkExists() [1/2]

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

Create an existential Quantifier.

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

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

Definition at line 3103 of file Context.cs.

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

◆ MkExists() [2/2]

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

Create an existential Quantifier.

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

Definition at line 3081 of file Context.cs.

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

Referenced by Context.MkQuantifier().

◆ MkExtract() [1/2]

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

Extract subsequence.

Definition at line 2501 of file Context.cs.

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

◆ MkExtract() [2/2]

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

Bit-vector extraction.

Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. The argument t must have a bit-vector sort.

Definition at line 1655 of file Context.cs.

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

◆ MkFalse()

BoolExpr MkFalse ( )
inline

The false Term.

Definition at line 824 of file Context.cs.

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

Referenced by Context.MkBool().

◆ MkFiniteDomainSort() [1/2]

FiniteDomainSort MkFiniteDomainSort ( string  name,
ulong  size 
)
inline

Create a new finite domain sort.

Returns
The result is a sort

Elements of the sort are created using

See also
MkNumeral(ulong, Sort)

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

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

Definition at line 356 of file Context.cs.

357  {
358 
359  return new FiniteDomainSort(this, MkSymbol(name), size);
360  }

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

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

◆ MkFixedpoint()

Fixedpoint MkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3778 of file Context.cs.

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

◆ MkForall() [1/2]

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

Create a universal Quantifier.

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

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

Definition at line 3063 of file Context.cs.

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

◆ MkForall() [2/2]

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

Create a universal Quantifier.

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

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

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

Referenced by Context.MkQuantifier().

◆ MkFP() [1/6]

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

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

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

Parameters
sgnbit-vector term (of size 1) representing the sign.
sigbit-vector term representing the significand.
expbit-vector term representing the exponent.

Definition at line 4368 of file Context.cs.

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

◆ MkFP() [2/6]

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

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

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

Definition at line 4089 of file Context.cs.

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

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

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

◆ MkFP() [4/6]

FPNum MkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4067 of file Context.cs.

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

◆ MkFP() [5/6]

FPNum MkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4057 of file Context.cs.

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

◆ MkFP() [6/6]

FPNum MkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4077 of file Context.cs.

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

◆ MkFPAbs()

FPExpr MkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term

Definition at line 4113 of file Context.cs.

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

◆ MkFPAdd()

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

Floating-point addition

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

Definition at line 4133 of file Context.cs.

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

◆ MkFPDiv()

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

Floating-point division

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

Definition at line 4166 of file Context.cs.

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

◆ MkFPEq()

BoolExpr MkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

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

Parameters
t1floating-point term
t2floating-point term

Definition at line 4285 of file Context.cs.

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

◆ MkFPFMA()

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

Floating-point fused multiply-add

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

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

Definition at line 4181 of file Context.cs.

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

◆ MkFPGEq()

BoolExpr MkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4262 of file Context.cs.

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

◆ MkFPGt()

BoolExpr MkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4272 of file Context.cs.

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

◆ MkFPInf()

FPNum MkFPInf ( FPSort  s,
bool  negative 
)
inline

Create a floating-point infinity of sort s.

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

Definition at line 3983 of file Context.cs.

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

◆ MkFPIsInfinite()

BoolExpr MkFPIsInfinite ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4321 of file Context.cs.

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

◆ MkFPIsNaN()

BoolExpr MkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term

Definition at line 4330 of file Context.cs.

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

◆ MkFPIsNegative()

BoolExpr MkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4339 of file Context.cs.

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

◆ MkFPIsNormal()

BoolExpr MkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4294 of file Context.cs.

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

◆ MkFPIsPositive()

BoolExpr MkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4348 of file Context.cs.

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

◆ MkFPIsSubnormal()

BoolExpr MkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4303 of file Context.cs.

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

◆ MkFPIsZero()

BoolExpr MkFPIsZero ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4312 of file Context.cs.

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

◆ MkFPLEq()

BoolExpr MkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4242 of file Context.cs.

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

◆ MkFPLt()

BoolExpr MkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4252 of file Context.cs.

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

◆ MkFPMax()

FPExpr MkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4232 of file Context.cs.

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

◆ MkFPMin()

FPExpr MkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4222 of file Context.cs.

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

◆ MkFPMul()

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

Floating-point multiplication

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

Definition at line 4155 of file Context.cs.

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

◆ MkFPNaN()

FPNum MkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.

Definition at line 3973 of file Context.cs.

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

◆ MkFPNeg()

FPExpr MkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term

Definition at line 4122 of file Context.cs.

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

◆ MkFPNumeral() [1/5]

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

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

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

Definition at line 4047 of file Context.cs.

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

◆ MkFPNumeral() [2/5]

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

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

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

Definition at line 4035 of file Context.cs.

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

◆ MkFPNumeral() [3/5]

FPNum MkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4013 of file Context.cs.

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

◆ MkFPNumeral() [4/5]

FPNum MkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4003 of file Context.cs.

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

Referenced by Context.MkFP().

◆ MkFPNumeral() [5/5]

FPNum MkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4023 of file Context.cs.

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

◆ MkFPRem()

FPExpr MkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term

Definition at line 4201 of file Context.cs.

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

◆ MkFPRNA()

FPRMNum MkFPRNA ( )
inline

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

Definition at line 3837 of file Context.cs.

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

◆ MkFPRNE()

FPRMNum MkFPRNE ( )
inline

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

Definition at line 3821 of file Context.cs.

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

◆ MkFPRoundingModeSort()

FPRMSort MkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Definition at line 3803 of file Context.cs.

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

◆ MkFPRoundNearestTiesToAway()

FPRMNum MkFPRoundNearestTiesToAway ( )
inline

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

Definition at line 3829 of file Context.cs.

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

◆ MkFPRoundNearestTiesToEven()

FPRMExpr MkFPRoundNearestTiesToEven ( )
inline

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

Definition at line 3813 of file Context.cs.

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

◆ MkFPRoundToIntegral()

FPExpr MkFPRoundToIntegral ( FPRMExpr  rm,
FPExpr  t 
)
inline

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

Parameters
rmterm of RoundingMode sort
tfloating-point term

Definition at line 4212 of file Context.cs.

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

◆ MkFPRoundTowardNegative()

FPRMNum MkFPRoundTowardNegative ( )
inline

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

Definition at line 3861 of file Context.cs.

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

◆ MkFPRoundTowardPositive()

FPRMNum MkFPRoundTowardPositive ( )
inline

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

Definition at line 3845 of file Context.cs.

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

◆ MkFPRoundTowardZero()

FPRMNum MkFPRoundTowardZero ( )
inline

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

Definition at line 3877 of file Context.cs.

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

◆ MkFPRTN()

FPRMNum MkFPRTN ( )
inline

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

Definition at line 3869 of file Context.cs.

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

◆ MkFPRTP()

FPRMNum MkFPRTP ( )
inline

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

Definition at line 3853 of file Context.cs.

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

◆ MkFPRTZ()

FPRMNum MkFPRTZ ( )
inline

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

Definition at line 3885 of file Context.cs.

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

◆ MkFPSort()

FPSort MkFPSort ( uint  ebits,
uint  sbits 
)
inline

Create a FloatingPoint sort.

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

Definition at line 3898 of file Context.cs.

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

◆ MkFPSort128()

FPSort MkFPSort128 ( )
inline

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

Definition at line 3962 of file Context.cs.

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

◆ MkFPSort16()

FPSort MkFPSort16 ( )
inline

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

Definition at line 3914 of file Context.cs.

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

◆ MkFPSort32()

FPSort MkFPSort32 ( )
inline

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

Definition at line 3930 of file Context.cs.

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

◆ MkFPSort64()

FPSort MkFPSort64 ( )
inline

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

Definition at line 3946 of file Context.cs.

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

◆ MkFPSortDouble()

FPSort MkFPSortDouble ( )
inline

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

Definition at line 3938 of file Context.cs.

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

◆ MkFPSortHalf()

FPSort MkFPSortHalf ( )
inline

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

Definition at line 3906 of file Context.cs.

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

◆ MkFPSortQuadruple()

FPSort MkFPSortQuadruple ( )
inline

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

Definition at line 3954 of file Context.cs.

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

◆ MkFPSortSingle()

FPSort MkFPSortSingle ( )
inline

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

Definition at line 3922 of file Context.cs.

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

◆ MkFPSqrt()

FPExpr MkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term

Definition at line 4191 of file Context.cs.

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

◆ MkFPSub()

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

Floating-point subtraction

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

Definition at line 4144 of file Context.cs.

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

◆ MkFPToBV()

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

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

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

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

Definition at line 4471 of file Context.cs.

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

◆ MkFPToFP() [1/6]

FPExpr MkFPToFP ( BitVecExpr  bv,
FPSort  s 
)
inline

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

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

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

Definition at line 4384 of file Context.cs.

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

◆ MkFPToFP() [2/6]

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

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

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

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

Definition at line 4434 of file Context.cs.

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

◆ MkFPToFP() [3/6]

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

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

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

Parameters
rmRoundingMode term.
tFloatingPoint term.
sFloatingPoint sort.

Definition at line 4400 of file Context.cs.

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

◆ MkFPToFP() [4/6]

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

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

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

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

Definition at line 4522 of file Context.cs.

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

◆ MkFPToFP() [5/6]

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

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

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

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

Definition at line 4416 of file Context.cs.

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

◆ MkFPToFP() [6/6]

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

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

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

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

Definition at line 4452 of file Context.cs.

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

◆ MkFPToIEEEBV()

BitVecExpr MkFPToIEEEBV ( FPExpr  t)
inline

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

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

Parameters
tFloatingPoint term.

Definition at line 4505 of file Context.cs.

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

◆ MkFPToReal()

RealExpr MkFPToReal ( FPExpr  t)
inline

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

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

Parameters
tFloatingPoint term

Definition at line 4488 of file Context.cs.

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

◆ MkFPZero()

FPNum MkFPZero ( FPSort  s,
bool  negative 
)
inline

Create a floating-point zero of sort s.

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

Definition at line 3993 of file Context.cs.

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

◆ MkFreshConst()

Expr MkFreshConst ( string  prefix,
Sort  range 
)
inline

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

Definition at line 687 of file Context.cs.

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

◆ MkFreshConstDecl()

FuncDecl MkFreshConstDecl ( string  prefix,
Sort  range 
)
inline

Creates a fresh constant function declaration with a name prefixed with prefix .

See also
MkFuncDecl(string,Sort,Sort), MkFuncDecl(string,Sort[],Sort)

Definition at line 620 of file Context.cs.

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

◆ MkFreshFuncDecl()

FuncDecl MkFreshFuncDecl ( string  prefix,
Sort[]  domain,
Sort  range 
)
inline

Creates a fresh function declaration with a name prefixed with prefix .

See also
MkFuncDecl(string,Sort,Sort), MkFuncDecl(string,Sort[],Sort)

Definition at line 581 of file Context.cs.

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

◆ MkFullRe()

ReExpr MkFullRe ( Sort  s)
inline

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

Definition at line 2650 of file Context.cs.

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

◆ MkFullSet()

ArrayExpr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2238 of file Context.cs.

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

◆ MkFuncDecl() [1/4]

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

Creates a new function declaration.

Definition at line 565 of file Context.cs.

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

◆ MkFuncDecl() [2/4]

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

Creates a new function declaration.

Definition at line 524 of file Context.cs.

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

◆ MkFuncDecl() [3/4]

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

Creates a new function declaration.

Definition at line 508 of file Context.cs.

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

◆ MkFuncDecl() [4/4]

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

Creates a new function declaration.

Definition at line 493 of file Context.cs.

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

◆ MkGe()

BoolExpr MkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 >= t2

Definition at line 1171 of file Context.cs.

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

Referenced by ArithExpr.operator>=().

◆ MkGoal()

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

Creates a new Goal.

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

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

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

◆ MkGt()

BoolExpr MkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 > t2

Definition at line 1158 of file Context.cs.

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

Referenced by ArithExpr.operator>().

◆ MkIff()

BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 897 of file Context.cs.

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

◆ MkImplies()

BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 910 of file Context.cs.

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

◆ MkIndexOf()

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

Extract index of sub-string starting at offset.

Definition at line 2513 of file Context.cs.

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

◆ MkInRe()

BoolExpr MkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2547 of file Context.cs.

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

◆ MkInt() [1/5]

IntNum MkInt ( int  v)
inline

Create an integer numeral.

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

Definition at line 2902 of file Context.cs.

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

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

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

◆ MkInt() [3/5]

IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2891 of file Context.cs.

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

◆ MkInt() [4/5]

IntNum MkInt ( uint  v)
inline

Create an integer numeral.

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

Definition at line 2913 of file Context.cs.

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

◆ MkInt() [5/5]

IntNum MkInt ( ulong  v)
inline

Create an integer numeral.

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

Definition at line 2935 of file Context.cs.

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

◆ MkInt2BV()

BitVecExpr MkInt2BV ( uint  n,
IntExpr  t 
)
inline

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

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The argument must be of integer sort.

Definition at line 1852 of file Context.cs.

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

◆ MkInt2Real()

RealExpr MkInt2Real ( IntExpr  t)
inline

Coerce an integer to a real.

There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

You can take the floor of a real by creating an auxiliary integer Term k and and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. The argument must be of integer sort.

Definition at line 1191 of file Context.cs.

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

◆ MkIntConst() [1/2]

IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 738 of file Context.cs.

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

◆ MkIntConst() [2/2]

IntExpr MkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 728 of file Context.cs.

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

◆ MkIntersect()

ReExpr MkIntersect ( params ReExpr[]  t)
inline

Create the intersection of regular languages.

Definition at line 2627 of file Context.cs.

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

◆ MkIntSort()

IntSort MkIntSort ( )
inline

Create a new integer sort.

Definition at line 202 of file Context.cs.

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

◆ MkIsInteger()

BoolExpr MkIsInteger ( RealExpr  t)
inline

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

Definition at line 1217 of file Context.cs.

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

◆ MkITE()

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

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

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

Definition at line 882 of file Context.cs.

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

◆ MkLambda() [1/2]

Lambda MkLambda ( Expr[]  boundConstants,
Expr  body 
)
inline

Create a lambda expression.

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

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

Definition at line 3192 of file Context.cs.

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

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

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

◆ MkLe()

BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1145 of file Context.cs.

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

Referenced by ArithExpr.operator<=().

◆ MkLength()

IntExpr MkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 2415 of file Context.cs.

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

◆ MkListSort() [1/2]

ListSort MkListSort ( string  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 326 of file Context.cs.

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

◆ MkListSort() [2/2]

ListSort MkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 313 of file Context.cs.

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

◆ MkLoop()

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

Take the bounded Kleene star of a regular expression.

Definition at line 2567 of file Context.cs.

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

◆ MkLt()

BoolExpr MkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 < t2

Definition at line 1132 of file Context.cs.

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

Referenced by ArithExpr.operator<().

◆ MkMap()

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

Maps f on the argument arrays.

Each element of args must be of an array sort [domain_i -> range_i]. The function declaration f must have type range_1 .. range_n -> range. v must have sort range. The sort of the result is [domain_i -> range].

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

Definition at line 2172 of file Context.cs.

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

◆ MkMod()

IntExpr MkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 1092 of file Context.cs.

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

◆ MkMul() [1/2]

ArithExpr MkMul ( IEnumerable< ArithExpr t)
inline

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

Definition at line 1043 of file Context.cs.

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

◆ MkMul() [2/2]

ArithExpr MkMul ( params ArithExpr[]  t)
inline

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

Definition at line 1031 of file Context.cs.

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

Referenced by ArithExpr.operator*().

◆ MkNot()

BoolExpr MkNot ( BoolExpr  a)
inline

Mk an expression representing not(a).

Definition at line 868 of file Context.cs.

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

Referenced by BoolExpr.operator!().

◆ MkNth()

Expr MkNth ( SeqExpr  s,
Expr  index 
)
inline

Retrieve element at index.

Definition at line 2490 of file Context.cs.

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

◆ MkNumeral() [1/5]

Expr MkNumeral ( int  v,
Sort  ty 
)
inline

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

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

Definition at line 2760 of file Context.cs.

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

◆ MkNumeral() [2/5]

Expr MkNumeral ( long  v,
Sort  ty 
)
inline

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

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

Definition at line 2790 of file Context.cs.

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

◆ MkNumeral() [3/5]

Expr MkNumeral ( string  v,
Sort  ty 
)
inline

Create a Term of a given sort.

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

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

Referenced by Context.MkBV().

◆ MkNumeral() [4/5]

Expr MkNumeral ( uint  v,
Sort  ty 
)
inline

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

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

Definition at line 2775 of file Context.cs.

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

◆ MkNumeral() [5/5]

Expr MkNumeral ( ulong  v,
Sort  ty 
)
inline

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

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

Definition at line 2805 of file Context.cs.

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

◆ MkOptimize()

Optimize MkOptimize ( )
inline

Create an Optimization context.

Definition at line 3789 of file Context.cs.

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

◆ MkOption()

ReExpr MkOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2585 of file Context.cs.

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

◆ MkOr() [1/2]

BoolExpr MkOr ( IEnumerable< BoolExpr t)
inline

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

Definition at line 992 of file Context.cs.

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

◆ MkOr() [2/2]

BoolExpr MkOr ( params BoolExpr[]  t)
inline

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

Definition at line 979 of file Context.cs.

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

◆ MkParams()

Params MkParams ( )
inline

Creates a new ParameterSet.

Definition at line 3290 of file Context.cs.

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

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

◆ MkPattern()

Pattern MkPattern ( params Expr[]  terms)
inline

Create a quantifier pattern.

Definition at line 647 of file Context.cs.

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

◆ MkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2724 of file Context.cs.

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

◆ MkPBGe()

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

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

Definition at line 2711 of file Context.cs.

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

◆ MkPBLe()

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

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

Definition at line 2697 of file Context.cs.

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

◆ MkPlus()

ReExpr MkPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2576 of file Context.cs.

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

◆ MkPower()

ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 1119 of file Context.cs.

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

◆ MkPrefixOf()

BoolExpr MkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 2424 of file Context.cs.

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

◆ MkProbe()

Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3596 of file Context.cs.

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

◆ MkQuantifier() [1/2]

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

Create a Quantifier.

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

Definition at line 3141 of file Context.cs.

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

◆ MkQuantifier() [2/2]

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

Create a Quantifier.

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

Definition at line 3118 of file Context.cs.

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

◆ MkRange()

ReExpr MkRange ( SeqExpr  lo,
SeqExpr  hi 
)
inline

Create a range expression.

Definition at line 2660 of file Context.cs.

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

◆ MkReal() [1/6]

RatNum MkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

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

Definition at line 2822 of file Context.cs.

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

◆ MkReal() [2/6]

RatNum MkReal ( int  v)
inline

Create a real numeral.

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

Definition at line 2846 of file Context.cs.

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

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

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

◆ MkReal() [4/6]

RatNum MkReal ( string  v)
inline

Create a real numeral.

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

Definition at line 2835 of file Context.cs.

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

◆ MkReal() [5/6]

RatNum MkReal ( uint  v)
inline

Create a real numeral.

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

Definition at line 2857 of file Context.cs.

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

◆ MkReal() [6/6]

RatNum MkReal ( ulong  v)
inline

Create a real numeral.

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

Definition at line 2879 of file Context.cs.

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

◆ MkReal2Int()

IntExpr MkReal2Int ( RealExpr  t)
inline

Coerce a real to an integer.

The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.

Definition at line 1206 of file Context.cs.

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

◆ MkRealConst() [1/2]

RealExpr MkRealConst ( string  name)
inline

Creates a real constant.

Definition at line 758 of file Context.cs.

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

◆ MkRealConst() [2/2]

RealExpr MkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 748 of file Context.cs.

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

◆ MkRealSort()

RealSort MkRealSort ( )
inline

Create a real sort.

Definition at line 211 of file Context.cs.

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

◆ MkRecFuncDecl()

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

Creates a new recursive function declaration.

Definition at line 537 of file Context.cs.

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

◆ MkRem()

IntExpr MkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 1106 of file Context.cs.

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

◆ MkRepeat()

BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1702 of file Context.cs.

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

◆ MkReplace()

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

Replace the first occurrence of src by dst in s.

Definition at line 2525 of file Context.cs.

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

◆ MkReSort()

ReSort MkReSort ( SeqSort  s)
inline

Create a new regular expression sort.

Definition at line 237 of file Context.cs.

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

◆ MkSelect() [1/2]

Expr MkSelect ( ArrayExpr  a,
Expr  i 
)
inline

Array read.

The argument a is the array and i is the index of the array that gets read.

The node a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range.

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

Definition at line 2048 of file Context.cs.

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

◆ MkSelect() [2/2]

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

Array read.

The argument a is the array and args are the indices of the array that gets read.

The node a must have an array sort [domain1,..,domaink -> range], and args must have the sort domain1,..,domaink. The sort of the result is range.

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

Definition at line 2071 of file Context.cs.

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

◆ MkSeqSort()

SeqSort MkSeqSort ( Sort  s)
inline

Create a new sequence sort.

Definition at line 228 of file Context.cs.

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

◆ MkSetAdd()

ArrayExpr MkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2249 of file Context.cs.

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

◆ MkSetComplement()

ArrayExpr MkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 2313 of file Context.cs.

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

◆ MkSetDel()

ArrayExpr MkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 2263 of file Context.cs.

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

◆ MkSetDifference()

ArrayExpr MkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2300 of file Context.cs.

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

◆ MkSetIntersection()

ArrayExpr MkSetIntersection ( params ArrayExpr[]  args)
inline

Take the intersection of a list of sets.

Definition at line 2288 of file Context.cs.

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

◆ MkSetMembership()

BoolExpr MkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 2324 of file Context.cs.

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

◆ MkSetSort()

SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2216 of file Context.cs.

2217  {
2218  Debug.Assert(ty != null);
2219 
2220  CheckContextMatch(ty);
2221  return new SetSort(this, ty);
2222  }

◆ MkSetSubset()

BoolExpr MkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2337 of file Context.cs.

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

◆ MkSetUnion()

ArrayExpr MkSetUnion ( params ArrayExpr[]  args)
inline

Take the union of a list of sets.

Definition at line 2276 of file Context.cs.

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

◆ MkSignExt()

BitVecExpr MkSignExt ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector sign extension.

Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 1671 of file Context.cs.

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

◆ MkSimpleSolver()

Solver MkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3753 of file Context.cs.

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

◆ MkSolver() [1/3]

Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 3744 of file Context.cs.

3745  {
3746 
3747  return MkSolver(MkSymbol(logic));
3748  }

◆ MkSolver() [2/3]

Solver MkSolver ( Symbol  logic = null)
inline

Creates a new (incremental) solver.

This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

Definition at line 3731 of file Context.cs.

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

Referenced by Context.MkSolver().

◆ MkSolver() [3/3]

Solver MkSolver ( Tactic  t)
inline

Creates a solver that is implemented using the given tactic.

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

Definition at line 3766 of file Context.cs.

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

◆ MkStar()

ReExpr MkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2558 of file Context.cs.

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

◆ MkStore() [1/2]

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

Array update.

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

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

Definition at line 2100 of file Context.cs.

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

◆ MkStore() [2/2]

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

Array update.

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

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

Definition at line 2130 of file Context.cs.

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

◆ MkString()

SeqExpr MkString ( string  s)
inline

Create a string constant.

Definition at line 2372 of file Context.cs.

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

◆ MkStringLe()

BoolExpr MkStringLe ( SeqExpr  s1,
SeqExpr  s2 
)
inline

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

Definition at line 2468 of file Context.cs.

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

◆ MkStringLt()

BoolExpr MkStringLt ( SeqExpr  s1,
SeqExpr  s2 
)
inline

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

Definition at line 2457 of file Context.cs.

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

◆ MkSub()

ArithExpr MkSub ( params ArithExpr[]  t)
inline

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

Definition at line 1055 of file Context.cs.

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

Referenced by ArithExpr.operator-().

◆ MkSuffixOf()

BoolExpr MkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 2435 of file Context.cs.

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

◆ MkSymbol() [1/2]

IntSymbol MkSymbol ( int  i)
inline

Creates a new symbol using an integer.

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

Definition at line 90 of file Context.cs.

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

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

◆ MkSymbol() [2/2]

StringSymbol MkSymbol ( string  name)
inline

Create a symbol using a string.

Definition at line 99 of file Context.cs.

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

◆ MkTactic()

Tactic MkTactic ( string  name)
inline

Creates a new Tactic.

Definition at line 3334 of file Context.cs.

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

Referenced by Goal.Simplify().

◆ MkTermArray()

Expr MkTermArray ( ArrayExpr  array)
inline

Access the array default value.

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

Definition at line 2189 of file Context.cs.

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

◆ MkToRe()

ReExpr MkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2537 of file Context.cs.

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

◆ MkTrue()

BoolExpr MkTrue ( )
inline

The true Term.

Definition at line 815 of file Context.cs.

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

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

◆ MkTupleSort()

TupleSort MkTupleSort ( Symbol  name,