Z3
Public Member Functions | Properties
Context Class Reference

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

+ Inheritance diagram for Context:

Public Member Functions

 Context ()
 Constructor. More...
 
 Context (Dictionary< string, string > settings)
 Constructor. More...
 
IntSymbol MkSymbol (int i)
 Creates a new symbol using an integer. More...
 
StringSymbol MkSymbol (string name)
 Create a symbol using a string. More...
 
BoolSort MkBoolSort ()
 Create a new Boolean sort. More...
 
UninterpretedSort MkUninterpretedSort (Symbol s)
 Create a new uninterpreted sort. More...
 
UninterpretedSort MkUninterpretedSort (string str)
 Create a new uninterpreted sort. More...
 
IntSort MkIntSort ()
 Create a new integer sort. More...
 
RealSort MkRealSort ()
 Create a real sort. More...
 
BitVecSort MkBitVecSort (uint size)
 Create a new bit-vector sort. More...
 
SeqSort MkSeqSort (Sort s)
 Create a new sequence sort. More...
 
ReSort MkReSort (SeqSort s)
 Create a new regular expression sort. More...
 
ArraySort MkArraySort (Sort domain, Sort range)
 Create a new array sort. More...
 
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 remainig 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 MkFuncDecl (string name, Sort domain, Sort range)
 Creates a new function declaration. More...
 
FuncDecl MkFreshFuncDecl (string prefix, Sort[] domain, Sort range)
 Creates a fresh function declaration with a name prefixed with prefix . More...
 
FuncDecl MkConstDecl (Symbol name, Sort range)
 Creates a new constant function declaration. More...
 
FuncDecl MkConstDecl (string name, Sort range)
 Creates a new constant function declaration. More...
 
FuncDecl MkFreshConstDecl (string prefix, Sort range)
 Creates a fresh constant function declaration with a name prefixed with prefix . More...
 
Expr MkBound (uint index, Sort ty)
 Creates a new bound variable. More...
 
Pattern MkPattern (params Expr[] terms)
 Create a quantifier pattern. More...
 
Expr MkConst (Symbol name, Sort range)
 Creates a new Constant of sort range and named name . More...
 
Expr MkConst (string name, Sort range)
 Creates a new Constant of sort range and named name . More...
 
Expr MkFreshConst (string prefix, Sort range)
 Creates a fresh Constant of sort range and a name prefixed with prefix . More...
 
Expr MkConst (FuncDecl f)
 Creates a fresh constant from the FuncDecl f . More...
 
BoolExpr MkBoolConst (Symbol name)
 Create a Boolean constant. More...
 
BoolExpr MkBoolConst (string name)
 Create a Boolean constant. More...
 
IntExpr MkIntConst (Symbol name)
 Creates an integer constant. More...
 
IntExpr MkIntConst (string name)
 Creates an integer constant. More...
 
RealExpr MkRealConst (Symbol name)
 Creates a real constant. More...
 
RealExpr MkRealConst (string name)
 Creates a real constant. More...
 
BitVecExpr MkBVConst (Symbol name, uint size)
 Creates a bit-vector constant. More...
 
BitVecExpr MkBVConst (string name, uint size)
 Creates a bit-vector constant. More...
 
Expr MkApp (FuncDecl f, params Expr[] args)
 Create a new function application. More...
 
Expr MkApp (FuncDecl f, IEnumerable< Expr > args)
 Create a new function application. More...
 
BoolExpr MkTrue ()
 The true Term. More...
 
BoolExpr MkFalse ()
 The false Term. More...
 
BoolExpr MkBool (bool value)
 Creates a Boolean value. More...
 
BoolExpr MkEq (Expr x, Expr y)
 Creates the equality x = y . More...
 
BoolExpr MkDistinct (params Expr[] args)
 Creates a distinct term. More...
 
BoolExpr MkNot (BoolExpr a)
 Mk an expression representing not(a). More...
 
Expr MkITE (BoolExpr t1, Expr t2, Expr t3)
 Create an expression representing an if-then-else: ite(t1, t2, t3). More...
 
