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...
 
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. More...
 
FiniteDomainSort MkFiniteDomainSort (string name, ulong size)
 Create a new finite domain sort. 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...
 
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 MkOr (params 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 MkMul (params 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...
 
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...
 
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...
 
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. 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...
 
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 31 of file Context.cs.

Constructor & Destructor Documentation

Context ( )
inline

Constructor.

Definition at line 37 of file Context.cs.

38  : base()
39  {
40  m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
41  InitContext();
42  }
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 62 of file Context.cs.

63  : base()
64  {
65  Contract.Requires(settings != null);
66 
67  IntPtr cfg = Native.Z3_mk_config();
68  foreach (KeyValuePair<string, string> kv in settings)
69  Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
70  m_ctx = Native.Z3_mk_context_rc(cfg);
71  Native.Z3_del_config(cfg);
72  InitContext();
73  }

Member Function Documentation

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

3377  {
3378  Contract.Requires(p1 != null);
3379  Contract.Requires(p2 != null);
3380  Contract.Ensures(Contract.Result<Probe>() != null);
3381 
3382  CheckContextMatch(p1);
3383  CheckContextMatch(p2);
3384  return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
3385  }
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 3011 of file Context.cs.

3012  {
3013  Contract.Requires(t1 != null);
3014  Contract.Requires(t2 != null);
3015  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3016  Contract.Ensures(Contract.Result<Tactic>() != null);
3017 
3018 
3019  CheckContextMatch(t1);
3020  CheckContextMatch(t2);
3021  CheckContextMatch(ts);
3022 
3023  IntPtr last = IntPtr.Zero;
3024  if (ts != null && ts.Length > 0)
3025  {
3026  last = ts[ts.Length - 1].NativeObject;
3027  for (int i = ts.Length - 2; i >= 0; i--)
3028  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
3029  }
3030  if (last != IntPtr.Zero)
3031  {
3032  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
3033  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
3034  }
3035  else
3036  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3037  }
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 2750 of file Context.cs.

2752  {
2753  Contract.Requires(assumptions != null);
2754  Contract.Requires(formula != null);
2755  Contract.Ensures(Contract.Result<string>() != null);
2756 
2757  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
2758  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
2759  formula.NativeObject);
2760  }
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 3108 of file Context.cs.

3109  {
3110  Contract.Requires(p != null);
3111  Contract.Requires(t1 != null);
3112  Contract.Requires(t2 != null);
3113  Contract.Ensures(Contract.Result<Tactic>() != null);
3114 
3115  CheckContextMatch(p);
3116  CheckContextMatch(t1);
3117  CheckContextMatch(t2);
3118  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3119  }
Probe ConstProbe ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3290 of file Context.cs.

3291  {
3292  Contract.Ensures(Contract.Result<Probe>() != null);
3293 
3294  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3295  }
void Dispose ( )
inline

Disposes of the context.

Definition at line 4565 of file Context.cs.

4566  {
4567  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
4568  AST_DRQ.Clear(this);
4569  ASTMap_DRQ.Clear(this);
4570  ASTVector_DRQ.Clear(this);
4571  ApplyResult_DRQ.Clear(this);
4572  FuncEntry_DRQ.Clear(this);
4573  FuncInterp_DRQ.Clear(this);
4574  Goal_DRQ.Clear(this);
4575  Model_DRQ.Clear(this);
4576  Params_DRQ.Clear(this);
4577  ParamDescrs_DRQ.Clear(this);
4578  Probe_DRQ.Clear(this);
4579  Solver_DRQ.Clear(this);
4580  Statistics_DRQ.Clear(this);
4581  Tactic_DRQ.Clear(this);
4582  Fixedpoint_DRQ.Clear(this);
4583  Optimize_DRQ.Clear(this);
4584 
4585  m_boolSort = null;
4586  m_intSort = null;
4587  m_realSort = null;
4588  }
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
Definition: Context.cs:4474
IDecRefQueue Tactic_DRQ
Tactic DRQ
Definition: Context.cs:4529
IDecRefQueue Optimize_DRQ
Optimize DRQ
Definition: Context.cs:4539
IDecRefQueue Statistics_DRQ
Statistics DRQ
Definition: Context.cs:4524
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4494
IDecRefQueue Params_DRQ
Params DRQ
Definition: Context.cs:4504
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
Definition: Context.cs:4484
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4519
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
Definition: Context.cs:4479
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
Definition: Context.cs:4489
IDecRefQueue AST_DRQ
AST DRQ
Definition: Context.cs:4464
IDecRefQueue Model_DRQ
Model DRQ
Definition: Context.cs:4499
IDecRefQueue ASTMap_DRQ
ASTMap DRQ
Definition: Context.cs:4469
IDecRefQueue Probe_DRQ
Probe DRQ
Definition: Context.cs:4514
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Definition: Context.cs:4534
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Definition: Context.cs:4509
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 3361 of file Context.cs.

3362  {
3363  Contract.Requires(p1 != null);
3364  Contract.Requires(p2 != null);
3365  Contract.Ensures(Contract.Result<Probe>() != null);
3366 
3367  CheckContextMatch(p1);
3368  CheckContextMatch(p2);
3369  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3370  }
Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3147 of file Context.cs.

3148  {
3149  Contract.Ensures(Contract.Result<Tactic>() != null);
3150 
3151  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3152  }
Tactic FailIf ( Probe  p)
inline

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

Definition at line 3157 of file Context.cs.

3158  {
3159  Contract.Requires(p != null);
3160  Contract.Ensures(Contract.Result<Tactic>() != null);
3161 
3162  CheckContextMatch(p);
3163  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3164  }
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 3170 of file Context.cs.

3171  {
3172  Contract.Ensures(Contract.Result<Tactic>() != null);
3173 
3174  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3175  }
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 3346 of file Context.cs.

3347  {
3348  Contract.Requires(p1 != null);
3349  Contract.Requires(p2 != null);
3350  Contract.Ensures(Contract.Result<Probe>() != null);
3351 
3352  CheckContextMatch(p1);
3353  CheckContextMatch(p2);
3354  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3355  }
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 3316 of file Context.cs.

3317  {
3318  Contract.Requires(p1 != null);
3319  Contract.Requires(p2 != null);
3320  Contract.Ensures(Contract.Result<Probe>() != null);
3321 
3322  CheckContextMatch(p1);
3323  CheckContextMatch(p2);
3324  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3325  }
void Interrupt ( )
inline

Interrupt the execution of a Z3 procedure.

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

Definition at line 3235 of file Context.cs.

3236  {
3237  Native.Z3_interrupt(nCtx);
3238  }
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 3331 of file Context.cs.

3332  {
3333  Contract.Requires(p1 != null);
3334  Contract.Requires(p2 != null);
3335  Contract.Ensures(Contract.Result<Probe>() != null);
3336 
3337  CheckContextMatch(p1);
3338  CheckContextMatch(p2);
3339  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3340  }
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 3301 of file Context.cs.

3302  {
3303  Contract.Requires(p1 != null);
3304  Contract.Requires(p2 != null);
3305  Contract.Ensures(Contract.Result<Probe>() != null);
3306 
3307  CheckContextMatch(p1);
3308  CheckContextMatch(p2);
3309  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3310  }
ArithExpr MkAdd ( params ArithExpr[]  t)
inline

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

Definition at line 940 of file Context.cs.

941  {
942  Contract.Requires(t != null);
943  Contract.Requires(Contract.ForAll(t, a => a != null));
944  Contract.Ensures(Contract.Result<ArithExpr>() != null);
945 
946  CheckContextMatch(t);
947  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
948  }
BoolExpr MkAnd ( params BoolExpr[]  t)
inline

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

Definition at line 910 of file Context.cs.

Referenced by Goal.AsBoolExpr().

911  {
912  Contract.Requires(t != null);
913  Contract.Requires(Contract.ForAll(t, a => a != null));
914  Contract.Ensures(Contract.Result<BoolExpr>() != null);
915 
916  CheckContextMatch(t);
917  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
918  }
Expr MkApp ( FuncDecl  f,
params Expr[]  args 
)
inline

Create a new function application.

Definition at line 764 of file Context.cs.

Referenced by EnumSort.Const().

765  {
766  Contract.Requires(f != null);
767  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
768  Contract.Ensures(Contract.Result<Expr>() != null);
769 
770  CheckContextMatch(f);
771  CheckContextMatch(args);
772  return Expr.Create(this, f, args);
773  }
ArrayExpr MkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1986 of file Context.cs.

1987  {
1988  Contract.Requires(name != null);
1989  Contract.Requires(domain != null);
1990  Contract.Requires(range != null);
1991  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1992 
1993  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
1994  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:223
ArrayExpr MkArrayConst ( string  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1999 of file Context.cs.

2000  {
2001  Contract.Requires(domain != null);
2002  Contract.Requires(range != null);
2003  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2004 
2005  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
2006  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
ArraySort MkArraySort(Sort domain, Sort range)
Create a new array sort.
Definition: Context.cs:223
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
ArraySort MkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 223 of file Context.cs.

224  {
225  Contract.Requires(domain != null);
226  Contract.Requires(range != null);
227  Contract.Ensures(Contract.Result<ArraySort>() != null);
228 
229  CheckContextMatch(domain);
230  CheckContextMatch(range);
231  return new ArraySort(this, domain, range);
232  }
def ArraySort(d, r)
Definition: z3py.py:4004
BoolExpr MkAtMost ( BoolExpr[]  args,
uint  k 
)
inline

Create an at-most-k constraint.

Definition at line 2272 of file Context.cs.

2273  {
2274  Contract.Requires(args != null);
2275  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2276  CheckContextMatch(args);
2277  return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
2278  AST.ArrayToNative(args), k));
2279  }
BitVecSort MkBitVecSort ( uint  size)
inline

Create a new bit-vector sort.

Definition at line 213 of file Context.cs.

214  {
215  Contract.Ensures(Contract.Result<BitVecSort>() != null);
216 
217  return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
218  }
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3460
BoolExpr MkBool ( bool  value)
inline

Creates a Boolean value.

Definition at line 799 of file Context.cs.

800  {
801  Contract.Ensures(Contract.Result<BoolExpr>() != null);
802 
803  return value ? MkTrue() : MkFalse();
804  }
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:779
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:789
BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 677 of file Context.cs.

678  {
679  Contract.Requires(name != null);
680  Contract.Ensures(Contract.Result<BoolExpr>() != null);
681 
682  return (BoolExpr)MkConst(name, BoolSort);
683  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:127
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 688 of file Context.cs.

689  {
690  Contract.Ensures(Contract.Result<BoolExpr>() != null);
691 
692  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
693  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:127
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
BoolSort MkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 163 of file Context.cs.

164  {
165  Contract.Ensures(Contract.Result<BoolSort>() != null);
166  return new BoolSort(this);
167  }
BoolSort BoolSort
Retrieves the Boolean sort of the context.
Definition: Context.cs:127
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 594 of file Context.cs.

595  {
596  Contract.Requires(ty != null);
597  Contract.Ensures(Contract.Result<Expr>() != null);
598 
599  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
600  }
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 2527 of file Context.cs.

2528  {
2529  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2530 
2531  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2532  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2306
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
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 2539 of file Context.cs.

2540  {
2541  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2542 
2543  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2544  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2306
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
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 2551 of file Context.cs.

2552  {
2553  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2554 
2555  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2556  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2306
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
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 2563 of file Context.cs.

2564  {
2565  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2566 
2567  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2568  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2306
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
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 2575 of file Context.cs.

2576  {
2577  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2578 
2579  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2580  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2306
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
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 1838 of file Context.cs.

1839  {
1840  Contract.Requires(t != null);
1841  Contract.Ensures(Contract.Result<IntExpr>() != null);
1842 
1843  CheckContextMatch(t);
1844  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1845  }
BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1297 of file Context.cs.

1298  {
1299  Contract.Requires(t1 != null);
1300  Contract.Requires(t2 != null);
1301  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1302 
1303  CheckContextMatch(t1);
1304  CheckContextMatch(t2);
1305  return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
1306  }
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 1853 of file Context.cs.

1854  {
1855  Contract.Requires(t1 != null);
1856  Contract.Requires(t2 != null);
1857  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1858 
1859  CheckContextMatch(t1);
1860  CheckContextMatch(t2);
1861  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1862  }
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 1870 of file Context.cs.

1871  {
1872  Contract.Requires(t1 != null);
1873  Contract.Requires(t2 != null);
1874  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1875 
1876  CheckContextMatch(t1);
1877  CheckContextMatch(t2);
1878  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1879  }
BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1194 of file Context.cs.

1195  {
1196  Contract.Requires(t1 != null);
1197  Contract.Requires(t2 != null);
1198  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1199 
1200  CheckContextMatch(t1);
1201  CheckContextMatch(t2);
1202  return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
1203  }
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 1725 of file Context.cs.

1726  {
1727  Contract.Requires(t1 != null);
1728  Contract.Requires(t2 != null);
1729  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1730 
1731  CheckContextMatch(t1);
1732  CheckContextMatch(t2);
1733  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1734  }
BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 741 of file Context.cs.

742  {
743  Contract.Requires(name != null);
744  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
745 
746  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
747  }
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 752 of file Context.cs.

753  {
754  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
755 
756  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
757  }
BitVecSort MkBitVecSort(uint size)
Create a new bit-vector sort.
Definition: Context.cs:213
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
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 1700 of file Context.cs.

1701  {
1702  Contract.Requires(t1 != null);
1703  Contract.Requires(t2 != null);
1704  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1705 
1706  CheckContextMatch(t1);
1707  CheckContextMatch(t2);
1708  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1709  }
BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1327 of file Context.cs.

1328  {
1329  Contract.Requires(t1 != null);
1330  Contract.Requires(t2 != null);
1331  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1332 
1333  CheckContextMatch(t1);
1334  CheckContextMatch(t2);
1335  return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
1336  }
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 1953 of file Context.cs.

1954  {
1955  Contract.Requires(t1 != null);
1956  Contract.Requires(t2 != null);
1957  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1958 
1959  CheckContextMatch(t1);
1960  CheckContextMatch(t2);
1961  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1962  }
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 1970 of file Context.cs.

1971  {
1972  Contract.Requires(t1 != null);
1973  Contract.Requires(t2 != null);
1974  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1975 
1976  CheckContextMatch(t1);
1977  CheckContextMatch(t2);
1978  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1979  }
BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1239 of file Context.cs.

1240  {
1241  Contract.Requires(t1 != null);
1242  Contract.Requires(t2 != null);
1243  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1244 
1245  CheckContextMatch(t1);
1246  CheckContextMatch(t2);
1247  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1248  }
BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1284 of file Context.cs.

1285  {
1286  Contract.Requires(t != null);
1287  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1288 
1289  CheckContextMatch(t);
1290  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1291  }
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 1938 of file Context.cs.

1939  {
1940  Contract.Requires(t != null);
1941  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1942 
1943  CheckContextMatch(t);
1944  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1945  }
BitVecExpr MkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1254 of file Context.cs.

1255  {
1256  Contract.Requires(t1 != null);
1257  Contract.Requires(t2 != null);
1258  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1259 
1260  CheckContextMatch(t1);
1261  CheckContextMatch(t2);
1262  return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
1263  }
BitVecExpr MkBVNot ( BitVecExpr  t)
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1155 of file Context.cs.

1156  {
1157  Contract.Requires(t != null);
1158  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1159 
1160  CheckContextMatch(t);
1161  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1162  }
BitVecExpr MkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1209 of file Context.cs.

1210  {
1211  Contract.Requires(t1 != null);
1212  Contract.Requires(t2 != null);
1213  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1214 
1215  CheckContextMatch(t1);
1216  CheckContextMatch(t2);
1217  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1218  }
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 1168 of file Context.cs.

1169  {
1170  Contract.Requires(t != null);
1171  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1172 
1173  CheckContextMatch(t);
1174  return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
1175  }
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 1181 of file Context.cs.

1182  {
1183  Contract.Requires(t != null);
1184  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1185 
1186  CheckContextMatch(t);
1187  return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
1188  }
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 1743 of file Context.cs.

1744  {
1745  Contract.Requires(t != null);
1746  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1747 
1748  CheckContextMatch(t);
1749  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1750  }
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 1775 of file Context.cs.

1776  {
1777  Contract.Requires(t1 != null);
1778  Contract.Requires(t2 != null);
1779  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1780 
1781  CheckContextMatch(t1);
1782  CheckContextMatch(t2);
1783  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1784  }
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 1759 of file Context.cs.

1760  {
1761  Contract.Requires(t != null);
1762  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1763 
1764  CheckContextMatch(t);
1765  return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
1766  }
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 1793 of file Context.cs.

1794  {
1795  Contract.Requires(t1 != null);
1796  Contract.Requires(t2 != null);
1797  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1798 
1799  CheckContextMatch(t1);
1800  CheckContextMatch(t2);
1801  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1802  }
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 1371 of file Context.cs.

1372  {
1373  Contract.Requires(t1 != null);
1374  Contract.Requires(t2 != null);
1375  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1376 
1377  CheckContextMatch(t1);
1378  CheckContextMatch(t2);
1379  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1380  }
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 1921 of file Context.cs.

1922  {
1923  Contract.Requires(t1 != null);
1924  Contract.Requires(t2 != null);
1925  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1926 
1927  CheckContextMatch(t1);
1928  CheckContextMatch(t2);
1929  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1930  }
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 1531 of file Context.cs.

1532  {
1533  Contract.Requires(t1 != null);
1534  Contract.Requires(t2 != null);
1535  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1536 
1537  CheckContextMatch(t1);
1538  CheckContextMatch(t2);
1539  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1540  }
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 1565 of file Context.cs.

1566  {
1567  Contract.Requires(t1 != null);
1568  Contract.Requires(t2 != null);
1569  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1570 
1571  CheckContextMatch(t1);
1572  CheckContextMatch(t2);
1573  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1574  }
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 1677 of file Context.cs.

1678  {
1679  Contract.Requires(t1 != null);
1680  Contract.Requires(t2 != null);
1681  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1682 
1683  CheckContextMatch(t1);
1684  CheckContextMatch(t2);
1685  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1686  }
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 1497 of file Context.cs.

1498  {
1499  Contract.Requires(t1 != null);
1500  Contract.Requires(t2 != null);
1501  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1502 
1503  CheckContextMatch(t1);
1504  CheckContextMatch(t2);
1505  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1506  }
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 1463 of file Context.cs.

1464  {
1465  Contract.Requires(t1 != null);
1466  Contract.Requires(t2 != null);
1467  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1468 
1469  CheckContextMatch(t1);
1470  CheckContextMatch(t2);
1471  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1472  }
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 1429 of file Context.cs.

1430  {
1431  Contract.Requires(t1 != null);
1432  Contract.Requires(t2 != null);
1433  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1434 
1435  CheckContextMatch(t1);
1436  CheckContextMatch(t2);
1437  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1438  }
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 1411 of file Context.cs.

1412  {
1413  Contract.Requires(t1 != null);
1414  Contract.Requires(t2 != null);
1415  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1416 
1417  CheckContextMatch(t1);
1418  CheckContextMatch(t2);
1419  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1420  }
BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1312 of file Context.cs.

1313  {
1314  Contract.Requires(t1 != null);
1315  Contract.Requires(t2 != null);
1316  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1317 
1318  CheckContextMatch(t1);
1319  CheckContextMatch(t2);
1320  return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
1321  }
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 1887 of file Context.cs.

1888  {
1889  Contract.Requires(t1 != null);
1890  Contract.Requires(t2 != null);
1891  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1892 
1893  CheckContextMatch(t1);
1894  CheckContextMatch(t2);
1895  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1896  }
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 1904 of file Context.cs.

1905  {
1906  Contract.Requires(t1 != null);
1907  Contract.Requires(t2 != null);
1908  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1909 
1910  CheckContextMatch(t1);
1911  CheckContextMatch(t2);
1912  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1913  }
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 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_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1356  }
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 1514 of file Context.cs.

1515  {
1516  Contract.Requires(t1 != null);
1517  Contract.Requires(t2 != null);
1518  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1519 
1520  CheckContextMatch(t1);
1521  CheckContextMatch(t2);
1522  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1523  }
BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1548 of file Context.cs.

1549  {
1550  Contract.Requires(t1 != null);
1551  Contract.Requires(t2 != null);
1552  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1553 
1554  CheckContextMatch(t1);
1555  CheckContextMatch(t2);
1556  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1557  }
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 1480 of file Context.cs.

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

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1446 of file Context.cs.

1447  {
1448  Contract.Requires(t1 != null);
1449  Contract.Requires(t2 != null);
1450  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1451 
1452  CheckContextMatch(t1);
1453  CheckContextMatch(t2);
1454  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1455  }
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 1390 of file Context.cs.

1391  {
1392  Contract.Requires(t1 != null);
1393  Contract.Requires(t2 != null);
1394  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1395 
1396  CheckContextMatch(t1);
1397  CheckContextMatch(t2);
1398  return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
1399  }
BitVecExpr MkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1269 of file Context.cs.

1270  {
1271  Contract.Requires(t1 != null);
1272  Contract.Requires(t2 != null);
1273  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1274 
1275  CheckContextMatch(t1);
1276  CheckContextMatch(t2);
1277  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1278  }
BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1224 of file Context.cs.

1225  {
1226  Contract.Requires(t1 != null);
1227  Contract.Requires(t2 != null);
1228  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1229 
1230  CheckContextMatch(t1);
1231  CheckContextMatch(t2);
1232  return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
1233  }
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 1586 of file Context.cs.

1587  {
1588  Contract.Requires(t1 != null);
1589  Contract.Requires(t2 != null);
1590  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1591 
1592  CheckContextMatch(t1);
1593  CheckContextMatch(t2);
1594  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1595  }
Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 626 of file Context.cs.

627  {
628  Contract.Requires(name != null);
629  Contract.Requires(range != null);
630  Contract.Ensures(Contract.Result<Expr>() != null);
631 
632  CheckContextMatch(name);
633  CheckContextMatch(range);
634 
635  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
636  }
Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 641 of file Context.cs.

642  {
643  Contract.Requires(range != null);
644  Contract.Ensures(Contract.Result<Expr>() != null);
645 
646  return MkConst(MkSymbol(name), range);
647  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
Expr MkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 666 of file Context.cs.

667  {
668  Contract.Requires(f != null);
669  Contract.Ensures(Contract.Result<Expr>() != null);
670 
671  return MkApp(f);
672  }
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:764
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 2071 of file Context.cs.

2072  {
2073  Contract.Requires(domain != null);
2074  Contract.Requires(v != null);
2075  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2076 
2077  CheckContextMatch(domain);
2078  CheckContextMatch(v);
2079  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2080  }
FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 550 of file Context.cs.

551  {
552  Contract.Requires(name != null);
553  Contract.Requires(range != null);
554  Contract.Ensures(Contract.Result<FuncDecl>() != null);
555 
556  CheckContextMatch(name);
557  CheckContextMatch(range);
558  return new FuncDecl(this, name, null, range);
559  }
FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 564 of file Context.cs.

565  {
566  Contract.Requires(range != null);
567  Contract.Ensures(Contract.Result<FuncDecl>() != null);
568 
569  CheckContextMatch(range);
570  return new FuncDecl(this, MkSymbol(name), null, range);
571  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
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 346 of file Context.cs.

347  {
348  Contract.Requires(name != null);
349  Contract.Requires(recognizer != null);
350  Contract.Ensures(Contract.Result<Constructor>() != null);
351 
352  return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
353  }
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 364 of file Context.cs.

365  {
366  Contract.Ensures(Contract.Result<Constructor>() != null);
367 
368  return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
369  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
DatatypeSort MkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 374 of file Context.cs.

375  {
376  Contract.Requires(name != null);
377  Contract.Requires(constructors != null);
378  Contract.Requires(Contract.ForAll(constructors, c => c != null));
379 
380  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
381 
382  CheckContextMatch(name);
383  CheckContextMatch(constructors);
384  return new DatatypeSort(this, name, constructors);
385  }
DatatypeSort MkDatatypeSort ( string  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 390 of file Context.cs.

391  {
392  Contract.Requires(constructors != null);
393  Contract.Requires(Contract.ForAll(constructors, c => c != null));
394  Contract.Ensures(Contract.Result<DatatypeSort>() != null);
395 
396  CheckContextMatch(constructors);
397  return new DatatypeSort(this, MkSymbol(name), constructors);
398  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
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 405 of file Context.cs.

406  {
407  Contract.Requires(names != null);
408  Contract.Requires(c != null);
409  Contract.Requires(names.Length == c.Length);
410  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
411  Contract.Requires(Contract.ForAll(names, name => name != null));
412  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
413 
414  CheckContextMatch(names);
415  uint n = (uint)names.Length;
416  ConstructorList[] cla = new ConstructorList[n];
417  IntPtr[] n_constr = new IntPtr[n];
418  for (uint i = 0; i < n; i++)
419  {
420  Constructor[] constructor = c[i];
421  Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
422  CheckContextMatch(constructor);
423  cla[i] = new ConstructorList(this, constructor);
424  n_constr[i] = cla[i].NativeObject;
425  }
426  IntPtr[] n_res = new IntPtr[n];
427  Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
428  DatatypeSort[] res = new DatatypeSort[n];
429  for (uint i = 0; i < n; i++)
430  res[i] = new DatatypeSort(this, n_res[i]);
431  return res;
432  }
DatatypeSort [] MkDatatypeSorts ( string[]  names,
Constructor  c[][] 
)
inline

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 440 of file Context.cs.

441  {
442  Contract.Requires(names != null);
443  Contract.Requires(c != null);
444  Contract.Requires(names.Length == c.Length);
445  Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
446  Contract.Requires(Contract.ForAll(names, name => name != null));
447  Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
448 
449  return MkDatatypeSorts(MkSymbols(names), c);
450  }
DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
Create mutually recursive datatypes.
Definition: Context.cs:405
BoolExpr MkDistinct ( params Expr[]  args)
inline

Creates a distinct term.

Definition at line 823 of file Context.cs.

824  {
825  Contract.Requires(args != null);
826  Contract.Requires(Contract.ForAll(args, a => a != null));
827 
828  Contract.Ensures(Contract.Result<BoolExpr>() != null);
829 
830  CheckContextMatch(args);
831  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
832  }
ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 991 of file Context.cs.

992  {
993  Contract.Requires(t1 != null);
994  Contract.Requires(t2 != null);
995  Contract.Ensures(Contract.Result<ArithExpr>() != null);
996 
997  CheckContextMatch(t1);
998  CheckContextMatch(t2);
999  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
1000  }
ArrayExpr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2137 of file Context.cs.

2138  {
2139  Contract.Requires(domain != null);
2140  Contract.Ensures(Contract.Result<Expr>() != null);
2141 
2142  CheckContextMatch(domain);
2143  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2144  }
EnumSort MkEnumSort ( Symbol  name,
params Symbol[]  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 254 of file Context.cs.

255  {
256  Contract.Requires(name != null);
257  Contract.Requires(enumNames != null);
258  Contract.Requires(Contract.ForAll(enumNames, f => f != null));
259 
260  Contract.Ensures(Contract.Result<EnumSort>() != null);
261 
262  CheckContextMatch(name);
263  CheckContextMatch(enumNames);
264  return new EnumSort(this, name, enumNames);
265  }
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4458
EnumSort MkEnumSort ( string  name,
params string[]  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 270 of file Context.cs.

271  {
272  Contract.Requires(enumNames != null);
273  Contract.Ensures(Contract.Result<EnumSort>() != null);
274 
275  return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
276  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4458
BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 809 of file Context.cs.

810  {
811  Contract.Requires(x != null);
812  Contract.Requires(y != null);
813  Contract.Ensures(Contract.Result<BoolExpr>() != null);
814 
815  CheckContextMatch(x);
816  CheckContextMatch(y);
817  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
818  }
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.

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

Definition at line 2641 of file Context.cs.

2642  {
2643  Contract.Requires(sorts != null);
2644  Contract.Requires(names != null);
2645  Contract.Requires(body != null);
2646  Contract.Requires(sorts.Length == names.Length);
2647  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2648  Contract.Requires(Contract.ForAll(names, n => n != null));
2649  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2650  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2651  Contract.Ensures(Contract.Result<Quantifier>() != null);
2652 
2653  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2654  }
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.

Definition at line 2659 of file Context.cs.

2660  {
2661  Contract.Requires(body != null);
2662  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2663  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2664  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2665  Contract.Ensures(Contract.Result<Quantifier>() != null);
2666 
2667  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2668  }
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 1606 of file Context.cs.

1607  {
1608  Contract.Requires(t != null);
1609  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1610 
1611  CheckContextMatch(t);
1612  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1613  }
BoolExpr MkFalse ( )
inline

The false Term.

Definition at line 789 of file Context.cs.

790  {
791  Contract.Ensures(Contract.Result<BoolExpr>() != null);
792 
793  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
794  }
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 310 of file Context.cs.

311  {
312  Contract.Requires(name != null);
313  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
314 
315  CheckContextMatch(name);
316  return new FiniteDomainSort(this, name, size);
317  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
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 327 of file Context.cs.

328  {
329  Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
330 
331  return new FiniteDomainSort(this, MkSymbol(name), size);
332  }
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
Fixedpoint MkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3476 of file Context.cs.

3477  {
3478  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3479 
3480  return new Fixedpoint(this);
3481  }
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.

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

2606  {
2607  Contract.Requires(sorts != null);
2608  Contract.Requires(names != null);
2609  Contract.Requires(body != null);
2610  Contract.Requires(sorts.Length == names.Length);
2611  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2612  Contract.Requires(Contract.ForAll(names, n => n != null));
2613  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2614  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2615 
2616  Contract.Ensures(Contract.Result<Quantifier>() != null);
2617 
2618  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2619  }
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.

Definition at line 2625 of file Context.cs.

2626  {
2627  Contract.Requires(body != null);
2628  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2629  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2630  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2631 
2632  Contract.Ensures(Contract.Result<Quantifier>() != null);
2633 
2634  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2635  }
FPNum MkFP ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 3785 of file Context.cs.

3786  {
3787  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3788  return MkFPNumeral(v, s);
3789  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3726
FPNum MkFP ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 3796 of file Context.cs.

3797  {
3798  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3799  return MkFPNumeral(v, s);
3800  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3726
FPNum MkFP ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 3807 of file Context.cs.

3808  {
3809  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3810  return MkFPNumeral(v, s);
3811  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3726
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 3820 of file Context.cs.

3821  {
3822  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3823  return MkFPNumeral(sgn, exp, sig, s);
3824  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3726
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 3833 of file Context.cs.

3834  {
3835  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3836  return MkFPNumeral(sgn, exp, sig, s);
3837  }
FPNum MkFPNumeral(float v, FPSort s)
Create a numeral of FloatingPoint sort from a float.
Definition: Context.cs:3726
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 4125 of file Context.cs.

4126  {
4127  Contract.Ensures(Contract.Result<FPExpr>() != null);
4128  return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
4129  }
FPExpr MkFPAbs ( FPExpr  t)
inline

Floating-point absolute value

Parameters
tfloating-point term

Definition at line 3846 of file Context.cs.

3847  {
3848  Contract.Ensures(Contract.Result<FPNum>() != null);
3849  return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
3850  }
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 3868 of file Context.cs.

3869  {
3870  Contract.Ensures(Contract.Result<FPNum>() != null);
3871  return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3872  }
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 3904 of file Context.cs.

3905  {
3906  Contract.Ensures(Contract.Result<FPNum>() != null);
3907  return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3908  }
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 4034 of file Context.cs.

4035  {
4036  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4037  return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
4038  }
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 3920 of file Context.cs.

3921  {
3922  Contract.Ensures(Contract.Result<FPNum>() != null);
3923  return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
3924  }
BoolExpr MkFPGEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4009 of file Context.cs.

4010  {
4011  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4012  return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
4013  }
BoolExpr MkFPGt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point greater than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 4020 of file Context.cs.

4021  {
4022  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4023  return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
4024  }
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 3704 of file Context.cs.

3705  {
3706  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3707  return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
3708  }
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 4074 of file Context.cs.

4075  {
4076  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4077  return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
4078  }
BoolExpr MkFPIsNaN ( FPExpr  t)
inline

Predicate indicating whether t is a NaN.

Parameters
tfloating-point term

Definition at line 4084 of file Context.cs.

4085  {
4086  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4087  return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
4088  }
BoolExpr MkFPIsNegative ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4094 of file Context.cs.

4095  {
4096  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4097  return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
4098  }
BoolExpr MkFPIsNormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4044 of file Context.cs.

4045  {
4046  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4047  return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
4048  }
BoolExpr MkFPIsPositive ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4104 of file Context.cs.

4105  {
4106  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4107  return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
4108  }
BoolExpr MkFPIsSubnormal ( FPExpr  t)
inline

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

Parameters
tfloating-point term

Definition at line 4054 of file Context.cs.

4055  {
4056  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4057  return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
4058  }
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 4064 of file Context.cs.

4065  {
4066  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4067  return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
4068  }
BoolExpr MkFPLEq ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than or equal.

Parameters
t1floating-point term
t2floating-point term

Definition at line 3987 of file Context.cs.

3988  {
3989  Contract.Ensures(Contract.Result<BoolExpr>() != null);
3990  return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
3991  }
BoolExpr MkFPLt ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point less than.

Parameters
t1floating-point term
t2floating-point term

Definition at line 3998 of file Context.cs.

3999  {
4000  Contract.Ensures(Contract.Result<BoolExpr>() != null);
4001  return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
4002  }
FPExpr MkFPMax ( FPExpr  t1,
FPExpr  t2 
)
inline

Maximum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 3976 of file Context.cs.

3977  {
3978  Contract.Ensures(Contract.Result<FPNum>() != null);
3979  return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
3980  }
FPExpr MkFPMin ( FPExpr  t1,
FPExpr  t2 
)
inline

Minimum of floating-point numbers.

Parameters
t1floating-point term
t2floating-point term

Definition at line 3965 of file Context.cs.

3966  {
3967  Contract.Ensures(Contract.Result<FPNum>() != null);
3968  return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
3969  }
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 3892 of file Context.cs.

3893  {
3894  Contract.Ensures(Contract.Result<FPNum>() != null);
3895  return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3896  }
FPNum MkFPNaN ( FPSort  s)
inline

Create a NaN of sort s.

Parameters
sFloatingPoint sort.

Definition at line 3693 of file Context.cs.

3694  {
3695  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3696  return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
3697  }
FPExpr MkFPNeg ( FPExpr  t)
inline

Floating-point negation

Parameters
tfloating-point term

Definition at line 3856 of file Context.cs.

3857  {
3858  Contract.Ensures(Contract.Result<FPNum>() != null);
3859  return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
3860  }
FPNum MkFPNumeral ( float  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 3726 of file Context.cs.

3727  {
3728  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3729  return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
3730  }
FPNum MkFPNumeral ( double  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from a float.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 3737 of file Context.cs.

3738  {
3739  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3740  return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
3741  }
FPNum MkFPNumeral ( int  v,
FPSort  s 
)
inline

Create a numeral of FloatingPoint sort from an int.

Parameters
vnumeral value.
sFloatingPoint sort.

Definition at line 3748 of file Context.cs.

3749  {
3750  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3751  return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
3752  }
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 3761 of file Context.cs.

3762  {
3763  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3764  return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
3765  }
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 3774 of file Context.cs.

3775  {
3776  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3777  return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
3778  }
FPExpr MkFPRem ( FPExpr  t1,
FPExpr  t2 
)
inline

Floating-point remainder

Parameters
t1floating-point term
t2floating-point term

Definition at line 3942 of file Context.cs.

3943  {
3944  Contract.Ensures(Contract.Result<FPNum>() != null);
3945  return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
3946  }
FPRMNum MkFPRNA ( )
inline

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

Definition at line 3541 of file Context.cs.

3542  {
3543  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3544  return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
3545  }
FPRMNum MkFPRNE ( )
inline

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

Definition at line 3523 of file Context.cs.

3524  {
3525  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3526  return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
3527  }
FPRMSort MkFPRoundingModeSort ( )
inline

Create the floating-point RoundingMode sort.

Definition at line 3503 of file Context.cs.

3504  {
3505  Contract.Ensures(Contract.Result<FPRMSort>() != null);
3506  return new FPRMSort(this);
3507  }
FPRMNum MkFPRoundNearestTiesToAway ( )
inline

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

Definition at line 3532 of file Context.cs.

3533  {
3534  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3535  return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
3536  }
FPRMExpr MkFPRoundNearestTiesToEven ( )
inline

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

Definition at line 3514 of file Context.cs.

3515  {
3516  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3517  return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
3518  }
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 3954 of file Context.cs.

3955  {
3956  Contract.Ensures(Contract.Result<FPNum>() != null);
3957  return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
3958  }
FPRMNum MkFPRoundTowardNegative ( )
inline

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

Definition at line 3568 of file Context.cs.

3569  {
3570  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3571  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
3572  }
FPRMNum MkFPRoundTowardPositive ( )
inline

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

Definition at line 3550 of file Context.cs.

3551  {
3552  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3553  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
3554  }
FPRMNum MkFPRoundTowardZero ( )
inline

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

Definition at line 3586 of file Context.cs.

3587  {
3588  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3589  return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
3590  }
FPRMNum MkFPRTN ( )
inline

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

Definition at line 3577 of file Context.cs.

3578  {
3579  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3580  return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
3581  }
FPRMNum MkFPRTP ( )
inline

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

Definition at line 3559 of file Context.cs.

3560  {
3561  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3562  return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
3563  }
FPRMNum MkFPRTZ ( )
inline

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

Definition at line 3595 of file Context.cs.

3596  {
3597  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3598  return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
3599  }
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 3609 of file Context.cs.

3610  {
3611  Contract.Ensures(Contract.Result<FPSort>() != null);
3612  return new FPSort(this, ebits, sbits);
3613  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSort128 ( )
inline

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

Definition at line 3681 of file Context.cs.

3682  {
3683  Contract.Ensures(Contract.Result<FPSort>() != null);
3684  return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
3685  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSort16 ( )
inline

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

Definition at line 3627 of file Context.cs.

3628  {
3629  Contract.Ensures(Contract.Result<FPSort>() != null);
3630  return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
3631  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSort32 ( )
inline

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

Definition at line 3645 of file Context.cs.

3646  {
3647  Contract.Ensures(Contract.Result<FPSort>() != null);
3648  return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
3649  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSort64 ( )
inline

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

Definition at line 3663 of file Context.cs.

3664  {
3665  Contract.Ensures(Contract.Result<FPSort>() != null);
3666  return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
3667  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSortDouble ( )
inline

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

Definition at line 3654 of file Context.cs.

3655  {
3656  Contract.Ensures(Contract.Result<FPSort>() != null);
3657  return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
3658  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSortHalf ( )
inline

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

Definition at line 3618 of file Context.cs.

3619  {
3620  Contract.Ensures(Contract.Result<FPSort>() != null);
3621  return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
3622  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSortQuadruple ( )
inline

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

Definition at line 3672 of file Context.cs.

3673  {
3674  Contract.Ensures(Contract.Result<FPSort>() != null);
3675  return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
3676  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPSort MkFPSortSingle ( )
inline

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

Definition at line 3636 of file Context.cs.

3637  {
3638  Contract.Ensures(Contract.Result<FPSort>() != null);
3639  return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
3640  }
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
FPExpr MkFPSqrt ( FPRMExpr  rm,
FPExpr  t 
)
inline

Floating-point square root

Parameters
rmrounding mode term
tfloating-point term

Definition at line 3931 of file Context.cs.

3932  {
3933  Contract.Ensures(Contract.Result<FPNum>() != null);
3934  return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
3935  }
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 3880 of file Context.cs.

3881  {
3882  Contract.Ensures(Contract.Result<FPNum>() != null);
3883  return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
3884  }
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 4234 of file Context.cs.

4235  {
4236  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4237  if (signed)
4238  return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4239  else
4240  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
4241  }
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 4142 of file Context.cs.

4143  {
4144  Contract.Ensures(Contract.Result<FPExpr>() != null);
4145  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
4146  }
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 4159 of file Context.cs.

4160  {
4161  Contract.Ensures(Contract.Result<FPExpr>() != null);
4162  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4163  }
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 4176 of file Context.cs.

4177  {
4178  Contract.Ensures(Contract.Result<FPExpr>() != null);
4179  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4180  }
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 4195 of file Context.cs.

4196  {
4197  Contract.Ensures(Contract.Result<FPExpr>() != null);
4198  if (signed)
4199  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4200  else
4201  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
4202  }
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 4214 of file Context.cs.

4215  {
4216  Contract.Ensures(Contract.Result<FPExpr>() != null);
4217  return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
4218  }
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 4288 of file Context.cs.

4289  {
4290  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4291  return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
4292  }
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 4270 of file Context.cs.

4271  {
4272  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
4273  return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
4274  }
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 4252 of file Context.cs.

4253  {
4254  Contract.Ensures(Contract.Result<RealExpr>() != null);
4255  return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
4256  }
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 3715 of file Context.cs.

3716  {
3717  Contract.Ensures(Contract.Result<FPRMExpr>() != null);
3718  return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
3719  }
Expr MkFreshConst ( string  prefix,
Sort  range 
)
inline

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

Definition at line 653 of file Context.cs.

654  {
655  Contract.Requires(range != null);
656  Contract.Ensures(Contract.Result<Expr>() != null);
657 
658  CheckContextMatch(range);
659  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
660  }
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 578 of file Context.cs.

579  {
580  Contract.Requires(range != null);
581  Contract.Ensures(Contract.Result<FuncDecl>() != null);
582 
583  CheckContextMatch(range);
584  return new FuncDecl(this, prefix, null, range);
585  }
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 536 of file Context.cs.

537  {
538  Contract.Requires(range != null);
539  Contract.Requires(Contract.ForAll(domain, d => d != null));
540  Contract.Ensures(Contract.Result<FuncDecl>() != null);
541 
542  CheckContextMatch(domain);
543  CheckContextMatch(range);
544  return new FuncDecl(this, prefix, domain, range);
545  }
ArrayExpr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2149 of file Context.cs.

2150  {
2151  Contract.Requires(domain != null);
2152  Contract.Ensures(Contract.Result<Expr>() != null);
2153 
2154  CheckContextMatch(domain);
2155  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2156  }
FuncDecl MkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 472 of file Context.cs.

473  {
474  Contract.Requires(name != null);
475  Contract.Requires(range != null);
476  Contract.Requires(Contract.ForAll(domain, d => d != null));
477  Contract.Ensures(Contract.Result<FuncDecl>() != null);
478 
479  CheckContextMatch(name);
480  CheckContextMatch(domain);
481  CheckContextMatch(range);
482  return new FuncDecl(this, name, domain, range);
483  }
FuncDecl MkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 488 of file Context.cs.

489  {
490  Contract.Requires(name != null);
491  Contract.Requires(domain != null);
492  Contract.Requires(range != null);
493  Contract.Ensures(Contract.Result<FuncDecl>() != null);
494 
495  CheckContextMatch(name);
496  CheckContextMatch(domain);
497  CheckContextMatch(range);
498  Sort[] q = new Sort[] { domain };
499  return new FuncDecl(this, name, q, range);
500  }
FuncDecl MkFuncDecl ( string  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 505 of file Context.cs.

506  {
507  Contract.Requires(range != null);
508  Contract.Requires(Contract.ForAll(domain, d => d != null));
509  Contract.Ensures(Contract.Result<FuncDecl>() != null);
510 
511  CheckContextMatch(domain);
512  CheckContextMatch(range);
513  return new FuncDecl(this, MkSymbol(name), domain, range);
514  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
FuncDecl MkFuncDecl ( string  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 519 of file Context.cs.

520  {
521  Contract.Requires(range != null);
522  Contract.Requires(domain != null);
523  Contract.Ensures(Contract.Result<FuncDecl>() != null);
524 
525  CheckContextMatch(domain);
526  CheckContextMatch(range);
527  Sort[] q = new Sort[] { domain };
528  return new FuncDecl(this, MkSymbol(name), q, range);
529  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
BoolExpr MkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 >= t2

Definition at line 1091 of file Context.cs.

1092  {
1093  Contract.Requires(t1 != null);
1094  Contract.Requires(t2 != null);
1095  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1096 
1097  CheckContextMatch(t1);
1098  CheckContextMatch(t2);
1099  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1100  }
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 2941 of file Context.cs.

2942  {
2943  Contract.Ensures(Contract.Result<Goal>() != null);
2944 
2945  return new Goal(this, models, unsatCores, proofs);
2946  }
BoolExpr MkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 > t2

Definition at line 1077 of file Context.cs.

1078  {
1079  Contract.Requires(t1 != null);
1080  Contract.Requires(t2 != null);
1081  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1082 
1083  CheckContextMatch(t1);
1084  CheckContextMatch(t2);
1085  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1086  }
BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 868 of file Context.cs.

869  {
870  Contract.Requires(t1 != null);
871  Contract.Requires(t2 != null);
872  Contract.Ensures(Contract.Result<BoolExpr>() != null);
873 
874  CheckContextMatch(t1);
875  CheckContextMatch(t2);
876  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
877  }
BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 882 of file Context.cs.

883  {
884  Contract.Requires(t1 != null);
885  Contract.Requires(t2 != null);
886  Contract.Ensures(Contract.Result<BoolExpr>() != null);
887 
888  CheckContextMatch(t1);
889  CheckContextMatch(t2);
890  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
891  }
IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2465 of file Context.cs.

2466  {
2467  Contract.Ensures(Contract.Result<IntNum>() != null);
2468 
2469  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2470  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
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 2477 of file Context.cs.

2478  {
2479  Contract.Ensures(Contract.Result<IntNum>() != null);
2480 
2481  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2482  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
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 2489 of file Context.cs.

2490  {
2491  Contract.Ensures(Contract.Result<IntNum>() != null);
2492 
2493  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2494  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
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 2501 of file Context.cs.

2502  {
2503  Contract.Ensures(Contract.Result<IntNum>() != null);
2504 
2505  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2506  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
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 2513 of file Context.cs.

2514  {
2515  Contract.Ensures(Contract.Result<IntNum>() != null);
2516 
2517  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2518  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
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 1814 of file Context.cs.

1815  {
1816  Contract.Requires(t != null);
1817  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1818 
1819  CheckContextMatch(t);
1820  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1821  }
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 1112 of file Context.cs.

1113  {
1114  Contract.Requires(t != null);
1115  Contract.Ensures(Contract.Result<RealExpr>() != null);
1116 
1117  CheckContextMatch(t);
1118  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1119  }
IntExpr MkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 698 of file Context.cs.

699  {
700  Contract.Requires(name != null);
701  Contract.Ensures(Contract.Result<IntExpr>() != null);
702 
703  return (IntExpr)MkConst(name, IntSort);
704  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 709 of file Context.cs.

710  {
711  Contract.Requires(name != null);
712  Contract.Ensures(Contract.Result<IntExpr>() != null);
713 
714  return (IntExpr)MkConst(name, IntSort);
715  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
IntSort MkIntSort ( )
inline

Create a new integer sort.

Definition at line 194 of file Context.cs.

195  {
196  Contract.Ensures(Contract.Result<IntSort>() != null);
197 
198  return new IntSort(this);
199  }
IntSort IntSort
Retrieves the Integer sort of the context.
Definition: Context.cs:139
BoolExpr MkIsInteger ( RealExpr  t)
inline

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

Definition at line 1140 of file Context.cs.

1141  {
1142  Contract.Requires(t != null);
1143  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1144 
1145  CheckContextMatch(t);
1146  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1147  }
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 852 of file Context.cs.

853  {
854  Contract.Requires(t1 != null);
855  Contract.Requires(t2 != null);
856  Contract.Requires(t3 != null);
857  Contract.Ensures(Contract.Result<Expr>() != null);
858 
859  CheckContextMatch(t1);
860  CheckContextMatch(t2);
861  CheckContextMatch(t3);
862  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
863  }
BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1063 of file Context.cs.

1064  {
1065  Contract.Requires(t1 != null);
1066  Contract.Requires(t2 != null);
1067  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1068 
1069  CheckContextMatch(t1);
1070  CheckContextMatch(t2);
1071  return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
1072  }
ListSort MkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 281 of file Context.cs.

282  {
283  Contract.Requires(name != null);
284  Contract.Requires(elemSort != null);
285  Contract.Ensures(Contract.Result<ListSort>() != null);
286 
287  CheckContextMatch(name);
288  CheckContextMatch(elemSort);
289  return new ListSort(this, name, elemSort);
290  }
ListSort MkListSort ( string  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 295 of file Context.cs.

296  {
297  Contract.Requires(elemSort != null);
298  Contract.Ensures(Contract.Result<ListSort>() != null);
299 
300  CheckContextMatch(elemSort);
301  return new ListSort(this, MkSymbol(name), elemSort);
302  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
BoolExpr MkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 < t2

Definition at line 1049 of file Context.cs.

1050  {
1051  Contract.Requires(t1 != null);
1052  Contract.Requires(t2 != null);
1053  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1054 
1055  CheckContextMatch(t1);
1056  CheckContextMatch(t2);
1057  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1058  }
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 2093 of file Context.cs.

2094  {
2095  Contract.Requires(f != null);
2096  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2097  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2098 
2099  CheckContextMatch(f);
2100  CheckContextMatch(args);
2101  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2102  }
IntExpr MkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 1006 of file Context.cs.

1007  {
1008  Contract.Requires(t1 != null);
1009  Contract.Requires(t2 != null);
1010  Contract.Ensures(Contract.Result<IntExpr>() != null);
1011 
1012  CheckContextMatch(t1);
1013  CheckContextMatch(t2);
1014  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1015  }
ArithExpr MkMul ( params ArithExpr[]  t)
inline

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

Definition at line 953 of file Context.cs.

954  {
955  Contract.Requires(t != null);
956  Contract.Requires(Contract.ForAll(t, a => a != null));
957  Contract.Ensures(Contract.Result<ArithExpr>() != null);
958 
959  CheckContextMatch(t);
960  return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
961  }
BoolExpr MkNot ( BoolExpr  a)
inline

Mk an expression representing not(a).

Definition at line 837 of file Context.cs.

838  {
839  Contract.Requires(a != null);
840  Contract.Ensures(Contract.Result<BoolExpr>() != null);
841 
842  CheckContextMatch(a);
843  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
844  }
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 2306 of file Context.cs.

2307  {
2308  Contract.Requires(ty != null);
2309  Contract.Ensures(Contract.Result<Expr>() != null);
2310 
2311  CheckContextMatch(ty);
2312  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2313  }
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 2322 of file Context.cs.

2323  {
2324  Contract.Requires(ty != null);
2325  Contract.Ensures(Contract.Result<Expr>() != null);
2326 
2327  CheckContextMatch(ty);
2328  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2329  }
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 2338 of file Context.cs.

2339  {
2340  Contract.Requires(ty != null);
2341  Contract.Ensures(Contract.Result<Expr>() != null);
2342 
2343  CheckContextMatch(ty);
2344  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2345  }
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 2354 of file Context.cs.

2355  {
2356  Contract.Requires(ty != null);
2357  Contract.Ensures(Contract.Result<Expr>() != null);
2358 
2359  CheckContextMatch(ty);
2360  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2361  }
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 2370 of file Context.cs.

2371  {
2372  Contract.Requires(ty != null);
2373  Contract.Ensures(Contract.Result<Expr>() != null);
2374 
2375  CheckContextMatch(ty);
2376  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2377  }
Optimize MkOptimize ( )
inline

Create an Optimization context.

Definition at line 3488 of file Context.cs.

3489  {
3490  Contract.Ensures(Contract.Result<Optimize>() != null);
3491 
3492  return new Optimize(this);
3493  }
BoolExpr MkOr ( params BoolExpr[]  t)
inline

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

Definition at line 923 of file Context.cs.

924  {
925  Contract.Requires(t != null);
926  Contract.Requires(Contract.ForAll(t, a => a != null));
927  Contract.Ensures(Contract.Result<BoolExpr>() != null);
928 
929  CheckContextMatch(t);
930  return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
931  }
Params MkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2953 of file Context.cs.

2954  {
2955  Contract.Ensures(Contract.Result<Params>() != null);
2956 
2957  return new Params(this);
2958  }
Pattern MkPattern ( params Expr[]  terms)
inline

Create a quantifier pattern.

Definition at line 607 of file Context.cs.

608  {
609  Contract.Requires(terms != null);
610  if (terms.Length == 0)
611  throw new Z3Exception("Cannot create a pattern from zero terms");
612 
613  Contract.Ensures(Contract.Result<Pattern>() != null);
614 
615  Contract.EndContractBlock();
616 
617  IntPtr[] termsNative = AST.ArrayToNative(terms);
618  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
619  }
BoolExpr MkPBLe ( int[]  coeffs,
BoolExpr[]  args,
int  k 
)
inline

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

Definition at line 2284 of file Context.cs.

2285  {
2286  Contract.Requires(args != null);
2287  Contract.Requires(coeffs != null);
2288  Contract.Requires(args.Length == coeffs.Length);
2289  Contract.Requires(Contract.Result<BoolExpr[]>() != null);
2290  CheckContextMatch(args);
2291  return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
2292  AST.ArrayToNative(args),
2293  coeffs, k));
2294  }
ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 1035 of file Context.cs.

1036  {
1037  Contract.Requires(t1 != null);
1038  Contract.Requires(t2 != null);
1039  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1040 
1041  CheckContextMatch(t1);
1042  CheckContextMatch(t2);
1043  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1044  }
Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3280 of file Context.cs.

3281  {
3282  Contract.Ensures(Contract.Result<Probe>() != null);
3283 
3284  return new Probe(this, name);
3285  }
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.

Definition at line 2674 of file Context.cs.

2675  {
2676  Contract.Requires(body != null);
2677  Contract.Requires(names != null);
2678  Contract.Requires(sorts != null);
2679  Contract.Requires(sorts.Length == names.Length);
2680  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2681  Contract.Requires(Contract.ForAll(names, n => n != null));
2682  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2683  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2684 
2685  Contract.Ensures(Contract.Result<Quantifier>() != null);
2686 
2687  if (universal)
2688  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2689  else
2690  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2691  }
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:2605
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:2641
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.

Definition at line 2697 of file Context.cs.

2698  {
2699  Contract.Requires(body != null);
2700  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2701  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2702  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2703 
2704  Contract.Ensures(Contract.Result<Quantifier>() != null);
2705 
2706  if (universal)
2707  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2708  else
2709  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2710  }
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:2605
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:2641
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 2388 of file Context.cs.

2389  {
2390  if (den == 0)
2391  throw new Z3Exception("Denominator is zero");
2392 
2393  Contract.Ensures(Contract.Result<RatNum>() != null);
2394  Contract.EndContractBlock();
2395 
2396  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2397  }
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 2404 of file Context.cs.

2405  {
2406  Contract.Ensures(Contract.Result<RatNum>() != null);
2407 
2408  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2409  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
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 2416 of file Context.cs.

2417  {
2418  Contract.Ensures(Contract.Result<RatNum>() != null);
2419 
2420  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2421  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
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 2428 of file Context.cs.

2429  {
2430  Contract.Ensures(Contract.Result<RatNum>() != null);
2431 
2432  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2433  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
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 2440 of file Context.cs.

2441  {
2442  Contract.Ensures(Contract.Result<RatNum>() != null);
2443 
2444  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2445  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
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 2452 of file Context.cs.

2453  {
2454  Contract.Ensures(Contract.Result<RatNum>() != null);
2455 
2456  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2457  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
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 1128 of file Context.cs.

1129  {
1130  Contract.Requires(t != null);
1131  Contract.Ensures(Contract.Result<IntExpr>() != null);
1132 
1133  CheckContextMatch(t);
1134  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1135  }
RealExpr MkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 720 of file Context.cs.

721  {
722  Contract.Requires(name != null);
723  Contract.Ensures(Contract.Result<RealExpr>() != null);
724 
725  return (RealExpr)MkConst(name, RealSort);
726  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
RealExpr MkRealConst ( string  name)
inline

Creates a real constant.

Definition at line 731 of file Context.cs.

732  {
733  Contract.Ensures(Contract.Result<RealExpr>() != null);
734 
735  return (RealExpr)MkConst(name, RealSort);
736  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:626
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
RealSort MkRealSort ( )
inline

Create a real sort.

Definition at line 204 of file Context.cs.

205  {
206  Contract.Ensures(Contract.Result<RealSort>() != null);
207  return new RealSort(this);
208  }
RealSort RealSort
Retrieves the Real sort of the context.
Definition: Context.cs:152
IntExpr MkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 1021 of file Context.cs.

1022  {
1023  Contract.Requires(t1 != null);
1024  Contract.Requires(t2 != null);
1025  Contract.Ensures(Contract.Result<IntExpr>() != null);
1026 
1027  CheckContextMatch(t1);
1028  CheckContextMatch(t2);
1029  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1030  }
BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1656 of file Context.cs.

1657  {
1658  Contract.Requires(t != null);
1659  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1660 
1661  CheckContextMatch(t);
1662  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1663  }
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 2021 of file Context.cs.

2022  {
2023  Contract.Requires(a != null);
2024  Contract.Requires(i != null);
2025  Contract.Ensures(Contract.Result<Expr>() != null);
2026 
2027  CheckContextMatch(a);
2028  CheckContextMatch(i);
2029  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2030  }
ArrayExpr MkSetAdd ( ArrayExpr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2161 of file Context.cs.

2162  {
2163  Contract.Requires(set != null);
2164  Contract.Requires(element != null);
2165  Contract.Ensures(Contract.Result<Expr>() != null);
2166 
2167  CheckContextMatch(set);
2168  CheckContextMatch(element);
2169  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2170  }
ArrayExpr MkSetComplement ( ArrayExpr  arg)
inline

Take the complement of a set.

Definition at line 2229 of file Context.cs.

2230  {
2231  Contract.Requires(arg != null);
2232  Contract.Ensures(Contract.Result<Expr>() != null);
2233 
2234  CheckContextMatch(arg);
2235  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2236  }
ArrayExpr MkSetDel ( ArrayExpr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 2176 of file Context.cs.

2177  {
2178  Contract.Requires(set != null);
2179  Contract.Requires(element != null);
2180  Contract.Ensures(Contract.Result<Expr>() != null);
2181 
2182  CheckContextMatch(set);
2183  CheckContextMatch(element);
2184  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2185  }
ArrayExpr MkSetDifference ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2215 of file Context.cs.

2216  {
2217  Contract.Requires(arg1 != null);
2218  Contract.Requires(arg2 != null);
2219  Contract.Ensures(Contract.Result<Expr>() != null);
2220 
2221  CheckContextMatch(arg1);
2222  CheckContextMatch(arg2);
2223  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2224  }
ArrayExpr MkSetIntersection ( params ArrayExpr[]  args)
inline

Take the intersection of a list of sets.

Definition at line 2202 of file Context.cs.

2203  {
2204  Contract.Requires(args != null);
2205  Contract.Requires(Contract.ForAll(args, a => a != null));
2206  Contract.Ensures(Contract.Result<Expr>() != null);
2207 
2208  CheckContextMatch(args);
2209  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2210  }
BoolExpr MkSetMembership ( Expr  elem,
ArrayExpr  set 
)
inline

Check for set membership.

Definition at line 2241 of file Context.cs.

2242  {
2243  Contract.Requires(elem != null);
2244  Contract.Requires(set != null);
2245  Contract.Ensures(Contract.Result<Expr>() != null);
2246 
2247  CheckContextMatch(elem);
2248  CheckContextMatch(set);
2249  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2250  }
SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2125 of file Context.cs.

2126  {
2127  Contract.Requires(ty != null);
2128  Contract.Ensures(Contract.Result<SetSort>() != null);
2129 
2130  CheckContextMatch(ty);
2131  return new SetSort(this, ty);
2132  }
BoolExpr MkSetSubset ( ArrayExpr  arg1,
ArrayExpr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2255 of file Context.cs.

2256  {
2257  Contract.Requires(arg1 != null);
2258  Contract.Requires(arg2 != null);
2259  Contract.Ensures(Contract.Result<Expr>() != null);
2260 
2261  CheckContextMatch(arg1);
2262  CheckContextMatch(arg2);
2263  return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2264  }
ArrayExpr MkSetUnion ( params ArrayExpr[]  args)
inline

Take the union of a list of sets.

Definition at line 2190 of file Context.cs.

2191  {
2192  Contract.Requires(args != null);
2193  Contract.Requires(Contract.ForAll(args, a => a != null));
2194 
2195  CheckContextMatch(args);
2196  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2197  }
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 1623 of file Context.cs.

1624  {
1625  Contract.Requires(t != null);
1626  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1627 
1628  CheckContextMatch(t);
1629  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1630  }
Solver MkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3449 of file Context.cs.

3450  {
3451  Contract.Ensures(Contract.Result<Solver>() != null);
3452 
3453  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3454  }
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 3425 of file Context.cs.

3426  {
3427  Contract.Ensures(Contract.Result<Solver>() != null);
3428 
3429  if (logic == null)
3430  return new Solver(this, Native.Z3_mk_solver(nCtx));
3431  else
3432  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3433  }
Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 3439 of file Context.cs.

3440  {
3441  Contract.Ensures(Contract.Result<Solver>() != null);
3442 
3443  return MkSolver(MkSymbol(logic));
3444  }
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3425
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
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 3463 of file Context.cs.

3464  {
3465  Contract.Requires(t != null);
3466  Contract.Ensures(Contract.Result<Solver>() != null);
3467 
3468  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3469  }
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 2049 of file Context.cs.

2050  {
2051  Contract.Requires(a != null);
2052  Contract.Requires(i != null);
2053  Contract.Requires(v != null);
2054  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2055 
2056  CheckContextMatch(a);
2057  CheckContextMatch(i);
2058  CheckContextMatch(v);
2059  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2060  }
ArithExpr MkSub ( params ArithExpr[]  t)
inline

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

Definition at line 966 of file Context.cs.

967  {
968  Contract.Requires(t != null);
969  Contract.Requires(Contract.ForAll(t, a => a != null));
970  Contract.Ensures(Contract.Result<ArithExpr>() != null);
971 
972  CheckContextMatch(t);
973  return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
974  }
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 84 of file Context.cs.

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

85  {
86  Contract.Ensures(Contract.Result<IntSymbol>() != null);
87 
88  return new IntSymbol(this, i);
89  }
StringSymbol MkSymbol ( string  name)
inline

Create a symbol using a string.

Definition at line 94 of file Context.cs.

95  {
96  Contract.Ensures(Contract.Result<StringSymbol>() != null);
97 
98  return new StringSymbol(this, name);
99  }
Tactic MkTactic ( string  name)
inline

Creates a new Tactic.

Definition at line 3000 of file Context.cs.

Referenced by Goal.Simplify().

3001  {
3002  Contract.Ensures(Contract.Result<Tactic>() != null);
3003 
3004  return new Tactic(this, name);
3005  }
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 2111 of file Context.cs.

2112  {
2113  Contract.Requires(array != null);
2114  Contract.Ensures(Contract.Result<Expr>() != null);
2115 
2116  CheckContextMatch(array);
2117  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2118  }
BoolExpr MkTrue ( )
inline

The true Term.

Definition at line 779 of file Context.cs.

Referenced by Goal.AsBoolExpr().

780  {
781  Contract.Ensures(Contract.Result<BoolExpr>() != null);
782 
783  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
784  }
TupleSort MkTupleSort ( Symbol  name,
Symbol[]  fieldNames,
Sort[]  fieldSorts 
)
inline

Create a new tuple sort.

Definition at line 237 of file Context.cs.

238  {
239  Contract.Requires(name != null);
240  Contract.Requires(fieldNames != null);
241  Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
242  Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
243  Contract.Ensures(Contract.Result<TupleSort>() != null);
244 
245  CheckContextMatch(name);
246  CheckContextMatch(fieldNames);
247  CheckContextMatch(fieldSorts);
248  return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
249  }
ArithExpr MkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing -t.

Definition at line 979 of file Context.cs.

980  {
981  Contract.Requires(t != null);
982  Contract.Ensures(Contract.Result<ArithExpr>() != null);
983 
984  CheckContextMatch(t);
985  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
986  }
UninterpretedSort MkUninterpretedSort ( Symbol  s)
inline

Create a new uninterpreted sort.

Definition at line 172 of file Context.cs.

173  {
174  Contract.Requires(s != null);
175  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
176 
177  CheckContextMatch(s);
178  return new UninterpretedSort(this, s);
179  }
UninterpretedSort MkUninterpretedSort ( string  str)
inline

Create a new uninterpreted sort.

Definition at line 184 of file Context.cs.

185  {
186  Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
187 
188  return MkUninterpretedSort(MkSymbol(str));
189  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
UninterpretedSort MkUninterpretedSort(Symbol s)
Create a new uninterpreted sort.
Definition: Context.cs:172
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 458 of file Context.cs.

459  {
460  return Expr.Create(this, Native.Z3_datatype_update_field(
461  nCtx, field.NativeObject,
462  t.NativeObject, v.NativeObject));
463  }
BoolExpr MkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 896 of file Context.cs.

897  {
898  Contract.Requires(t1 != null);
899  Contract.Requires(t2 != null);
900  Contract.Ensures(Contract.Result<BoolExpr>() != null);
901 
902  CheckContextMatch(t1);
903  CheckContextMatch(t2);
904  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
905  }
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 1641 of file Context.cs.

1642  {
1643  Contract.Requires(t != null);
1644  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1645 
1646  CheckContextMatch(t);
1647  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1648  }
Probe Not ( Probe  p)
inline

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

Definition at line 3406 of file Context.cs.

3407  {
3408  Contract.Requires(p != null);
3409  Contract.Ensures(Contract.Result<Probe>() != null);
3410 
3411  CheckContextMatch(p);
3412  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3413  }
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 3391 of file Context.cs.

3392  {
3393  Contract.Requires(p1 != null);
3394  Contract.Requires(p2 != null);
3395  Contract.Ensures(Contract.Result<Probe>() != null);
3396 
3397  CheckContextMatch(p1);
3398  CheckContextMatch(p2);
3399  return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
3400  }
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 3060 of file Context.cs.

3061  {
3062  Contract.Requires(t1 != null);
3063  Contract.Requires(t2 != null);
3064  Contract.Ensures(Contract.Result<Tactic>() != null);
3065 
3066  CheckContextMatch(t1);
3067  CheckContextMatch(t2);
3068  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3069  }
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 3220 of file Context.cs.

3221  {
3222  Contract.Requires(t1 != null);
3223  Contract.Requires(t2 != null);
3224  Contract.Ensures(Contract.Result<Tactic>() != null);
3225 
3226  CheckContextMatch(t1);
3227  CheckContextMatch(t2);
3228  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3229  }
Tactic ParOr ( params Tactic[]  t)
inline

Create a tactic that applies the given tactics in parallel.

Definition at line 3207 of file Context.cs.

3208  {
3209  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3210  Contract.Ensures(Contract.Result<Tactic>() != null);
3211 
3212  CheckContextMatch(t);
3213  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3214  }
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 2914 of file Context.cs.

2915  {
2916  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2917 
2918  uint csn = Symbol.ArrayLength(sortNames);
2919  uint cs = Sort.ArrayLength(sorts);
2920  uint cdn = Symbol.ArrayLength(declNames);
2921  uint cd = AST.ArrayLength(decls);
2922  if (csn != cs || cdn != cd)
2923  throw new Z3Exception("Argument size mismatch");
2924  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
2925  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2926  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2927  }
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 2895 of file Context.cs.

2896  {
2897  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2898 
2899  uint csn = Symbol.ArrayLength(sortNames);
2900  uint cs = Sort.ArrayLength(sorts);
2901  uint cdn = Symbol.ArrayLength(declNames);
2902  uint cd = AST.ArrayLength(decls);
2903  if (csn != cs || cdn != cd)
2904  throw new Z3Exception("Argument size mismatch");
2905  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
2906  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2907  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2908  }
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 2789 of file Context.cs.

2790  {
2791  uint csn = Symbol.ArrayLength(sortNames);
2792  uint cs = Sort.ArrayLength(sorts);
2793  uint cdn = Symbol.ArrayLength(declNames);
2794  uint cd = AST.ArrayLength(decls);
2795  if (csn != cs || cdn != cd)
2796  throw new Z3Exception("Argument size mismatch");
2797  Native.Z3_parse_smtlib_file(nCtx, fileName,
2798  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2799  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2800  }
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 2772 of file Context.cs.

2773  {
2774  uint csn = Symbol.ArrayLength(sortNames);
2775  uint cs = Sort.ArrayLength(sorts);
2776  uint cdn = Symbol.ArrayLength(declNames);
2777  uint cd = AST.ArrayLength(decls);
2778  if (csn != cs || cdn != cd)
2779  throw new Z3Exception("Argument size mismatch");
2780  Native.Z3_parse_smtlib_string(nCtx, str,
2781  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2782  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2783  }
string ProbeDescription ( string  name)
inline

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

Definition at line 3270 of file Context.cs.

3271  {
3272  Contract.Ensures(Contract.Result<string>() != null);
3273 
3274  return Native.Z3_probe_get_descr(nCtx, name);
3275  }
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 3125 of file Context.cs.

3126  {
3127  Contract.Requires(t != null);
3128  Contract.Ensures(Contract.Result<Tactic>() != null);
3129 
3130  CheckContextMatch(t);
3131  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3132  }
string SimplifyHelp ( )
inline

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

Definition at line 4332 of file Context.cs.

4333  {
4334  Contract.Ensures(Contract.Result<string>() != null);
4335 
4336  return Native.Z3_simplify_get_help(nCtx);
4337  }
Tactic Skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 3137 of file Context.cs.

3138  {
3139  Contract.Ensures(Contract.Result<Tactic>() != null);
3140 
3141  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3142  }
string TacticDescription ( string  name)
inline

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

Definition at line 2990 of file Context.cs.

2991  {
2992  Contract.Ensures(Contract.Result<string>() != null);
2993 
2994  return Native.Z3_tactic_get_descr(nCtx, name);
2995  }
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 3046 of file Context.cs.

3047  {
3048  Contract.Requires(t1 != null);
3049  Contract.Requires(t2 != null);
3050  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3051  Contract.Ensures(Contract.Result<Tactic>() != null);
3052 
3053  return AndThen(t1, t2, ts);
3054  }
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:3011
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 3077 of file Context.cs.

3078  {
3079  Contract.Requires(t != null);
3080  Contract.Ensures(Contract.Result<Tactic>() != null);
3081 
3082  CheckContextMatch(t);
3083  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3084  }
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 4324 of file Context.cs.

4325  {
4326  return a.NativeObject;
4327  }
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 4374 of file Context.cs.

4375  {
4376  Native.Z3_update_param_value(nCtx, id, value);
4377  }
Tactic UsingParams ( Tactic  t,
Params  p 
)
inline

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

Definition at line 3180 of file Context.cs.

3181  {
3182  Contract.Requires(t != null);
3183  Contract.Requires(p != null);
3184  Contract.Ensures(Contract.Result<Tactic>() != null);
3185 
3186  CheckContextMatch(t);
3187  CheckContextMatch(p);
3188  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3189  }
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 3093 of file Context.cs.

3094  {
3095  Contract.Requires(p != null);
3096  Contract.Requires(t != null);
3097  Contract.Ensures(Contract.Result<Tactic>() != null);
3098 
3099  CheckContextMatch(t);
3100  CheckContextMatch(p);
3101  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3102  }
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 3195 of file Context.cs.

3196  {
3197  Contract.Requires(t != null);
3198  Contract.Requires(p != null);
3199  Contract.Ensures(Contract.Result<Tactic>() != null);
3200 
3201  return UsingParams(t, p);
3202  }
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3180
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 4307 of file Context.cs.

4308  {
4309  Contract.Ensures(Contract.Result<AST>() != null);
4310  return AST.Create(this, nativeObject);
4311  }

Property Documentation

IDecRefQueue ApplyResult_DRQ
get

ApplyResult DRQ

Definition at line 4479 of file Context.cs.

Referenced by ApplyResult.ToString().

IDecRefQueue AST_DRQ
get

AST DRQ

Definition at line 4464 of file Context.cs.

Referenced by AST.SExpr().

IDecRefQueue ASTMap_DRQ
get

ASTMap DRQ

Definition at line 4469 of file Context.cs.

IDecRefQueue ASTVector_DRQ
get

ASTVector DRQ

Definition at line 4474 of file Context.cs.

Referenced by ASTVector.ToRealExprArray().

Retrieves the Boolean sort of the context.

Definition at line 127 of file Context.cs.

IDecRefQueue Fixedpoint_DRQ
get

FixedPoint DRQ

Definition at line 4534 of file Context.cs.

Referenced by Fixedpoint.ParseString().

IDecRefQueue FuncEntry_DRQ
get

FuncEntry DRQ

Definition at line 4484 of file Context.cs.

Referenced by FuncInterp.Entry.ToString().

IDecRefQueue FuncInterp_DRQ
get

FuncInterp DRQ

Definition at line 4489 of file Context.cs.

Referenced by FuncInterp.ToString().

IDecRefQueue Goal_DRQ
get

Goal DRQ

Definition at line 4494 of file Context.cs.

Referenced by Goal.AsBoolExpr().

Retrieves the Integer sort of the context.

Definition at line 139 of file Context.cs.

IDecRefQueue Model_DRQ
get

Model DRQ

Definition at line 4499 of file Context.cs.

Referenced by Model.ToString().

uint NumProbes
get

The number of supported Probes.

Definition at line 3246 of file Context.cs.

uint NumSMTLIBAssumptions
get

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

Definition at line 2827 of file Context.cs.

uint NumSMTLIBDecls
get

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

Definition at line 2849 of file Context.cs.

uint NumSMTLIBFormulas
get

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

Definition at line 2805 of file Context.cs.

uint NumSMTLIBSorts
get

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

Definition at line 2871 of file Context.cs.

uint NumTactics
get

The number of supported tactics.

Definition at line 2966 of file Context.cs.

IDecRefQueue Optimize_DRQ
get

Optimize DRQ

Definition at line 4539 of file Context.cs.

IDecRefQueue ParamDescrs_DRQ
get

ParamDescrs DRQ

Definition at line 4509 of file Context.cs.

Referenced by ParamDescrs.ToString().

IDecRefQueue Params_DRQ
get

Params DRQ

Definition at line 4504 of file Context.cs.

Referenced by Params.ToString().

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

IDecRefQueue Probe_DRQ
get

Probe DRQ

Definition at line 4514 of file Context.cs.

string [] ProbeNames
get

The names of all supported Probes.

Definition at line 3254 of file Context.cs.

Retrieves the Real sort of the context.

Definition at line 152 of file Context.cs.

ParamDescrs SimplifyParameterDescriptions
get

Retrieves parameter descriptions for simplifier.

Definition at line 4343 of file Context.cs.

BoolExpr [] SMTLIBAssumptions
get

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

Definition at line 2833 of file Context.cs.

FuncDecl [] SMTLIBDecls
get

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

Definition at line 2855 of file Context.cs.

BoolExpr [] SMTLIBFormulas
get

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

Definition at line 2811 of file Context.cs.

Sort [] SMTLIBSorts
get

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

Definition at line 2877 of file Context.cs.

IDecRefQueue Solver_DRQ
get

Solver DRQ

Definition at line 4519 of file Context.cs.

Referenced by Solver.ToString().

IDecRefQueue Statistics_DRQ
get

Statistics DRQ

Definition at line 4524 of file Context.cs.

IDecRefQueue Tactic_DRQ
get

Tactic DRQ

Definition at line 4529 of file Context.cs.

string [] TacticNames
get

The names of all supported tactics.

Definition at line 2974 of file Context.cs.