RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_context.html below:

Z3: Context Class Reference

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

Returns: The result is a sort

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

Returns: The result is a sort

Elements of the sort are created using

See also: MkNumeral(ulong, Sort)

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

Constructor MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null) Create a datatype constructor. More...
Constructor MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null) Create a datatype constructor. More...
DatatypeSort MkDatatypeSort (Symbol name, Constructor[] constructors) Create a new datatype sort. More...
DatatypeSort MkDatatypeSort (string name, Constructor[] constructors) Create a new datatype sort. More...
DatatypeSort[] MkDatatypeSorts (Symbol[] names, Constructor[][] c) Create mutually recursive datatypes. More...
DatatypeSort[] MkDatatypeSorts (string[] names, Constructor[][] c) Create mutually recursive data-types. More...
Expr MkUpdateField (FuncDecl field, Expr t, Expr v) Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remaining fields of t are unchanged. More...
FuncDecl MkFuncDecl (Symbol name, Sort[] domain, Sort range) Creates a new function declaration. More...
FuncDecl MkFuncDecl (Symbol name, Sort domain, Sort range) Creates a new function declaration. More...
FuncDecl MkFuncDecl (string name, Sort[] domain, Sort range) Creates a new function declaration. More...
FuncDecl MkRecFuncDecl (string name, Sort[] domain, Sort range) Creates a new recursive function declaration. More...
void AddRecDef (FuncDecl f, Expr[] args, Expr body) Bind a definition to a recursive function declaration. The function must have previously been created using MkRecFuncDecl. The body may contain recursive uses of the function or other mutually recursive functions. More...
FuncDecl MkFuncDecl (string name, Sort domain, Sort range) Creates a new function declaration. More...
FuncDecl MkFreshFuncDecl (string prefix, Sort[] domain, Sort range) Creates a fresh function declaration with a name prefixed with prefix . More...
FuncDecl MkConstDecl (Symbol name, Sort range) Creates a new constant function declaration. More...
FuncDecl MkConstDecl (string name, Sort range) Creates a new constant function declaration. More...
FuncDecl MkFreshConstDecl (string prefix, Sort range) Creates a fresh constant function declaration with a name prefixed with prefix . More...
FuncDecl MkUserPropagatorFuncDecl (string name, Sort[] domain, Sort range) Declare a function to be processed by the user propagator plugin. More...
Expr MkBound (uint index, Sort ty) Creates a new bound variable. More...
Pattern MkPattern (params Expr[] terms) Create a quantifier pattern. More...
Expr MkConst (Symbol name, Sort range) Creates a new Constant of sort range and named name . More...
Expr MkConst (string name, Sort range) Creates a new Constant of sort range and named name . More...
Expr MkFreshConst (string prefix, Sort range) Creates a fresh Constant of sort range and a name prefixed with prefix . More...
Expr MkConst (FuncDecl f) Creates a fresh constant from the FuncDecl f . More...
BoolExpr MkBoolConst (Symbol name) Create a Boolean constant. More...
BoolExpr MkBoolConst (string name) Create a Boolean constant. More...
IntExpr MkIntConst (Symbol name) Creates an integer constant. More...
IntExpr MkIntConst (string name) Creates an integer constant. More...
RealExpr MkRealConst (Symbol name) Creates a real constant. More...
RealExpr MkRealConst (string name) Creates a real constant. More...
BitVecExpr MkBVConst (Symbol name, uint size) Creates a bit-vector constant. More...
BitVecExpr MkBVConst (string name, uint size) Creates a bit-vector constant. More...
Expr MkApp (FuncDecl f, params Expr[] args) Create a new function application. More...
Expr MkApp (FuncDecl f, IEnumerable< Expr > args) Create a new function application. More...
BoolExpr MkTrue () The true Term. More...
BoolExpr MkFalse () The false Term. More...
BoolExpr MkBool (bool value) Creates a Boolean value. More...
BoolExpr MkEq (Expr x, Expr y) Creates the equality x = y . More...
BoolExpr MkDistinct (params Expr[] args) Creates a distinct term. More...
BoolExpr MkDistinct (IEnumerable< Expr > args) Creates a distinct term. More...
BoolExpr MkNot (BoolExpr a) Mk an expression representing not(a). More...
Expr MkITE (BoolExpr t1, Expr t2, Expr t3) Create an expression representing an if-then-else: ite(t1, t2, t3). More...
BoolExpr MkIff (BoolExpr t1, BoolExpr t2) Create an expression representing t1 iff t2. More...
BoolExpr MkImplies (BoolExpr t1, BoolExpr t2) Create an expression representing t1 -> t2. More...
BoolExpr MkXor (BoolExpr t1, BoolExpr t2) Create an expression representing t1 xor t2. More...
BoolExpr MkXor (IEnumerable< BoolExpr > ts) Create an expression representing t1 xor t2 xor t3 ... . More...
BoolExpr MkAnd (params BoolExpr[] t) Create an expression representing t[0] and t[1] and .... More...
BoolExpr MkAnd (IEnumerable< BoolExpr > t) Create an expression representing t[0] and t[1] and .... More...
BoolExpr MkOr (params BoolExpr[] t) Create an expression representing t[0] or t[1] or .... More...
BoolExpr MkOr (IEnumerable< BoolExpr > t) Create an expression representing t[0] or t[1] or .... More...
ArithExpr MkAdd (params ArithExpr[] t) Create an expression representing t[0] + t[1] + .... More...
ArithExpr MkAdd (IEnumerable< ArithExpr > t) Create an expression representing t[0] + t[1] + .... More...
ArithExpr MkMul (params ArithExpr[] t) Create an expression representing t[0] * t[1] * .... More...
ArithExpr MkMul (IEnumerable< ArithExpr > t) Create an expression representing t[0] * t[1] * .... More...
ArithExpr MkSub (params ArithExpr[] t) Create an expression representing t[0] - t[1] - .... More...
ArithExpr MkUnaryMinus (ArithExpr t) Create an expression representing -t. More...
ArithExpr MkDiv (ArithExpr t1, ArithExpr t2) Create an expression representing t1 / t2. More...
IntExpr MkMod (IntExpr t1, IntExpr t2) Create an expression representing t1 mod t2. More...
IntExpr MkRem (IntExpr t1, IntExpr t2) Create an expression representing t1 rem t2. More...
ArithExpr MkPower (ArithExpr t1, ArithExpr t2) Create an expression representing t1 ^ t2. More...
BoolExpr MkLt (ArithExpr t1, ArithExpr t2) Create an expression representing t1 < t2 More...
BoolExpr MkLe (ArithExpr t1, ArithExpr t2) Create an expression representing t1 <= t2 More...
BoolExpr MkGt (ArithExpr t1, ArithExpr t2) Create an expression representing t1 > t2 More...
BoolExpr MkGe (ArithExpr t1, ArithExpr t2) Create an expression representing t1 >= t2 More...
RealExpr MkInt2Real (IntExpr t) Coerce an integer to a real. More...
IntExpr MkReal2Int (RealExpr t) Coerce a real to an integer. More...
BoolExpr MkIsInteger (RealExpr t) Creates an expression that checks whether a real number is an integer. More...
BitVecExpr MkBVNot (BitVecExpr t) Bitwise negation. More...
BitVecExpr MkBVRedAND (BitVecExpr t) Take conjunction of bits in a vector, return vector of length 1. More...
BitVecExpr MkBVRedOR (BitVecExpr t) Take disjunction of bits in a vector, return vector of length 1. More...
BitVecExpr MkBVAND (BitVecExpr t1, BitVecExpr t2) Bitwise conjunction. More...
BitVecExpr MkBVOR (BitVecExpr t1, BitVecExpr t2) Bitwise disjunction. More...
BitVecExpr MkBVXOR (BitVecExpr t1, BitVecExpr t2) Bitwise XOR. More...
BitVecExpr MkBVNAND (BitVecExpr t1, BitVecExpr t2) Bitwise NAND. More...
BitVecExpr MkBVNOR (BitVecExpr t1, BitVecExpr t2) Bitwise NOR. More...
BitVecExpr MkBVXNOR (BitVecExpr t1, BitVecExpr t2) Bitwise XNOR. More...
BitVecExpr MkBVNeg (BitVecExpr t) Standard two's complement unary minus. More...
BitVecExpr MkBVAdd (BitVecExpr t1, BitVecExpr t2) Two's complement addition. More...
BitVecExpr MkBVSub (BitVecExpr t1, BitVecExpr t2) Two's complement subtraction. More...
BitVecExpr MkBVMul (BitVecExpr t1, BitVecExpr t2) Two's complement multiplication. More...
BitVecExpr MkBVUDiv (BitVecExpr t1, BitVecExpr t2) Unsigned division. More...
BitVecExpr MkBVSDiv (BitVecExpr t1, BitVecExpr t2) Signed division. More...
BitVecExpr MkBVURem (BitVecExpr t1, BitVecExpr t2) Unsigned remainder. More...
BitVecExpr MkBVSRem (BitVecExpr t1, BitVecExpr t2) Signed remainder. More...
BitVecExpr MkBVSMod (BitVecExpr t1, BitVecExpr t2) Two's complement signed remainder (sign follows divisor). More...
BoolExpr MkBVULT (BitVecExpr t1, BitVecExpr t2) Unsigned less-than More...
BoolExpr MkBVSLT (BitVecExpr t1, BitVecExpr t2) Two's complement signed less-than More...
BoolExpr MkBVULE (BitVecExpr t1, BitVecExpr t2) Unsigned less-than or equal to. More...
BoolExpr MkBVSLE (BitVecExpr t1, BitVecExpr t2) Two's complement signed less-than or equal to. More...
BoolExpr MkBVUGE (BitVecExpr t1, BitVecExpr t2) Unsigned greater than or equal to. More...
BoolExpr MkBVSGE (BitVecExpr t1, BitVecExpr t2) Two's complement signed greater than or equal to. More...
BoolExpr MkBVUGT (BitVecExpr t1, BitVecExpr t2) Unsigned greater-than. More...
BoolExpr MkBVSGT (BitVecExpr t1, BitVecExpr t2) Two's complement signed greater-than. More...
BitVecExpr MkConcat (BitVecExpr t1, BitVecExpr t2) Bit-vector concatenation. More...
BitVecExpr MkExtract (uint high, uint low, BitVecExpr t) Bit-vector extraction. More...
BitVecExpr MkSignExt (uint i, BitVecExpr t) Bit-vector sign extension. More...
BitVecExpr MkZeroExt (uint i, BitVecExpr t) Bit-vector zero extension. More...
BitVecExpr MkRepeat (uint i, BitVecExpr t) Bit-vector repetition. More...
BitVecExpr MkBVSHL (BitVecExpr t1, BitVecExpr t2) Shift left. More...
BitVecExpr MkBVLSHR (BitVecExpr t1, BitVecExpr t2) Logical shift right More...
BitVecExpr MkBVASHR (BitVecExpr t1, BitVecExpr t2) Arithmetic shift right More...
BitVecExpr MkBVRotateLeft (uint i, BitVecExpr t) Rotate Left. More...
BitVecExpr MkBVRotateRight (uint i, BitVecExpr t) Rotate Right. More...
BitVecExpr MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) Rotate Left. More...
BitVecExpr MkBVRotateRight (BitVecExpr t1, BitVecExpr t2) Rotate Right. More...
BitVecExpr MkInt2BV (uint n, IntExpr t) Create an n bit bit-vector from the integer argument t . More...
IntExpr MkBV2Int (BitVecExpr t, bool signed) Create an integer from the bit-vector argument t . More...
BoolExpr MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) Create a predicate that checks that the bit-wise addition does not overflow. More...
BoolExpr MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) Create a predicate that checks that the bit-wise addition does not underflow. More...
BoolExpr MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) Create a predicate that checks that the bit-wise subtraction does not overflow. More...
BoolExpr MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) Create a predicate that checks that the bit-wise subtraction does not underflow. More...
BoolExpr MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) Create a predicate that checks that the bit-wise signed division does not overflow. More...
BoolExpr MkBVNegNoOverflow (BitVecExpr t) Create a predicate that checks that the bit-wise negation does not overflow. More...
BoolExpr MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned) Create a predicate that checks that the bit-wise multiplication does not overflow. More...
BoolExpr MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) Create a predicate that checks that the bit-wise multiplication does not underflow. More...
ArrayExpr MkArrayConst (Symbol name, Sort domain, Sort range) Create an array constant. More...
ArrayExpr MkArrayConst (string name, Sort domain, Sort range) Create an array constant. More...
Expr MkSelect (ArrayExpr a, Expr i) Array read. More...
Expr MkSelect (ArrayExpr a, params Expr[] args) Array read. More...
ArrayExpr MkStore (ArrayExpr a, Expr i, Expr v) Array update. More...
ArrayExpr MkStore (ArrayExpr a, Expr[] args, Expr v) Array update. More...
ArrayExpr MkConstArray (Sort domain, Expr v) Create a constant array. More...
ArrayExpr MkMap (FuncDecl f, params ArrayExpr[] args) Maps f on the argument arrays. More...
Expr MkTermArray (ArrayExpr array) Access the array default value. More...
Expr MkArrayExt (ArrayExpr arg1, ArrayExpr arg2) Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt. More...
SetSort MkSetSort (Sort ty) Create a set type. More...
ArrayExpr MkEmptySet (Sort domain) Create an empty set. More...
ArrayExpr MkFullSet (Sort domain) Create the full set. More...
ArrayExpr MkSetAdd (ArrayExpr set, Expr element) Add an element to the set. More...
ArrayExpr MkSetDel (ArrayExpr set, Expr element) Remove an element from a set. More...
ArrayExpr MkSetUnion (params ArrayExpr[] args) Take the union of a list of sets. More...
ArrayExpr MkSetIntersection (params ArrayExpr[] args) Take the intersection of a list of sets. More...
ArrayExpr MkSetDifference (ArrayExpr arg1, ArrayExpr arg2) Take the difference between two sets. More...
ArrayExpr MkSetComplement (ArrayExpr arg) Take the complement of a set. More...
BoolExpr MkSetMembership (Expr elem, ArrayExpr set) Check for set membership. More...
BoolExpr MkSetSubset (ArrayExpr arg1, ArrayExpr arg2) Check for subsetness of sets. More...
SeqExpr MkEmptySeq (Sort s) Create the empty sequence. More...
SeqExpr MkUnit (Expr elem) Create the singleton sequence. More...
SeqExpr MkString (string s) Create a string constant. More...
SeqExpr IntToString (Expr e) Convert an integer expression to a string. More...
SeqExpr UbvToString (Expr e) Convert a bit-vector expression, represented as an unsigned number, to a string. More...
SeqExpr SbvToString (Expr e) Convert a bit-vector expression, represented as an signed number, to a string. More...
IntExpr StringToInt (Expr e) Convert an integer expression to a string. More...
SeqExpr MkConcat (params SeqExpr[] t) Concatenate sequences. More...
IntExpr MkLength (SeqExpr s) Retrieve the length of a given sequence. More...
BoolExpr MkPrefixOf (SeqExpr s1, SeqExpr s2) Check for sequence prefix. More...
BoolExpr MkSuffixOf (SeqExpr s1, SeqExpr s2) Check for sequence suffix. More...
BoolExpr MkContains (SeqExpr s1, SeqExpr s2) Check for sequence containment of s2 in s1. More...
BoolExpr MkStringLt (SeqExpr s1, SeqExpr s2) Check if the string s1 is lexicographically strictly less than s2. More...
BoolExpr MkStringLe (SeqExpr s1, SeqExpr s2) Check if the string s1 is lexicographically less or equal to s2. More...
SeqExpr MkAt (SeqExpr s, Expr index) Retrieve sequence of length one at index. More...
Expr MkNth (SeqExpr s, Expr index) Retrieve element at index. More...
SeqExpr MkExtract (SeqExpr s, IntExpr offset, IntExpr length) Extract subsequence. More...
IntExpr MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset) Extract index of sub-string starting at offset. More...
SeqExpr MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst) Replace the first occurrence of src by dst in s. More...
ReExpr MkToRe (SeqExpr s) Convert a regular expression that accepts sequence s. More...
BoolExpr MkInRe (SeqExpr s, ReExpr re) Check for regular expression membership. More...
ReExpr MkStar (ReExpr re) Take the Kleene star of a regular expression. More...
ReExpr MkLoop (ReExpr re, uint lo, uint hi=0) Take the bounded Kleene star of a regular expression. More...
ReExpr MkPlus (ReExpr re) Take the Kleene plus of a regular expression. More...
ReExpr MkOption (ReExpr re) Create the optional regular expression. More...
ReExpr MkComplement (ReExpr re) Create the complement regular expression. More...
ReExpr MkConcat (params ReExpr[] t) Create the concatenation of regular languages. More...
ReExpr MkUnion (params ReExpr[] t) Create the union of regular languages. More...
ReExpr MkIntersect (params ReExpr[] t) Create the intersection of regular languages. More...
ReExpr MkDiff (ReExpr a, ReExpr b) Create a difference regular expression. More...
ReExpr MkEmptyRe (Sort s) Create the empty regular expression. The sort s should be a regular expression. More...
ReExpr MkFullRe (Sort s) Create the full regular expression. The sort s should be a regular expression. More...
ReExpr MkRange (SeqExpr lo, SeqExpr hi) Create a range expression. More...
BoolExpr MkCharLe (Expr ch1, Expr ch2) Create less than or equal to between two characters. More...
IntExpr CharToInt (Expr ch) Create an integer (code point) from character. More...
BitVecExpr CharToBV (Expr ch) Create a bit-vector (code point) from character. More...
Expr CharFromBV (BitVecExpr bv) Create a character from a bit-vector (code point). More...
BoolExpr MkIsDigit (Expr ch) Create a check if the character is a digit. More...
BoolExpr MkAtMost (IEnumerable< BoolExpr > args, uint k) Create an at-most-k constraint. More...
BoolExpr MkAtLeast (IEnumerable< BoolExpr > args, uint k) Create an at-least-k constraint. More...
BoolExpr MkPBLe (int[] coeffs, BoolExpr[] args, int k) Create a pseudo-Boolean less-or-equal constraint. More...
BoolExpr MkPBGe (int[] coeffs, BoolExpr[] args, int k) Create a pseudo-Boolean greater-or-equal constraint. More...
BoolExpr MkPBEq (int[] coeffs, BoolExpr[] args, int k) Create a pseudo-Boolean equal constraint. More...
Expr MkNumeral (string v, Sort ty) Create a Term of a given sort. More...
Expr MkNumeral (int v, Sort ty) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More...
Expr MkNumeral (uint v, Sort ty) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More...
Expr MkNumeral (long v, Sort ty) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More...
Expr MkNumeral (ulong v, Sort ty) Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string. More...
RatNum MkReal (int num, int den) Create a real from a fraction. More...
RatNum MkReal (string v) Create a real numeral. More...
RatNum MkReal (int v) Create a real numeral. More...
RatNum MkReal (uint v) Create a real numeral. More...
RatNum MkReal (long v) Create a real numeral. More...
RatNum MkReal (ulong v) Create a real numeral. More...
IntNum MkInt (string v) Create an integer numeral. More...
IntNum MkInt (int v) Create an integer numeral. More...
IntNum MkInt (uint v) Create an integer numeral. More...
IntNum MkInt (long v) Create an integer numeral. More...
IntNum MkInt (ulong v) Create an integer numeral. More...
BitVecNum MkBV (string v, uint size) Create a bit-vector numeral. More...
BitVecNum MkBV (int v, uint size) Create a bit-vector numeral. More...
BitVecNum MkBV (uint v, uint size) Create a bit-vector numeral. More...
BitVecNum MkBV (long v, uint size) Create a bit-vector numeral. More...
BitVecNum MkBV (ulong v, uint size) Create a bit-vector numeral. More...
BitVecNum MkBV (bool[] bits) Create a bit-vector numeral. More...
Quantifier MkForall (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) Create a universal Quantifier. More...
Quantifier MkForall (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) Create a universal Quantifier. More...
Quantifier MkExists (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) Create an existential Quantifier. More...
Quantifier MkExists (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) Create an existential Quantifier. More...
Quantifier MkQuantifier (bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) Create a Quantifier. More...
Quantifier MkQuantifier (bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null) Create a Quantifier. More...
Lambda MkLambda (Sort[] sorts, Symbol[] names, Expr body) Create a lambda expression. More...
Lambda MkLambda (Expr[] boundConstants, Expr body) Create a lambda expression. More...
BoolExpr[] ParseSMTLIB2String (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) Parse the given string using the SMT-LIB2 parser. More...
BoolExpr[] ParseSMTLIB2File (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null) Parse the given file using the SMT-LIB2 parser. More...
Goal MkGoal (bool models=true, bool unsatCores=false, bool proofs=false) Creates a new Goal. More...
Params MkParams () Creates a new ParameterSet. More...
string TacticDescription (string name) Returns a string containing a description of the tactic with the given name. More...
Tactic MkTactic (string name) Creates a new Tactic. More...
Tactic AndThen (Tactic t1, Tactic t2, params Tactic[] ts) Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . More...
Tactic Then (Tactic t1, Tactic t2, params Tactic[] ts) Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . More...
Tactic OrElse (Tactic t1, Tactic t2) Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal. More...
Tactic TryFor (Tactic t, uint ms) Create a tactic that applies t to a goal for ms milliseconds. More...
Tactic When (Probe p, Tactic t) Create a tactic that applies t to a given goal if the probe p evaluates to true. More...
Tactic Cond (Probe p, Tactic t1, Tactic t2) Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise. More...
Tactic Repeat (Tactic t, uint max=uint.MaxValue) Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached. More...
Tactic Skip () Create a tactic that just returns the given goal. More...
Tactic Fail () Create a tactic always fails. More...
Tactic FailIf (Probe p) Create a tactic that fails if the probe p evaluates to false. More...
Tactic FailIfNotDecided () Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’). More...
Tactic UsingParams (Tactic t, Params p) Create a tactic that applies t using the given set of parameters p . More...
Tactic With (Tactic t, Params p) Create a tactic that applies t using the given set of parameters p . More...
Tactic ParOr (params Tactic[] t) Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). More...
Tactic ParAndThen (Tactic t1, Tactic t2) Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel. More...
void Interrupt () Interrupt the execution of a Z3 procedure. More...
string 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...

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4