BoolExpr MkIff (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 iff t2. More...
 
BoolExpr MkImplies (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 -> t2. More...
 
BoolExpr MkXor (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 xor t2. More...
 
BoolExpr 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...
 
ArrayExpr MkStore (ArrayExpr a, Expr i, 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 MkConcat (params SeqExpr[] t)
 Concatentate 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...
 
SeqExpr MkAt (SeqExpr s, IntExpr index)
 Retrieve sequence of length one 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 MPlus (ReExpr re)
 Take the Kleene plus of a regular expression. More...
 
ReExpr MOption (ReExpr re)
 Create the optional 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...
 
BoolExpr MkAtMost (BoolExpr[] args, uint k)
 Create an at-most-k constraint. More...
 
BoolExpr MkPBLe (int[] coeffs, BoolExpr[] args, int k)
 Create a pseudo-Boolean less-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 use 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 use 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 use 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 use 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...
 
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...
 
string BenchmarkToSMTString (string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
 Convert a benchmark into an SMT-LIB formatted string. More...
 
void ParseSMTLIBString (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
 Parse the given string using the SMT-LIB parser. More...
 
void ParseSMTLIBFile (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
 Parse the given file using the SMT-LIB parser. 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 triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false'). More...
 
Tactic UsingParams (Tactic t, Params p)
 Create a tactic that applies t using the given set of parameters p . More...
 
Tactic With (Tactic t, Params p)
 Create a tactic that applies t using the given set of parameters p . More...
 
Tactic ParOr (params Tactic[] t)
 Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). More...
 
Tactic ParAndThen (Tactic t1, Tactic t2)
 Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel. More...
 
void Interrupt ()
 Interrupt the execution of a Z3 procedure. More...
 
string ProbeDescription (string name)
 Returns a string containing a description of the probe with the given name. More...
 
Probe MkProbe (string name)
 Creates a new Probe. More...
 
Probe ConstProbe (double val)
 Create a probe that always evaluates to val . More...
 
Probe Lt (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2 More...
 
Probe Gt (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2 More...
 
Probe Le (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the value returned by p2 More...
 
Probe Ge (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the value returned by p2 More...
 
Probe Eq (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2 More...
 
Probe And (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true". More...
 
Probe Or (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true". More...
 
Probe Not (Probe p)
 Create a probe that evaluates to "true" when the value p does not evaluate to "true". More...
 
Solver MkSolver (Symbol logic=null)
 Creates a new (incremental) solver. More...
 
Solver MkSolver (string logic)
 Creates a new (incremental) solver. More...
 
Solver MkSimpleSolver ()
 Creates a new (incremental) solver. More...
 
Solver MkSolver (Tactic t)
 Creates a solver that is implemented using the given tactic. More...
 
Fixedpoint MkFixedpoint ()
 Create a Fixedpoint context. More...
 
Optimize MkOptimize ()
 Create an Optimization context. More...
 
FPRMSort MkFPRoundingModeSort ()
 Create the floating-point RoundingMode sort. More...
 
FPRMExpr MkFPRoundNearestTiesToEven ()
 Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More...
 
FPRMNum MkFPRNE ()
 Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More...
 
FPRMNum MkFPRoundNearestTiesToAway ()
 Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More...
 
FPRMNum MkFPRNA ()
 Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More...
 
FPRMNum MkFPRoundTowardPositive ()
 Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More...
 
FPRMNum MkFPRTP ()
 Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. More...
 
FPRMNum MkFPRoundTowardNegative ()
 Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More...
 
FPRMNum MkFPRTN ()
 Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. More...
 
FPRMNum MkFPRoundTowardZero ()
 Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More...
 
FPRMNum MkFPRTZ ()
 Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. More...
 
FPSort MkFPSort (uint ebits, uint sbits)
 Create a FloatingPoint sort. More...
 
FPSort MkFPSortHalf ()
 Create the half-precision (16-bit) FloatingPoint sort. More...
 
FPSort MkFPSort16 ()
 Create the half-precision (16-bit) FloatingPoint sort. More...
 
FPSort MkFPSortSingle ()
 Create the single-precision (32-bit) FloatingPoint sort. More...
 
FPSort MkFPSort32 ()
 Create the single-precision (32-bit) FloatingPoint sort. More...
 
FPSort MkFPSortDouble ()
 Create the double-precision (64-bit) FloatingPoint sort. More...
 
FPSort MkFPSort64 ()
 Create the double-precision (64-bit) FloatingPoint sort. More...
 
FPSort MkFPSortQuadruple ()
 Create the quadruple-precision (128-bit) FloatingPoint sort. More...
 
FPSort MkFPSort128 ()
 Create the quadruple-precision (128-bit) FloatingPoint sort. More...
 
FPNum MkFPNaN (FPSort s)
 Create a NaN of sort s. More...
 
FPNum MkFPInf (FPSort s, bool negative)
 Create a floating-point infinity of sort s. More...
 
FPNum MkFPZero (FPSort s, bool negative)
 Create a floating-point zero of sort s. More...
 
FPNum MkFPNumeral (float v, FPSort s)
 Create a numeral of FloatingPoint sort from a float. More...
 
FPNum MkFPNumeral (double v, FPSort s)
 Create a numeral of FloatingPoint sort from a float. More...
 
FPNum MkFPNumeral (int v, FPSort s)
 Create a numeral of FloatingPoint sort from an int. More...
 
FPNum MkFPNumeral (bool sgn, uint sig, int exp, FPSort s)
 Create a numeral of FloatingPoint sort from a sign bit and two integers. More...
 
FPNum MkFPNumeral (bool sgn, Int64 exp, UInt64 sig, FPSort s)
 Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More...
 
FPNum MkFP (float v, FPSort s)
 Create a numeral of FloatingPoint sort from a float. More...
 
FPNum MkFP (double v, FPSort s)
 Create a numeral of FloatingPoint sort from a float. More...
 
FPNum MkFP (int v, FPSort s)
 Create a numeral of FloatingPoint sort from an int. More...
 
FPNum MkFP (bool sgn, int exp, uint sig, FPSort s)
 Create a numeral of FloatingPoint sort from a sign bit and two integers. More...
 
FPNum MkFP (bool sgn, Int64 exp, UInt64 sig, FPSort s)
 Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More...
 
FPExpr MkFPAbs (FPExpr t)
 Floating-point absolute value More...
 
FPExpr MkFPNeg (FPExpr t)
 Floating-point negation More...
 
FPExpr MkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)
 Floating-point addition More...
 
FPExpr MkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)
 Floating-point subtraction More...
 
FPExpr MkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)
 Floating-point multiplication More...
 
FPExpr MkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)
 Floating-point division More...
 
FPExpr MkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
 Floating-point fused multiply-add More...
 
FPExpr MkFPSqrt (FPRMExpr rm, FPExpr t)
 Floating-point square root More...
 
FPExpr MkFPRem (FPExpr t1, FPExpr t2)
 Floating-point remainder More...
 
FPExpr MkFPRoundToIntegral (FPRMExpr rm, FPExpr t)
 Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number. More...
 
FPExpr MkFPMin (FPExpr t1, FPExpr t2)
 Minimum of floating-point numbers. More...
 
FPExpr MkFPMax (FPExpr t1, FPExpr t2)
 Maximum of floating-point numbers. More...
 
BoolExpr MkFPLEq (FPExpr t1, FPExpr t2)
 Floating-point less than or equal. More...
 
BoolExpr MkFPLt (FPExpr t1, FPExpr t2)
 Floating-point less than. More...
 
BoolExpr MkFPGEq (FPExpr t1, FPExpr t2)
 Floating-point greater than or equal. More...
 
BoolExpr MkFPGt (FPExpr t1, FPExpr t2)
 Floating-point greater than. More...
 
BoolExpr MkFPEq (FPExpr t1, FPExpr t2)
 Floating-point equality. More...
 
BoolExpr MkFPIsNormal (FPExpr t)
 Predicate indicating whether t is a normal floating-point number. More...
 
BoolExpr MkFPIsSubnormal (FPExpr t)
 Predicate indicating whether t is a subnormal floating-point number. More...
 
BoolExpr MkFPIsZero (FPExpr t)
 Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0. More...
 
BoolExpr MkFPIsInfinite (FPExpr t)
 Predicate indicating whether t is a floating-point number representing +oo or -oo. More...
 
BoolExpr MkFPIsNaN (FPExpr t)
 Predicate indicating whether t is a NaN. More...
 
BoolExpr MkFPIsNegative (FPExpr t)
 Predicate indicating whether t is a negative floating-point number. More...
 
BoolExpr MkFPIsPositive (FPExpr t)
 Predicate indicating whether t is a positive floating-point number. More...
 
FPExpr MkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
 Create an expression of FloatingPoint sort from three bit-vector expressions. More...
 
FPExpr MkFPToFP (BitVecExpr bv, FPSort s)
 Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. More...
 
FPExpr MkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)
 Conversion of a FloatingPoint term into another term of different FloatingPoint sort. More...
 
FPExpr MkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)
 Conversion of a term of real sort into a term of FloatingPoint sort. More...
 
FPExpr MkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
 Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. More...
 
FPExpr MkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)
 Conversion of a floating-point number to another FloatingPoint sort s. More...
 
BitVecExpr MkFPToBV (FPRMExpr rm, FPExpr t, uint sz, bool signed)
 Conversion of a floating-point term into a bit-vector. More...
 
RealExpr MkFPToReal (FPExpr t)
 Conversion of a floating-point term into a real-numbered term. More...
 
BitVecExpr MkFPToIEEEBV (FPExpr t)
 Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. More...
 
BitVecExpr MkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
 Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. More...
 
AST WrapAST (IntPtr nativeObject)
 Wraps an AST. More...
 
IntPtr UnwrapAST (AST a)
 Unwraps an AST. More...
 
string SimplifyHelp ()
 Return a string describing all available parameters to Expr.Simplify. More...
 
void UpdateParamValue (string id, string value)
 Update a mutable configuration parameter. More...
 
void Dispose ()
 Disposes of the context. More...
 

Properties

BoolSort BoolSort [get]
 Retrieves the Boolean sort of the context. More...
 
IntSort IntSort [get]
 Retrieves the Integer sort of the context. More...
 
RealSort RealSort [get]
 Retrieves the Real sort of the context. More...
 
SeqSort StringSort [get]
 Retrieves the String sort of the context. More...
 
Z3_ast_print_mode PrintMode [set]
 Selects the format used for pretty-printing expressions. More...
 
uint NumSMTLIBFormulas [get]
 The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
BoolExpr [] SMTLIBFormulas [get]
 The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
uint NumSMTLIBAssumptions [get]
 The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
BoolExpr [] SMTLIBAssumptions [get]
 The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
uint NumSMTLIBDecls [get]
 The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
FuncDecl [] SMTLIBDecls [get]
 The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
uint NumSMTLIBSorts [get]
 The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
Sort [] SMTLIBSorts [get]
 The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. More...
 
uint NumTactics [get]
 The number of supported tactics. More...
 
string [] TacticNames [get]
 The names of all supported tactics. More...
 
uint NumProbes [get]
 The number of supported Probes. More...
 
string [] ProbeNames [get]
 The names of all supported Probes. More...
 
ParamDescrs SimplifyParameterDescriptions [get]
 Retrieves parameter descriptions for simplifier. More...
 
IDecRefQueue AST_DRQ [get]
 AST DRQ More...
 
IDecRefQueue ASTMap_DRQ [get]
 ASTMap DRQ More...
 
IDecRefQueue ASTVector_DRQ [get]
 ASTVector DRQ More...
 
IDecRefQueue ApplyResult_DRQ [get]
 ApplyResult DRQ More...
 
IDecRefQueue FuncEntry_DRQ [get]
 FuncEntry DRQ More...
 
IDecRefQueue FuncInterp_DRQ [get]
 FuncInterp DRQ More...
 
IDecRefQueue Goal_DRQ [get]
 Goal DRQ More...
 
IDecRefQueue Model_DRQ [get]
 Model DRQ More...
 
IDecRefQueue Params_DRQ [get]
 Params DRQ More...
 
IDecRefQueue ParamDescrs_DRQ [get]
 ParamDescrs DRQ More...
 
IDecRefQueue Probe_DRQ [get]
 Probe DRQ More...
 
IDecRefQueue Solver_DRQ [get]
 Solver DRQ More...
 
IDecRefQueue Statistics_DRQ [get]
 Statistics DRQ More...
 
IDecRefQueue Tactic_DRQ [get]
 Tactic DRQ More...
 
IDecRefQueue Fixedpoint_DRQ [get]
 FixedPoint DRQ More...
 
IDecRefQueue Optimize_DRQ [get]
 Optimize DRQ More...
 

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 32 of file Context.cs.

Constructor & Destructor Documentation

§ Context() [1/2]

Context ( )
inline

Constructor.

Definition at line 38 of file Context.cs.

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

§ Context() [2/2]

Context ( Dictionary< string, string >  settings)
inline

Constructor.

The following parameters can be set:

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

Definition at line 66 of file Context.cs.

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

Member Function Documentation

§ And()

Probe And ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3759 of file Context.cs.

3760  {
3761  Contract.Requires(p1 != null);
3762  Contract.Requires(p2 != null);
3763  Contract.Ensures(Contract.Result<Probe>() != null);
3764 
3765  CheckContextMatch(p1);
3766  CheckContextMatch(p2);
3767  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3768  }

§ AndThen()

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

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

Definition at line 3394 of file Context.cs.

3395  {
3396  Contract.Requires(t1 != null);
3397  Contract.Requires(t2 != null);
3398  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3399  Contract.Ensures(Contract.Result<Tactic>() != null);
3400 
3401 
3402  CheckContextMatch(t1);
3403  CheckContextMatch(t2);
3404  CheckContextMatch<Tactic>(ts);
3405 
3406  IntPtr last = IntPtr.Zero;
3407  if (ts != null && ts.Length > 0)
3408  {
3409  last = ts[ts.Length - 1].NativeObject;
3410  for (int i = ts.Length - 2; i >= 0; i--)
3411  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3412  }
3413  if (last != IntPtr.Zero)
3414  {
3415  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3416  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3417  }
3418  else
3419  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3420  }

§ BenchmarkToSMTString()

string BenchmarkToSMTString ( string  name,
string  logic,
string  status,
string  attributes,
BoolExpr []  assumptions,
BoolExpr  formula 
)
inline

Convert a benchmark into an SMT-LIB formatted string.

Parameters
nameName of the benchmark. The argument is optional.
logicThe benchmark logic.
statusThe status string (sat, unsat, or unknown)
attributesOther attributes, such as source, difficulty or category.
assumptionsAuxiliary assumptions.
formulaFormula to be checked for consistency in conjunction with assumptions.
Returns
A string representation of the benchmark.

Definition at line 3133 of file Context.cs.

3135  {
3136  Contract.Requires(assumptions != null);
3137  Contract.Requires(formula != null);
3138  Contract.Ensures(Contract.Result<string>() != null);
3139 
3140  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
3141  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
3142  formula.NativeObject);
3143  }

§ Cond()

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

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

Definition at line 3491 of file Context.cs.

3492  {
3493  Contract.Requires(p != null);
3494  Contract.Requires(t1 != null);
3495  Contract.Requires(t2 != null);
3496  Contract.Ensures(Contract.Result<Tactic>() != null);
3497 
3498  CheckContextMatch(p);
3499  CheckContextMatch(t1);
3500  CheckContextMatch(t2);
3501  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3502  }

§ ConstProbe()

Probe ConstProbe ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3673 of file Context.cs.

3674  {
3675  Contract.Ensures(Contract.Result<Probe>() != null);
3676 
3677  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3678  }

§ Dispose()

void Dispose ( )
inline

Disposes of the context.

Definition at line 4985 of file Context.cs.

4986  {
4987  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4988  AST_DRQ.Clear(this);
4989  ASTMap_DRQ.Clear(this);
4990  ASTVector_DRQ.Clear(this);
4991  ApplyResult_DRQ.Clear(this);
4992  FuncEntry_DRQ.Clear(this);
4993  FuncInterp_DRQ.Clear(this);
4994  Goal_DRQ.Clear(this);
4995  Model_DRQ.Clear(this);
4996  Params_DRQ.Clear(this);
4997  ParamDescrs_DRQ.Clear(this);
4998  Probe_DRQ.Clear(this);
4999  Solver_DRQ.Clear(this);
5000  Statistics_DRQ.Clear(this);
5001  Tactic_DRQ.Clear(this);
5002  Fixedpoint_DRQ.Clear(this);
5003  Optimize_DRQ.Clear(this);
5004 
5005  m_boolSort = null;
5006  m_intSort = null;
5007  m_realSort = null;
5008  m_stringSort = null;
5009  }
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
Definition: Context.cs:4893
IDecRefQueue Tactic_DRQ
Tactic DRQ
Definition: Context.cs:4948
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4958
IDecRefQueue Statistics_DRQ
Statistics DRQ
Definition: Context.cs:4943
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4913
IDecRefQueue Params_DRQ
Params DRQ
Definition: Context.cs:4923
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
Definition: Context.cs:4903
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4938
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
Definition: Context.cs:4898
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Definition: Context.cs:4908
IDecRefQueue AST_DRQ
AST DRQ
Definition: Context.cs:4883
IDecRefQueue Model_DRQ
Model DRQ
Definition: Context.cs:4918
IDecRefQueue ASTMap_DRQ
ASTMap DRQ
Definition: Context.cs:4888
IDecRefQueue Probe_DRQ
Probe DRQ
Definition: Context.cs:4933
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Definition: Context.cs:4953
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Definition: Context.cs:4928

§ Eq()

Probe Eq ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3744 of file Context.cs.

3745  {
3746  Contract.Requires(p1 != null);
3747  Contract.Requires(p2 != null);
3748  Contract.Ensures(Contract.Result<Probe>() != null);
3749 
3750  CheckContextMatch(p1);
3751  CheckContextMatch(p2);
3752  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3753  }

§ Fail()

Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3530 of file Context.cs.

3531  {
3532  Contract.Ensures(Contract.Result<Tactic>() != null);
3533 
3534  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3535  }

§ FailIf()

Tactic FailIf ( Probe  p)
inline

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

Definition at line 3540 of file Context.cs.

3541  {
3542  Contract.Requires(p != null);
3543  Contract.Ensures(Contract.Result<Tactic>() != null);
3544 
3545  CheckContextMatch(p);
3546  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3547  }

§ FailIfNotDecided()

Tactic FailIfNotDecided ( )
inline

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

Definition at line 3553 of file Context.cs.

3554  {
3555  Contract.Ensures(Contract.Result<Tactic>() != null);
3556 
3557  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3558  }

§ Ge()

Probe Ge ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3729 of file Context.cs.

3730  {
3731  Contract.Requires(p1 != null);
3732  Contract.Requires(p2 != null);
3733  Contract.Ensures(Contract.Result<Probe>() != null);
3734 
3735  CheckContextMatch(p1);
3736  CheckContextMatch(p2);
3737  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3738  }

§ Gt()

Probe Gt ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3699 of file Context.cs.

3700  {
3701  Contract.Requires(p1 != null);
3702  Contract.Requires(p2 != null);
3703  Contract.Ensures(Contract.Result<Probe>() != null);
3704 
3705  CheckContextMatch(p1);
3706  CheckContextMatch(p2);
3707  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3708  }

§ Interrupt()

void Interrupt ( )
inline

Interrupt the execution of a Z3 procedure.

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

Definition at line 3618 of file Context.cs.

3619  {
3620  Native.Z3_interrupt(nCtx);
3621  }

§ Le()

Probe Le ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3714 of file Context.cs.

3715  {
3716  Contract.Requires(p1 != null);
3717  Contract.Requires(p2 != null);
3718  Contract.Ensures(Contract.Result<Probe>() != null);
3719 
3720  CheckContextMatch(p1);
3721  CheckContextMatch(p2);
3722  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3723  }

§ Lt()

Probe Lt ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3684 of file Context.cs.

3685  {
3686  Contract.Requires(p1 != null);
3687  Contract.Requires(p2 != null);
3688  Contract.Ensures(Contract.Result<Probe>() != null);
3689 
3690  CheckContextMatch(p1);
3691  CheckContextMatch(p2);
3692  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3693  }

§ MkAdd() [1/2]

ArithExpr MkAdd ( params ArithExpr []  t)
inline

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

Definition at line 1022 of file Context.cs.

Referenced by ArithExpr.operator+().

1023  {
1024  Contract.Requires(t != null);
1025  Contract.Requires(Contract.ForAll(t, a => a != null));
1026  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1027 
1028  CheckContextMatch<ArithExpr>(t);
1029  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1030  }

§ MkAdd() [2/2]

ArithExpr MkAdd ( IEnumerable< ArithExpr t)
inline

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

Definition at line 1035 of file Context.cs.

1036  {
1037  Contract.Requires(t != null);
1038  Contract.Requires(Contract.ForAll(t, a => a != null));
1039  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1040 
1041  CheckContextMatch(t);
1042  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1043  }

§ MkAnd() [1/2]

BoolExpr MkAnd ( params BoolExpr []  t)
inline

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

Definition at line 967 of file Context.cs.

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

968  {
969  Contract.Requires(t != null);
970  Contract.Requires(Contract.ForAll(t, a => a != null));
971  Contract.Ensures(Contract.Result<BoolExpr>() != null);
972 
973  CheckContextMatch<BoolExpr>(t);
974  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
975  }

§ MkAnd() [2/2]

BoolExpr MkAnd ( IEnumerable< BoolExpr t)
inline

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

Definition at line 980 of file Context.cs.

981  {
982  Contract.Requires(t != null);
983  Contract.Requires(Contract.ForAll(t, a => a != null));
984  Contract.Ensures(Contract.Result<BoolExpr>() != null);
985  CheckContextMatch<BoolExpr>(t);
986  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
987  }

§ MkApp() [1/2]

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

Create a new function application.

Definition at line 807 of file Context.cs.

Referenced by EnumSort.Const().

808  {
809  Contract.Requires(f != null);
810  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
811  Contract.Ensures(Contract.Result<Expr>() != null);
812 
813  CheckContextMatch(f);
814  CheckContextMatch<Expr>(args);
815  return Expr.Create(this, f, args);
816  }

§ MkApp() [2/2]

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

Create a new function application.

Definition at line 821 of file Context.cs.

822  {
823  Contract.Requires(f != null);
824  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
825  Contract.Ensures(Contract.Result<Expr>() != null);
826 
827  CheckContextMatch(f);
828  CheckContextMatch(args);
829  return Expr.Create(this, f, args.ToArray());
830  }

§ MkArrayConst() [1/2]

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

Create an array constant.

Definition at line 2094 of file Context.cs.

2095  {
2096  Contract.Requires(name != null);
2097  Contract.Requires(domain != null);
2098  Contract.Requires(range != null);
2099  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2100 
2101  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
2102  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:266

§ MkArrayConst() [2/2]

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

Create an array constant.

Definition at line 2107 of file Context.cs.

2108  {
2109  Contract.Requires(domain != null);
2110  Contract.Requires(range != null);
2111  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2112 
2113  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2114  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:266
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkArrayExt()

Expr MkArrayExt ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

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

Definition at line 2231 of file Context.cs.

2232  {
2233  Contract.Requires(arg1 != null);
2234  Contract.Requires(arg2 != null);
2235  Contract.Ensures(Contract.Result<Expr>() != null);
2236 
2237  CheckContextMatch(arg1);
2238  CheckContextMatch(arg2);
2239  return Expr.Create(this, Native.Z3_mk_array_ext(nCtx, arg1.NativeObject, arg2.NativeObject));
2240  }

§ MkArraySort()

ArraySort MkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 266 of file Context.cs.

267  {
268  Contract.Requires(domain != null);
269  Contract.Requires(range != null);
270  Contract.Ensures(Contract.Result<ArraySort>() != null);
271 
272  CheckContextMatch(domain);
273  CheckContextMatch(range);
274  return new ArraySort(this, domain, range);
275  }
def ArraySort(d, r)
Definition: z3py.py:4110

§ MkAt()

SeqExpr MkAt ( SeqExpr  s,
IntExpr  index 
)
inline

Retrieve sequence of length one at index.

Definition at line 2486 of file Context.cs.

2487  {
2488  Contract.Requires(s != null);
2489  Contract.Requires(index != null);
2490  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2491  CheckContextMatch(s, index);
2492  return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
2493  }

§ MkAtMost()

BoolExpr MkAtMost ( BoolExpr []  args,
uint  k 
)
inline

Create an at-most-k constraint.

Definition at line 2620 of file Context.cs.

2621  {
2622  Contract.Requires(args != null);
2623  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2624  CheckContextMatch<BoolExpr>(args);
2625  return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
2626  AST.ArrayToNative(args), k));
2627  }

§ MkBitVecSort()

BitVecSort MkBitVecSort ( uint  size)
inline

Create a new bit-vector sort.

Definition at line 235 of file Context.cs.

236  {
237  Contract.Ensures(Contract.Result<BitVecSort>() != null);
238 
239  return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
240  }
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3530

§ MkBool()

BoolExpr MkBool ( bool  value)
inline

Creates a Boolean value.

Definition at line 856 of file Context.cs.

857  {
858  Contract.Ensures(Contract.Result<BoolExpr>() != null);
859 
860  return value ? MkTrue() : MkFalse();
861  }
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:836
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:846

§ MkBoolConst() [1/2]

BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 720 of file Context.cs.

721  {
722  Contract.Requires(name != null);
723  Contract.Ensures(Contract.Result<BoolExpr>() != null);
724 
725  return (BoolExpr)MkConst(name, BoolSort);
726  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:135
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669

§ MkBoolConst() [2/2]

BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 731 of file Context.cs.

732  {
733  Contract.Ensures(Contract.Result<BoolExpr>() != null);
734 
735  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
736  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:135
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkBoolSort()

BoolSort MkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 185 of file Context.cs.

186  {
187  Contract.Ensures(Contract.Result<BoolSort>() != null);
188  return new BoolSort(this);
189  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:135

§ MkBound()

Expr MkBound ( uint  index,
Sort  ty 
)
inline

Creates a new bound variable.

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

Definition at line 637 of file Context.cs.

638  {
639  Contract.Requires(ty != null);
640  Contract.Ensures(Contract.Result<Expr>() != null);
641 
642  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
643  }

§ MkBV() [1/5]

BitVecNum MkBV ( string  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2890 of file Context.cs.

2891  {
2892  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2893 
2894  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2895  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2669
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235

§ MkBV() [2/5]

BitVecNum MkBV ( int  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2902 of file Context.cs.

2903  {
2904  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2905 
2906  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2907  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2669
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235

§ MkBV() [3/5]

BitVecNum MkBV ( uint  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2914 of file Context.cs.

2915  {
2916  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2917 
2918  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2919  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2669
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235

§ MkBV() [4/5]

BitVecNum MkBV ( long  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2926 of file Context.cs.

2927  {
2928  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2929 
2930  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2931  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2669
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235

§ MkBV() [5/5]

BitVecNum MkBV ( ulong  v,
uint  size 
)
inline

Create a bit-vector numeral.

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

Definition at line 2938 of file Context.cs.

2939  {
2940  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2941 
2942  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2943  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2669
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235

§ MkBV2Int()

IntExpr MkBV2Int ( BitVecExpr  t,
bool  signed 
)
inline

Create an integer from the bit-vector argument t .

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

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

The argument must be of bit-vector sort.

Definition at line 1946 of file Context.cs.

1947  {
1948  Contract.Requires(t != null);
1949  Contract.Ensures(Contract.Result<IntExpr>() != null);
1950 
1951  CheckContextMatch(t);
1952  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1953  }

§ MkBVAdd()

BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1405 of file Context.cs.

1406  {
1407  Contract.Requires(t1 != null);
1408  Contract.Requires(t2 != null);
1409  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1410 
1411  CheckContextMatch(t1);
1412  CheckContextMatch(t2);
1413  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1414  }

§ MkBVAddNoOverflow()

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

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

The arguments must be of bit-vector sort.

Definition at line 1961 of file Context.cs.

1962  {
1963  Contract.Requires(t1 != null);
1964  Contract.Requires(t2 != null);
1965  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1966 
1967  CheckContextMatch(t1);
1968  CheckContextMatch(t2);
1969  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1970  }

§ MkBVAddNoUnderflow()

BoolExpr MkBVAddNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1978 of file Context.cs.

1979  {
1980  Contract.Requires(t1 != null);
1981  Contract.Requires(t2 != null);
1982  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1983 
1984  CheckContextMatch(t1);
1985  CheckContextMatch(t2);
1986  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1987  }

§ MkBVAND()

BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1302 of file Context.cs.

1303  {
1304  Contract.Requires(t1 != null);
1305  Contract.Requires(t2 != null);
1306  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1307 
1308  CheckContextMatch(t1);
1309  CheckContextMatch(t2);
1310  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1311  }

§ MkBVASHR()

BitVecExpr MkBVASHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Arithmetic shift right

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

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

The arguments must have a bit-vector sort.

Definition at line 1833 of file Context.cs.

1834  {
1835  Contract.Requires(t1 != null);
1836  Contract.Requires(t2 != null);
1837  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1838 
1839  CheckContextMatch(t1);
1840  CheckContextMatch(t2);
1841  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1842  }

§ MkBVConst() [1/2]

BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 784 of file Context.cs.

785  {
786  Contract.Requires(name != null);
787  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
788 
789  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
790  }
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669

§ MkBVConst() [2/2]

BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 795 of file Context.cs.

796  {
797  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
798 
799  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
800  }
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:235
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669

§ MkBVLSHR()

BitVecExpr MkBVLSHR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Logical shift right

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

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

The arguments must have a bit-vector sort.

Definition at line 1808 of file Context.cs.

1809  {
1810  Contract.Requires(t1 != null);
1811  Contract.Requires(t2 != null);
1812  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1813 
1814  CheckContextMatch(t1);
1815  CheckContextMatch(t2);
1816  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1817  }

§ MkBVMul()

BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1435 of file Context.cs.

1436  {
1437  Contract.Requires(t1 != null);
1438  Contract.Requires(t2 != null);
1439  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1440 
1441  CheckContextMatch(t1);
1442  CheckContextMatch(t2);
1443  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1444  }

§ MkBVMulNoOverflow()

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

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

The arguments must be of bit-vector sort.

Definition at line 2061 of file Context.cs.

2062  {
2063  Contract.Requires(t1 != null);
2064  Contract.Requires(t2 != null);
2065  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2066 
2067  CheckContextMatch(t1);
2068  CheckContextMatch(t2);
2069  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
2070  }

§ MkBVMulNoUnderflow()

BoolExpr MkBVMulNoUnderflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 2078 of file Context.cs.

2079  {
2080  Contract.Requires(t1 != null);
2081  Contract.Requires(t2 != null);
2082  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2083 
2084  CheckContextMatch(t1);
2085  CheckContextMatch(t2);
2086  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
2087  }

§ MkBVNAND()

BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1347 of file Context.cs.

1348  {
1349  Contract.Requires(t1 != null);
1350  Contract.Requires(t2 != null);
1351  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1352 
1353  CheckContextMatch(t1);
1354  CheckContextMatch(t2);
1355  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1356  }

§ MkBVNeg()

BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1392 of file Context.cs.

1393  {
1394  Contract.Requires(t != null);
1395  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1396 
1397  CheckContextMatch(t);
1398  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1399  }

§ MkBVNegNoOverflow()

BoolExpr MkBVNegNoOverflow ( BitVecExpr  t)
inline

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

The arguments must be of bit-vector sort.

Definition at line 2046 of file Context.cs.

2047  {
2048  Contract.Requires(t != null);
2049  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2050 
2051  CheckContextMatch(t);
2052  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
2053  }

§ MkBVNOR()

BitVecExpr MkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1362 of file Context.cs.

1363  {
1364  Contract.Requires(t1 != null);
1365  Contract.Requires(t2 != null);
1366  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1367 
1368  CheckContextMatch(t1);
1369  CheckContextMatch(t2);
1370  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1371  }

§ MkBVNot()

BitVecExpr MkBVNot ( BitVecExpr  t)
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1263 of file Context.cs.

1264  {
1265  Contract.Requires(t != null);
1266  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1267 
1268  CheckContextMatch(t);
1269  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1270  }

§ MkBVOR()

BitVecExpr MkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1317 of file Context.cs.

1318  {
1319  Contract.Requires(t1 != null);
1320  Contract.Requires(t2 != null);
1321  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1322 
1323  CheckContextMatch(t1);
1324  CheckContextMatch(t2);
1325  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1326  }

§ MkBVRedAND()

BitVecExpr MkBVRedAND ( BitVecExpr  t)
inline

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

The argument must have a bit-vector sort.

Definition at line 1276 of file Context.cs.

1277  {
1278  Contract.Requires(t != null);
1279  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1280 
1281  CheckContextMatch(t);
1282  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1283  }

§ MkBVRedOR()

BitVecExpr MkBVRedOR ( BitVecExpr  t)
inline

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

The argument must have a bit-vector sort.

Definition at line 1289 of file Context.cs.

1290  {
1291  Contract.Requires(t != null);
1292  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1293 
1294  CheckContextMatch(t);
1295  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1296  }

§ MkBVRotateLeft() [1/2]

BitVecExpr MkBVRotateLeft ( uint  i,
BitVecExpr  t 
)
inline

Rotate Left.

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

Definition at line 1851 of file Context.cs.

1852  {
1853  Contract.Requires(t != null);
1854  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1855 
1856  CheckContextMatch(t);
1857  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1858  }

§ MkBVRotateLeft() [2/2]

BitVecExpr MkBVRotateLeft ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Left.

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

Definition at line 1883 of file Context.cs.

1884  {
1885  Contract.Requires(t1 != null);
1886  Contract.Requires(t2 != null);
1887  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1888 
1889  CheckContextMatch(t1);
1890  CheckContextMatch(t2);
1891  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1892  }

§ MkBVRotateRight() [1/2]

BitVecExpr MkBVRotateRight ( uint  i,
BitVecExpr  t 
)
inline

Rotate Right.

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

Definition at line 1867 of file Context.cs.

1868  {
1869  Contract.Requires(t != null);
1870  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1871 
1872  CheckContextMatch(t);
1873  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1874  }

§ MkBVRotateRight() [2/2]

BitVecExpr MkBVRotateRight ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Rotate Right.

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

Definition at line 1901 of file Context.cs.

1902  {
1903  Contract.Requires(t1 != null);
1904  Contract.Requires(t2 != null);
1905  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1906 
1907  CheckContextMatch(t1);
1908  CheckContextMatch(t2);
1909  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1910  }

§ MkBVSDiv()

BitVecExpr MkBVSDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed division.

It is defined in the following way:

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

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

Definition at line 1479 of file Context.cs.

1480  {
1481  Contract.Requires(t1 != null);
1482  Contract.Requires(t2 != null);
1483  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1484 
1485  CheckContextMatch(t1);
1486  CheckContextMatch(t2);
1487  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1488  }

§ MkBVSDivNoOverflow()

BoolExpr MkBVSDivNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 2029 of file Context.cs.

2030  {
2031  Contract.Requires(t1 != null);
2032  Contract.Requires(t2 != null);
2033  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2034 
2035  CheckContextMatch(t1);
2036  CheckContextMatch(t2);
2037  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2038  }

§ MkBVSGE()

BoolExpr MkBVSGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1639 of file Context.cs.

1640  {
1641  Contract.Requires(t1 != null);
1642  Contract.Requires(t2 != null);
1643  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1644 
1645  CheckContextMatch(t1);
1646  CheckContextMatch(t2);
1647  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1648  }

§ MkBVSGT()

BoolExpr MkBVSGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1673 of file Context.cs.

1674  {
1675  Contract.Requires(t1 != null);
1676  Contract.Requires(t2 != null);
1677  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1678 
1679  CheckContextMatch(t1);
1680  CheckContextMatch(t2);
1681  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1682  }

§ MkBVSHL()

BitVecExpr MkBVSHL ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Shift left.

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

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

The arguments must have a bit-vector sort.

Definition at line 1785 of file Context.cs.

1786  {
1787  Contract.Requires(t1 != null);
1788  Contract.Requires(t2 != null);
1789  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1790 
1791  CheckContextMatch(t1);
1792  CheckContextMatch(t2);
1793  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1794  }

§ MkBVSLE()

BoolExpr MkBVSLE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must have the same bit-vector sort.

Definition at line 1605 of file Context.cs.

1606  {
1607  Contract.Requires(t1 != null);
1608  Contract.Requires(t2 != null);
1609  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1610 
1611  CheckContextMatch(t1);
1612  CheckContextMatch(t2);
1613  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1614  }

§ MkBVSLT()

BoolExpr MkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement signed less-than

The arguments must have the same bit-vector sort.

Definition at line 1571 of file Context.cs.

1572  {
1573  Contract.Requires(t1 != null);
1574  Contract.Requires(t2 != null);
1575  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1576 
1577  CheckContextMatch(t1);
1578  CheckContextMatch(t2);
1579  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1580  }

§ MkBVSMod()

BitVecExpr MkBVSMod ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

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

Definition at line 1537 of file Context.cs.

1538  {
1539  Contract.Requires(t1 != null);
1540  Contract.Requires(t2 != null);
1541  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1542 
1543  CheckContextMatch(t1);
1544  CheckContextMatch(t2);
1545  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1546  }

§ MkBVSRem()

BitVecExpr MkBVSRem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Signed remainder.

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

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

Definition at line 1519 of file Context.cs.

1520  {
1521  Contract.Requires(t1 != null);
1522  Contract.Requires(t2 != null);
1523  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1524 
1525  CheckContextMatch(t1);
1526  CheckContextMatch(t2);
1527  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1528  }

§ MkBVSub()

BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1420 of file Context.cs.

1421  {
1422  Contract.Requires(t1 != null);
1423  Contract.Requires(t2 != null);
1424  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1425 
1426  CheckContextMatch(t1);
1427  CheckContextMatch(t2);
1428  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1429  }

§ MkBVSubNoOverflow()

BoolExpr MkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

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

The arguments must be of bit-vector sort.

Definition at line 1995 of file Context.cs.

1996  {
1997  Contract.Requires(t1 != null);
1998  Contract.Requires(t2 != null);
1999  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2000 
2001  CheckContextMatch(t1);
2002  CheckContextMatch(t2);
2003  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
2004  }

§ MkBVSubNoUnderflow()

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

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

The arguments must be of bit-vector sort.

Definition at line 2012 of file Context.cs.

2013  {
2014  Contract.Requires(t1 != null);
2015  Contract.Requires(t2 != null);
2016  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2017 
2018  CheckContextMatch(t1);
2019  CheckContextMatch(t2);
2020  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
2021  }

§ MkBVUDiv()

BitVecExpr MkBVUDiv ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned division.

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

Definition at line 1455 of file Context.cs.

1456  {
1457  Contract.Requires(t1 != null);
1458  Contract.Requires(t2 != null);
1459  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1460 
1461  CheckContextMatch(t1);
1462  CheckContextMatch(t2);
1463  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1464  }

§ MkBVUGE()

BoolExpr MkBVUGE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1622 of file Context.cs.

1623  {
1624  Contract.Requires(t1 != null);
1625  Contract.Requires(t2 != null);
1626  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1627 
1628  CheckContextMatch(t1);
1629  CheckContextMatch(t2);
1630  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1631  }

§ MkBVUGT()

BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1656 of file Context.cs.

1657  {
1658  Contract.Requires(t1 != null);
1659  Contract.Requires(t2 != null);
1660  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1661 
1662  CheckContextMatch(t1);
1663  CheckContextMatch(t2);
1664  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1665  }

§ MkBVULE()

BoolExpr MkBVULE ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than or equal to.

The arguments must have the same bit-vector sort.

Definition at line 1588 of file Context.cs.

1589  {
1590  Contract.Requires(t1 != null);
1591  Contract.Requires(t2 != null);
1592  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1593 
1594  CheckContextMatch(t1);
1595  CheckContextMatch(t2);
1596  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1597  }

§ MkBVULT()

BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1554 of file Context.cs.

1555  {
1556  Contract.Requires(t1 != null);
1557  Contract.Requires(t2 != null);
1558  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1559 
1560  CheckContextMatch(t1);
1561  CheckContextMatch(t2);
1562  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1563  }

§ MkBVURem()

BitVecExpr MkBVURem ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned remainder.

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

Definition at line 1498 of file Context.cs.

1499  {
1500  Contract.Requires(t1 != null);
1501  Contract.Requires(t2 != null);
1502  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1503 
1504  CheckContextMatch(t1);
1505  CheckContextMatch(t2);
1506  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1507  }

§ MkBVXNOR()

BitVecExpr MkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1377 of file Context.cs.

1378  {
1379  Contract.Requires(t1 != null);
1380  Contract.Requires(t2 != null);
1381  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1382 
1383  CheckContextMatch(t1);
1384  CheckContextMatch(t2);
1385  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1386  }

§ MkBVXOR()

BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1332 of file Context.cs.

1333  {
1334  Contract.Requires(t1 != null);
1335  Contract.Requires(t2 != null);
1336  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1337 
1338  CheckContextMatch(t1);
1339  CheckContextMatch(t2);
1340  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1341  }

§ MkConcat() [1/3]

BitVecExpr MkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bit-vector concatenation.

The arguments must have a bit-vector sort.

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

Definition at line 1694 of file Context.cs.

1695  {
1696  Contract.Requires(t1 != null);
1697  Contract.Requires(t2 != null);
1698  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1699 
1700  CheckContextMatch(t1);
1701  CheckContextMatch(t2);
1702  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1703  }

§ MkConcat() [2/3]

SeqExpr MkConcat ( params SeqExpr []  t)
inline

Concatentate sequences.

Definition at line 2426 of file Context.cs.

2427  {
2428  Contract.Requires(t != null);
2429  Contract.Requires(Contract.ForAll(t, a => a != null));
2430  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2431 
2432  CheckContextMatch<SeqExpr>(t);
2433  return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2434  }

§ MkConcat() [3/3]

ReExpr MkConcat ( params ReExpr []  t)
inline

Create the concatenation of regular languages.

Definition at line 2590 of file Context.cs.

2591  {
2592  Contract.Requires(t != null);
2593  Contract.Requires(Contract.ForAll(t, a => a != null));
2594  Contract.Ensures(Contract.Result<ReExpr>() != null);
2595 
2596  CheckContextMatch<ReExpr>(t);
2597  return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2598  }

§ MkConst() [1/3]

Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 669 of file Context.cs.

670  {
671  Contract.Requires(name != null);
672  Contract.Requires(range != null);
673  Contract.Ensures(Contract.Result<Expr>() != null);
674 
675  CheckContextMatch(name);
676  CheckContextMatch(range);
677 
678  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
679  }

§ MkConst() [2/3]

Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 684 of file Context.cs.

685  {
686  Contract.Requires(range != null);
687  Contract.Ensures(Contract.Result<Expr>() != null);
688 
689  return MkConst(MkSymbol(name), range);
690  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkConst() [3/3]

Expr MkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 709 of file Context.cs.

710  {
711  Contract.Requires(f != null);
712  Contract.Ensures(Contract.Result<Expr>() != null);
713 
714  return MkApp(f);
715  }
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:807

§ MkConstArray()

ArrayExpr MkConstArray ( Sort  domain,
Expr  v 
)
inline

Create a constant array.

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

See also
MkArraySort, MkSelect

Definition at line 2179 of file Context.cs.

2180  {
2181  Contract.Requires(domain != null);
2182  Contract.Requires(v != null);
2183  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2184 
2185  CheckContextMatch(domain);
2186  CheckContextMatch(v);
2187  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2188  }

§ MkConstDecl() [1/2]

FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 593 of file Context.cs.

594  {
595  Contract.Requires(name != null);
596  Contract.Requires(range != null);
597  Contract.Ensures(Contract.Result<FuncDecl>() != null);
598 
599  CheckContextMatch(name);
600  CheckContextMatch(range);
601  return new FuncDecl(this, name, null, range);
602  }

§ MkConstDecl() [2/2]

FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 607 of file Context.cs.

608  {
609  Contract.Requires(range != null);
610  Contract.Ensures(Contract.Result<FuncDecl>() != null);
611 
612  CheckContextMatch(range);
613  return new FuncDecl(this, MkSymbol(name), null, range);
614  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkConstructor() [1/2]

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

Create a datatype constructor.

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

Definition at line 389 of file Context.cs.

390  {
391  Contract.Requires(name != null);
392  Contract.Requires(recognizer != null);
393  Contract.Ensures(Contract.Result<Constructor>() != null);
394 
395  return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
396  }

§ MkConstructor() [2/2]

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

Create a datatype constructor.

Parameters
name
recognizer
fieldNames
sorts
sortRefs
Returns

Definition at line 407 of file Context.cs.

408  {
409  Contract.Ensures(Contract.Result<Constructor>() != null);
410 
411  return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
412  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkContains()

BoolExpr MkContains ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence containment of s2 in s1.

Definition at line 2474 of file Context.cs.

2475  {
2476  Contract.Requires(s1 != null);
2477  Contract.Requires(s2 != null);
2478  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2479  CheckContextMatch(s1, s2);
2480  return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
2481  }

§ MkDatatypeSort() [1/2]

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

Create a new datatype sort.

Definition at line 417 of file Context.cs.

418  {
419  Contract.Requires(name != null);
420  Contract.Requires(constructors != null);
421  Contract.Requires(Contract.ForAll(constructors, c => c != null));
422 
423  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
424 
425  CheckContextMatch(name);
426  CheckContextMatch<Constructor>(constructors);
427  return new DatatypeSort(this, name, constructors);
428  }

§ MkDatatypeSort() [2/2]

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

Create a new datatype sort.

Definition at line 433 of file Context.cs.

434  {
435  Contract.Requires(constructors != null);
436  Contract.Requires(Contract.ForAll(constructors, c => c != null));
437  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
438 
439  CheckContextMatch<Constructor>(constructors);
440  return new DatatypeSort(this, MkSymbol(name), constructors);
441  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkDatatypeSorts() [1/2]

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

Create mutually recursive datatypes.

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

Definition at line 448 of file Context.cs.

449  {
450  Contract.Requires(names != null);
451  Contract.Requires(c != null);
452  Contract.Requires(names.Length == c.Length);
453  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
454  Contract.Requires(Contract.ForAll(names, name => name != null));
455  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
456 
457  CheckContextMatch<Symbol>(names);
458  uint n = (uint)names.Length;
459  ConstructorList[] cla = new ConstructorList[n];
460  IntPtr[] n_constr = new IntPtr[n];
461  for (uint i = 0; i < n; i++)
462  {
463  Constructor[] constructor = c[i];
464  Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
465  CheckContextMatch<Constructor>(constructor);
466  cla[i] = new ConstructorList(this, constructor);
467  n_constr[i] = cla[i].NativeObject;
468  }
469  IntPtr[] n_res = new IntPtr[n];
470  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
471  DatatypeSort[] res = new DatatypeSort[n];
472  for (uint i = 0; i < n; i++)
473  res[i] = new DatatypeSort(this, n_res[i]);
474  return res;
475  }

§ MkDatatypeSorts() [2/2]

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

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 483 of file Context.cs.

484  {
485  Contract.Requires(names != null);
486  Contract.Requires(c != null);
487  Contract.Requires(names.Length == c.Length);
488  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
489  Contract.Requires(Contract.ForAll(names, name => name != null));
490  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
491 
492  return MkDatatypeSorts(MkSymbols(names), c);
493  }
DatatypeSort [] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:448

§ MkDistinct()

BoolExpr MkDistinct ( params Expr []  args)
inline

Creates a distinct term.

Definition at line 880 of file Context.cs.

881  {
882  Contract.Requires(args != null);
883  Contract.Requires(Contract.ForAll(args, a => a != null));
884 
885  Contract.Ensures(Contract.Result<BoolExpr>() != null);
886 
887  CheckContextMatch<Expr>(args);
888  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
889  }

§ MkDiv()

ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 1099 of file Context.cs.

Referenced by ArithExpr.operator/().

1100  {
1101  Contract.Requires(t1 != null);
1102  Contract.Requires(t2 != null);
1103  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1104 
1105  CheckContextMatch(t1);
1106  CheckContextMatch(t2);
1107  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1108  }

§ MkEmptySeq()

SeqExpr MkEmptySeq ( Sort  s)
inline

Create the empty sequence.

Definition at line 2396 of file Context.cs.

2397  {
2398  Contract.Requires(s != null);
2399  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2400  return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
2401  }

§ MkEmptySet()

ArrayExpr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2260 of file Context.cs.

2261  {
2262  Contract.Requires(domain != null);
2263  Contract.Ensures(Contract.Result<Expr>() != null);
2264 
2265  CheckContextMatch(domain);
2266  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2267  }

§ MkEnumSort() [1/2]

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

Create a new enumeration sort.

Definition at line 297 of file Context.cs.

298  {
299  Contract.Requires(name != null);
300  Contract.Requires(enumNames != null);
301  Contract.Requires(Contract.ForAll(enumNames, f => f != null));
302 
303  Contract.Ensures(Contract.Result<EnumSort>() != null);
304 
305  CheckContextMatch(name);
306  CheckContextMatch<Symbol>(enumNames);
307  return new EnumSort(this, name, enumNames);
308  }
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574

§ MkEnumSort() [2/2]

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

Create a new enumeration sort.

Definition at line 313 of file Context.cs.

314  {
315  Contract.Requires(enumNames != null);
316  Contract.Ensures(Contract.Result<EnumSort>() != null);
317 
318  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
319  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574

§ MkEq()

BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 866 of file Context.cs.

867  {
868  Contract.Requires(x != null);
869  Contract.Requires(y != null);
870  Contract.Ensures(Contract.Result<BoolExpr>() != null);
871 
872  CheckContextMatch(x);
873  CheckContextMatch(y);
874  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
875  }

§ MkExists() [1/2]

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

Create an existential Quantifier.

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

Definition at line 3017 of file Context.cs.

3018  {
3019  Contract.Requires(sorts != null);
3020  Contract.Requires(names != null);
3021  Contract.Requires(body != null);
3022  Contract.Requires(sorts.Length == names.Length);
3023  Contract.Requires(Contract.ForAll(sorts, s => s != null));
3024  Contract.Requires(Contract.ForAll(names, n => n != null));
3025  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3026  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3027  Contract.Ensures(Contract.Result<Quantifier>() != null);
3028 
3029  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3030  }

§ MkExists() [2/2]

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

Create an existential Quantifier.

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

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

Definition at line 3040 of file Context.cs.

3041  {
3042  Contract.Requires(body != null);
3043  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
3044  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3045  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3046  Contract.Ensures(Contract.Result<Quantifier>() != null);
3047 
3048  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3049  }

§ MkExtract() [1/2]

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

Bit-vector extraction.

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

Definition at line 1714 of file Context.cs.

1715  {
1716  Contract.Requires(t != null);
1717  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1718 
1719  CheckContextMatch(t);
1720  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1721  }

§ MkExtract() [2/2]

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

Extract subsequence.

Definition at line 2498 of file Context.cs.

2499  {
2500  Contract.Requires(s != null);
2501  Contract.Requires(offset != null);
2502  Contract.Requires(length != null);
2503  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2504  CheckContextMatch(s, offset, length);
2505  return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
2506  }

§ MkFalse()

BoolExpr MkFalse ( )
inline

The false Term.

Definition at line 846 of file Context.cs.

847  {
848  Contract.Ensures(Contract.Result<BoolExpr>() != null);
849 
850  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
851  }

§ MkFiniteDomainSort() [1/2]

FiniteDomainSort MkFiniteDomainSort ( Symbol  name,
ulong  size 
)
inline

Create a new finite domain sort.

Returns
The result is a sort

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

Definition at line 353 of file Context.cs.

354  {
355  Contract.Requires(name != null);
356  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
357 
358  CheckContextMatch(name);
359  return new FiniteDomainSort(this, name, size);
360  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563

§ MkFiniteDomainSort() [2/2]

FiniteDomainSort MkFiniteDomainSort ( string  name,
ulong  size 
)
inline

Create a new finite domain sort.

Returns
The result is a sort

Elements of the sort are created using

See also
MkNumeral(ulong, Sort)

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

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

Definition at line 370 of file Context.cs.

371  {
372  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
373 
374  return new FiniteDomainSort(this, MkSymbol(name), size);
375  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkFixedpoint()

Fixedpoint MkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3859 of file Context.cs.

3860  {
3861  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3862 
3863  return new Fixedpoint(this);
3864  }

§ MkForall() [1/2]

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

Create a universal Quantifier.

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

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

Definition at line 2973 of file Context.cs.

2974  {
2975  Contract.Requires(sorts != null);
2976  Contract.Requires(names != null);
2977  Contract.Requires(body != null);
2978  Contract.Requires(sorts.Length == names.Length);
2979  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2980  Contract.Requires(Contract.ForAll(names, n => n != null));
2981  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2982  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2983 
2984  Contract.Ensures(Contract.Result<Quantifier>() != null);
2985 
2986  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2987  }

§ MkForall() [2/2]

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

Create a universal Quantifier.

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

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

Definition at line 2998 of file Context.cs.

2999  {
3000  Contract.Requires(body != null);
3001  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
3002  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3003  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3004 
3005  Contract.Ensures(Contract.Result<Quantifier>() != null);
3006 
3007  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3008  }

§ MkFP() [1/6]

FPNum MkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4168 of file Context.cs.

4169  {
4170  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4171  return MkFPNumeral(v, s);
4172  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4109

§ MkFP() [2/6]

FPNum MkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4179 of file Context.cs.

4180  {
4181  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4182  return MkFPNumeral(v, s);
4183  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4109

§ MkFP() [3/6]

FPNum MkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4190 of file Context.cs.

4191  {
4192  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4193  return MkFPNumeral(v, s);
4194  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4109

§ MkFP() [4/6]

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

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

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

Definition at line 4203 of file Context.cs.

4204  {
4205  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4206  return MkFPNumeral(sgn, exp, sig, s);
4207  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4109

§ MkFP() [5/6]

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

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

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

Definition at line 4216 of file Context.cs.

4217  {
4218  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4219  return MkFPNumeral(sgn, exp, sig, s);
4220  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:4109

§ MkFP() [6/6]

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

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

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

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

Definition at line 4508 of file Context.cs.

4509  {
4510  Contract.Ensures(Contract.Result<FPExpr>() != null);
4511  return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4512  }

§ MkFPAbs()

FPExpr MkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term

Definition at line 4229 of file Context.cs.

4230  {
4231  Contract.Ensures(Contract.Result<FPNum>() != null);
4232  return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
4233  }

§ MkFPAdd()

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

Floating-point addition

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

Definition at line 4251 of file Context.cs.

4252  {
4253  Contract.Ensures(Contract.Result<FPNum>() != null);
4254  return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4255  }

§ MkFPDiv()

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

Floating-point division

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

Definition at line 4287 of file Context.cs.

4288  {
4289  Contract.Ensures(Contract.Result<FPNum>() != null);
4290  return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4291  }

§ MkFPEq()

BoolExpr MkFPEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point equality.

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

Parameters
t1floating-point term
t2floating-point term

Definition at line 4417 of file Context.cs.

4418  {
4419  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4420  return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4421  }

§ MkFPFMA()

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

Floating-point fused multiply-add

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

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

Definition at line 4303 of file Context.cs.

4304  {
4305  Contract.Ensures(Contract.Result<FPNum>() != null);
4306  return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
4307  }

§ MkFPGEq()

BoolExpr MkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4392 of file Context.cs.

4393  {
4394  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4395  return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4396  }

§ MkFPGt()

BoolExpr MkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4403 of file Context.cs.

4404  {
4405  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4406  return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4407  }

§ MkFPInf()

FPNum MkFPInf ( FPSort  s,
bool  negative 
)
inline

Create a floating-point infinity of sort s.

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

Definition at line 4087 of file Context.cs.

4088  {
4089  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4090  return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
4091  }

§ MkFPIsInfinite()

BoolExpr MkFPIsInfinite ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4457 of file Context.cs.

4458  {
4459  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4460  return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4461  }

§ MkFPIsNaN()

BoolExpr MkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term

Definition at line 4467 of file Context.cs.

4468  {
4469  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4470  return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4471  }

§ MkFPIsNegative()

BoolExpr MkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4477 of file Context.cs.

4478  {
4479  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4480  return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4481  }

§ MkFPIsNormal()

BoolExpr MkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4427 of file Context.cs.

4428  {
4429  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4430  return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4431  }

§ MkFPIsPositive()

BoolExpr MkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4487 of file Context.cs.

4488  {
4489  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4490  return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4491  }

§ MkFPIsSubnormal()

BoolExpr MkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4437 of file Context.cs.

4438  {
4439  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4440  return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4441  }

§ MkFPIsZero()

BoolExpr MkFPIsZero ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4447 of file Context.cs.

4448  {
4449  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4450  return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4451  }

§ MkFPLEq()

BoolExpr MkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4370 of file Context.cs.

4371  {
4372  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4373  return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
4374  }

§ MkFPLt()

BoolExpr MkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4381 of file Context.cs.

4382  {
4383  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4384  return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4385  }

§ MkFPMax()

FPExpr MkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4359 of file Context.cs.

4360  {
4361  Contract.Ensures(Contract.Result<FPNum>() != null);
4362  return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
4363  }

§ MkFPMin()

FPExpr MkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4348 of file Context.cs.

4349  {
4350  Contract.Ensures(Contract.Result<FPNum>() != null);
4351  return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
4352  }

§ MkFPMul()

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

Floating-point multiplication

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

Definition at line 4275 of file Context.cs.

4276  {
4277  Contract.Ensures(Contract.Result<FPNum>() != null);
4278  return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4279  }

§ MkFPNaN()

FPNum MkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.

Definition at line 4076 of file Context.cs.

4077  {
4078  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4079  return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
4080  }

§ MkFPNeg()

FPExpr MkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term

Definition at line 4239 of file Context.cs.

4240  {
4241  Contract.Ensures(Contract.Result<FPNum>() != null);
4242  return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
4243  }

§ MkFPNumeral() [1/5]

FPNum MkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4109 of file Context.cs.

4110  {
4111  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4112  return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
4113  }

§ MkFPNumeral() [2/5]

FPNum MkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4120 of file Context.cs.

4121  {
4122  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4123  return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
4124  }

§ MkFPNumeral() [3/5]

FPNum MkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 4131 of file Context.cs.

4132  {
4133  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4134  return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
4135  }

§ MkFPNumeral() [4/5]

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

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

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

Definition at line 4144 of file Context.cs.

4145  {
4146  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4147  return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
4148  }

§ MkFPNumeral() [5/5]

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

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

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

Definition at line 4157 of file Context.cs.

4158  {
4159  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4160  return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
4161  }

§ MkFPRem()

FPExpr MkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term

Definition at line 4325 of file Context.cs.

4326  {
4327  Contract.Ensures(Contract.Result<FPNum>() != null);
4328  return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
4329  }

§ MkFPRNA()

FPRMNum MkFPRNA ( )
inline

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

Definition at line 3924 of file Context.cs.

3925  {
3926  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3927  return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
3928  }

§ MkFPRNE()

FPRMNum MkFPRNE ( )
inline

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

Definition at line 3906 of file Context.cs.

3907  {
3908  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3909  return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
3910  }

§ MkFPRoundingModeSort()

FPRMSort MkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Definition at line 3886 of file Context.cs.

3887  {
3888  Contract.Ensures(Contract.Result<FPRMSort>() != null);
3889  return new FPRMSort(this);
3890  }

§ MkFPRoundNearestTiesToAway()

FPRMNum MkFPRoundNearestTiesToAway ( )
inline

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

Definition at line 3915 of file Context.cs.

3916  {
3917  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3918  return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3919  }

§ MkFPRoundNearestTiesToEven()

FPRMExpr MkFPRoundNearestTiesToEven ( )
inline

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

Definition at line 3897 of file Context.cs.

3898  {
3899  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3900  return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3901  }

§ MkFPRoundToIntegral()

FPExpr MkFPRoundToIntegral ( FPRMExpr  rm,
FPExpr  t 
)
inline

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

Parameters
rmterm of RoundingMode sort
tfloating-point term

Definition at line 4337 of file Context.cs.

4338  {
4339  Contract.Ensures(Contract.Result<FPNum>() != null);
4340  return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
4341  }

§ MkFPRoundTowardNegative()

FPRMNum MkFPRoundTowardNegative ( )
inline

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

Definition at line 3951 of file Context.cs.

3952  {
3953  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3954  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3955  }

§ MkFPRoundTowardPositive()

FPRMNum MkFPRoundTowardPositive ( )
inline

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

Definition at line 3933 of file Context.cs.

3934  {
3935  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3936  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3937  }

§ MkFPRoundTowardZero()

FPRMNum MkFPRoundTowardZero ( )
inline

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

Definition at line 3969 of file Context.cs.

3970  {
3971  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3972  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3973  }

§ MkFPRTN()

FPRMNum MkFPRTN ( )
inline

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

Definition at line 3960 of file Context.cs.

3961  {
3962  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3963  return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
3964  }

§ MkFPRTP()

FPRMNum MkFPRTP ( )
inline

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

Definition at line 3942 of file Context.cs.

3943  {
3944  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3945  return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
3946  }

§ MkFPRTZ()

FPRMNum MkFPRTZ ( )
inline

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

Definition at line 3978 of file Context.cs.

3979  {
3980  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3981  return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
3982  }

§ MkFPSort()

FPSort MkFPSort ( uint  ebits,
uint  sbits 
)
inline

Create a FloatingPoint sort.

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

Definition at line 3992 of file Context.cs.

3993  {
3994  Contract.Ensures(Contract.Result<FPSort>() != null);
3995  return new FPSort(this, ebits, sbits);
3996  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSort128()

FPSort MkFPSort128 ( )
inline

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

Definition at line 4064 of file Context.cs.

4065  {
4066  Contract.Ensures(Contract.Result<FPSort>() != null);
4067  return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
4068  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSort16()

FPSort MkFPSort16 ( )
inline

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

Definition at line 4010 of file Context.cs.

4011  {
4012  Contract.Ensures(Contract.Result<FPSort>() != null);
4013  return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
4014  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSort32()

FPSort MkFPSort32 ( )
inline

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

Definition at line 4028 of file Context.cs.

4029  {
4030  Contract.Ensures(Contract.Result<FPSort>() != null);
4031  return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
4032  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSort64()

FPSort MkFPSort64 ( )
inline

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

Definition at line 4046 of file Context.cs.

4047  {
4048  Contract.Ensures(Contract.Result<FPSort>() != null);
4049  return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
4050  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSortDouble()

FPSort MkFPSortDouble ( )
inline

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

Definition at line 4037 of file Context.cs.

4038  {
4039  Contract.Ensures(Contract.Result<FPSort>() != null);
4040  return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
4041  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSortHalf()

FPSort MkFPSortHalf ( )
inline

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

Definition at line 4001 of file Context.cs.

4002  {
4003  Contract.Ensures(Contract.Result<FPSort>() != null);
4004  return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
4005  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSortQuadruple()

FPSort MkFPSortQuadruple ( )
inline

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

Definition at line 4055 of file Context.cs.

4056  {
4057  Contract.Ensures(Contract.Result<FPSort>() != null);
4058  return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
4059  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSortSingle()

FPSort MkFPSortSingle ( )
inline

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

Definition at line 4019 of file Context.cs.

4020  {
4021  Contract.Ensures(Contract.Result<FPSort>() != null);
4022  return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
4023  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556

§ MkFPSqrt()

FPExpr MkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term

Definition at line 4314 of file Context.cs.

4315  {
4316  Contract.Ensures(Contract.Result<FPNum>() != null);
4317  return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
4318  }

§ MkFPSub()

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

Floating-point subtraction

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

Definition at line 4263 of file Context.cs.

4264  {
4265  Contract.Ensures(Contract.Result<FPNum>() != null);
4266  return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
4267  }

§ MkFPToBV()

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

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

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

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

Definition at line 4617 of file Context.cs.

4618  {
4619  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4620  if (signed)
4621  return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4622  else
4623  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4624  }

§ MkFPToFP() [1/6]

FPExpr MkFPToFP ( BitVecExpr  bv,
FPSort  s 
)
inline

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

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

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

Definition at line 4525 of file Context.cs.

4526  {
4527  Contract.Ensures(Contract.Result<FPExpr>() != null);
4528  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4529  }

§ MkFPToFP() [2/6]

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

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

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

Parameters
rmRoundingMode term.
tFloatingPoint term.
sFloatingPoint sort.

Definition at line 4542 of file Context.cs.

4543  {
4544  Contract.Ensures(Contract.Result<FPExpr>() != null);
4545  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4546  }

§ MkFPToFP() [3/6]

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

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

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

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

Definition at line 4559 of file Context.cs.

4560  {
4561  Contract.Ensures(Contract.Result<FPExpr>() != null);
4562  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4563  }

§ MkFPToFP() [4/6]

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

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

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

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

Definition at line 4578 of file Context.cs.

4579  {
4580  Contract.Ensures(Contract.Result<FPExpr>() != null);
4581  if (signed)
4582  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4583  else
4584  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4585  }

§ MkFPToFP() [5/6]

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

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

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

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

Definition at line 4597 of file Context.cs.

4598  {
4599  Contract.Ensures(Contract.Result<FPExpr>() != null);
4600  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4601  }

§ MkFPToFP() [6/6]

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

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

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

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

Definition at line 4671 of file Context.cs.

4672  {
4673  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4674  return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4675  }

§ MkFPToIEEEBV()

BitVecExpr MkFPToIEEEBV ( FPExpr  t)
inline

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

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

Parameters
tFloatingPoint term.

Definition at line 4653 of file Context.cs.

4654  {
4655  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4656  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4657  }

§ MkFPToReal()

RealExpr MkFPToReal ( FPExpr  t)
inline

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

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

Parameters
tFloatingPoint term

Definition at line 4635 of file Context.cs.

4636  {
4637  Contract.Ensures(Contract.Result<RealExpr>() != null);
4638  return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4639  }

§ MkFPZero()

FPNum MkFPZero ( FPSort  s,
bool  negative 
)
inline

Create a floating-point zero of sort s.

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

Definition at line 4098 of file Context.cs.

4099  {
4100  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
4101  return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
4102  }

§ MkFreshConst()

Expr MkFreshConst ( string  prefix,
Sort  range 
)
inline

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

Definition at line 696 of file Context.cs.

697  {
698  Contract.Requires(range != null);
699  Contract.Ensures(Contract.Result<Expr>() != null);
700 
701  CheckContextMatch(range);
702  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
703  }

§ MkFreshConstDecl()

FuncDecl MkFreshConstDecl ( string  prefix,
Sort  range 
)
inline

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

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

Definition at line 621 of file Context.cs.

622  {
623  Contract.Requires(range != null);
624  Contract.Ensures(Contract.Result<FuncDecl>() != null);
625 
626  CheckContextMatch(range);
627  return new FuncDecl(this, prefix, null, range);
628  }

§ MkFreshFuncDecl()

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

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

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

Definition at line 579 of file Context.cs.

580  {
581  Contract.Requires(range != null);
582  Contract.Requires(Contract.ForAll(domain, d => d != null));
583  Contract.Ensures(Contract.Result<FuncDecl>() != null);
584 
585  CheckContextMatch<Sort>(domain);
586  CheckContextMatch(range);
587  return new FuncDecl(this, prefix, domain, range);
588  }

§ MkFullSet()

ArrayExpr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2272 of file Context.cs.

2273  {
2274  Contract.Requires(domain != null);
2275  Contract.Ensures(Contract.Result<Expr>() != null);
2276 
2277  CheckContextMatch(domain);
2278  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2279  }

§ MkFuncDecl() [1/4]

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

Creates a new function declaration.

Definition at line 515 of file Context.cs.

516  {
517  Contract.Requires(name != null);
518  Contract.Requires(range != null);
519  Contract.Requires(Contract.ForAll(domain, d => d != null));
520  Contract.Ensures(Contract.Result<FuncDecl>() != null);
521 
522  CheckContextMatch(name);
523  CheckContextMatch<Sort>(domain);
524  CheckContextMatch(range);
525  return new FuncDecl(this, name, domain, range);
526  }

§ MkFuncDecl() [2/4]

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

Creates a new function declaration.

Definition at line 531 of file Context.cs.

532  {
533  Contract.Requires(name != null);
534  Contract.Requires(domain != null);
535  Contract.Requires(range != null);
536  Contract.Ensures(Contract.Result<FuncDecl>() != null);
537 
538  CheckContextMatch(name);
539  CheckContextMatch(domain);
540  CheckContextMatch(range);
541  Sort[] q = new Sort[] { domain };
542  return new FuncDecl(this, name, q, range);
543  }

§ MkFuncDecl() [3/4]

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

Creates a new function declaration.

Definition at line 548 of file Context.cs.

549  {
550  Contract.Requires(range != null);
551  Contract.Requires(Contract.ForAll(domain, d => d != null));
552  Contract.Ensures(Contract.Result<FuncDecl>() != null);
553 
554  CheckContextMatch<Sort>(domain);
555  CheckContextMatch(range);
556  return new FuncDecl(this, MkSymbol(name), domain, range);
557  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkFuncDecl() [4/4]

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

Creates a new function declaration.

Definition at line 562 of file Context.cs.

563  {
564  Contract.Requires(range != null);
565  Contract.Requires(domain != null);
566  Contract.Ensures(Contract.Result<FuncDecl>() != null);
567 
568  CheckContextMatch(domain);
569  CheckContextMatch(range);
570  Sort[] q = new Sort[] { domain };
571  return new FuncDecl(this, MkSymbol(name), q, range);
572  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkGe()

BoolExpr MkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 >= t2

Definition at line 1199 of file Context.cs.

Referenced by ArithExpr.operator>=().

1200  {
1201  Contract.Requires(t1 != null);
1202  Contract.Requires(t2 != null);
1203  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1204 
1205  CheckContextMatch(t1);
1206  CheckContextMatch(t2);
1207  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1208  }

§ MkGoal()

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

Creates a new Goal.

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

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

Definition at line 3324 of file Context.cs.

3325  {
3326  Contract.Ensures(Contract.Result<Goal>() != null);
3327 
3328  return new Goal(this, models, unsatCores, proofs);
3329  }

§ MkGt()

BoolExpr MkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 > t2

Definition at line 1185 of file Context.cs.

Referenced by ArithExpr.operator>().

1186  {
1187  Contract.Requires(t1 != null);
1188  Contract.Requires(t2 != null);
1189  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1190 
1191  CheckContextMatch(t1);
1192  CheckContextMatch(t2);
1193  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1194  }

§ MkIff()

BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 925 of file Context.cs.

926  {
927  Contract.Requires(t1 != null);
928  Contract.Requires(t2 != null);
929  Contract.Ensures(Contract.Result<BoolExpr>() != null);
930 
931  CheckContextMatch(t1);
932  CheckContextMatch(t2);
933  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
934  }

§ MkImplies()

BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 939 of file Context.cs.

940  {
941  Contract.Requires(t1 != null);
942  Contract.Requires(t2 != null);
943  Contract.Ensures(Contract.Result<BoolExpr>() != null);
944 
945  CheckContextMatch(t1);
946  CheckContextMatch(t2);
947  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
948  }

§ MkIndexOf()

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

Extract index of sub-string starting at offset.

Definition at line 2511 of file Context.cs.

2512  {
2513  Contract.Requires(s != null);
2514  Contract.Requires(offset != null);
2515  Contract.Requires(substr != null);
2516  Contract.Ensures(Contract.Result<IntExpr>() != null);
2517  CheckContextMatch(s, substr, offset);
2518  return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
2519  }

§ MkInRe()

BoolExpr MkInRe ( SeqExpr  s,
ReExpr  re 
)
inline

Check for regular expression membership.

Definition at line 2548 of file Context.cs.

2549  {
2550  Contract.Requires(s != null);
2551  Contract.Requires(re != null);
2552  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2553  CheckContextMatch(s, re);
2554  return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
2555  }

§ MkInt() [1/5]

IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2828 of file Context.cs.

2829  {
2830  Contract.Ensures(Contract.Result<IntNum>() != null);
2831 
2832  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2833  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147

§ MkInt() [2/5]

IntNum MkInt ( int  v)
inline

Create an integer numeral.

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

Definition at line 2840 of file Context.cs.

2841  {
2842  Contract.Ensures(Contract.Result<IntNum>() != null);
2843 
2844  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2845  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147

§ MkInt() [3/5]

IntNum MkInt ( uint  v)
inline

Create an integer numeral.

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

Definition at line 2852 of file Context.cs.

2853  {
2854  Contract.Ensures(Contract.Result<IntNum>() != null);
2855 
2856  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2857  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147

§ MkInt() [4/5]

IntNum MkInt ( long  v)
inline

Create an integer numeral.

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

Definition at line 2864 of file Context.cs.

2865  {
2866  Contract.Ensures(Contract.Result<IntNum>() != null);
2867 
2868  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2869  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147

§ MkInt() [5/5]

IntNum MkInt ( ulong  v)
inline

Create an integer numeral.

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

Definition at line 2876 of file Context.cs.

2877  {
2878  Contract.Ensures(Contract.Result<IntNum>() != null);
2879 
2880  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2881  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147

§ MkInt2BV()

BitVecExpr MkInt2BV ( uint  n,
IntExpr  t 
)
inline

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

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

The argument must be of integer sort.

Definition at line 1922 of file Context.cs.

1923  {
1924  Contract.Requires(t != null);
1925  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1926 
1927  CheckContextMatch(t);
1928  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1929  }

§ MkInt2Real()

RealExpr MkInt2Real ( IntExpr  t)
inline

Coerce an integer to a real.

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

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

Definition at line 1220 of file Context.cs.

1221  {
1222  Contract.Requires(t != null);
1223  Contract.Ensures(Contract.Result<RealExpr>() != null);
1224 
1225  CheckContextMatch(t);
1226  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1227  }

§ MkIntConst() [1/2]

IntExpr MkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 741 of file Context.cs.

742  {
743  Contract.Requires(name != null);
744  Contract.Ensures(Contract.Result<IntExpr>() != null);
745 
746  return (IntExpr)MkConst(name, IntSort);
747  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669

§ MkIntConst() [2/2]

IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 752 of file Context.cs.

753  {
754  Contract.Requires(name != null);
755  Contract.Ensures(Contract.Result<IntExpr>() != null);
756 
757  return (IntExpr)MkConst(name, IntSort);
758  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669

§ MkIntSort()

IntSort MkIntSort ( )
inline

Create a new integer sort.

Definition at line 216 of file Context.cs.

217  {
218  Contract.Ensures(Contract.Result<IntSort>() != null);
219 
220  return new IntSort(this);
221  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:147

§ MkIsInteger()

BoolExpr MkIsInteger ( RealExpr  t)
inline

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

Definition at line 1248 of file Context.cs.

1249  {
1250  Contract.Requires(t != null);
1251  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1252 
1253  CheckContextMatch(t);
1254  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1255  }

§ MkITE()

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

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

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

Definition at line 909 of file Context.cs.

910  {
911  Contract.Requires(t1 != null);
912  Contract.Requires(t2 != null);
913  Contract.Requires(t3 != null);
914  Contract.Ensures(Contract.Result<Expr>() != null);
915 
916  CheckContextMatch(t1);
917  CheckContextMatch(t2);
918  CheckContextMatch(t3);
919  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
920  }

§ MkLe()

BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1171 of file Context.cs.

Referenced by ArithExpr.operator<=().

1172  {
1173  Contract.Requires(t1 != null);
1174  Contract.Requires(t2 != null);
1175  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1176 
1177  CheckContextMatch(t1);
1178  CheckContextMatch(t2);
1179  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1180  }

§ MkLength()

IntExpr MkLength ( SeqExpr  s)
inline

Retrieve the length of a given sequence.

Definition at line 2440 of file Context.cs.

2441  {
2442  Contract.Requires(s != null);
2443  Contract.Ensures(Contract.Result<IntExpr>() != null);
2444  return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
2445  }

§ MkListSort() [1/2]

ListSort MkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 324 of file Context.cs.

325  {
326  Contract.Requires(name != null);
327  Contract.Requires(elemSort != null);
328  Contract.Ensures(Contract.Result<ListSort>() != null);
329 
330  CheckContextMatch(name);
331  CheckContextMatch(elemSort);
332  return new ListSort(this, name, elemSort);
333  }

§ MkListSort() [2/2]

ListSort MkListSort ( string  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 338 of file Context.cs.

339  {
340  Contract.Requires(elemSort != null);
341  Contract.Ensures(Contract.Result<ListSort>() != null);
342 
343  CheckContextMatch(elemSort);
344  return new ListSort(this, MkSymbol(name), elemSort);
345  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkLt()

BoolExpr MkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 < t2

Definition at line 1157 of file Context.cs.

Referenced by ArithExpr.operator<().

1158  {
1159  Contract.Requires(t1 != null);
1160  Contract.Requires(t2 != null);
1161  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1162 
1163  CheckContextMatch(t1);
1164  CheckContextMatch(t2);
1165  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1166  }

§ MkMap()

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

Maps f on the argument arrays.

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

See also
MkArraySort, MkSelect, MkStore

Definition at line 2201 of file Context.cs.

2202  {
2203  Contract.Requires(f != null);
2204  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2205  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2206 
2207  CheckContextMatch(f);
2208  CheckContextMatch<ArrayExpr>(args);
2209  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2210  }

§ MkMod()

IntExpr MkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 1114 of file Context.cs.

1115  {
1116  Contract.Requires(t1 != null);
1117  Contract.Requires(t2 != null);
1118  Contract.Ensures(Contract.Result<IntExpr>() != null);
1119 
1120  CheckContextMatch(t1);
1121  CheckContextMatch(t2);
1122  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1123  }

§ MkMul() [1/2]

ArithExpr MkMul ( params ArithExpr []  t)
inline

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

Definition at line 1048 of file Context.cs.

Referenced by ArithExpr.operator*().

1049  {
1050  Contract.Requires(t != null);
1051  Contract.Requires(Contract.ForAll(t, a => a != null));
1052  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1053 
1054  CheckContextMatch<ArithExpr>(t);
1055  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1056  }

§ MkMul() [2/2]

ArithExpr MkMul ( IEnumerable< ArithExpr t)
inline

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

Definition at line 1061 of file Context.cs.

1062  {
1063  Contract.Requires(t != null);
1064  Contract.Requires(Contract.ForAll(t, a => a != null));
1065  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1066 
1067  CheckContextMatch<ArithExpr>(t);
1068  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1069  }

§ MkNot()

BoolExpr MkNot ( BoolExpr  a)
inline

Mk an expression representing not(a).

Definition at line 894 of file Context.cs.

Referenced by BoolExpr.operator!().

895  {
896  Contract.Requires(a != null);
897  Contract.Ensures(Contract.Result<BoolExpr>() != null);
898 
899  CheckContextMatch(a);
900  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
901  }

§ MkNumeral() [1/5]

Expr MkNumeral ( string  v,
Sort  ty 
)
inline

Create a Term of a given sort.

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

Definition at line 2669 of file Context.cs.

2670  {
2671  Contract.Requires(ty != null);
2672  Contract.Ensures(Contract.Result<Expr>() != null);
2673 
2674  CheckContextMatch(ty);
2675  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2676  }

§ MkNumeral() [2/5]

Expr MkNumeral ( int  v,
Sort  ty 
)
inline

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

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

Definition at line 2685 of file Context.cs.

2686  {
2687  Contract.Requires(ty != null);
2688  Contract.Ensures(Contract.Result<Expr>() != null);
2689 
2690  CheckContextMatch(ty);
2691  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2692  }

§ MkNumeral() [3/5]

Expr MkNumeral ( uint  v,
Sort  ty 
)
inline

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

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

Definition at line 2701 of file Context.cs.

2702  {
2703  Contract.Requires(ty != null);
2704  Contract.Ensures(Contract.Result<Expr>() != null);
2705 
2706  CheckContextMatch(ty);
2707  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2708  }

§ MkNumeral() [4/5]

Expr MkNumeral ( long  v,
Sort  ty 
)
inline

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

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

Definition at line 2717 of file Context.cs.

2718  {
2719  Contract.Requires(ty != null);
2720  Contract.Ensures(Contract.Result<Expr>() != null);
2721 
2722  CheckContextMatch(ty);
2723  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2724  }

§ MkNumeral() [5/5]

Expr MkNumeral ( ulong  v,
Sort  ty 
)
inline

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

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

Definition at line 2733 of file Context.cs.

2734  {
2735  Contract.Requires(ty != null);
2736  Contract.Ensures(Contract.Result<Expr>() != null);
2737 
2738  CheckContextMatch(ty);
2739  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2740  }

§ MkOptimize()

Optimize MkOptimize ( )
inline

Create an Optimization context.

Definition at line 3871 of file Context.cs.

3872  {
3873  Contract.Ensures(Contract.Result<Optimize>() != null);
3874 
3875  return new Optimize(this);
3876  }

§ MkOr() [1/2]

BoolExpr MkOr ( params BoolExpr []  t)
inline

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

Definition at line 992 of file Context.cs.

993  {
994  Contract.Requires(t != null);
995  Contract.Requires(Contract.ForAll(t, a => a != null));
996  Contract.Ensures(Contract.Result<BoolExpr>() != null);
997 
998  CheckContextMatch<BoolExpr>(t);
999  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1000  }

§ MkOr() [2/2]

BoolExpr MkOr ( IEnumerable< BoolExpr t)
inline

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

Definition at line 1006 of file Context.cs.

1007  {
1008  Contract.Requires(t != null);
1009  Contract.Requires(Contract.ForAll(t, a => a != null));
1010  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1011 
1012  CheckContextMatch(t);
1013  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
1014  }

§ MkParams()

Params MkParams ( )
inline

Creates a new ParameterSet.

Definition at line 3336 of file Context.cs.

3337  {
3338  Contract.Ensures(Contract.Result<Params>() != null);
3339 
3340  return new Params(this);
3341  }

§ MkPattern()

Pattern MkPattern ( params Expr []  terms)
inline

Create a quantifier pattern.

Definition at line 650 of file Context.cs.

651  {
652  Contract.Requires(terms != null);
653  if (terms.Length == 0)
654  throw new Z3Exception("Cannot create a pattern from zero terms");
655 
656  Contract.Ensures(Contract.Result<Pattern>() != null);
657 
658  Contract.EndContractBlock();
659 
660  IntPtr[] termsNative = AST.ArrayToNative(terms);
661  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
662  }

§ MkPBEq()

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

Create a pseudo-Boolean equal constraint.

Definition at line 2647 of file Context.cs.

2648  {
2649  Contract.Requires(args != null);
2650  Contract.Requires(coeffs != null);
2651  Contract.Requires(args.Length == coeffs.Length);
2652  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2653  CheckContextMatch<BoolExpr>(args);
2654  return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
2655  AST.ArrayToNative(args),
2656  coeffs, k));
2657  }

§ MkPBLe()

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

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

Definition at line 2632 of file Context.cs.

2633  {
2634  Contract.Requires(args != null);
2635  Contract.Requires(coeffs != null);
2636  Contract.Requires(args.Length == coeffs.Length);
2637  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2638  CheckContextMatch<BoolExpr>(args);
2639  return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2640  AST.ArrayToNative(args),
2641  coeffs, k));
2642  }

§ MkPower()

ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 1143 of file Context.cs.

1144  {
1145  Contract.Requires(t1 != null);
1146  Contract.Requires(t2 != null);
1147  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1148 
1149  CheckContextMatch(t1);
1150  CheckContextMatch(t2);
1151  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1152  }

§ MkPrefixOf()

BoolExpr MkPrefixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence prefix.

Definition at line 2450 of file Context.cs.

2451  {
2452  Contract.Requires(s1 != null);
2453  Contract.Requires(s2 != null);
2454  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2455  CheckContextMatch(s1, s2);
2456  return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
2457  }

§ MkProbe()

Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3663 of file Context.cs.

3664  {
3665  Contract.Ensures(Contract.Result<Probe>() != null);
3666 
3667  return new Probe(this, name);
3668  }

§ MkQuantifier() [1/2]

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

Create a Quantifier.

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

Definition at line 3056 of file Context.cs.

3057  {
3058  Contract.Requires(body != null);
3059  Contract.Requires(names != null);
3060  Contract.Requires(sorts != null);
3061  Contract.Requires(sorts.Length == names.Length);
3062  Contract.Requires(Contract.ForAll(sorts, s => s != null));
3063  Contract.Requires(Contract.ForAll(names, n => n != null));
3064  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3065  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3066 
3067  Contract.Ensures(Contract.Result<Quantifier>() != null);
3068 
3069  if (universal)
3070  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3071  else
3072  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
3073  }
Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a universal Quantifier.
Definition: Context.cs:2973
Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create an existential Quantifier.
Definition: Context.cs:3017

§ MkQuantifier() [2/2]

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

Create a Quantifier.

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

Definition at line 3080 of file Context.cs.

3081  {
3082  Contract.Requires(body != null);
3083  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
3084  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
3085  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
3086 
3087  Contract.Ensures(Contract.Result<Quantifier>() != null);
3088 
3089  if (universal)
3090  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3091  else
3092  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
3093  }
Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create a universal Quantifier.
Definition: Context.cs:2973
Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
Create an existential Quantifier.
Definition: Context.cs:3017

§ MkReal() [1/6]

RatNum MkReal ( int  num,
int  den 
)
inline

Create a real from a fraction.

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

Definition at line 2751 of file Context.cs.

2752  {
2753  if (den == 0)
2754  throw new Z3Exception("Denominator is zero");
2755 
2756  Contract.Ensures(Contract.Result<RatNum>() != null);
2757  Contract.EndContractBlock();
2758 
2759  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2760  }

§ MkReal() [2/6]

RatNum MkReal ( string  v)
inline

Create a real numeral.

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

Definition at line 2767 of file Context.cs.

2768  {
2769  Contract.Ensures(Contract.Result<RatNum>() != null);
2770 
2771  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2772  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkReal() [3/6]

RatNum MkReal ( int  v)
inline

Create a real numeral.

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

Definition at line 2779 of file Context.cs.

2780  {
2781  Contract.Ensures(Contract.Result<RatNum>() != null);
2782 
2783  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2784  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkReal() [4/6]

RatNum MkReal ( uint  v)
inline

Create a real numeral.

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

Definition at line 2791 of file Context.cs.

2792  {
2793  Contract.Ensures(Contract.Result<RatNum>() != null);
2794 
2795  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2796  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkReal() [5/6]

RatNum MkReal ( long  v)
inline

Create a real numeral.

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

Definition at line 2803 of file Context.cs.

2804  {
2805  Contract.Ensures(Contract.Result<RatNum>() != null);
2806 
2807  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2808  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkReal() [6/6]

RatNum MkReal ( ulong  v)
inline

Create a real numeral.

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

Definition at line 2815 of file Context.cs.

2816  {
2817  Contract.Ensures(Contract.Result<RatNum>() != null);
2818 
2819  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2820  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkReal2Int()

IntExpr MkReal2Int ( RealExpr  t)
inline

Coerce a real to an integer.

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

Definition at line 1236 of file Context.cs.

1237  {
1238  Contract.Requires(t != null);
1239  Contract.Ensures(Contract.Result<IntExpr>() != null);
1240 
1241  CheckContextMatch(t);
1242  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1243  }

§ MkRealConst() [1/2]

RealExpr MkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 763 of file Context.cs.

764  {
765  Contract.Requires(name != null);
766  Contract.Ensures(Contract.Result<RealExpr>() != null);
767 
768  return (RealExpr)MkConst(name, RealSort);
769  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkRealConst() [2/2]

RealExpr MkRealConst ( string  name)
inline

Creates a real constant.

Definition at line 774 of file Context.cs.

775  {
776  Contract.Ensures(Contract.Result<RealExpr>() != null);
777 
778  return (RealExpr)MkConst(name, RealSort);
779  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:669
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkRealSort()

RealSort MkRealSort ( )
inline

Create a real sort.

Definition at line 226 of file Context.cs.

227  {
228  Contract.Ensures(Contract.Result<RealSort>() != null);
229  return new RealSort(this);
230  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:160

§ MkRem()

IntExpr MkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 1129 of file Context.cs.

1130  {
1131  Contract.Requires(t1 != null);
1132  Contract.Requires(t2 != null);
1133  Contract.Ensures(Contract.Result<IntExpr>() != null);
1134 
1135  CheckContextMatch(t1);
1136  CheckContextMatch(t2);
1137  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1138  }

§ MkRepeat()

BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1764 of file Context.cs.

1765  {
1766  Contract.Requires(t != null);
1767  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1768 
1769  CheckContextMatch(t);
1770  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1771  }

§ MkReplace()

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

Replace the first occurrence of src by dst in s.

Definition at line 2524 of file Context.cs.

2525  {
2526  Contract.Requires(s != null);
2527  Contract.Requires(src != null);
2528  Contract.Requires(dst != null);
2529  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2530  CheckContextMatch(s, src, dst);
2531  return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
2532  }

§ MkReSort()

ReSort MkReSort ( SeqSort  s)
inline

Create a new regular expression sort.

Definition at line 256 of file Context.cs.

257  {
258  Contract.Requires(s != null);
259  Contract.Ensures(Contract.Result<ReSort>() != null);
260  return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
261  }
def ReSort(s)
Definition: z3py.py:9584

§ MkSelect()

Expr MkSelect ( ArrayExpr  a,
Expr  i 
)
inline

Array read.

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

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

See also
MkArraySort, MkStore

Definition at line 2129 of file Context.cs.

2130  {
2131  Contract.Requires(a != null);
2132  Contract.Requires(i != null);
2133  Contract.Ensures(Contract.Result<Expr>() != null);
2134 
2135  CheckContextMatch(a);
2136  CheckContextMatch(i);
2137  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2138  }

§ MkSeqSort()

SeqSort MkSeqSort ( Sort  s)
inline

Create a new sequence sort.

Definition at line 246 of file Context.cs.

247  {
248  Contract.Requires(s != null);
249  Contract.Ensures(Contract.Result<SeqSort>() != null);
250  return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
251  }
def SeqSort(s)
Definition: z3py.py:9357

§ MkSetAdd()

ArrayExpr MkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2284 of file Context.cs.

2285  {
2286  Contract.Requires(set != null);
2287  Contract.Requires(element != null);
2288  Contract.Ensures(Contract.Result<Expr>() != null);
2289 
2290  CheckContextMatch(set);
2291  CheckContextMatch(element);
2292  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2293  }

§ MkSetComplement()

ArrayExpr MkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 2352 of file Context.cs.

2353  {
2354  Contract.Requires(arg != null);
2355  Contract.Ensures(Contract.Result<Expr>() != null);
2356 
2357  CheckContextMatch(arg);
2358  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2359  }

§ MkSetDel()

ArrayExpr MkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 2299 of file Context.cs.

2300  {
2301  Contract.Requires(set != null);
2302  Contract.Requires(element != null);
2303  Contract.Ensures(Contract.Result<Expr>() != null);
2304 
2305  CheckContextMatch(set);
2306  CheckContextMatch(element);
2307  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2308  }

§ MkSetDifference()

ArrayExpr MkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2338 of file Context.cs.

2339  {
2340  Contract.Requires(arg1 != null);
2341  Contract.Requires(arg2 != null);
2342  Contract.Ensures(Contract.Result<Expr>() != null);
2343 
2344  CheckContextMatch(arg1);
2345  CheckContextMatch(arg2);
2346  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2347  }

§ MkSetIntersection()

ArrayExpr MkSetIntersection ( params ArrayExpr []  args)
inline

Take the intersection of a list of sets.

Definition at line 2325 of file Context.cs.

2326  {
2327  Contract.Requires(args != null);
2328  Contract.Requires(Contract.ForAll(args, a => a != null));
2329  Contract.Ensures(Contract.Result<Expr>() != null);
2330 
2331  CheckContextMatch<ArrayExpr>(args);
2332  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2333  }

§ MkSetMembership()

BoolExpr MkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 2364 of file Context.cs.

2365  {
2366  Contract.Requires(elem != null);
2367  Contract.Requires(set != null);
2368  Contract.Ensures(Contract.Result<Expr>() != null);
2369 
2370  CheckContextMatch(elem);
2371  CheckContextMatch(set);
2372  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2373  }

§ MkSetSort()

SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2248 of file Context.cs.

2249  {
2250  Contract.Requires(ty != null);
2251  Contract.Ensures(Contract.Result<SetSort>() != null);
2252 
2253  CheckContextMatch(ty);
2254  return new SetSort(this, ty);
2255  }

§ MkSetSubset()

BoolExpr MkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2378 of file Context.cs.

2379  {
2380  Contract.Requires(arg1 != null);
2381  Contract.Requires(arg2 != null);
2382  Contract.Ensures(Contract.Result<Expr>() != null);
2383 
2384  CheckContextMatch(arg1);
2385  CheckContextMatch(arg2);
2386  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2387  }

§ MkSetUnion()

ArrayExpr MkSetUnion ( params ArrayExpr []  args)
inline

Take the union of a list of sets.

Definition at line 2313 of file Context.cs.

2314  {
2315  Contract.Requires(args != null);
2316  Contract.Requires(Contract.ForAll(args, a => a != null));
2317 
2318  CheckContextMatch<ArrayExpr>(args);
2319  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2320  }

§ MkSignExt()

BitVecExpr MkSignExt ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector sign extension.

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

Definition at line 1731 of file Context.cs.

1732  {
1733  Contract.Requires(t != null);
1734  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1735 
1736  CheckContextMatch(t);
1737  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1738  }

§ MkSimpleSolver()

Solver MkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3832 of file Context.cs.

3833  {
3834  Contract.Ensures(Contract.Result<Solver>() != null);
3835 
3836  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3837  }

§ MkSolver() [1/3]

Solver MkSolver ( Symbol  logic = null)
inline

Creates a new (incremental) solver.

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

Definition at line 3808 of file Context.cs.

3809  {
3810  Contract.Ensures(Contract.Result<Solver>() != null);
3811 
3812  if (logic == null)
3813  return new Solver(this, Native.Z3_mk_solver(nCtx));
3814  else
3815  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3816  }

§ MkSolver() [2/3]

Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 3822 of file Context.cs.

3823  {
3824  Contract.Ensures(Contract.Result<Solver>() != null);
3825 
3826  return MkSolver(MkSymbol(logic));
3827  }
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3808
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ MkSolver() [3/3]

Solver MkSolver ( Tactic  t)
inline

Creates a solver that is implemented using the given tactic.

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

Definition at line 3846 of file Context.cs.

3847  {
3848  Contract.Requires(t != null);
3849  Contract.Ensures(Contract.Result<Solver>() != null);
3850 
3851  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3852  }

§ MkStar()

ReExpr MkStar ( ReExpr  re)
inline

Take the Kleene star of a regular expression.

Definition at line 2560 of file Context.cs.

2561  {
2562  Contract.Requires(re != null);
2563  Contract.Ensures(Contract.Result<ReExpr>() != null);
2564  return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
2565  }

§ MkStore()

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

Array update.

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

See also
MkArraySort, MkSelect

Definition at line 2157 of file Context.cs.

2158  {
2159  Contract.Requires(a != null);
2160  Contract.Requires(i != null);
2161  Contract.Requires(v != null);
2162  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2163 
2164  CheckContextMatch(a);
2165  CheckContextMatch(i);
2166  CheckContextMatch(v);
2167  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2168  }

§ MkString()

SeqExpr MkString ( string  s)
inline

Create a string constant.

Definition at line 2416 of file Context.cs.

2417  {
2418  Contract.Requires(s != null);
2419  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2420  return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
2421  }

§ MkSub()

ArithExpr MkSub ( params ArithExpr []  t)
inline

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

Definition at line 1074 of file Context.cs.

Referenced by ArithExpr.operator-().

1075  {
1076  Contract.Requires(t != null);
1077  Contract.Requires(Contract.ForAll(t, a => a != null));
1078  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1079 
1080  CheckContextMatch<ArithExpr>(t);
1081  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
1082  }

§ MkSuffixOf()

BoolExpr MkSuffixOf ( SeqExpr  s1,
SeqExpr  s2 
)
inline

Check for sequence suffix.

Definition at line 2462 of file Context.cs.

2463  {
2464  Contract.Requires(s1 != null);
2465  Contract.Requires(s2 != null);
2466  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2467  CheckContextMatch(s1, s2);
2468  return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
2469  }

§ MkSymbol() [1/2]

IntSymbol MkSymbol ( int  i)
inline

Creates a new symbol using an integer.

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

Definition at line 91 of file Context.cs.

Referenced by Params.Add(), and Optimize.AssertSoft().

92  {
93  Contract.Ensures(Contract.Result<IntSymbol>() != null);
94 
95  return new IntSymbol(this, i);
96  }

§ MkSymbol() [2/2]

StringSymbol MkSymbol ( string  name)
inline

Create a symbol using a string.

Definition at line 101 of file Context.cs.

102  {
103  Contract.Ensures(Contract.Result<StringSymbol>() != null);
104 
105  return new StringSymbol(this, name);
106  }

§ MkTactic()

Tactic MkTactic ( string  name)
inline

Creates a new Tactic.

Definition at line 3383 of file Context.cs.

Referenced by Goal.Simplify().

3384  {
3385  Contract.Ensures(Contract.Result<Tactic>() != null);
3386 
3387  return new Tactic(this, name);
3388  }

§ MkTermArray()

Expr MkTermArray ( ArrayExpr  array)
inline

Access the array default value.

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

Definition at line 2219 of file Context.cs.

2220  {
2221  Contract.Requires(array != null);
2222  Contract.Ensures(Contract.Result<Expr>() != null);
2223 
2224  CheckContextMatch(array);
2225  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2226  }

§ MkToRe()

ReExpr MkToRe ( SeqExpr  s)
inline

Convert a regular expression that accepts sequence s.

Definition at line 2537 of file Context.cs.

2538  {
2539  Contract.Requires(s != null);
2540  Contract.Ensures(Contract.Result<ReExpr>() != null);
2541  return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
2542  }

§ MkTrue()

BoolExpr MkTrue ( )
inline

The true Term.

Definition at line 836 of file Context.cs.

Referenced by Goal.AsBoolExpr().

837  {
838  Contract.Ensures(Contract.Result<BoolExpr>() != null);
839 
840  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
841  }

§ MkTupleSort()

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

Create a new tuple sort.

Definition at line 280 of file Context.cs.

281  {
282  Contract.Requires(name != null);
283  Contract.Requires(fieldNames != null);
284  Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
285  Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
286  Contract.Ensures(Contract.Result<TupleSort>() != null);
287 
288  CheckContextMatch(name);
289  CheckContextMatch<Symbol>(fieldNames);
290  CheckContextMatch<Sort>(fieldSorts);
291  return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
292  }

§ MkUnaryMinus()

ArithExpr MkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing -t.

Definition at line 1087 of file Context.cs.

Referenced by ArithExpr.operator-().

1088  {
1089  Contract.Requires(t != null);
1090  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1091 
1092  CheckContextMatch(t);
1093  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
1094  }

§ MkUninterpretedSort() [1/2]

UninterpretedSort MkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 194 of file Context.cs.

195  {
196  Contract.Requires(s != null);
197  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
198 
199  CheckContextMatch(s);
200  return new UninterpretedSort(this, s);
201  }

§ MkUninterpretedSort() [2/2]

UninterpretedSort MkUninterpretedSort ( string  str)
inline

Create a new uninterpreted sort.

Definition at line 206 of file Context.cs.

207  {
208  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
209 
210  return MkUninterpretedSort(MkSymbol(str));
211  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:194

§ MkUnion()

ReExpr MkUnion ( params ReExpr []  t)
inline

Create the union of regular languages.

Definition at line 2603 of file Context.cs.

2604  {
2605  Contract.Requires(t != null);
2606  Contract.Requires(Contract.ForAll(t, a => a != null));
2607  Contract.Ensures(Contract.Result<ReExpr>() != null);
2608 
2609  CheckContextMatch<ReExpr>(t);
2610  return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
2611  }

§ MkUnit()

SeqExpr MkUnit ( Expr  elem)
inline

Create the singleton sequence.

Definition at line 2406 of file Context.cs.

2407  {
2408  Contract.Requires(elem != null);
2409  Contract.Ensures(Contract.Result<SeqExpr>() != null);
2410  return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
2411  }

§ MkUpdateField()

Expr MkUpdateField ( FuncDecl  field,
Expr  t,
Expr  v 
)
inline

Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remainig fields of t are unchanged.

Definition at line 501 of file Context.cs.

502  {
503  return Expr.Create(this, Native.Z3_datatype_update_field(
504  nCtx, field.NativeObject,
505  t.NativeObject, v.NativeObject));
506  }

§ MkXor()

BoolExpr MkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 953 of file Context.cs.

Referenced by BoolExpr.operator^().

954  {
955  Contract.Requires(t1 != null);
956  Contract.Requires(t2 != null);
957  Contract.Ensures(Contract.Result<BoolExpr>() != null);
958 
959  CheckContextMatch(t1);
960  CheckContextMatch(t2);
961  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
962  }

§ MkZeroExt()

BitVecExpr MkZeroExt ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector zero extension.

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 1749 of file Context.cs.

1750  {
1751  Contract.Requires(t != null);
1752  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1753 
1754  CheckContextMatch(t);
1755  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1756  }

§ MOption()

ReExpr MOption ( ReExpr  re)
inline

Create the optional regular expression.

Definition at line 2580 of file Context.cs.

2581  {
2582  Contract.Requires(re != null);
2583  Contract.Ensures(Contract.Result<ReExpr>() != null);
2584  return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
2585  }

§ MPlus()

ReExpr MPlus ( ReExpr  re)
inline

Take the Kleene plus of a regular expression.

Definition at line 2570 of file Context.cs.

2571  {
2572  Contract.Requires(re != null);
2573  Contract.Ensures(Contract.Result<ReExpr>() != null);
2574  return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
2575  }

§ Not()

Probe Not ( Probe  p)
inline

Create a probe that evaluates to "true" when the value p does not evaluate to "true".

Definition at line 3789 of file Context.cs.

3790  {
3791  Contract.Requires(p != null);
3792  Contract.Ensures(Contract.Result<Probe>() != null);
3793 
3794  CheckContextMatch(p);
3795  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3796  }

§ Or()

Probe Or ( Probe  p1,
Probe  p2 
)
inline

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

Definition at line 3774 of file Context.cs.

3775  {
3776  Contract.Requires(p1 != null);
3777  Contract.Requires(p2 != null);
3778  Contract.Ensures(Contract.Result<Probe>() != null);
3779 
3780  CheckContextMatch(p1);
3781  CheckContextMatch(p2);
3782  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3783  }

§ OrElse()

Tactic OrElse ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.

Definition at line 3443 of file Context.cs.

3444  {
3445  Contract.Requires(t1 != null);
3446  Contract.Requires(t2 != null);
3447  Contract.Ensures(Contract.Result<Tactic>() != null);
3448 
3449  CheckContextMatch(t1);
3450  CheckContextMatch(t2);
3451  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3452  }

§ ParAndThen()

Tactic ParAndThen ( Tactic  t1,
Tactic  t2 
)
inline

Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.

Definition at line 3603 of file Context.cs.

3604  {
3605  Contract.Requires(t1 != null);
3606  Contract.Requires(t2 != null);
3607  Contract.Ensures(Contract.Result<Tactic>() != null);
3608 
3609  CheckContextMatch(t1);
3610  CheckContextMatch(t2);
3611  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3612  }

§ ParOr()

Tactic ParOr ( params Tactic []  t)
inline

Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).

Definition at line 3590 of file Context.cs.

3591  {
3592  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3593  Contract.Ensures(Contract.Result<Tactic>() != null);
3594 
3595  CheckContextMatch<Tactic>(t);
3596  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3597  }

§ ParseSMTLIB2File()

BoolExpr ParseSMTLIB2File ( string  fileName,
Symbol []  sortNames = null,
Sort []  sorts = null,
Symbol []  declNames = null,
FuncDecl []  decls = null 
)
inline

Parse the given file using the SMT-LIB2 parser.

See also
ParseSMTLIB2String

Definition at line 3297 of file Context.cs.

3298  {
3299  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3300 
3301  uint csn = Symbol.ArrayLength(sortNames);
3302  uint cs = Sort.ArrayLength(sorts);
3303  uint cdn = Symbol.ArrayLength(declNames);
3304  uint cd = AST.ArrayLength(decls);
3305  if (csn != cs || cdn != cd)
3306  throw new Z3Exception("Argument size mismatch");
3307  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
3308  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3309  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3310  }

§ ParseSMTLIB2String()

BoolExpr ParseSMTLIB2String ( string  str,
Symbol []  sortNames = null,
Sort []  sorts = null,
Symbol []  declNames = null,
FuncDecl []  decls = null 
)
inline

Parse the given string using the SMT-LIB2 parser.

See also
ParseSMTLIBString
Returns
A conjunction of assertions in the scope (up to push/pop) at the end of the string.

Definition at line 3278 of file Context.cs.

3279  {
3280  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3281 
3282  uint csn = Symbol.ArrayLength(sortNames);
3283  uint cs = Sort.ArrayLength(sorts);
3284  uint cdn = Symbol.ArrayLength(declNames);
3285  uint cd = AST.ArrayLength(decls);
3286  if (csn != cs || cdn != cd)
3287  throw new Z3Exception("Argument size mismatch");
3288  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
3289  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3290  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
3291  }

§ ParseSMTLIBFile()

void ParseSMTLIBFile ( string  fileName,
Symbol []  sortNames = null,
Sort []  sorts = null,
Symbol []  declNames = null,
FuncDecl []  decls = null 
)
inline

Parse the given file using the SMT-LIB parser.

See also
ParseSMTLIBString

Definition at line 3172 of file Context.cs.

3173  {
3174  uint csn = Symbol.ArrayLength(sortNames);
3175  uint cs = Sort.ArrayLength(sorts);
3176  uint cdn = Symbol.ArrayLength(declNames);
3177  uint cd = AST.ArrayLength(decls);
3178  if (csn != cs || cdn != cd)
3179  throw new Z3Exception("Argument size mismatch");
3180  Native.Z3_parse_smtlib_file(nCtx, fileName,
3181  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3182  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
3183  }

§ ParseSMTLIBString()

void ParseSMTLIBString ( string  str,
Symbol []  sortNames = null,
Sort []  sorts = null,
Symbol []  declNames = null,
FuncDecl []  decls = null 
)
inline

Parse the given string using the SMT-LIB parser.

The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays sortNames and declNames don't need to match the names of the sorts and declarations in the arrays sorts and decls . This is a useful feature since we can use arbitrary names to reference sorts and declarations.

Definition at line 3155 of file Context.cs.

3156  {
3157  uint csn = Symbol.ArrayLength(sortNames);
3158  uint cs = Sort.ArrayLength(sorts);
3159  uint cdn = Symbol.ArrayLength(declNames);
3160  uint cd = AST.ArrayLength(decls);
3161  if (csn != cs || cdn != cd)
3162  throw new Z3Exception("Argument size mismatch");
3163  Native.Z3_parse_smtlib_string(nCtx, str,
3164  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
3165  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
3166  }

§ ProbeDescription()

string ProbeDescription ( string  name)
inline

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

Definition at line 3653 of file Context.cs.

3654  {
3655  Contract.Ensures(Contract.Result<string>() != null);
3656 
3657  return Native.Z3_probe_get_descr(nCtx, name);
3658  }

§ Repeat()

Tactic Repeat ( Tactic  t,
uint  max = uint.MaxValue 
)
inline

Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.

Definition at line 3508 of file Context.cs.

3509  {
3510  Contract.Requires(t != null);
3511  Contract.Ensures(Contract.Result<Tactic>() != null);
3512 
3513  CheckContextMatch(t);
3514  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3515  }

§ SimplifyHelp()

string SimplifyHelp ( )
inline

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

Definition at line 4715 of file Context.cs.

4716  {
4717  Contract.Ensures(Contract.Result<string>() != null);
4718 
4719  return Native.Z3_simplify_get_help(nCtx);
4720  }

§ Skip()

Tactic Skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 3520 of file Context.cs.

3521  {
3522  Contract.Ensures(Contract.Result<Tactic>() != null);
3523 
3524  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3525  }

§ TacticDescription()

string TacticDescription ( string  name)
inline

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

Definition at line 3373 of file Context.cs.

3374  {
3375  Contract.Ensures(Contract.Result<string>() != null);
3376 
3377  return Native.Z3_tactic_get_descr(nCtx, name);
3378  }

§ Then()

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

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

Shorthand for AndThen.

Definition at line 3429 of file Context.cs.

3430  {
3431  Contract.Requires(t1 != null);
3432  Contract.Requires(t2 != null);
3433  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3434  Contract.Ensures(Contract.Result<Tactic>() != null);
3435 
3436  return AndThen(t1, t2, ts);
3437  }
Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 ...
Definition: Context.cs:3394

§ TryFor()

Tactic TryFor ( Tactic  t,
uint  ms 
)
inline

Create a tactic that applies t to a goal for ms milliseconds.

If t does not terminate within ms milliseconds, then it fails.

Definition at line 3460 of file Context.cs.

3461  {
3462  Contract.Requires(t != null);
3463  Contract.Ensures(Contract.Result<Tactic>() != null);
3464 
3465  CheckContextMatch(t);
3466  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3467  }

§ UnwrapAST()

IntPtr UnwrapAST ( AST  a)
inline

Unwraps an AST.

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

See also
Native.Z3_inc_ref

).

See also
WrapAST
Parameters
aThe AST to unwrap.

Definition at line 4707 of file Context.cs.

4708  {
4709  return a.NativeObject;
4710  }

§ UpdateParamValue()

void UpdateParamValue ( string  id,
string  value 
)
inline

Update a mutable configuration parameter.

The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -p Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

Definition at line 4757 of file Context.cs.

4758  {
4759  Native.Z3_update_param_value(nCtx, id, value);
4760  }

§ UsingParams()

Tactic UsingParams ( Tactic  t,
Params  p 
)
inline

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

Definition at line 3563 of file Context.cs.

3564  {
3565  Contract.Requires(t != null);
3566  Contract.Requires(p != null);
3567  Contract.Ensures(Contract.Result<Tactic>() != null);
3568 
3569  CheckContextMatch(t);
3570  CheckContextMatch(p);
3571  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3572  }

§ When()

Tactic When ( Probe  p,
Tactic  t 
)
inline

Create a tactic that applies t to a given goal if the probe p evaluates to true.

If p evaluates to false, then the new tactic behaves like the skip tactic.

Definition at line 3476 of file Context.cs.

3477  {
3478  Contract.Requires(p != null);
3479  Contract.Requires(t != null);
3480  Contract.Ensures(Contract.Result<Tactic>() != null);
3481 
3482  CheckContextMatch(t);
3483  CheckContextMatch(p);
3484  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3485  }

§ With()

Tactic With ( Tactic  t,
Params  p 
)
inline

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

Alias for UsingParams

Definition at line 3578 of file Context.cs.

3579  {
3580  Contract.Requires(t != null);
3581  Contract.Requires(p != null);
3582  Contract.Ensures(Contract.Result<Tactic>() != null);
3583 
3584  return UsingParams(t, p);
3585  }
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3563

§ WrapAST()

AST WrapAST ( IntPtr  nativeObject)
inline

Wraps an AST.

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

See also
UnwrapAST, Native.Z3_inc_ref

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

See also
UnwrapAST
Parameters
nativeObjectThe native pointer to wrap.

Definition at line 4690 of file Context.cs.

4691  {
4692  Contract.Ensures(Contract.Result<AST>() != null);
4693  return AST.Create(this, nativeObject);
4694  }

Property Documentation

§ ApplyResult_DRQ

IDecRefQueue ApplyResult_DRQ
get

ApplyResult DRQ

Definition at line 4898 of file Context.cs.

Referenced by ApplyResult.ToString().

§ AST_DRQ

IDecRefQueue AST_DRQ
get

AST DRQ

Definition at line 4883 of file Context.cs.

Referenced by AST.SExpr().

§ ASTMap_DRQ

IDecRefQueue ASTMap_DRQ
get

ASTMap DRQ

Definition at line 4888 of file Context.cs.

§ ASTVector_DRQ

IDecRefQueue ASTVector_DRQ
get

ASTVector DRQ

Definition at line 4893 of file Context.cs.

Referenced by ASTVector.ToRealExprArray().

§ BoolSort

Retrieves the Boolean sort of the context.

Definition at line 135 of file Context.cs.

§ Fixedpoint_DRQ

IDecRefQueue Fixedpoint_DRQ
get

FixedPoint DRQ

Definition at line 4953 of file Context.cs.

Referenced by Fixedpoint.ParseString().

§ FuncEntry_DRQ

IDecRefQueue FuncEntry_DRQ
get

FuncEntry DRQ

Definition at line 4903 of file Context.cs.

Referenced by FuncInterp.Entry.ToString().

§ FuncInterp_DRQ

IDecRefQueue FuncInterp_DRQ
get

FuncInterp DRQ

Definition at line 4908 of file Context.cs.

Referenced by FuncInterp.ToString().

§ Goal_DRQ

IDecRefQueue Goal_DRQ
get

Goal DRQ

Definition at line 4913 of file Context.cs.

Referenced by Goal.AsBoolExpr().

§ IntSort

Retrieves the Integer sort of the context.

Definition at line 147 of file Context.cs.

§ Model_DRQ

IDecRefQueue Model_DRQ
get

Model DRQ

Definition at line 4918 of file Context.cs.

Referenced by Model.ToString().

§ NumProbes

uint NumProbes
get

The number of supported Probes.

Definition at line 3629 of file Context.cs.

§ NumSMTLIBAssumptions

uint NumSMTLIBAssumptions
get

The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3210 of file Context.cs.

§ NumSMTLIBDecls

uint NumSMTLIBDecls
get

The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3232 of file Context.cs.

§ NumSMTLIBFormulas

uint NumSMTLIBFormulas
get

The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3188 of file Context.cs.

§ NumSMTLIBSorts

uint NumSMTLIBSorts
get

The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3254 of file Context.cs.

§ NumTactics

uint NumTactics
get

The number of supported tactics.

Definition at line 3349 of file Context.cs.

§ Optimize_DRQ

IDecRefQueue Optimize_DRQ
get

Optimize DRQ

Definition at line 4958 of file Context.cs.

§ ParamDescrs_DRQ

IDecRefQueue ParamDescrs_DRQ
get

ParamDescrs DRQ

Definition at line 4928 of file Context.cs.

Referenced by ParamDescrs.ToString().

§ Params_DRQ

IDecRefQueue Params_DRQ
get

Params DRQ

Definition at line 4923 of file Context.cs.

Referenced by Params.ToString().

§ PrintMode

Z3_ast_print_mode PrintMode
set

Selects the format used for pretty-printing expressions.

The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.

See also
AST.ToString(), Pattern.ToString(), FuncDecl.ToString(), Sort.ToString()

Definition at line 3117 of file Context.cs.

§ Probe_DRQ

IDecRefQueue Probe_DRQ
get

Probe DRQ

Definition at line 4933 of file Context.cs.

§ ProbeNames

string [] ProbeNames
get

The names of all supported Probes.

Definition at line 3637 of file Context.cs.

§ RealSort

Retrieves the Real sort of the context.

Definition at line 160 of file Context.cs.

§ SimplifyParameterDescriptions

ParamDescrs SimplifyParameterDescriptions
get

Retrieves parameter descriptions for simplifier.

Definition at line 4726 of file Context.cs.

§ SMTLIBAssumptions

BoolExpr [] SMTLIBAssumptions
get

The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3216 of file Context.cs.

§ SMTLIBDecls

FuncDecl [] SMTLIBDecls
get

The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3238 of file Context.cs.

§ SMTLIBFormulas

BoolExpr [] SMTLIBFormulas
get

The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3194 of file Context.cs.

§ SMTLIBSorts

Sort [] SMTLIBSorts
get

The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.

Definition at line 3260 of file Context.cs.

§ Solver_DRQ

IDecRefQueue Solver_DRQ
get

Solver DRQ

Definition at line 4938 of file Context.cs.

Referenced by Solver.ToString().

§ Statistics_DRQ

IDecRefQueue Statistics_DRQ
get

Statistics DRQ

Definition at line 4943 of file Context.cs.

§ StringSort

SeqSort StringSort
get

Retrieves the String sort of the context.

Definition at line 172 of file Context.cs.

§ Tactic_DRQ

IDecRefQueue Tactic_DRQ
get

Tactic DRQ

Definition at line 4948 of file Context.cs.

§ TacticNames

string [] TacticNames
get

The names of all supported tactics.

Definition at line 3357 of file Context.cs.