|
Z3
|
|
|
Z3
|
|
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.
| |
| FiniteDomainSort | MkFiniteDomainSort (string name, ulong size) |
Create a new finite domain sort.
Elements of the sort are created using
, and the elements range from 0 to | |
| Constructor | MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null) |
| Create a datatype constructor. More... | |
| Constructor | MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null) |
| Create a datatype constructor. More... | |
| DatatypeSort | MkDatatypeSort (Symbol name, Constructor[] constructors) |
| Create a new datatype sort. More... | |
| DatatypeSort | MkDatatypeSort (string name, Constructor[] constructors) |
| Create a new datatype sort. More... | |
| DatatypeSort[] | MkDatatypeSorts (Symbol[] names, Constructor[][] c) |
| Create mutually recursive datatypes. More... | |
| DatatypeSort[] | MkDatatypeSorts (string[] names, Constructor[][] c) |
| Create mutually recursive data-types. More... | |
| Expr | MkUpdateField (FuncDecl field, Expr t, Expr v) |
| Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remaining fields of t are unchanged. More... | |
| FuncDecl | MkFuncDecl (Symbol name, Sort[] domain, Sort range) |
| Creates a new function declaration. More... | |
| FuncDecl | MkFuncDecl (Symbol name, Sort domain, Sort range) |
| Creates a new function declaration. More... | |
| FuncDecl | MkFuncDecl (string name, Sort[] domain, Sort range) |
| Creates a new function declaration. More... | |
| FuncDecl | MkRecFuncDecl (string name, Sort[] domain, Sort range) |
| Creates a new recursive function declaration. More... | |
| void | AddRecDef (FuncDecl f, Expr[] args, Expr body) |
| Bind a definition to a recursive function declaration. The function must have previously been created using MkRecFuncDecl. The body may contain recursive uses of the function or other mutually recursive functions. More... | |
| FuncDecl | MkFuncDecl (string name, Sort domain, Sort range) |
| Creates a new function declaration. More... | |
| FuncDecl | MkFreshFuncDecl (string prefix, Sort[] domain, Sort range) |
| Creates a fresh function declaration with a name prefixed with prefix . More... | |
| FuncDecl | MkConstDecl (Symbol name, Sort range) |
| Creates a new constant function declaration. More... | |
| FuncDecl | MkConstDecl (string name, Sort range) |
| Creates a new constant function declaration. More... | |
| FuncDecl | MkFreshConstDecl (string prefix, Sort range) |
| Creates a fresh constant function declaration with a name prefixed with prefix . More... | |
| FuncDecl | MkUserPropagatorFuncDecl (string name, Sort[] domain, Sort range) |
| Declare a function to be processed by the user propagator plugin. More... | |
| Expr | MkBound (uint index, Sort ty) |
| Creates a new bound variable. More... | |
| Pattern | MkPattern (params Expr[] terms) |
| Create a quantifier pattern. More... | |
| Expr | MkConst (Symbol name, Sort range) |
| Creates a new Constant of sort range and named name . More... | |
| Expr | MkConst (string name, Sort range) |
| Creates a new Constant of sort range and named name . More... | |
| Expr | MkFreshConst (string prefix, Sort range) |
| Creates a fresh Constant of sort range and a name prefixed with prefix . More... | |
| Expr | MkConst (FuncDecl f) |
| Creates a fresh constant from the FuncDecl f . More... | |
| BoolExpr | MkBoolConst (Symbol name) |
| Create a Boolean constant. More... | |
| BoolExpr | MkBoolConst (string name) |
| Create a Boolean constant. More... | |
| IntExpr | MkIntConst (Symbol name) |
| Creates an integer constant. More... | |
| IntExpr | MkIntConst (string name) |
| Creates an integer constant. More... | |
| RealExpr | MkRealConst (Symbol name) |
| Creates a real constant. More... | |
| RealExpr | MkRealConst (string name) |
| Creates a real constant. More... | |
| BitVecExpr | MkBVConst (Symbol name, uint size) |
| Creates a bit-vector constant. More... | |
| BitVecExpr | MkBVConst (string name, uint size) |
| Creates a bit-vector constant. More... | |
| Expr | MkApp (FuncDecl f, params Expr[] args) |
| Create a new function application. More... | |
| Expr | MkApp (FuncDecl f, IEnumerable< Expr > args) |
| Create a new function application. More... | |
| BoolExpr | MkTrue () |
| The true Term. More... | |
| BoolExpr | MkFalse () |
| The false Term. More... | |
| BoolExpr | MkBool (bool value) |
| Creates a Boolean value. More... | |
| BoolExpr | MkEq (Expr x, Expr y) |
| Creates the equality x = y . More... | |
| BoolExpr | MkDistinct (params Expr[] args) |
Creates a distinct term. More... | |
| BoolExpr | MkDistinct (IEnumerable< Expr > args) |
Creates a distinct term. More... | |
| BoolExpr | MkNot (BoolExpr a) |
Mk an expression representing not(a). More... | |
| Expr | MkITE (BoolExpr t1, Expr t2, Expr t3) |
Create an expression representing an if-then-else: ite(t1, t2, t3). More... | |
| BoolExpr | MkIff (BoolExpr t1, BoolExpr t2) |
Create an expression representing t1 iff t2. More... | |
| BoolExpr | MkImplies (BoolExpr t1, BoolExpr t2) |
Create an expression representing t1 -> t2. More... | |
| BoolExpr | MkXor (BoolExpr t1, BoolExpr t2) |
Create an expression representing t1 xor t2. More... | |
| BoolExpr | MkXor (IEnumerable< BoolExpr > ts) |
Create an expression representing t1 xor t2 xor t3 ... . More... | |
| BoolExpr | MkAnd (params BoolExpr[] t) |
Create an expression representing t[0] and t[1] and .... More... | |
| BoolExpr | MkAnd (IEnumerable< BoolExpr > t) |
Create an expression representing t[0] and t[1] and .... More... | |
| BoolExpr | MkOr (params BoolExpr[] t) |
Create an expression representing t[0] or t[1] or .... More... | |
| BoolExpr | MkOr (IEnumerable< BoolExpr > t) |
Create an expression representing t[0] or t[1] or .... More... | |
| ArithExpr | MkAdd (params ArithExpr[] t) |
Create an expression representing t[0] + t[1] + .... More... | |
| ArithExpr | MkAdd (IEnumerable< ArithExpr > t) |
Create an expression representing t[0] + t[1] + .... More... | |
| ArithExpr | MkMul (params ArithExpr[] t) |
Create an expression representing t[0] * t[1] * .... More... | |
| ArithExpr | MkMul (IEnumerable< ArithExpr > t) |
Create an expression representing t[0] * t[1] * .... More... | |
| ArithExpr | MkSub (params ArithExpr[] t) |
Create an expression representing t[0] - t[1] - .... More... | |
| ArithExpr | MkUnaryMinus (ArithExpr t) |
Create an expression representing -t. More... | |
| ArithExpr | MkDiv (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 / t2. More... | |
| IntExpr | MkMod (IntExpr t1, IntExpr t2) |
Create an expression representing t1 mod t2. More... | |
| IntExpr | MkRem (IntExpr t1, IntExpr t2) |
Create an expression representing t1 rem t2. More... | |
| ArithExpr | MkPower (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 ^ t2. More... | |
| BoolExpr | MkLt (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 < t2 More... | |
| BoolExpr | MkLe (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 <= t2 More... | |
| BoolExpr | MkGt (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 > t2 More... | |
| BoolExpr | MkGe (ArithExpr t1, ArithExpr t2) |
Create an expression representing t1 >= t2 More... | |
| RealExpr | MkInt2Real (IntExpr t) |
| Coerce an integer to a real. More... | |
| IntExpr | MkReal2Int (RealExpr t) |
| Coerce a real to an integer. More... | |
| BoolExpr | MkIsInteger (RealExpr t) |
| Creates an expression that checks whether a real number is an integer. More... | |
| BitVecExpr | MkBVNot (BitVecExpr t) |
| Bitwise negation. More... | |
| BitVecExpr | MkBVRedAND (BitVecExpr t) |
| Take conjunction of bits in a vector, return vector of length 1. More... | |
| BitVecExpr | MkBVRedOR (BitVecExpr t) |
| Take disjunction of bits in a vector, return vector of length 1. More... | |
| BitVecExpr | MkBVAND (BitVecExpr t1, BitVecExpr t2) |
| Bitwise conjunction. More... | |
| BitVecExpr | MkBVOR (BitVecExpr t1, BitVecExpr t2) |
| Bitwise disjunction. More... | |
| BitVecExpr | MkBVXOR (BitVecExpr t1, BitVecExpr t2) |
| Bitwise XOR. More... | |
| BitVecExpr | MkBVNAND (BitVecExpr t1, BitVecExpr t2) |
| Bitwise NAND. More... | |
| BitVecExpr | MkBVNOR (BitVecExpr t1, BitVecExpr t2) |
| Bitwise NOR. More... | |
| BitVecExpr | MkBVXNOR (BitVecExpr t1, BitVecExpr t2) |
| Bitwise XNOR. More... | |
| BitVecExpr | MkBVNeg (BitVecExpr t) |
| Standard two's complement unary minus. More... | |
| BitVecExpr | MkBVAdd (BitVecExpr t1, BitVecExpr t2) |
| Two's complement addition. More... | |
| BitVecExpr | MkBVSub (BitVecExpr t1, BitVecExpr t2) |
| Two's complement subtraction. More... | |
| BitVecExpr | MkBVMul (BitVecExpr t1, BitVecExpr t2) |
| Two's complement multiplication. More... | |
| BitVecExpr | MkBVUDiv (BitVecExpr t1, BitVecExpr t2) |
| Unsigned division. More... | |
| BitVecExpr | MkBVSDiv (BitVecExpr t1, BitVecExpr t2) |
| Signed division. More... | |
| BitVecExpr | MkBVURem (BitVecExpr t1, BitVecExpr t2) |
| Unsigned remainder. More... | |
| BitVecExpr | MkBVSRem (BitVecExpr t1, BitVecExpr t2) |
| Signed remainder. More... | |
| BitVecExpr | MkBVSMod (BitVecExpr t1, BitVecExpr t2) |
| Two's complement signed remainder (sign follows divisor). More... | |
| BoolExpr | MkBVULT (BitVecExpr t1, BitVecExpr t2) |
| Unsigned less-than More... | |
| BoolExpr | MkBVSLT (BitVecExpr t1, BitVecExpr t2) |
| Two's complement signed less-than More... | |
| BoolExpr | MkBVULE (BitVecExpr t1, BitVecExpr t2) |
| Unsigned less-than or equal to. More... | |
| BoolExpr | MkBVSLE (BitVecExpr t1, BitVecExpr t2) |
| Two's complement signed less-than or equal to. More... | |
| BoolExpr | MkBVUGE (BitVecExpr t1, BitVecExpr t2) |
| Unsigned greater than or equal to. More... | |
| BoolExpr | MkBVSGE (BitVecExpr t1, BitVecExpr t2) |
| Two's complement signed greater than or equal to. More... | |
| BoolExpr | MkBVUGT (BitVecExpr t1, BitVecExpr t2) |
| Unsigned greater-than. More... | |
| BoolExpr | MkBVSGT (BitVecExpr t1, BitVecExpr t2) |
| Two's complement signed greater-than. More... | |
| BitVecExpr | MkConcat (BitVecExpr t1, BitVecExpr t2) |
| Bit-vector concatenation. More... | |
| BitVecExpr | MkExtract (uint high, uint low, BitVecExpr t) |
| Bit-vector extraction. More... | |
| BitVecExpr | MkSignExt (uint i, BitVecExpr t) |
| Bit-vector sign extension. More... | |
| BitVecExpr | MkZeroExt (uint i, BitVecExpr t) |
| Bit-vector zero extension. More... | |
| BitVecExpr | MkRepeat (uint i, BitVecExpr t) |
| Bit-vector repetition. More... | |
| BitVecExpr | MkBVSHL (BitVecExpr t1, BitVecExpr t2) |
| Shift left. More... | |
| BitVecExpr | MkBVLSHR (BitVecExpr t1, BitVecExpr t2) |
| Logical shift right More... | |
| BitVecExpr | MkBVASHR (BitVecExpr t1, BitVecExpr t2) |
| Arithmetic shift right More... | |
| BitVecExpr | MkBVRotateLeft (uint i, BitVecExpr t) |
| Rotate Left. More... | |
| BitVecExpr | MkBVRotateRight (uint i, BitVecExpr t) |
| Rotate Right. More... | |
| BitVecExpr | MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) |
| Rotate Left. More... | |
| BitVecExpr | MkBVRotateRight (BitVecExpr t1, BitVecExpr t2) |
| Rotate Right. More... | |
| BitVecExpr | MkInt2BV (uint n, IntExpr t) |
| Create an n bit bit-vector from the integer argument t . More... | |
| IntExpr | MkBV2Int (BitVecExpr t, bool signed) |
| Create an integer from the bit-vector argument t . More... | |
| BoolExpr | MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) |
| Create a predicate that checks that the bit-wise addition does not overflow. More... | |
| BoolExpr | MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) |
| Create a predicate that checks that the bit-wise addition does not underflow. More... | |
| BoolExpr | MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) |
| Create a predicate that checks that the bit-wise subtraction does not overflow. More... | |
| BoolExpr | MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) |
| Create a predicate that checks that the bit-wise subtraction does not underflow. More... | |
| BoolExpr | MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) |
| Create a predicate that checks that the bit-wise signed division does not overflow. More... | |
| BoolExpr | MkBVNegNoOverflow (BitVecExpr t) |
| Create a predicate that checks that the bit-wise negation does not overflow. More... | |
| BoolExpr | MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) |
| Create a predicate that checks that the bit-wise multiplication does not overflow. More... | |
| BoolExpr | MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) |
| Create a predicate that checks that the bit-wise multiplication does not underflow. More... | |
| ArrayExpr | MkArrayConst (Symbol name, Sort domain, Sort range) |
| Create an array constant. More... | |
| ArrayExpr | MkArrayConst (string name, Sort domain, Sort range) |
| Create an array constant. More... | |
| Expr | MkSelect (ArrayExpr a, Expr i) |
| Array read. More... | |
| Expr | MkSelect (ArrayExpr a, params Expr[] args) |
| Array read. More... | |
| ArrayExpr | MkStore (ArrayExpr a, Expr i, Expr v) |
| Array update. More... | |
| ArrayExpr | MkStore (ArrayExpr a, Expr[] args, Expr v) |
| Array update. More... | |
| ArrayExpr | MkConstArray (Sort domain, Expr v) |
| Create a constant array. More... | |
| ArrayExpr | MkMap (FuncDecl f, params ArrayExpr[] args) |
| Maps f on the argument arrays. More... | |
| Expr | MkTermArray (ArrayExpr array) |
| Access the array default value. More... | |
| Expr | MkArrayExt (ArrayExpr arg1, ArrayExpr arg2) |
| Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. More... | |
| SetSort | MkSetSort (Sort ty) |
| Create a set type. More... | |
| ArrayExpr | MkEmptySet (Sort domain) |
| Create an empty set. More... | |
| ArrayExpr | MkFullSet (Sort domain) |
| Create the full set. More... | |
| ArrayExpr | MkSetAdd (ArrayExpr set, Expr element) |
| Add an element to the set. More... | |
| ArrayExpr | MkSetDel (ArrayExpr set, Expr element) |
| Remove an element from a set. More... | |
| ArrayExpr | MkSetUnion (params ArrayExpr[] args) |
| Take the union of a list of sets. More... | |
| ArrayExpr | MkSetIntersection (params ArrayExpr[] args) |
| Take the intersection of a list of sets. More... | |
| ArrayExpr | MkSetDifference (ArrayExpr arg1, ArrayExpr arg2) |
| Take the difference between two sets. More... | |
| ArrayExpr | MkSetComplement (ArrayExpr arg) |
| Take the complement of a set. More... | |
| BoolExpr | MkSetMembership (Expr elem, ArrayExpr set) |
| Check for set membership. More... | |
| BoolExpr | MkSetSubset (ArrayExpr arg1, ArrayExpr arg2) |
| Check for subsetness of sets. More... | |
| SeqExpr | MkEmptySeq (Sort s) |
| Create the empty sequence. More... | |
| SeqExpr | MkUnit (Expr elem) |
| Create the singleton sequence. More... | |
| SeqExpr | MkString (string s) |
| Create a string constant. More... | |
| SeqExpr | IntToString (Expr e) |
| Convert an integer expression to a string. More... | |
| SeqExpr | UbvToString (Expr e) |
| Convert a bit-vector expression, represented as an unsigned number, to a string. More... | |
| SeqExpr | SbvToString (Expr e) |
| Convert a bit-vector expression, represented as an signed number, to a string. More... | |
| IntExpr | StringToInt (Expr e) |
| Convert an integer expression to a string. More... | |
| SeqExpr | MkConcat (params SeqExpr[] t) |
| Concatenate sequences. More... | |
| IntExpr | MkLength (SeqExpr s) |
| Retrieve the length of a given sequence. More... | |
| BoolExpr | MkPrefixOf (SeqExpr s1, SeqExpr s2) |
| Check for sequence prefix. More... | |
| BoolExpr | MkSuffixOf (SeqExpr s1, SeqExpr s2) |
| Check for sequence suffix. More... | |
| BoolExpr | MkContains (SeqExpr s1, SeqExpr s2) |
| Check for sequence containment of s2 in s1. More... | |
| BoolExpr | MkStringLt (SeqExpr s1, SeqExpr s2) |
| Check if the string s1 is lexicographically strictly less than s2. More... | |
| BoolExpr | MkStringLe (SeqExpr s1, SeqExpr s2) |
| Check if the string s1 is lexicographically less or equal to s2. More... | |
| SeqExpr | MkAt (SeqExpr s, Expr index) |
| Retrieve sequence of length one at index. More... | |
| Expr | MkNth (SeqExpr s, Expr index) |
| Retrieve element at index. More... | |
| SeqExpr | MkExtract (SeqExpr s, IntExpr offset, IntExpr length) |
| Extract subsequence. More... | |
| IntExpr | MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset) |
| Extract index of sub-string starting at offset. More... | |
| SeqExpr | MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst) |
| Replace the first occurrence of src by dst in s. More... | |
| ReExpr | MkToRe (SeqExpr s) |
| Convert a regular expression that accepts sequence s. More... | |
| BoolExpr | MkInRe (SeqExpr s, ReExpr re) |
| Check for regular expression membership. More... | |
| ReExpr | MkStar (ReExpr re) |
| Take the Kleene star of a regular expression. More... | |
| ReExpr | MkLoop (ReExpr re, uint lo, uint hi=0) |
| Take the bounded Kleene star of a regular expression. More... | |
| ReExpr | MkPlus (ReExpr re) |
| Take the Kleene plus of a regular expression. More... | |
| ReExpr | MkOption (ReExpr re) |
| Create the optional regular expression. More... | |
| ReExpr | MkComplement (ReExpr re) |
| Create the complement regular expression. More... | |
| ReExpr | MkConcat (params ReExpr[] t) |
| Create the concatenation of regular languages. More... | |
| ReExpr | MkUnion (params ReExpr[] t) |
| Create the union of regular languages. More... | |
| ReExpr | MkIntersect (params ReExpr[] t) |
| Create the intersection of regular languages. More... | |
| ReExpr | MkDiff (ReExpr a, ReExpr b) |
| Create a difference regular expression. More... | |
| ReExpr | MkEmptyRe (Sort s) |
| Create the empty regular expression. The sort s should be a regular expression. More... | |
| ReExpr | MkFullRe (Sort s) |
| Create the full regular expression. The sort s should be a regular expression. More... | |
| ReExpr | MkRange (SeqExpr lo, SeqExpr hi) |
| Create a range expression. More... | |
| BoolExpr | MkCharLe (Expr ch1, Expr ch2) |
| Create less than or equal to between two characters. More... | |
| IntExpr | CharToInt (Expr ch) |
| Create an integer (code point) from character. More... | |
| BitVecExpr | CharToBV (Expr ch) |
| Create a bit-vector (code point) from character. More... | |
| Expr | CharFromBV (BitVecExpr bv) |
| Create a character from a bit-vector (code point). More... | |
| BoolExpr | MkIsDigit (Expr ch) |
| Create a check if the character is a digit. More... | |
| BoolExpr | MkAtMost (IEnumerable< BoolExpr > args, uint k) |
| Create an at-most-k constraint. More... | |
| BoolExpr | MkAtLeast (IEnumerable< BoolExpr > args, uint k) |
| Create an at-least-k constraint. More... | |
| BoolExpr | MkPBLe (int[] coeffs, BoolExpr[] args, int k) |
| Create a pseudo-Boolean less-or-equal constraint. More... | |
| BoolExpr | MkPBGe (int[] coeffs, BoolExpr[] args, int k) |
| Create a pseudo-Boolean greater-or-equal constraint. More... | |
| BoolExpr | MkPBEq (int[] coeffs, BoolExpr[] args, int k) |
| Create a pseudo-Boolean equal constraint. More... | |
| Expr | MkNumeral (string v, Sort ty) |
| Create a Term of a given sort. More... | |
| Expr | MkNumeral (int v, Sort ty) |
Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More... | |
| Expr | MkNumeral (uint v, Sort ty) |
Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More... | |
| Expr | MkNumeral (long v, Sort ty) |
Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More... | |
| Expr | MkNumeral (ulong v, Sort ty) |
Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More... | |
| RatNum | MkReal (int num, int den) |
| Create a real from a fraction. More... | |
| RatNum | MkReal (string v) |
| Create a real numeral. More... | |
| RatNum | MkReal (int v) |
| Create a real numeral. More... | |
| RatNum | MkReal (uint v) |
| Create a real numeral. More... | |
| RatNum | MkReal (long v) |
| Create a real numeral. More... | |
| RatNum | MkReal (ulong v) |
| Create a real numeral. More... | |
| IntNum | MkInt (string v) |
| Create an integer numeral. More... | |
| IntNum | MkInt (int v) |
| Create an integer numeral. More... | |
| IntNum | MkInt (uint v) |
| Create an integer numeral. More... | |
| IntNum | MkInt (long v) |
| Create an integer numeral. More... | |
| IntNum | MkInt (ulong v) |
| Create an integer numeral. More... | |
| BitVecNum | MkBV (string v, uint size) |
| Create a bit-vector numeral. More... | |
| BitVecNum | MkBV (int v, uint size) |
| Create a bit-vector numeral. More... | |
| BitVecNum | MkBV (uint v, uint size) |
| Create a bit-vector numeral. More... | |
| BitVecNum | MkBV (long v, uint size) |
| Create a bit-vector numeral. More... | |
| BitVecNum | MkBV (ulong v, uint size) |
| Create a bit-vector numeral. More... | |
| BitVecNum | MkBV (bool[] bits) |
| Create a bit-vector numeral. More... | |
| Quantifier | MkForall (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
| Create a universal Quantifier. More... | |
| Quantifier | MkForall (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
| Create a universal Quantifier. More... | |
| Quantifier | MkExists (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
| Create an existential Quantifier. More... | |
| Quantifier | MkExists (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
| Create an existential Quantifier. More... | |
| Quantifier | MkQuantifier (bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
| Create a Quantifier. More... | |
| Quantifier | MkQuantifier (bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) |
| Create a Quantifier. More... | |
| Lambda | MkLambda (Sort[] sorts, Symbol[] names, Expr body) |
| Create a lambda expression. More... | |
| Lambda | MkLambda (Expr[] boundConstants, Expr body) |
| Create a lambda expression. More... | |
| BoolExpr[] | ParseSMTLIB2String (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) |
| Parse the given string using the SMT-LIB2 parser. More... | |
| BoolExpr[] | ParseSMTLIB2File (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) |
| Parse the given file using the SMT-LIB2 parser. More... | |
| Goal | MkGoal (bool models=true, bool unsatCores=false, bool proofs=false) |
| Creates a new Goal. More... | |
| Params | MkParams () |
| Creates a new ParameterSet. More... | |
| string | TacticDescription (string name) |
| Returns a string containing a description of the tactic with the given name. More... | |
| Tactic | MkTactic (string name) |
| Creates a new Tactic. More... | |
| Tactic | AndThen (Tactic t1, Tactic t2, params Tactic[] ts) |
| Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . More... | |
| Tactic | Then (Tactic t1, Tactic t2, params Tactic[] ts) |
| Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . More... | |
| Tactic | OrElse (Tactic t1, Tactic t2) |
| Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal. More... | |
| Tactic | TryFor (Tactic t, uint ms) |
| Create a tactic that applies t to a goal for ms milliseconds. More... | |
| Tactic | When (Probe p, Tactic t) |
| Create a tactic that applies t to a given goal if the probe p evaluates to true. More... | |
| Tactic | Cond (Probe p, Tactic t1, Tactic t2) |
| Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise. More... | |
| Tactic | Repeat (Tactic t, uint max=uint.MaxValue) |
| Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached. More... | |
| Tactic | Skip () |
| Create a tactic that just returns the given goal. More... | |
| Tactic | Fail () |
| Create a tactic always fails. More... | |
| Tactic | FailIf (Probe p) |
| Create a tactic that fails if the probe p evaluates to false. More... | |
| Tactic | FailIfNotDecided () |
| Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’). More... | |
| Tactic | UsingParams (Tactic t, Params p) |
| Create a tactic that applies t using the given set of parameters p . More... | |
| Tactic | With (Tactic t, Params p) |
| Create a tactic that applies t using the given set of parameters p . More... | |
| Tactic | ParOr (params Tactic[] t) |
| Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). More... | |
| Tactic | ParAndThen (Tactic t1, Tactic t2) |
| Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel. More... | |
| void | Interrupt () |
| Interrupt the execution of a Z3 procedure. More... | |
| string | SimplifierDescription (string name) |
| Returns a string containing a description of the simplifier with the given name. More... | |
| Simplifier | MkSimplifier (string name) |
| Creates a new Tactic. More... | |
| Simplifier | AndThen (Simplifier t1, Simplifier t2, params Simplifier[] ts) |
| Create a simplifier that applies t1 and then t2 . More... | |
| Simplifier | Then (Simplifier t1, Simplifier t2, params Simplifier[] ts) |
| Create a simplifier that applies t1 and then then t2 . More... | |
| Simplifier | UsingParams (Simplifier t, Params p) |
| Create a tactic that applies t using the given set of parameters p . 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 (Solver s, Simplifier t) |
| Creates a solver that uses an incremental simplifier. More... | |
| Solver | MkSolver (Tactic t) |
| Creates a solver that is implemented using the given tactic. More... | |
| Fixedpoint | MkFixedpoint () |
| Create a Fixedpoint context. More... | |
| Optimize | MkOptimize () |
| Create an Optimization context. More... | |
| FPRMSort | MkFPRoundingModeSort () |
| Create the floating-point RoundingMode sort. More... | |
| FPRMExpr | MkFPRoundNearestTiesToEven () |
| Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
| FPRMNum | MkFPRNE () |
| Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
| FPRMNum | MkFPRoundNearestTiesToAway () |
| Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
| FPRMNum | MkFPRNA () |
| Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
| FPRMNum | MkFPRoundTowardPositive () |
| Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More... | |
| FPRMNum | MkFPRTP () |
| Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More... | |
| FPRMNum | MkFPRoundTowardNegative () |
| Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More... | |
| FPRMNum | MkFPRTN () |
| Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More... | |
| FPRMNum | MkFPRoundTowardZero () |
| Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More... | |
| FPRMNum | MkFPRTZ () |
| Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More... | |
| FPSort | MkFPSort (uint ebits, uint sbits) |
| Create a FloatingPoint sort. More... | |
| FPSort | MkFPSortHalf () |
| Create the half-precision (16-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSort16 () |
| Create the half-precision (16-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSortSingle () |
| Create the single-precision (32-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSort32 () |
| Create the single-precision (32-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSortDouble () |
| Create the double-precision (64-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSort64 () |
| Create the double-precision (64-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSortQuadruple () |
| Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
| FPSort | MkFPSort128 () |
| Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
| FPNum | MkFPNaN (FPSort s) |
| Create a NaN of sort s. More... | |
| FPNum | MkFPInf (FPSort s, bool negative) |
| Create a floating-point infinity of sort s. More... | |
| FPNum | MkFPZero (FPSort s, bool negative) |
| Create a floating-point zero of sort s. More... | |
| FPNum | MkFPNumeral (float v, FPSort s) |
| Create a numeral of FloatingPoint sort from a float. More... | |
| FPNum | MkFPNumeral (double v, FPSort s) |
| Create a numeral of FloatingPoint sort from a float. More... | |
| FPNum | MkFPNumeral (int v, FPSort s) |
| Create a numeral of FloatingPoint sort from an int. More... | |
| FPNum | MkFPNumeral (bool sgn, uint sig, int exp, FPSort s) |
| Create a numeral of FloatingPoint sort from a sign bit and two integers. More... | |
| FPNum | MkFPNumeral (bool sgn, Int64 exp, UInt64 sig, FPSort s) |
| Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More... | |
| FPNum | MkFP (float v, FPSort s) |
| Create a numeral of FloatingPoint sort from a float. More... | |
| FPNum | MkFP (double v, FPSort s) |
| Create a numeral of FloatingPoint sort from a float. More... | |
| FPNum | MkFP (int v, FPSort s) |
| Create a numeral of FloatingPoint sort from an int. More... | |
| FPNum | MkFP (bool sgn, int exp, uint sig, FPSort s) |
| Create a numeral of FloatingPoint sort from a sign bit and two integers. More... | |
| FPNum | MkFP (bool sgn, Int64 exp, UInt64 sig, FPSort s) |
| Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More... | |
| FPExpr | MkFPAbs (FPExpr t) |
| Floating-point absolute value More... | |
| FPExpr | MkFPNeg (FPExpr t) |
| Floating-point negation More... | |
| FPExpr | MkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2) |
| Floating-point addition More... | |
| FPExpr | MkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2) |
| Floating-point subtraction More... | |
| FPExpr | MkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2) |
| Floating-point multiplication More... | |
| FPExpr | MkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2) |
| Floating-point division More... | |
| FPExpr | MkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) |
| Floating-point fused multiply-add More... | |
| FPExpr | MkFPSqrt (FPRMExpr rm, FPExpr t) |
| Floating-point square root More... | |
| FPExpr | MkFPRem (FPExpr t1, FPExpr t2) |
| Floating-point remainder More... | |
| FPExpr | MkFPRoundToIntegral (FPRMExpr rm, FPExpr t) |
| Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number. More... | |
| FPExpr | MkFPMin (FPExpr t1, FPExpr t2) |
| Minimum of floating-point numbers. More... | |
| FPExpr | MkFPMax (FPExpr t1, FPExpr t2) |
| Maximum of floating-point numbers. More... | |
| BoolExpr | MkFPLEq (FPExpr t1, FPExpr t2) |
| Floating-point less than or equal. More... | |
| BoolExpr | MkFPLt (FPExpr t1, FPExpr t2) |
| Floating-point less than. More... | |
| BoolExpr | MkFPGEq (FPExpr t1, FPExpr t2) |
| Floating-point greater than or equal. More... | |
| BoolExpr | MkFPGt (FPExpr t1, FPExpr t2) |
| Floating-point greater than. More... | |
| BoolExpr | MkFPEq (FPExpr t1, FPExpr t2) |
| Floating-point equality. More... | |
| BoolExpr | MkFPIsNormal (FPExpr t) |
| Predicate indicating whether t is a normal floating-point number. More... | |
| BoolExpr | MkFPIsSubnormal (FPExpr t) |
| Predicate indicating whether t is a subnormal floating-point number. More... | |
| BoolExpr | MkFPIsZero (FPExpr t) |
| Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0. More... | |
| BoolExpr | MkFPIsInfinite (FPExpr t) |
| Predicate indicating whether t is a floating-point number representing +oo or -oo. More... | |
| BoolExpr | MkFPIsNaN (FPExpr t) |
| Predicate indicating whether t is a NaN. More... | |
| BoolExpr | MkFPIsNegative (FPExpr t) |
| Predicate indicating whether t is a negative floating-point number. More... | |
| BoolExpr | MkFPIsPositive (FPExpr t) |
| Predicate indicating whether t is a positive floating-point number. More... | |
| FPExpr | MkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) |
| Create an expression of FloatingPoint sort from three bit-vector expressions. More... | |
| FPExpr | MkFPToFP (BitVecExpr bv, FPSort s) |
| Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. More... | |
| FPExpr | MkFPToFP (FPRMExpr rm, FPExpr t, FPSort s) |
| Conversion of a FloatingPoint term into another term of different FloatingPoint sort. More... | |
| FPExpr | MkFPToFP (FPRMExpr rm, RealExpr t, FPSort s) |
| Conversion of a term of real sort into a term of FloatingPoint sort. More... | |
| FPExpr | MkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, bool signed) |
| Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. More... | |
| FPExpr | MkFPToFP (FPSort s, FPRMExpr rm, FPExpr t) |
| Conversion of a floating-point number to another FloatingPoint sort s. More... | |
| BitVecExpr | MkFPToBV (FPRMExpr rm, FPExpr t, uint sz, bool sign) |
| Conversion of a floating-point term into a bit-vector. More... | |
| RealExpr | MkFPToReal (FPExpr t) |
| Conversion of a floating-point term into a real-numbered term. More... | |
| BitVecExpr | MkFPToIEEEBV (FPExpr t) |
| Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. More... | |
| BitVecExpr | MkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) |
| Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. More... | |
| AST | WrapAST (IntPtr nativeObject) |
| Wraps an AST. More... | |
| IntPtr | UnwrapAST (AST a) |
| Unwraps an AST. More... | |
| string | SimplifyHelp () |
Return a string describing all available parameters to Expr.Simplify. More... | |
| void | UpdateParamValue (string id, string value) |
| Update a mutable configuration parameter. More... | |
| void | Dispose () |
| Disposes of the context. More... | |
Properties | |
| BoolSort | BoolSort [get] |
| Retrieves the Boolean sort of the context. More... | |
| IntSort | IntSort [get] |
| Retrieves the Integer sort of the context. More... | |
| RealSort | RealSort [get] |
| Retrieves the Real sort of the context. More... | |
| CharSort | CharSort [get] |
| Retrieves the String sort of the context. More... | |
| SeqSort | StringSort [get] |
| Retrieves the String sort of the context. More... | |
| Z3_ast_print_mode | PrintMode [set] |
| Selects the format used for pretty-printing expressions. More... | |
| uint | NumTactics [get] |
| The number of supported tactics. More... | |
| string[] | TacticNames [get] |
| The names of all supported tactics. More... | |
| uint | NumSimplifiers [get] |
| The number of supported simplifiers. More... | |
| string[] | SimplifierNames [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... | |
The main interaction with Z3 happens via the Context.
Definition at line 33 of file Context.cs.
|
inline |
Definition at line 39 of file Context.cs.
|
inline |
The following parameters can be set:
Definition at line 68 of file Context.cs.
Bind a definition to a recursive function declaration. The function must have previously been created using MkRecFuncDecl. The body may contain recursive uses of the function or other mutually recursive functions.
Definition at line 617 of file Context.cs.
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
Definition at line 3959 of file Context.cs.
|
inline |
Create a simplifier that applies t1 and then t2 .
Definition at line 3776 of file Context.cs.
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Definition at line 3514 of file Context.cs.
Referenced by Context.Then().
|
inline |
Create a character from a bit-vector (code point).
Definition at line 2821 of file Context.cs.
|
inline |
Create a bit-vector (code point) from character.
Definition at line 2812 of file Context.cs.
Create an integer (code point) from character.
Definition at line 2803 of file Context.cs.
Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.
Definition at line 3606 of file Context.cs.
|
inline |
Create a probe that always evaluates to val .
Definition at line 3879 of file Context.cs.
|
inline |
Disposes of the context.
Definition at line 4987 of file Context.cs.
Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2
Definition at line 3945 of file Context.cs.
|
inline |
Create a tactic always fails.
Definition at line 3642 of file Context.cs.
Create a tactic that fails if the probe p evaluates to false.
Definition at line 3651 of file Context.cs.
|
inline |
Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’).
Definition at line 3663 of file Context.cs.
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 3931 of file Context.cs.
Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2
Definition at line 3903 of file Context.cs.
|
inline |
Interrupt the execution of a Z3 procedure.
This procedure can be used to interrupt: solvers, simplifiers and tactics.
Definition at line 3723 of file Context.cs.
Convert an integer expression to a string.
Definition at line 2472 of file Context.cs.
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 3917 of file Context.cs.
Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2
Definition at line 3889 of file Context.cs.
Create an expression representing t[0] + t[1] + ....
Definition at line 1104 of file Context.cs.
Create an expression representing t[0] + t[1] + ....
Definition at line 1092 of file Context.cs.
Referenced by ArithExpr.operator+().
Create an expression representing t[0] and t[1] and ....
Definition at line 1051 of file Context.cs.
Create an expression representing t[0] and t[1] and ....
Definition at line 1039 of file Context.cs.
Referenced by Goal.AsBoolExpr(), and BoolExpr.operator&().
Create a new function application.
Definition at line 879 of file Context.cs.
Create a new function application.
Definition at line 866 of file Context.cs.
Referenced by EnumSort.Const(), and Context.MkConst().
Create an array constant.
Definition at line 2115 of file Context.cs.
Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
Definition at line 2291 of file Context.cs.
Create a new array sort.
Definition at line 276 of file Context.cs.
Referenced by Context.MkArrayConst().
Retrieve sequence of length one at index.
Definition at line 2590 of file Context.cs.
Create an at-least-k constraint.
Definition at line 2855 of file Context.cs.
Create an at-most-k constraint.
Definition at line 2843 of file Context.cs.
|
inline |
Create a new bit-vector sort.
Definition at line 250 of file Context.cs.
Referenced by Context.MkBV(), and Context.MkBVConst().
|
inline |
|
inline |
Create a Boolean constant.
Definition at line 796 of file Context.cs.
Create a Boolean constant.
Definition at line 786 of file Context.cs.
|
inline |
Create a new Boolean sort.
Definition at line 205 of file Context.cs.
Creates a new bound variable.
| index | The de-Bruijn index of the variable |
| ty | The sort of the variable |
Definition at line 711 of file Context.cs.
|
inline |
Create a bit-vector numeral.
| bits | An array of bits representing the bit-vector. Least significant bit is at position 0. |
Definition at line 3172 of file Context.cs.
|
inline |
Create a bit-vector numeral.
| v | value of the numeral. |
| size | the size of the bit-vector |
Definition at line 3129 of file Context.cs.
|
inline |
Create a bit-vector numeral.
| v | value of the numeral. |
| size | the size of the bit-vector |
Definition at line 3151 of file Context.cs.
|
inline |
Create a bit-vector numeral.
| v | A string representing the value in decimal notation. |
| size | the size of the bit-vector |
Definition at line 3118 of file Context.cs.
|
inline |
Create a bit-vector numeral.
| v | value of the numeral. |
| size | the size of the bit-vector |
Definition at line 3140 of file Context.cs.
|
inline |
Create a bit-vector numeral.
| v | value of the numeral. |
| size | the size of the bit-vector |
Definition at line 3162 of file Context.cs.
|
inline |
Create an integer from the bit-vector argument t .
If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t . If is_signed is true, t1 is treated as a signed bit-vector.
NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of bit-vector sort.
Definition at line 1963 of file Context.cs.
|
inline |
Two's complement addition.
The arguments must have the same bit-vector sort.
Definition at line 1451 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise addition does not overflow.
The arguments must be of bit-vector sort.
Definition at line 1977 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise addition does not underflow.
The arguments must be of bit-vector sort.
Definition at line 1993 of file Context.cs.
|
inline |
Bitwise conjunction.
The arguments must have a bit-vector sort.
Definition at line 1355 of file Context.cs.
|
inline |
Arithmetic shift right
It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1856 of file Context.cs.
|
inline |
Creates a bit-vector constant.
Definition at line 855 of file Context.cs.
|
inline |
|
inline |
Logical shift right
It is equivalent to unsigned division by 2^x where x is the value of t2 .
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1832 of file Context.cs.
|
inline |
Two's complement multiplication.
The arguments must have the same bit-vector sort.
Definition at line 1479 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise multiplication does not overflow.
The arguments must be of bit-vector sort.
Definition at line 2071 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise multiplication does not underflow.
The arguments must be of bit-vector sort.
Definition at line 2087 of file Context.cs.
|
inline |
Bitwise NAND.
The arguments must have a bit-vector sort.
Definition at line 1397 of file Context.cs.
|
inline |
Standard two's complement unary minus.
The arguments must have a bit-vector sort.
Definition at line 1439 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise negation does not overflow.
The arguments must be of bit-vector sort.
Definition at line 2057 of file Context.cs.
|
inline |
|
inline |
Bitwise negation.
The argument must have a bit-vector sort.
Definition at line 1319 of file Context.cs.
|
inline |
Bitwise disjunction.
The arguments must have a bit-vector sort.
Definition at line 1369 of file Context.cs.
|
inline |
Take conjunction of bits in a vector, return vector of length 1.
The argument must have a bit-vector sort.
Definition at line 1331 of file Context.cs.
|
inline |
Take disjunction of bits in a vector, return vector of length 1.
The argument must have a bit-vector sort.
Definition at line 1343 of file Context.cs.
|
inline |
Rotate Left.
Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.
Definition at line 1903 of file Context.cs.
|
inline |
Rotate Left.
Rotate bits of t to the left i times. The argument t must have a bit-vector sort.
Definition at line 1873 of file Context.cs.
|
inline |
Rotate Right.
Rotate bits of t1 to the rightt2 times. The arguments must have the same bit-vector sort.
Definition at line 1920 of file Context.cs.
|
inline |
Rotate Right.
Rotate bits of t to the right i times. The argument t must have a bit-vector sort.
Definition at line 1888 of file Context.cs.
|
inline |
Signed division.
It is defined in the following way:
floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0.If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1521 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise signed division does not overflow.
The arguments must be of bit-vector sort.
Definition at line 2041 of file Context.cs.
|
inline |
Two's complement signed greater than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1672 of file Context.cs.
|
inline |
Two's complement signed greater-than.
The arguments must have the same bit-vector sort.
Definition at line 1704 of file Context.cs.
|
inline |
Shift left.
It is equivalent to multiplication by 2^x where x is the value of t2 .
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1810 of file Context.cs.
|
inline |
Two's complement signed less-than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1640 of file Context.cs.
|
inline |
Two's complement signed less-than
The arguments must have the same bit-vector sort.
Definition at line 1608 of file Context.cs.
|
inline |
Two's complement signed remainder (sign follows divisor).
If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1576 of file Context.cs.
|
inline |
Signed remainder.
It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.
If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1559 of file Context.cs.
|
inline |
Two's complement subtraction.
The arguments must have the same bit-vector sort.
Definition at line 1465 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise subtraction does not overflow.
The arguments must be of bit-vector sort.
Definition at line 2009 of file Context.cs.
|
inline |
Create a predicate that checks that the bit-wise subtraction does not underflow.
The arguments must be of bit-vector sort.
Definition at line 2025 of file Context.cs.
|
inline |
Unsigned division.
It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1498 of file Context.cs.
|
inline |
Unsigned greater than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1656 of file Context.cs.
|
inline |
Unsigned greater-than.
The arguments must have the same bit-vector sort.
Definition at line 1688 of file Context.cs.
|
inline |
Unsigned less-than or equal to.
The arguments must have the same bit-vector sort.
Definition at line 1624 of file Context.cs.
|
inline |
Unsigned less-than
The arguments must have the same bit-vector sort.
Definition at line 1592 of file Context.cs.
|
inline |
Unsigned remainder.
It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1539 of file Context.cs.
|
inline |
Bitwise XNOR.
The arguments must have a bit-vector sort.
Definition at line 1425 of file Context.cs.
|
inline |
Create less than or equal to between two characters.
Definition at line 2793 of file Context.cs.
Create the complement regular expression.
Definition at line 2705 of file Context.cs.
|
inline |
Bit-vector concatenation.
The arguments must have a bit-vector sort.
n1+n2, where n1 (n2) is the size of t1 (t2). Definition at line 1724 of file Context.cs.
Create the concatenation of regular languages.
Definition at line 2714 of file Context.cs.
Concatenate sequences.
Definition at line 2513 of file Context.cs.
Creates a fresh constant from the FuncDecl f .
| f | A decl of a 0-arity function |
Definition at line 776 of file Context.cs.
Creates a new Constant of sort range and named name .
Definition at line 738 of file Context.cs.
Referenced by Context.MkArrayConst(), Context.MkBoolConst(), Context.MkBVConst(), Context.MkConst(), Context.MkIntConst(), and Context.MkRealConst().
Create a constant array.
The resulting term is an array, such that a selecton an arbitrary index produces the value v.
Definition at line 2242 of file Context.cs.
Creates a new constant function declaration.
Definition at line 659 of file Context.cs.
|
inline |
Create a datatype constructor.
| name | |
| recognizer | |
| fieldNames | |
| sorts | |
| sortRefs |
Definition at line 432 of file Context.cs.
|
inline |
Create a datatype constructor.
| name | constructor name |
| recognizer | name of recognizer function. |
| fieldNames | names of the constructor fields. |
| sorts | field sorts, 0 if the field sort refers to a recursive sort. |
| sortRefs | reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. |
Definition at line 415 of file Context.cs.
Check for sequence containment of s2 in s1.
Definition at line 2557 of file Context.cs.
|
inline |
|
inline |
|
inline |
Create mutually recursive data-types.
| names | |
| c |
Definition at line 515 of file Context.cs.
|
inline |
Create mutually recursive datatypes.
| names | names of datatype sorts |
| c | list of constructors, one list per sort. |
Definition at line 482 of file Context.cs.
Referenced by Context.MkDatatypeSorts().
Create a difference regular expression.
Definition at line 2750 of file Context.cs.
Creates a distinct term.
Definition at line 946 of file Context.cs.
Creates a distinct term.
Definition at line 933 of file Context.cs.
Referenced by Context.MkDistinct().
Create an expression representing t1 / t2.
Definition at line 1166 of file Context.cs.
Referenced by ArithExpr.operator/().
Create the empty regular expression. The sort s should be a regular expression.
Definition at line 2762 of file Context.cs.
Create the empty sequence.
Definition at line 2445 of file Context.cs.
Create an empty set.
Definition at line 2318 of file Context.cs.
|
inline |
Creates the equality x = y .
Definition at line 920 of file Context.cs.
|
inline |
Create an existential Quantifier.
Creates an existential quantifier using a list of constants that will form the set of bound variables.
Definition at line 3273 of file Context.cs.
|
inline |
Create an existential Quantifier.
Creates an existential quantifier using de-Bruijn indexed variables. (MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)).
Definition at line 3251 of file Context.cs.
Referenced by Context.MkQuantifier().
Extract subsequence.
Definition at line 2612 of file Context.cs.
|
inline |
Bit-vector extraction.
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. The argument t must have a bit-vector sort.
Definition at line 1743 of file Context.cs.
|
inline |
The false Term.
Definition at line 902 of file Context.cs.
Referenced by Context.MkBool(), and Context.MkXor().
|
inline |
Create a new finite domain sort.
Elements of the sort are created using
, and the elements range from 0 to size-1.
| name | The name used to identify the sort |
| size | The size of the sort |
Definition at line 397 of file Context.cs.
|
inline |
Create a new finite domain sort.
| name | The name used to identify the sort |
| size | The size of the sort |
Definition at line 381 of file Context.cs.
|
inline |
Create a Fixedpoint context.
Definition at line 4064 of file Context.cs.
|
inline |
Create a universal Quantifier.
Creates a universal quantifier using a list of constants that will form the set of bound variables.
Definition at line 3233 of file Context.cs.
|
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.
| sorts | the sorts of the bound variables. |
| names | names of the bound variables |
| body | the body of the quantifier. |
| weight | quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. |
| patterns | array containing the patterns created using MkPattern. |
| noPatterns | array containing the anti-patterns created using MkPattern. |
| quantifierID | optional symbol to track quantifier. |
| skolemID | optional symbol to track skolem constants. |
Definition at line 3209 of file Context.cs.
Referenced by Context.MkQuantifier().
|
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.
| sgn | bit-vector term (of size 1) representing the sign. |
| sig | bit-vector term representing the significand. |
| exp | bit-vector term representing the exponent. |
Definition at line 4654 of file Context.cs.
Create a numeral of FloatingPoint sort from a sign bit and two integers.
| sgn | the sign. |
| exp | the exponent. |
| sig | the significand. |
| s | FloatingPoint sort. |
Definition at line 4375 of file Context.cs.
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
| sgn | the sign. |
| exp | the exponent. |
| sig | the significand. |
| s | FloatingPoint sort. |
Definition at line 4387 of file Context.cs.
Create a numeral of FloatingPoint sort from a float.
| v | numeral value. |
| s | FloatingPoint sort. |
Definition at line 4353 of file Context.cs.
Create a numeral of FloatingPoint sort from a float.
| v | numeral value. |
| s | FloatingPoint sort. |
Definition at line 4343 of file Context.cs.
Create a numeral of FloatingPoint sort from an int.
| v | numeral value. |
| s | FloatingPoint sort. |
Definition at line 4363 of file Context.cs.
Floating-point absolute value
| t | floating-point term |
Definition at line 4399 of file Context.cs.
Floating-point addition
| rm | rounding mode term |
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4419 of file Context.cs.
Floating-point division
| rm | rounding mode term |
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4452 of file Context.cs.
Floating-point equality.
Note that this is IEEE 754 equality (as opposed to standard =).
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4571 of file Context.cs.
Floating-point fused multiply-add
The result is round((t1 * t2) + t3)
| rm | rounding mode term |
| t1 | floating-point term |
| t2 | floating-point term |
| t3 | floating-point term |
Definition at line 4467 of file Context.cs.
Floating-point greater than or equal.
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4548 of file Context.cs.
Floating-point greater than.
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4558 of file Context.cs.
Create a floating-point infinity of sort s.
| s | FloatingPoint sort. |
| negative | indicates whether the result should be negative. |
Definition at line 4269 of file Context.cs.
Predicate indicating whether t is a floating-point number representing +oo or -oo.
| t | floating-point term |
Definition at line 4607 of file Context.cs.
Predicate indicating whether t is a NaN.
| t | floating-point term |
Definition at line 4616 of file Context.cs.
Predicate indicating whether t is a negative floating-point number.
| t | floating-point term |
Definition at line 4625 of file Context.cs.
Predicate indicating whether t is a normal floating-point number.
| t | floating-point term |
Definition at line 4580 of file Context.cs.
Predicate indicating whether t is a positive floating-point number.
| t | floating-point term |
Definition at line 4634 of file Context.cs.
Predicate indicating whether t is a subnormal floating-point number.
| t | floating-point term |
Definition at line 4589 of file Context.cs.
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
| t | floating-point term |
Definition at line 4598 of file Context.cs.
Floating-point less than or equal.
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4528 of file Context.cs.
Floating-point less than.
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4538 of file Context.cs.
Maximum of floating-point numbers.
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4518 of file Context.cs.
Minimum of floating-point numbers.
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4508 of file Context.cs.
Floating-point multiplication
| rm | rounding mode term |
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4441 of file Context.cs.
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
| sgn | the sign. |
| sig | the significand. |
| exp | the exponent. |
| s | FloatingPoint sort. |
Definition at line 4333 of file Context.cs.
Create a numeral of FloatingPoint sort from a sign bit and two integers.
| sgn | the sign. |
| sig | the significand. |
| exp | the exponent. |
| s | FloatingPoint sort. |
Definition at line 4321 of file Context.cs.
Create a numeral of FloatingPoint sort from a float.
| v | numeral value. |
| s | FloatingPoint sort. |
Definition at line 4299 of file Context.cs.
Create a numeral of FloatingPoint sort from a float.
| v | numeral value. |
| s | FloatingPoint sort. |
Definition at line 4289 of file Context.cs.
Referenced by Context.MkFP().
Create a numeral of FloatingPoint sort from an int.
| v | numeral value. |
| s | FloatingPoint sort. |
Definition at line 4309 of file Context.cs.
Floating-point remainder
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4487 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition at line 4123 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition at line 4107 of file Context.cs.
|
inline |
Create the floating-point RoundingMode sort.
Definition at line 4089 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Definition at line 4115 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Definition at line 4099 of file Context.cs.
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
| rm | term of RoundingMode sort |
| t | floating-point term |
Definition at line 4498 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition at line 4147 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition at line 4131 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition at line 4163 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Definition at line 4155 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Definition at line 4139 of file Context.cs.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Definition at line 4171 of file Context.cs.
|
inline |
Create a FloatingPoint sort.
| ebits | exponent bits in the FloatingPoint sort. |
| sbits | significand bits in the FloatingPoint sort. |
Definition at line 4184 of file Context.cs.
|
inline |
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition at line 4248 of file Context.cs.
|
inline |
Create the half-precision (16-bit) FloatingPoint sort.
Definition at line 4200 of file Context.cs.
|
inline |
Create the single-precision (32-bit) FloatingPoint sort.
Definition at line 4216 of file Context.cs.
|
inline |
Create the double-precision (64-bit) FloatingPoint sort.
Definition at line 4232 of file Context.cs.
|
inline |
Create the double-precision (64-bit) FloatingPoint sort.
Definition at line 4224 of file Context.cs.
|
inline |
Create the half-precision (16-bit) FloatingPoint sort.
Definition at line 4192 of file Context.cs.
|
inline |
Create the quadruple-precision (128-bit) FloatingPoint sort.
Definition at line 4240 of file Context.cs.
|
inline |
Create the single-precision (32-bit) FloatingPoint sort.
Definition at line 4208 of file Context.cs.
Floating-point square root
| rm | rounding mode term |
| t | floating-point term |
Definition at line 4477 of file Context.cs.
Floating-point subtraction
| rm | rounding mode term |
| t1 | floating-point term |
| t2 | floating-point term |
Definition at line 4430 of file Context.cs.
|
inline |
Conversion of a floating-point term into a bit-vector.
Produces a term that represents the conversion of the floating-point term t into a bit-vector term of size sz in 2's complement format (signed when sign==true). If necessary, the result will be rounded according to rounding mode rm.
| rm | RoundingMode term. |
| t | FloatingPoint term |
| sz | Size of the resulting bit-vector. |
| sign | Indicates whether the result is a signed or unsigned bit-vector. |
Definition at line 4757 of file Context.cs.
|
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.
| bv | bit-vector value (of size m). |
| s | FloatingPoint sort (ebits+sbits == m) |
Definition at line 4670 of file Context.cs.
|
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.
| rm | RoundingMode term. |
| t | term of bit-vector sort. |
| s | FloatingPoint sort. |
| signed | flag indicating whether t is interpreted as signed or unsigned bit-vector. |
Definition at line 4720 of file Context.cs.
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.
| rm | RoundingMode term. |
| t | FloatingPoint term. |
| s | FloatingPoint sort. |
Definition at line 4686 of file Context.cs.
|
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.
| rm | RoundingMode term. |
| exp | Exponent term of Int sort. |
| sig | Significand term of Real sort. |
| s | FloatingPoint sort. |
Definition at line 4808 of file Context.cs.
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.
| rm | RoundingMode term. |
| t | term of Real sort. |
| s | FloatingPoint sort. |
Definition at line 4702 of file Context.cs.
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.
| s | FloatingPoint sort |
| rm | floating-point rounding mode term |
| t | floating-point term |
Definition at line 4738 of file Context.cs.
|
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.
| t | FloatingPoint term. |
Definition at line 4791 of file Context.cs.
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.
| t | FloatingPoint term |
Definition at line 4774 of file Context.cs.
Create a floating-point zero of sort s.
| s | FloatingPoint sort. |
| negative | indicates whether the result should be negative. |
Definition at line 4279 of file Context.cs.
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition at line 764 of file Context.cs.
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition at line 686 of file Context.cs.
Creates a fresh function declaration with a name prefixed with prefix .
Definition at line 646 of file Context.cs.
Create the full regular expression. The sort s should be a regular expression.
Definition at line 2772 of file Context.cs.
Create the full set.
Definition at line 2329 of file Context.cs.
Creates a new function declaration.
Definition at line 629 of file Context.cs.
Creates a new function declaration.
Definition at line 586 of file Context.cs.
Creates a new function declaration.
Definition at line 570 of file Context.cs.
Creates a new function declaration.
Definition at line 555 of file Context.cs.
Create an expression representing t1 >= t2
Definition at line 1259 of file Context.cs.
Referenced by ArithExpr.operator>=().
|
inline |
Creates a new Goal.
Note that the Context must have been created with proof generation support if proofs is set to true here.
| models | Indicates whether model generation should be enabled. |
| unsatCores | Indicates whether unsat core generation should be enabled. |
| proofs | Indicates whether proof generation should be enabled. |
Definition at line 3449 of file Context.cs.
Create an expression representing t1 > t2
Definition at line 1246 of file Context.cs.
Referenced by ArithExpr.operator>().
Create an expression representing t1 iff t2.
Definition at line 984 of file Context.cs.
Create an expression representing t1 -> t2.
Definition at line 997 of file Context.cs.
Extract index of sub-string starting at offset.
Definition at line 2624 of file Context.cs.
Check for regular expression membership.
Definition at line 2658 of file Context.cs.
|
inline |
Create an integer numeral.
| v | value of the numeral. |
Definition at line 3072 of file Context.cs.
|
inline |
Create an integer numeral.
| v | value of the numeral. |
Definition at line 3094 of file Context.cs.
|
inline |
Create an integer numeral.
| v | A string representing the Term value in decimal notation. |
Definition at line 3061 of file Context.cs.
|
inline |
Create an integer numeral.
| v | value of the numeral. |
Definition at line 3083 of file Context.cs.
|
inline |
Create an integer numeral.
| v | value of the numeral. |
Definition at line 3105 of file Context.cs.
|
inline |
Create an n bit bit-vector from the integer argument t .
NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of integer sort.
Definition at line 1940 of file Context.cs.
Coerce an integer to a real.
There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
You can take the floor of a real by creating an auxiliary integer Term k and and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. The argument must be of integer sort.
Definition at line 1279 of file Context.cs.
|
inline |
Creates an integer constant.
Definition at line 815 of file Context.cs.
Creates an integer constant.
Definition at line 805 of file Context.cs.
Create the intersection of regular languages.
Definition at line 2738 of file Context.cs.
|
inline |
Create a new integer sort.
Definition at line 233 of file Context.cs.
Create a check if the character is a digit.
Definition at line 2830 of file Context.cs.
Creates an expression that checks whether a real number is an integer.
Definition at line 1305 of file Context.cs.
Create an expression representing an if-then-else: ite(t1, t2, t3).
| t1 | An expression with Boolean sort |
| t2 | An expression |
| t3 | An expression with the same sort as t2 |
Definition at line 969 of file Context.cs.
Create a lambda expression.
Creates a lambda expression using a list of constants that will form the set of bound variables.
Definition at line 3362 of file Context.cs.
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.
| sorts | the sorts of the bound variables. |
| names | names of the bound variables |
| body | the body of the quantifier. |
Definition at line 3343 of file Context.cs.
Create an expression representing t1 <= t2
Definition at line 1233 of file Context.cs.
Referenced by ArithExpr.operator<=().
Retrieve the length of a given sequence.
Definition at line 2526 of file Context.cs.
Create a new list sort.
Definition at line 353 of file Context.cs.
Take the bounded Kleene star of a regular expression.
Definition at line 2678 of file Context.cs.
Create an expression representing t1 < t2
Definition at line 1220 of file Context.cs.
Referenced by ArithExpr.operator<().
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].
Definition at line 2263 of file Context.cs.
Create an expression representing t1 mod t2.
The arguments must have int type.
Definition at line 1180 of file Context.cs.
Create an expression representing t[0] * t[1] * ....
Definition at line 1130 of file Context.cs.
Create an expression representing t[0] * t[1] * ....
Definition at line 1117 of file Context.cs.
Referenced by ArithExpr.operator*().
Mk an expression representing not(a).
Definition at line 955 of file Context.cs.
Referenced by BoolExpr.operator!().
Retrieve element at index.
Definition at line 2601 of file Context.cs.
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.
| v | Value of the numeral |
| ty | Sort of the numeral |
Definition at line 2930 of file Context.cs.
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.
| v | Value of the numeral |
| ty | Sort of the numeral |
Definition at line 2960 of file Context.cs.
Create a Term of a given sort.
| v | A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*. |
| ty | The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. |
Definition at line 2915 of file Context.cs.
Referenced by Context.MkBV().
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.
| v | Value of the numeral |
| ty | Sort of the numeral |
Definition at line 2945 of file Context.cs.
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.
| v | Value of the numeral |
| ty | Sort of the numeral |
Definition at line 2975 of file Context.cs.
|
inline |
Create an Optimization context.
Definition at line 4075 of file Context.cs.
Create the optional regular expression.
Definition at line 2696 of file Context.cs.
Create an expression representing t[0] or t[1] or ....
Definition at line 1076 of file Context.cs.
Create an expression representing t[0] or t[1] or ....
Definition at line 1063 of file Context.cs.
Referenced by BoolExpr.operator|().
|
inline |
Creates a new ParameterSet.
Definition at line 3460 of file Context.cs.
Referenced by Optimize.Set(), and Solver.Set().
Create a quantifier pattern.
Definition at line 723 of file Context.cs.
Create a pseudo-Boolean equal constraint.
Definition at line 2894 of file Context.cs.
Create a pseudo-Boolean greater-or-equal constraint.
Definition at line 2881 of file Context.cs.
Create a pseudo-Boolean less-or-equal constraint.
Definition at line 2867 of file Context.cs.
Take the Kleene plus of a regular expression.
Definition at line 2687 of file Context.cs.
Create an expression representing t1 ^ t2.
Definition at line 1207 of file Context.cs.
Check for sequence prefix.
Definition at line 2535 of file Context.cs.
|
inline |
Creates a new Probe.
Definition at line 3870 of file Context.cs.
|
inline |
Create a Quantifier.
MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)
Definition at line 3311 of file Context.cs.
|
inline |
Create a Quantifier.
MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)
Definition at line 3288 of file Context.cs.
Create a range expression.
Definition at line 2782 of file Context.cs.
|
inline |
Create a real from a fraction.
| num | numerator of rational. |
| den | denominator of rational. |
Definition at line 2992 of file Context.cs.
|
inline |
Create a real numeral.
| v | value of the numeral. |
Definition at line 3016 of file Context.cs.
|
inline |
Create a real numeral.
| v | value of the numeral. |
Definition at line 3038 of file Context.cs.
|
inline |
Create a real numeral.
| v | A string representing the Term value in decimal notation. |
Definition at line 3005 of file Context.cs.
|
inline |
Create a real numeral.
| v | value of the numeral. |
Definition at line 3027 of file Context.cs.
|
inline |
Create a real numeral.
| v | value of the numeral. |
Definition at line 3049 of file Context.cs.
Coerce a real to an integer.
The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.
Definition at line 1294 of file Context.cs.
|
inline |
Creates a real constant.
Definition at line 835 of file Context.cs.
Creates a real constant.
Definition at line 825 of file Context.cs.
|
inline |
Create a real sort.
Definition at line 242 of file Context.cs.
Creates a new recursive function declaration.
Definition at line 600 of file Context.cs.
Create an expression representing t1 rem t2.
The arguments must have int type.
Definition at line 1194 of file Context.cs.
|
inline |
Bit-vector repetition.
The argument t must have a bit-vector sort.
Definition at line 1790 of file Context.cs.
Replace the first occurrence of src by dst in s.
Definition at line 2636 of file Context.cs.
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.
Definition at line 2139 of file Context.cs.
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.
Definition at line 2162 of file Context.cs.
Add an element to the set.
Definition at line 2340 of file Context.cs.
Take the complement of a set.
Definition at line 2404 of file Context.cs.
Remove an element from a set.
Definition at line 2354 of file Context.cs.
Take the difference between two sets.
Definition at line 2391 of file Context.cs.
Take the intersection of a list of sets.
Definition at line 2379 of file Context.cs.
Check for set membership.
Definition at line 2415 of file Context.cs.
Check for subsetness of sets.
Definition at line 2428 of file Context.cs.
Take the union of a list of sets.
Definition at line 2367 of file Context.cs.
|
inline |
Bit-vector sign extension.
Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.
Definition at line 1759 of file Context.cs.
|
inline |
Creates a new (incremental) solver.
Definition at line 4027 of file Context.cs.
|
inline |
Creates a new Tactic.
Definition at line 3766 of file Context.cs.
|
inline |
Creates a solver that uses an incremental simplifier.
Definition at line 4036 of file Context.cs.
|
inline |
Creates a new (incremental) solver.
Definition at line 4018 of file Context.cs.
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 4005 of file Context.cs.
Referenced by Context.MkSolver().
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 4050 of file Context.cs.
Take the Kleene star of a regular expression.
Definition at line 2669 of file Context.cs.
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).
Definition at line 2191 of file Context.cs.
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).
Definition at line 2221 of file Context.cs.
|
inline |
Create a string constant.
Definition at line 2463 of file Context.cs.
Check if the string s1 is lexicographically less or equal to s2.
Definition at line 2579 of file Context.cs.
Check if the string s1 is lexicographically strictly less than s2.
Definition at line 2568 of file Context.cs.
Create an expression representing t[0] - t[1] - ....
Definition at line 1143 of file Context.cs.
Referenced by ArithExpr.operator-().
Check for sequence suffix.
Definition at line 2546 of file Context.cs.
|
inline |
Creates a new symbol using an integer.
Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.
Definition at line 111 of file Context.cs.
Referenced by Params.Add(), Optimize.AssertSoft(), Context.MkArrayConst(), Context.MkBoolConst(), Context.MkConst(), Context.MkConstDecl(), Context.MkConstructor(), Context.MkDatatypeSort(), Context.MkEnumSort(), Context.MkFiniteDomainSort(), Context.MkFuncDecl(), Context.MkListSort(), Context.MkRecFuncDecl(), Context.MkSolver(), Context.MkUninterpretedSort(), and Context.MkUserPropagatorFuncDecl().
|
inline |
Create a symbol using a string.
Definition at line 119 of file Context.cs.
|
inline |
Access the array default value.
Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Definition at line 2280 of file Context.cs.
Convert a regular expression that accepts sequence s.
Definition at line 2648 of file Context.cs.
|
inline |
The true Term.
Definition at line 893 of file Context.cs.
Referenced by Goal.AsBoolExpr(), and Context.MkBool().
Create an expression representing -t.
Definition at line 1155 of file Context.cs.
Referenced by ArithExpr.operator-().
|
inline |
Create a new uninterpreted sort.
Definition at line 224 of file Context.cs.
|
inline |
Create a new uninterpreted sort.
Definition at line 213 of file Context.cs.
Referenced by Context.MkUninterpretedSort().
Create the union of regular languages.
Definition at line 2726 of file Context.cs.
Create the singleton sequence.
Definition at line 2454 of file Context.cs.
Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remaining fields of t are unchanged.
Definition at line 541 of file Context.cs.
Declare a function to be processed by the user propagator plugin.
Definition at line 697 of file Context.cs.
Create an expression representing t1 xor t2.
Definition at line 1010 of file Context.cs.
Referenced by Context.MkXor(), and BoolExpr.operator^().
Create an expression representing t1 xor t2 xor t3 ... .
Definition at line 1023 of file Context.cs.
|
inline |
Bit-vector zero extension.
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.
Definition at line 1776 of file Context.cs.
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition at line 3987 of file Context.cs.
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
Definition at line 3973 of file Context.cs.
Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.
Definition at line 3561 of file Context.cs.
Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.
Definition at line 3709 of file Context.cs.
Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).
Definition at line 3697 of file Context.cs.
|
inline |
Parse the given file using the SMT-LIB2 parser.
Definition at line 3422 of file Context.cs.
|
inline |
Parse the given string using the SMT-LIB2 parser.
Definition at line 3403 of file Context.cs.
|
inline |
Returns a string containing a description of the probe with the given name.
Definition at line 3861 of file Context.cs.
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
Definition at line 3622 of file Context.cs.
Convert a bit-vector expression, represented as an signed number, to a string.
Definition at line 2492 of file Context.cs.
|
inline |
Returns a string containing a description of the simplifier with the given name.
Definition at line 3757 of file Context.cs.
|
inline |
Return a string describing all available parameters to Expr.Simplify.
Definition at line 4850 of file Context.cs.
|
inline |
Create a tactic that just returns the given goal.
Definition at line 3633 of file Context.cs.
Convert an integer expression to a string.
Definition at line 2502 of file Context.cs.
|
inline |
Returns a string containing a description of the tactic with the given name.
Definition at line 3495 of file Context.cs.
|
inline |
Create a simplifier that applies t1 and then then t2 .
Shorthand for AndThen.
Definition at line 3810 of file Context.cs.
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Shorthand for AndThen.
Definition at line 3548 of file Context.cs.
Create a tactic that applies t to a goal for ms milliseconds.
If t does not terminate within ms milliseconds, then it fails.
Definition at line 3577 of file Context.cs.
Convert a bit-vector expression, represented as an unsigned number, to a string.
Definition at line 2482 of file Context.cs.
|
inline |
Unwraps an AST.
This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,
).
| a | The AST to unwrap. |
Definition at line 4842 of file Context.cs.
|
inline |
Update a mutable configuration parameter.
The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -p Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.
Definition at line 4891 of file Context.cs.
|
inline |
Create a tactic that applies t using the given set of parameters p .
Definition at line 3822 of file Context.cs.
Create a tactic that applies t using the given set of parameters p .
Definition at line 3672 of file Context.cs.
Referenced by Context.With().
Create a tactic that applies t to a given goal if the probe p evaluates to true.
If p evaluates to false, then the new tactic behaves like the skip tactic.
Definition at line 3592 of file Context.cs.
Create a tactic that applies t using the given set of parameters p .
Alias for UsingParams
Definition at line 3686 of file Context.cs.
|
inline |
Wraps an AST.
This function is used for transitions between native and managed objects. Note that nativeObject must be a native object obtained from Z3 (e.g., through
) and that it must have a correct reference count (see e.g., .
| nativeObject | The native pointer to wrap. |
Definition at line 4826 of file Context.cs.
Retrieves the Boolean sort of the context.
Definition at line 146 of file Context.cs.
Referenced by Context.MkBoolSort().
Retrieves the String sort of the context.
Definition at line 180 of file Context.cs.
Retrieves the Integer sort of the context.
Definition at line 157 of file Context.cs.
Referenced by Context.MkIntSort().
|
get |
The number of supported Probes.
Definition at line 3837 of file Context.cs.
|
get |
The number of supported simplifiers.
Definition at line 3733 of file Context.cs.
|
get |
The number of supported tactics.
Definition at line 3471 of file Context.cs.
|
set |
Selects the format used for pretty-printing expressions.
The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
Definition at line 3391 of file Context.cs.
|
get |
The names of all supported Probes.
Definition at line 3845 of file Context.cs.
Retrieves the Real sort of the context.
Definition at line 169 of file Context.cs.
Referenced by Context.MkRealSort().
|
get |
The names of all supported tactics.
Definition at line 3741 of file Context.cs.
|
get |
Retrieves parameter descriptions for simplifier.
Definition at line 4859 of file Context.cs.
|
get |
|
get |
The names of all supported tactics.
Definition at line 3479 of file Context.cs.
1.9.1