Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Static 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...
 
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...
 
Expr MkEmptySet (Sort domain)
 Create an empty set. More...
 
Expr MkFullSet (Sort domain)
 Create the full set. More...
 
Expr MkSetAdd (Expr set, Expr element)
 Add an element to the set. More...
 
Expr MkSetDel (Expr set, Expr element)
 Remove an element from a set. More...
 
Expr MkSetUnion (params Expr[] args)
 Take the union of a list of sets. More...
 
Expr MkSetIntersection (params Expr[] args)
 Take the intersection of a list of sets. More...
 
Expr MkSetDifference (Expr arg1, Expr arg2)
 Take the difference between two sets. More...
 
Expr MkSetComplement (Expr arg)
 Take the complement of a set. More...
 
Expr MkSetMembership (Expr elem, Expr set)
 Check for set membership. More...
 
Expr MkSetSubset (Expr arg1, Expr arg2)
 Check for subsetness of sets. 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...
 
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...
 

Static Public Member Functions

static void ToggleWarningMessages (bool enabled)
 Enable/disable printing of warning messages to the console. 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...
 

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

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

2969  {
2970  Contract.Requires(t1 != null);
2971  Contract.Requires(t2 != null);
2972  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
2973  Contract.Ensures(Contract.Result<Tactic>() != null);
2974 
2975 
2976  CheckContextMatch(t1);
2977  CheckContextMatch(t2);
2978  CheckContextMatch(ts);
2979 
2980  IntPtr last = IntPtr.Zero;
2981  if (ts != null && ts.Length > 0)
2982  {
2983  last = ts[ts.Length - 1].NativeObject;
2984  for (int i = ts.Length - 2; i >= 0; i--)
2985  last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
2986  }
2987  if (last != IntPtr.Zero)
2988  {
2989  last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
2990  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
2991  }
2992  else
2993  return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
2994  }
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 2707 of file Context.cs.

2709  {
2710  Contract.Requires(assumptions != null);
2711  Contract.Requires(formula != null);
2712  Contract.Ensures(Contract.Result<string>() != null);
2713 
2714  return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
2715  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
2716  formula.NativeObject);
2717  }
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 3065 of file Context.cs.

3066  {
3067  Contract.Requires(p != null);
3068  Contract.Requires(t1 != null);
3069  Contract.Requires(t2 != null);
3070  Contract.Ensures(Contract.Result<Tactic>() != null);
3071 
3072  CheckContextMatch(p);
3073  CheckContextMatch(t1);
3074  CheckContextMatch(t2);
3075  return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
3076  }
Probe ConstProbe ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3247 of file Context.cs.

3248  {
3249  Contract.Ensures(Contract.Result<Probe>() != null);
3250 
3251  return new Probe(this, Native.Z3_probe_const(nCtx, val));
3252  }
void Dispose ( )
inline

Disposes of the context.

Definition at line 3655 of file Context.cs.

3656  {
3657  // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
3658  AST_DRQ.Clear(this);
3659  ASTMap_DRQ.Clear(this);
3660  ASTVector_DRQ.Clear(this);
3661  ApplyResult_DRQ.Clear(this);
3662  FuncEntry_DRQ.Clear(this);
3663  FuncInterp_DRQ.Clear(this);
3664  Goal_DRQ.Clear(this);
3665  Model_DRQ.Clear(this);
3666  Params_DRQ.Clear(this);
3667  ParamDescrs_DRQ.Clear(this);
3668  Probe_DRQ.Clear(this);
3669  Solver_DRQ.Clear(this);
3670  Statistics_DRQ.Clear(this);
3671  Tactic_DRQ.Clear(this);
3672  Fixedpoint_DRQ.Clear(this);
3673 
3674  m_boolSort = null;
3675  m_intSort = null;
3676  m_realSort = null;
3677  }
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 3318 of file Context.cs.

3319  {
3320  Contract.Requires(p1 != null);
3321  Contract.Requires(p2 != null);
3322  Contract.Ensures(Contract.Result<Probe>() != null);
3323 
3324  CheckContextMatch(p1);
3325  CheckContextMatch(p2);
3326  return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
3327  }
Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3104 of file Context.cs.

3105  {
3106  Contract.Ensures(Contract.Result<Tactic>() != null);
3107 
3108  return new Tactic(this, Native.Z3_tactic_fail(nCtx));
3109  }
Tactic FailIf ( Probe  p)
inline

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

Definition at line 3114 of file Context.cs.

3115  {
3116  Contract.Requires(p != null);
3117  Contract.Ensures(Contract.Result<Tactic>() != null);
3118 
3119  CheckContextMatch(p);
3120  return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
3121  }
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 3127 of file Context.cs.

3128  {
3129  Contract.Ensures(Contract.Result<Tactic>() != null);
3130 
3131  return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
3132  }
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 3303 of file Context.cs.

3304  {
3305  Contract.Requires(p1 != null);
3306  Contract.Requires(p2 != null);
3307  Contract.Ensures(Contract.Result<Probe>() != null);
3308 
3309  CheckContextMatch(p1);
3310  CheckContextMatch(p2);
3311  return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
3312  }
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 3273 of file Context.cs.

3274  {
3275  Contract.Requires(p1 != null);
3276  Contract.Requires(p2 != null);
3277  Contract.Ensures(Contract.Result<Probe>() != null);
3278 
3279  CheckContextMatch(p1);
3280  CheckContextMatch(p2);
3281  return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
3282  }
void Interrupt ( )
inline

Interrupt the execution of a Z3 procedure.

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

Definition at line 3192 of file Context.cs.

3193  {
3194  Native.Z3_interrupt(nCtx);
3195  }
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 3288 of file Context.cs.

3289  {
3290  Contract.Requires(p1 != null);
3291  Contract.Requires(p2 != null);
3292  Contract.Ensures(Contract.Result<Probe>() != null);
3293 
3294  CheckContextMatch(p1);
3295  CheckContextMatch(p2);
3296  return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
3297  }
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 3258 of file Context.cs.

3259  {
3260  Contract.Requires(p1 != null);
3261  Contract.Requires(p2 != null);
3262  Contract.Ensures(Contract.Result<Probe>() != null);
3263 
3264  CheckContextMatch(p1);
3265  CheckContextMatch(p2);
3266  return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
3267  }
ArithExpr MkAdd ( params ArithExpr[]  t)
inline

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

Definition at line 927 of file Context.cs.

928  {
929  Contract.Requires(t != null);
930  Contract.Requires(Contract.ForAll(t, a => a != null));
931  Contract.Ensures(Contract.Result<ArithExpr>() != null);
932 
933  CheckContextMatch(t);
934  return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
935  }
BoolExpr MkAnd ( params BoolExpr[]  t)
inline

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

Definition at line 897 of file Context.cs.

898  {
899  Contract.Requires(t != null);
900  Contract.Requires(Contract.ForAll(t, a => a != null));
901  Contract.Ensures(Contract.Result<BoolExpr>() != null);
902 
903  CheckContextMatch(t);
904  return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
905  }
Expr MkApp ( FuncDecl  f,
params Expr[]  args 
)
inline

Create a new function application.

Definition at line 751 of file Context.cs.

752  {
753  Contract.Requires(f != null);
754  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
755  Contract.Ensures(Contract.Result<Expr>() != null);
756 
757  CheckContextMatch(f);
758  CheckContextMatch(args);
759  return Expr.Create(this, f, args);
760  }
ArrayExpr MkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1973 of file Context.cs.

1974  {
1975  Contract.Requires(name != null);
1976  Contract.Requires(domain != null);
1977  Contract.Requires(range != null);
1978  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1979 
1980  return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
1981  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:613
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 1986 of file Context.cs.

1987  {
1988  Contract.Requires(domain != null);
1989  Contract.Requires(range != null);
1990  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
1991 
1992  return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
1993  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:613
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
Definition: z3py.py:3955
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
Definition: z3py.py:3435
BoolExpr MkBool ( bool  value)
inline

Creates a Boolean value.

Definition at line 786 of file Context.cs.

787  {
788  Contract.Ensures(Contract.Result<BoolExpr>() != null);
789 
790  return value ? MkTrue() : MkFalse();
791  }
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:766
BoolExpr MkFalse()
The false Term.
Definition: Context.cs:776
BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 664 of file Context.cs.

665  {
666  Contract.Requires(name != null);
667  Contract.Ensures(Contract.Result<BoolExpr>() != null);
668 
669  return (BoolExpr)MkConst(name, BoolSort);
670  }
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:613
BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 675 of file Context.cs.

676  {
677  Contract.Ensures(Contract.Result<BoolExpr>() != null);
678 
679  return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
680  }
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:613
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 581 of file Context.cs.

582  {
583  Contract.Requires(ty != null);
584  Contract.Ensures(Contract.Result<Expr>() != null);
585 
586  return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
587  }
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 2484 of file Context.cs.

2485  {
2486  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2487 
2488  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2489  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2263
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 2496 of file Context.cs.

2497  {
2498  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2499 
2500  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2501  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2263
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 2508 of file Context.cs.

2509  {
2510  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2511 
2512  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2513  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2263
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.

///

Parameters
sizethe size of the bit-vector

Definition at line 2520 of file Context.cs.

2521  {
2522  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2523 
2524  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2525  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2263
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 2532 of file Context.cs.

2533  {
2534  Contract.Ensures(Contract.Result<BitVecNum>() != null);
2535 
2536  return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
2537  }
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2263
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 1825 of file Context.cs.

1826  {
1827  Contract.Requires(t != null);
1828  Contract.Ensures(Contract.Result<IntExpr>() != null);
1829 
1830  CheckContextMatch(t);
1831  return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
1832  }
BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1284 of file Context.cs.

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

1841  {
1842  Contract.Requires(t1 != null);
1843  Contract.Requires(t2 != null);
1844  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1845 
1846  CheckContextMatch(t1);
1847  CheckContextMatch(t2);
1848  return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1849  }
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 1857 of file Context.cs.

1858  {
1859  Contract.Requires(t1 != null);
1860  Contract.Requires(t2 != null);
1861  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1862 
1863  CheckContextMatch(t1);
1864  CheckContextMatch(t2);
1865  return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1866  }
BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1181 of file Context.cs.

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

1713  {
1714  Contract.Requires(t1 != null);
1715  Contract.Requires(t2 != null);
1716  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1717 
1718  CheckContextMatch(t1);
1719  CheckContextMatch(t2);
1720  return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
1721  }
BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 728 of file Context.cs.

729  {
730  Contract.Requires(name != null);
731  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
732 
733  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
734  }
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:613
BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 739 of file Context.cs.

740  {
741  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
742 
743  return (BitVecExpr)MkConst(name, MkBitVecSort(size));
744  }
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:613
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 1687 of file Context.cs.

1688  {
1689  Contract.Requires(t1 != null);
1690  Contract.Requires(t2 != null);
1691  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1692 
1693  CheckContextMatch(t1);
1694  CheckContextMatch(t2);
1695  return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
1696  }
BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1314 of file Context.cs.

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

1941  {
1942  Contract.Requires(t1 != null);
1943  Contract.Requires(t2 != null);
1944  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1945 
1946  CheckContextMatch(t1);
1947  CheckContextMatch(t2);
1948  return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1949  }
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 1957 of file Context.cs.

1958  {
1959  Contract.Requires(t1 != null);
1960  Contract.Requires(t2 != null);
1961  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1962 
1963  CheckContextMatch(t1);
1964  CheckContextMatch(t2);
1965  return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
1966  }
BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1226 of file Context.cs.

1227  {
1228  Contract.Requires(t1 != null);
1229  Contract.Requires(t2 != null);
1230  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1231 
1232  CheckContextMatch(t1);
1233  CheckContextMatch(t2);
1234  return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
1235  }
BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1271 of file Context.cs.

1272  {
1273  Contract.Requires(t != null);
1274  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1275 
1276  CheckContextMatch(t);
1277  return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
1278  }
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 1925 of file Context.cs.

1926  {
1927  Contract.Requires(t != null);
1928  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1929 
1930  CheckContextMatch(t);
1931  return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
1932  }
BitVecExpr MkBVNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1241 of file Context.cs.

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

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1142 of file Context.cs.

1143  {
1144  Contract.Requires(t != null);
1145  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1146 
1147  CheckContextMatch(t);
1148  return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
1149  }
BitVecExpr MkBVOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1196 of file Context.cs.

1197  {
1198  Contract.Requires(t1 != null);
1199  Contract.Requires(t2 != null);
1200  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1201 
1202  CheckContextMatch(t1);
1203  CheckContextMatch(t2);
1204  return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
1205  }
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 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_bvredand(nCtx, t.NativeObject));
1162  }
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 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_bvredor(nCtx, t.NativeObject));
1175  }
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 1730 of file Context.cs.

1731  {
1732  Contract.Requires(t != null);
1733  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1734 
1735  CheckContextMatch(t);
1736  return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
1737  }
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 1762 of file Context.cs.

1763  {
1764  Contract.Requires(t1 != null);
1765  Contract.Requires(t2 != null);
1766  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1767 
1768  CheckContextMatch(t1);
1769  CheckContextMatch(t2);
1770  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
1771  }
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 1746 of file Context.cs.

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

1781  {
1782  Contract.Requires(t1 != null);
1783  Contract.Requires(t2 != null);
1784  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1785 
1786  CheckContextMatch(t1);
1787  CheckContextMatch(t2);
1788  return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
1789  }
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 1358 of file Context.cs.

1359  {
1360  Contract.Requires(t1 != null);
1361  Contract.Requires(t2 != null);
1362  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1363 
1364  CheckContextMatch(t1);
1365  CheckContextMatch(t2);
1366  return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
1367  }
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 1908 of file Context.cs.

1909  {
1910  Contract.Requires(t1 != null);
1911  Contract.Requires(t2 != null);
1912  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1913 
1914  CheckContextMatch(t1);
1915  CheckContextMatch(t2);
1916  return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1917  }
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 1518 of file Context.cs.

1519  {
1520  Contract.Requires(t1 != null);
1521  Contract.Requires(t2 != null);
1522  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1523 
1524  CheckContextMatch(t1);
1525  CheckContextMatch(t2);
1526  return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
1527  }
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 1552 of file Context.cs.

1553  {
1554  Contract.Requires(t1 != null);
1555  Contract.Requires(t2 != null);
1556  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1557 
1558  CheckContextMatch(t1);
1559  CheckContextMatch(t2);
1560  return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
1561  }
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 1664 of file Context.cs.

1665  {
1666  Contract.Requires(t1 != null);
1667  Contract.Requires(t2 != null);
1668  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1669 
1670  CheckContextMatch(t1);
1671  CheckContextMatch(t2);
1672  return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
1673  }
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 1484 of file Context.cs.

1485  {
1486  Contract.Requires(t1 != null);
1487  Contract.Requires(t2 != null);
1488  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1489 
1490  CheckContextMatch(t1);
1491  CheckContextMatch(t2);
1492  return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
1493  }
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 1450 of file Context.cs.

1451  {
1452  Contract.Requires(t1 != null);
1453  Contract.Requires(t2 != null);
1454  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1455 
1456  CheckContextMatch(t1);
1457  CheckContextMatch(t2);
1458  return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
1459  }
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 1416 of file Context.cs.

1417  {
1418  Contract.Requires(t1 != null);
1419  Contract.Requires(t2 != null);
1420  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1421 
1422  CheckContextMatch(t1);
1423  CheckContextMatch(t2);
1424  return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
1425  }
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 1398 of file Context.cs.

1399  {
1400  Contract.Requires(t1 != null);
1401  Contract.Requires(t2 != null);
1402  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1403 
1404  CheckContextMatch(t1);
1405  CheckContextMatch(t2);
1406  return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
1407  }
BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1299 of file Context.cs.

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

1875  {
1876  Contract.Requires(t1 != null);
1877  Contract.Requires(t2 != null);
1878  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1879 
1880  CheckContextMatch(t1);
1881  CheckContextMatch(t2);
1882  return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
1883  }
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 1891 of file Context.cs.

1892  {
1893  Contract.Requires(t1 != null);
1894  Contract.Requires(t2 != null);
1895  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1896 
1897  CheckContextMatch(t1);
1898  CheckContextMatch(t2);
1899  return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
1900  }
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 1334 of file Context.cs.

1335  {
1336  Contract.Requires(t1 != null);
1337  Contract.Requires(t2 != null);
1338  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1339 
1340  CheckContextMatch(t1);
1341  CheckContextMatch(t2);
1342  return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
1343  }
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 1501 of file Context.cs.

1502  {
1503  Contract.Requires(t1 != null);
1504  Contract.Requires(t2 != null);
1505  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1506 
1507  CheckContextMatch(t1);
1508  CheckContextMatch(t2);
1509  return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
1510  }
BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1535 of file Context.cs.

1536  {
1537  Contract.Requires(t1 != null);
1538  Contract.Requires(t2 != null);
1539  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1540 
1541  CheckContextMatch(t1);
1542  CheckContextMatch(t2);
1543  return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
1544  }
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 1467 of file Context.cs.

1468  {
1469  Contract.Requires(t1 != null);
1470  Contract.Requires(t2 != null);
1471  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1472 
1473  CheckContextMatch(t1);
1474  CheckContextMatch(t2);
1475  return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
1476  }
BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1433 of file Context.cs.

1434  {
1435  Contract.Requires(t1 != null);
1436  Contract.Requires(t2 != null);
1437  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1438 
1439  CheckContextMatch(t1);
1440  CheckContextMatch(t2);
1441  return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
1442  }
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 1377 of file Context.cs.

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

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1256 of file Context.cs.

1257  {
1258  Contract.Requires(t1 != null);
1259  Contract.Requires(t2 != null);
1260  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1261 
1262  CheckContextMatch(t1);
1263  CheckContextMatch(t2);
1264  return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
1265  }
BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1211 of file Context.cs.

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

1574  {
1575  Contract.Requires(t1 != null);
1576  Contract.Requires(t2 != null);
1577  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1578 
1579  CheckContextMatch(t1);
1580  CheckContextMatch(t2);
1581  return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
1582  }
Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 613 of file Context.cs.

614  {
615  Contract.Requires(name != null);
616  Contract.Requires(range != null);
617  Contract.Ensures(Contract.Result<Expr>() != null);
618 
619  CheckContextMatch(name);
620  CheckContextMatch(range);
621 
622  return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
623  }
Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 628 of file Context.cs.

629  {
630  Contract.Requires(range != null);
631  Contract.Ensures(Contract.Result<Expr>() != null);
632 
633  return MkConst(MkSymbol(name), range);
634  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:613
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 653 of file Context.cs.

654  {
655  Contract.Requires(f != null);
656  Contract.Ensures(Contract.Result<Expr>() != null);
657 
658  return MkApp(f);
659  }
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:751
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 2058 of file Context.cs.

2059  {
2060  Contract.Requires(domain != null);
2061  Contract.Requires(v != null);
2062  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2063 
2064  CheckContextMatch(domain);
2065  CheckContextMatch(v);
2066  return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
2067  }
FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 537 of file Context.cs.

538  {
539  Contract.Requires(name != null);
540  Contract.Requires(range != null);
541  Contract.Ensures(Contract.Result<FuncDecl>() != null);
542 
543  CheckContextMatch(name);
544  CheckContextMatch(range);
545  return new FuncDecl(this, name, null, range);
546  }
FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 551 of file Context.cs.

552  {
553  Contract.Requires(range != null);
554  Contract.Ensures(Contract.Result<FuncDecl>() != null);
555 
556  CheckContextMatch(range);
557  return new FuncDecl(this, MkSymbol(name), null, range);
558  }
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 810 of file Context.cs.

811  {
812  Contract.Requires(args != null);
813  Contract.Requires(Contract.ForAll(args, a => a != null));
814 
815  Contract.Ensures(Contract.Result<BoolExpr>() != null);
816 
817  CheckContextMatch(args);
818  return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
819  }
ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 / t2.

Definition at line 978 of file Context.cs.

979  {
980  Contract.Requires(t1 != null);
981  Contract.Requires(t2 != null);
982  Contract.Ensures(Contract.Result<ArithExpr>() != null);
983 
984  CheckContextMatch(t1);
985  CheckContextMatch(t2);
986  return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
987  }
Expr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2124 of file Context.cs.

2125  {
2126  Contract.Requires(domain != null);
2127  Contract.Ensures(Contract.Result<Expr>() != null);
2128 
2129  CheckContextMatch(domain);
2130  return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
2131  }
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
Definition: z3py.py:4398
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  }
def EnumSort
Definition: z3py.py:4398
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 796 of file Context.cs.

797  {
798  Contract.Requires(x != null);
799  Contract.Requires(y != null);
800  Contract.Ensures(Contract.Result<BoolExpr>() != null);
801 
802  CheckContextMatch(x);
803  CheckContextMatch(y);
804  return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
805  }
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 2598 of file Context.cs.

2599  {
2600  Contract.Requires(sorts != null);
2601  Contract.Requires(names != null);
2602  Contract.Requires(body != null);
2603  Contract.Requires(sorts.Length == names.Length);
2604  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2605  Contract.Requires(Contract.ForAll(names, n => n != null));
2606  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2607  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2608  Contract.Ensures(Contract.Result<Quantifier>() != null);
2609 
2610  return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2611  }
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 2616 of file Context.cs.

2617  {
2618  Contract.Requires(body != null);
2619  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2620  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2621  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2622  Contract.Ensures(Contract.Result<Quantifier>() != null);
2623 
2624  return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2625  }
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 1593 of file Context.cs.

1594  {
1595  Contract.Requires(t != null);
1596  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1597 
1598  CheckContextMatch(t);
1599  return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
1600  }
BoolExpr MkFalse ( )
inline

The false Term.

Definition at line 776 of file Context.cs.

777  {
778  Contract.Ensures(Contract.Result<BoolExpr>() != null);
779 
780  return new BoolExpr(this, Native.Z3_mk_false(nCtx));
781  }
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  }
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  }
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 3433 of file Context.cs.

3434  {
3435  Contract.Ensures(Contract.Result<Fixedpoint>() != null);
3436 
3437  return new Fixedpoint(this);
3438  }
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 2562 of file Context.cs.

2563  {
2564  Contract.Requires(sorts != null);
2565  Contract.Requires(names != null);
2566  Contract.Requires(body != null);
2567  Contract.Requires(sorts.Length == names.Length);
2568  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2569  Contract.Requires(Contract.ForAll(names, n => n != null));
2570  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2571  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2572 
2573  Contract.Ensures(Contract.Result<Quantifier>() != null);
2574 
2575  return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2576  }
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 2582 of file Context.cs.

2583  {
2584  Contract.Requires(body != null);
2585  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
2586  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2587  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2588 
2589  Contract.Ensures(Contract.Result<Quantifier>() != null);
2590 
2591  return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2592  }
Expr MkFreshConst ( string  prefix,
Sort  range 
)
inline

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

Definition at line 640 of file Context.cs.

641  {
642  Contract.Requires(range != null);
643  Contract.Ensures(Contract.Result<Expr>() != null);
644 
645  CheckContextMatch(range);
646  return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
647  }
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 565 of file Context.cs.

566  {
567  Contract.Requires(range != null);
568  Contract.Ensures(Contract.Result<FuncDecl>() != null);
569 
570  CheckContextMatch(range);
571  return new FuncDecl(this, prefix, null, range);
572  }
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 523 of file Context.cs.

524  {
525  Contract.Requires(range != null);
526  Contract.Requires(Contract.ForAll(domain, d => d != null));
527  Contract.Ensures(Contract.Result<FuncDecl>() != null);
528 
529  CheckContextMatch(domain);
530  CheckContextMatch(range);
531  return new FuncDecl(this, prefix, domain, range);
532  }
Expr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2136 of file Context.cs.

2137  {
2138  Contract.Requires(domain != null);
2139  Contract.Ensures(Contract.Result<Expr>() != null);
2140 
2141  CheckContextMatch(domain);
2142  return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
2143  }
FuncDecl MkFuncDecl ( Symbol  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 459 of file Context.cs.

460  {
461  Contract.Requires(name != null);
462  Contract.Requires(range != null);
463  Contract.Requires(Contract.ForAll(domain, d => d != null));
464  Contract.Ensures(Contract.Result<FuncDecl>() != null);
465 
466  CheckContextMatch(name);
467  CheckContextMatch(domain);
468  CheckContextMatch(range);
469  return new FuncDecl(this, name, domain, range);
470  }
FuncDecl MkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 475 of file Context.cs.

476  {
477  Contract.Requires(name != null);
478  Contract.Requires(domain != null);
479  Contract.Requires(range != null);
480  Contract.Ensures(Contract.Result<FuncDecl>() != null);
481 
482  CheckContextMatch(name);
483  CheckContextMatch(domain);
484  CheckContextMatch(range);
485  Sort[] q = new Sort[] { domain };
486  return new FuncDecl(this, name, q, range);
487  }
FuncDecl MkFuncDecl ( string  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 492 of file Context.cs.

493  {
494  Contract.Requires(range != null);
495  Contract.Requires(Contract.ForAll(domain, d => d != null));
496  Contract.Ensures(Contract.Result<FuncDecl>() != null);
497 
498  CheckContextMatch(domain);
499  CheckContextMatch(range);
500  return new FuncDecl(this, MkSymbol(name), domain, range);
501  }
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 506 of file Context.cs.

507  {
508  Contract.Requires(range != null);
509  Contract.Requires(domain != null);
510  Contract.Ensures(Contract.Result<FuncDecl>() != null);
511 
512  CheckContextMatch(domain);
513  CheckContextMatch(range);
514  Sort[] q = new Sort[] { domain };
515  return new FuncDecl(this, MkSymbol(name), q, range);
516  }
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 1078 of file Context.cs.

1079  {
1080  Contract.Requires(t1 != null);
1081  Contract.Requires(t2 != null);
1082  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1083 
1084  CheckContextMatch(t1);
1085  CheckContextMatch(t2);
1086  return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
1087  }
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 2898 of file Context.cs.

2899  {
2900  Contract.Ensures(Contract.Result<Goal>() != null);
2901 
2902  return new Goal(this, models, unsatCores, proofs);
2903  }
BoolExpr MkGt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 > t2

Definition at line 1064 of file Context.cs.

1065  {
1066  Contract.Requires(t1 != null);
1067  Contract.Requires(t2 != null);
1068  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1069 
1070  CheckContextMatch(t1);
1071  CheckContextMatch(t2);
1072  return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
1073  }
BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 855 of file Context.cs.

856  {
857  Contract.Requires(t1 != null);
858  Contract.Requires(t2 != null);
859  Contract.Ensures(Contract.Result<BoolExpr>() != null);
860 
861  CheckContextMatch(t1);
862  CheckContextMatch(t2);
863  return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
864  }
BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 869 of file Context.cs.

870  {
871  Contract.Requires(t1 != null);
872  Contract.Requires(t2 != null);
873  Contract.Ensures(Contract.Result<BoolExpr>() != null);
874 
875  CheckContextMatch(t1);
876  CheckContextMatch(t2);
877  return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
878  }
IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2422 of file Context.cs.

2423  {
2424  Contract.Ensures(Contract.Result<IntNum>() != null);
2425 
2426  return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
2427  }
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 2434 of file Context.cs.

2435  {
2436  Contract.Ensures(Contract.Result<IntNum>() != null);
2437 
2438  return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
2439  }
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 2446 of file Context.cs.

2447  {
2448  Contract.Ensures(Contract.Result<IntNum>() != null);
2449 
2450  return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
2451  }
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 2458 of file Context.cs.

2459  {
2460  Contract.Ensures(Contract.Result<IntNum>() != null);
2461 
2462  return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
2463  }
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 2470 of file Context.cs.

2471  {
2472  Contract.Ensures(Contract.Result<IntNum>() != null);
2473 
2474  return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
2475  }
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 1801 of file Context.cs.

1802  {
1803  Contract.Requires(t != null);
1804  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1805 
1806  CheckContextMatch(t);
1807  return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
1808  }
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 1099 of file Context.cs.

1100  {
1101  Contract.Requires(t != null);
1102  Contract.Ensures(Contract.Result<RealExpr>() != null);
1103 
1104  CheckContextMatch(t);
1105  return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
1106  }
IntExpr MkIntConst ( Symbol  name)
inline

Creates an integer constant.

Definition at line 685 of file Context.cs.

686  {
687  Contract.Requires(name != null);
688  Contract.Ensures(Contract.Result<IntExpr>() != null);
689 
690  return (IntExpr)MkConst(name, IntSort);
691  }
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:613
IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 696 of file Context.cs.

697  {
698  Contract.Requires(name != null);
699  Contract.Ensures(Contract.Result<IntExpr>() != null);
700 
701  return (IntExpr)MkConst(name, IntSort);
702  }
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:613
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 1127 of file Context.cs.

1128  {
1129  Contract.Requires(t != null);
1130  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1131 
1132  CheckContextMatch(t);
1133  return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
1134  }
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 839 of file Context.cs.

840  {
841  Contract.Requires(t1 != null);
842  Contract.Requires(t2 != null);
843  Contract.Requires(t3 != null);
844  Contract.Ensures(Contract.Result<Expr>() != null);
845 
846  CheckContextMatch(t1);
847  CheckContextMatch(t2);
848  CheckContextMatch(t3);
849  return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
850  }
BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1050 of file Context.cs.

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

1037  {
1038  Contract.Requires(t1 != null);
1039  Contract.Requires(t2 != null);
1040  Contract.Ensures(Contract.Result<BoolExpr>() != null);
1041 
1042  CheckContextMatch(t1);
1043  CheckContextMatch(t2);
1044  return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
1045  }
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 2080 of file Context.cs.

2081  {
2082  Contract.Requires(f != null);
2083  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
2084  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2085 
2086  CheckContextMatch(f);
2087  CheckContextMatch(args);
2088  return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
2089  }
IntExpr MkMod ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 993 of file Context.cs.

994  {
995  Contract.Requires(t1 != null);
996  Contract.Requires(t2 != null);
997  Contract.Ensures(Contract.Result<IntExpr>() != null);
998 
999  CheckContextMatch(t1);
1000  CheckContextMatch(t2);
1001  return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
1002  }
ArithExpr MkMul ( 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_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
948  }
BoolExpr MkNot ( BoolExpr  a)
inline

Mk an expression representing not(a).

Definition at line 824 of file Context.cs.

825  {
826  Contract.Requires(a != null);
827  Contract.Ensures(Contract.Result<BoolExpr>() != null);
828 
829  CheckContextMatch(a);
830  return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
831  }
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 2263 of file Context.cs.

2264  {
2265  Contract.Requires(ty != null);
2266  Contract.Ensures(Contract.Result<Expr>() != null);
2267 
2268  CheckContextMatch(ty);
2269  return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
2270  }
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 2279 of file Context.cs.

2280  {
2281  Contract.Requires(ty != null);
2282  Contract.Ensures(Contract.Result<Expr>() != null);
2283 
2284  CheckContextMatch(ty);
2285  return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
2286  }
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 2295 of file Context.cs.

2296  {
2297  Contract.Requires(ty != null);
2298  Contract.Ensures(Contract.Result<Expr>() != null);
2299 
2300  CheckContextMatch(ty);
2301  return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
2302  }
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 2311 of file Context.cs.

2312  {
2313  Contract.Requires(ty != null);
2314  Contract.Ensures(Contract.Result<Expr>() != null);
2315 
2316  CheckContextMatch(ty);
2317  return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
2318  }
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 2327 of file Context.cs.

2328  {
2329  Contract.Requires(ty != null);
2330  Contract.Ensures(Contract.Result<Expr>() != null);
2331 
2332  CheckContextMatch(ty);
2333  return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
2334  }
BoolExpr MkOr ( params BoolExpr[]  t)
inline

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

Definition at line 910 of file Context.cs.

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_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
918  }
Params MkParams ( )
inline

Creates a new ParameterSet.

Definition at line 2910 of file Context.cs.

2911  {
2912  Contract.Ensures(Contract.Result<Params>() != null);
2913 
2914  return new Params(this);
2915  }
Pattern MkPattern ( params Expr[]  terms)
inline

Create a quantifier pattern.

Definition at line 594 of file Context.cs.

595  {
596  Contract.Requires(terms != null);
597  if (terms.Length == 0)
598  throw new Z3Exception("Cannot create a pattern from zero terms");
599 
600  Contract.Ensures(Contract.Result<Pattern>() != null);
601 
602  Contract.EndContractBlock();
603 
604  IntPtr[] termsNative = AST.ArrayToNative(terms);
605  return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
606  }
ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 ^ t2.

Definition at line 1022 of file Context.cs.

1023  {
1024  Contract.Requires(t1 != null);
1025  Contract.Requires(t2 != null);
1026  Contract.Ensures(Contract.Result<ArithExpr>() != null);
1027 
1028  CheckContextMatch(t1);
1029  CheckContextMatch(t2);
1030  return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
1031  }
Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3237 of file Context.cs.

3238  {
3239  Contract.Ensures(Contract.Result<Probe>() != null);
3240 
3241  return new Probe(this, name);
3242  }
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 2631 of file Context.cs.

2632  {
2633  Contract.Requires(body != null);
2634  Contract.Requires(names != null);
2635  Contract.Requires(sorts != null);
2636  Contract.Requires(sorts.Length == names.Length);
2637  Contract.Requires(Contract.ForAll(sorts, s => s != null));
2638  Contract.Requires(Contract.ForAll(names, n => n != null));
2639  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2640  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2641 
2642  Contract.Ensures(Contract.Result<Quantifier>() != null);
2643 
2644  if (universal)
2645  return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2646  else
2647  return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
2648  }
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:2562
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:2598
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 2654 of file Context.cs.

2655  {
2656  Contract.Requires(body != null);
2657  Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
2658  Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
2659  Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
2660 
2661  Contract.Ensures(Contract.Result<Quantifier>() != null);
2662 
2663  if (universal)
2664  return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2665  else
2666  return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
2667  }
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:2562
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:2598
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 2345 of file Context.cs.

2346  {
2347  if (den == 0)
2348  throw new Z3Exception("Denominator is zero");
2349 
2350  Contract.Ensures(Contract.Result<RatNum>() != null);
2351  Contract.EndContractBlock();
2352 
2353  return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
2354  }
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 2361 of file Context.cs.

2362  {
2363  Contract.Ensures(Contract.Result<RatNum>() != null);
2364 
2365  return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
2366  }
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 2373 of file Context.cs.

2374  {
2375  Contract.Ensures(Contract.Result<RatNum>() != null);
2376 
2377  return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
2378  }
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 2385 of file Context.cs.

2386  {
2387  Contract.Ensures(Contract.Result<RatNum>() != null);
2388 
2389  return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
2390  }
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 2397 of file Context.cs.

2398  {
2399  Contract.Ensures(Contract.Result<RatNum>() != null);
2400 
2401  return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
2402  }
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 2409 of file Context.cs.

2410  {
2411  Contract.Ensures(Contract.Result<RatNum>() != null);
2412 
2413  return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
2414  }
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 1115 of file Context.cs.

1116  {
1117  Contract.Requires(t != null);
1118  Contract.Ensures(Contract.Result<IntExpr>() != null);
1119 
1120  CheckContextMatch(t);
1121  return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
1122  }
RealExpr MkRealConst ( Symbol  name)
inline

Creates a real constant.

Definition at line 707 of file Context.cs.

708  {
709  Contract.Requires(name != null);
710  Contract.Ensures(Contract.Result<RealExpr>() != null);
711 
712  return (RealExpr)MkConst(name, RealSort);
713  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:613
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 718 of file Context.cs.

719  {
720  Contract.Ensures(Contract.Result<RealExpr>() != null);
721 
722  return (RealExpr)MkConst(name, RealSort);
723  }
Expr MkConst(Symbol name, Sort range)
Creates a new Constant of sort range and named name .
Definition: Context.cs:613
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 1008 of file Context.cs.

1009  {
1010  Contract.Requires(t1 != null);
1011  Contract.Requires(t2 != null);
1012  Contract.Ensures(Contract.Result<IntExpr>() != null);
1013 
1014  CheckContextMatch(t1);
1015  CheckContextMatch(t2);
1016  return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
1017  }
BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1643 of file Context.cs.

1644  {
1645  Contract.Requires(t != null);
1646  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1647 
1648  CheckContextMatch(t);
1649  return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
1650  }
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 2008 of file Context.cs.

2009  {
2010  Contract.Requires(a != null);
2011  Contract.Requires(i != null);
2012  Contract.Ensures(Contract.Result<Expr>() != null);
2013 
2014  CheckContextMatch(a);
2015  CheckContextMatch(i);
2016  return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
2017  }
Expr MkSetAdd ( Expr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2148 of file Context.cs.

2149  {
2150  Contract.Requires(set != null);
2151  Contract.Requires(element != null);
2152  Contract.Ensures(Contract.Result<Expr>() != null);
2153 
2154  CheckContextMatch(set);
2155  CheckContextMatch(element);
2156  return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
2157  }
Expr MkSetComplement ( Expr  arg)
inline

Take the complement of a set.

Definition at line 2216 of file Context.cs.

2217  {
2218  Contract.Requires(arg != null);
2219  Contract.Ensures(Contract.Result<Expr>() != null);
2220 
2221  CheckContextMatch(arg);
2222  return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
2223  }
Expr MkSetDel ( Expr  set,
Expr  element 
)
inline

Remove an element from a set.

Definition at line 2163 of file Context.cs.

2164  {
2165  Contract.Requires(set != null);
2166  Contract.Requires(element != null);
2167  Contract.Ensures(Contract.Result<Expr>() != null);
2168 
2169  CheckContextMatch(set);
2170  CheckContextMatch(element);
2171  return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
2172  }
Expr MkSetDifference ( Expr  arg1,
Expr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2202 of file Context.cs.

2203  {
2204  Contract.Requires(arg1 != null);
2205  Contract.Requires(arg2 != null);
2206  Contract.Ensures(Contract.Result<Expr>() != null);
2207 
2208  CheckContextMatch(arg1);
2209  CheckContextMatch(arg2);
2210  return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
2211  }
Expr MkSetIntersection ( params Expr[]  args)
inline

Take the intersection of a list of sets.

Definition at line 2189 of file Context.cs.

2190  {
2191  Contract.Requires(args != null);
2192  Contract.Requires(Contract.ForAll(args, a => a != null));
2193  Contract.Ensures(Contract.Result<Expr>() != null);
2194 
2195  CheckContextMatch(args);
2196  return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2197  }
Expr MkSetMembership ( Expr  elem,
Expr  set 
)
inline

Check for set membership.

Definition at line 2228 of file Context.cs.

2229  {
2230  Contract.Requires(elem != null);
2231  Contract.Requires(set != null);
2232  Contract.Ensures(Contract.Result<Expr>() != null);
2233 
2234  CheckContextMatch(elem);
2235  CheckContextMatch(set);
2236  return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
2237  }
SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2112 of file Context.cs.

2113  {
2114  Contract.Requires(ty != null);
2115  Contract.Ensures(Contract.Result<SetSort>() != null);
2116 
2117  CheckContextMatch(ty);
2118  return new SetSort(this, ty);
2119  }
Expr MkSetSubset ( Expr  arg1,
Expr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2242 of file Context.cs.

2243  {
2244  Contract.Requires(arg1 != null);
2245  Contract.Requires(arg2 != null);
2246  Contract.Ensures(Contract.Result<Expr>() != null);
2247 
2248  CheckContextMatch(arg1);
2249  CheckContextMatch(arg2);
2250  return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
2251  }
Expr MkSetUnion ( params Expr[]  args)
inline

Take the union of a list of sets.

Definition at line 2177 of file Context.cs.

2178  {
2179  Contract.Requires(args != null);
2180  Contract.Requires(Contract.ForAll(args, a => a != null));
2181 
2182  CheckContextMatch(args);
2183  return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
2184  }
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 1610 of file Context.cs.

1611  {
1612  Contract.Requires(t != null);
1613  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1614 
1615  CheckContextMatch(t);
1616  return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
1617  }
Solver MkSimpleSolver ( )
inline

Creates a new (incremental) solver.

Definition at line 3406 of file Context.cs.

3407  {
3408  Contract.Ensures(Contract.Result<Solver>() != null);
3409 
3410  return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
3411  }
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 3382 of file Context.cs.

3383  {
3384  Contract.Ensures(Contract.Result<Solver>() != null);
3385 
3386  if (logic == null)
3387  return new Solver(this, Native.Z3_mk_solver(nCtx));
3388  else
3389  return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
3390  }
Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See also
MkSolver(Symbol)

Definition at line 3396 of file Context.cs.

3397  {
3398  Contract.Ensures(Contract.Result<Solver>() != null);
3399 
3400  return MkSolver(MkSymbol(logic));
3401  }
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3382
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 3420 of file Context.cs.

3421  {
3422  Contract.Requires(t != null);
3423  Contract.Ensures(Contract.Result<Solver>() != null);
3424 
3425  return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
3426  }
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 2036 of file Context.cs.

2037  {
2038  Contract.Requires(a != null);
2039  Contract.Requires(i != null);
2040  Contract.Requires(v != null);
2041  Contract.Ensures(Contract.Result<ArrayExpr>() != null);
2042 
2043  CheckContextMatch(a);
2044  CheckContextMatch(i);
2045  CheckContextMatch(v);
2046  return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
2047  }
ArithExpr MkSub ( 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_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
961  }
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().

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

Referenced by Goal.Simplify().

2958  {
2959  Contract.Ensures(Contract.Result<Tactic>() != null);
2960 
2961  return new Tactic(this, name);
2962  }
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 2098 of file Context.cs.

2099  {
2100  Contract.Requires(array != null);
2101  Contract.Ensures(Contract.Result<Expr>() != null);
2102 
2103  CheckContextMatch(array);
2104  return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
2105  }
BoolExpr MkTrue ( )
inline

The true Term.

Definition at line 766 of file Context.cs.

767  {
768  Contract.Ensures(Contract.Result<BoolExpr>() != null);
769 
770  return new BoolExpr(this, Native.Z3_mk_true(nCtx));
771  }
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 966 of file Context.cs.

967  {
968  Contract.Requires(t != null);
969  Contract.Ensures(Contract.Result<ArithExpr>() != null);
970 
971  CheckContextMatch(t);
972  return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
973  }
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
BoolExpr MkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 883 of file Context.cs.

884  {
885  Contract.Requires(t1 != null);
886  Contract.Requires(t2 != null);
887  Contract.Ensures(Contract.Result<BoolExpr>() != null);
888 
889  CheckContextMatch(t1);
890  CheckContextMatch(t2);
891  return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
892  }
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 1628 of file Context.cs.

1629  {
1630  Contract.Requires(t != null);
1631  Contract.Ensures(Contract.Result<BitVecExpr>() != null);
1632 
1633  CheckContextMatch(t);
1634  return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
1635  }
Probe Not ( Probe  p)
inline

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

Definition at line 3363 of file Context.cs.

3364  {
3365  Contract.Requires(p != null);
3366  Contract.Ensures(Contract.Result<Probe>() != null);
3367 
3368  CheckContextMatch(p);
3369  return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
3370  }
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 3348 of file Context.cs.

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

3018  {
3019  Contract.Requires(t1 != null);
3020  Contract.Requires(t2 != null);
3021  Contract.Ensures(Contract.Result<Tactic>() != null);
3022 
3023  CheckContextMatch(t1);
3024  CheckContextMatch(t2);
3025  return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
3026  }
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 3177 of file Context.cs.

3178  {
3179  Contract.Requires(t1 != null);
3180  Contract.Requires(t2 != null);
3181  Contract.Ensures(Contract.Result<Tactic>() != null);
3182 
3183  CheckContextMatch(t1);
3184  CheckContextMatch(t2);
3185  return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
3186  }
Tactic ParOr ( params Tactic[]  t)
inline

Create a tactic that applies the given tactics in parallel.

Definition at line 3164 of file Context.cs.

3165  {
3166  Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
3167  Contract.Ensures(Contract.Result<Tactic>() != null);
3168 
3169  CheckContextMatch(t);
3170  return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
3171  }
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 2871 of file Context.cs.

2872  {
2873  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2874 
2875  uint csn = Symbol.ArrayLength(sortNames);
2876  uint cs = Sort.ArrayLength(sorts);
2877  uint cdn = Symbol.ArrayLength(declNames);
2878  uint cd = AST.ArrayLength(decls);
2879  if (csn != cs || cdn != cd)
2880  throw new Z3Exception("Argument size mismatch");
2881  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
2882  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2883  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2884  }
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 2852 of file Context.cs.

2853  {
2854  Contract.Ensures(Contract.Result<BoolExpr>() != null);
2855 
2856  uint csn = Symbol.ArrayLength(sortNames);
2857  uint cs = Sort.ArrayLength(sorts);
2858  uint cdn = Symbol.ArrayLength(declNames);
2859  uint cd = AST.ArrayLength(decls);
2860  if (csn != cs || cdn != cd)
2861  throw new Z3Exception("Argument size mismatch");
2862  return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
2863  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2864  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
2865  }
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 2746 of file Context.cs.

2747  {
2748  uint csn = Symbol.ArrayLength(sortNames);
2749  uint cs = Sort.ArrayLength(sorts);
2750  uint cdn = Symbol.ArrayLength(declNames);
2751  uint cd = AST.ArrayLength(decls);
2752  if (csn != cs || cdn != cd)
2753  throw new Z3Exception("Argument size mismatch");
2754  Native.Z3_parse_smtlib_file(nCtx, fileName,
2755  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2756  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2757  }
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 2729 of file Context.cs.

2730  {
2731  uint csn = Symbol.ArrayLength(sortNames);
2732  uint cs = Sort.ArrayLength(sorts);
2733  uint cdn = Symbol.ArrayLength(declNames);
2734  uint cd = AST.ArrayLength(decls);
2735  if (csn != cs || cdn != cd)
2736  throw new Z3Exception("Argument size mismatch");
2737  Native.Z3_parse_smtlib_string(nCtx, str,
2738  AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
2739  AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
2740  }
string ProbeDescription ( string  name)
inline

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

Definition at line 3227 of file Context.cs.

3228  {
3229  Contract.Ensures(Contract.Result<string>() != null);
3230 
3231  return Native.Z3_probe_get_descr(nCtx, name);
3232  }
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 3082 of file Context.cs.

3083  {
3084  Contract.Requires(t != null);
3085  Contract.Ensures(Contract.Result<Tactic>() != null);
3086 
3087  CheckContextMatch(t);
3088  return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
3089  }
string SimplifyHelp ( )
inline

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

Definition at line 3478 of file Context.cs.

3479  {
3480  Contract.Ensures(Contract.Result<string>() != null);
3481 
3482  return Native.Z3_simplify_get_help(nCtx);
3483  }
Tactic Skip ( )
inline

Create a tactic that just returns the given goal.

Definition at line 3094 of file Context.cs.

3095  {
3096  Contract.Ensures(Contract.Result<Tactic>() != null);
3097 
3098  return new Tactic(this, Native.Z3_tactic_skip(nCtx));
3099  }
string TacticDescription ( string  name)
inline

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

Definition at line 2947 of file Context.cs.

2948  {
2949  Contract.Ensures(Contract.Result<string>() != null);
2950 
2951  return Native.Z3_tactic_get_descr(nCtx, name);
2952  }
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 3003 of file Context.cs.

3004  {
3005  Contract.Requires(t1 != null);
3006  Contract.Requires(t2 != null);
3007  Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
3008  Contract.Ensures(Contract.Result<Tactic>() != null);
3009 
3010  return AndThen(t1, t2, ts);
3011  }
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:2968
static void ToggleWarningMessages ( bool  enabled)
inlinestatic

Enable/disable printing of warning messages to the console.

Note that this function is static and effects the behaviour of all contexts globally.

Definition at line 3498 of file Context.cs.

3499  {
3500  Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
3501  }
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 3034 of file Context.cs.

3035  {
3036  Contract.Requires(t != null);
3037  Contract.Ensures(Contract.Result<Tactic>() != null);
3038 
3039  CheckContextMatch(t);
3040  return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
3041  }
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 3470 of file Context.cs.

3471  {
3472  return a.NativeObject;
3473  }
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 3530 of file Context.cs.

3531  {
3532  Native.Z3_update_param_value(nCtx, id, value);
3533  }
Tactic UsingParams ( Tactic  t,
Params  p 
)
inline

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

Definition at line 3137 of file Context.cs.

3138  {
3139  Contract.Requires(t != null);
3140  Contract.Requires(p != null);
3141  Contract.Ensures(Contract.Result<Tactic>() != null);
3142 
3143  CheckContextMatch(t);
3144  CheckContextMatch(p);
3145  return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
3146  }
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 3050 of file Context.cs.

3051  {
3052  Contract.Requires(p != null);
3053  Contract.Requires(t != null);
3054  Contract.Ensures(Contract.Result<Tactic>() != null);
3055 
3056  CheckContextMatch(t);
3057  CheckContextMatch(p);
3058  return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
3059  }
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 3152 of file Context.cs.

3153  {
3154  Contract.Requires(t != null);
3155  Contract.Requires(p != null);
3156  Contract.Ensures(Contract.Result<Tactic>() != null);
3157 
3158  return UsingParams(t, p);
3159  }
Tactic UsingParams(Tactic t, Params p)
Create a tactic that applies t using the given set of parameters p .
Definition: Context.cs:3137
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 3453 of file Context.cs.

3454  {
3455  Contract.Ensures(Contract.Result<AST>() != null);
3456  return AST.Create(this, nativeObject);
3457  }

Property Documentation

BoolSort BoolSort
get

Retrieves the Boolean sort of the context.

Definition at line 127 of file Context.cs.

IntSort IntSort
get

Retrieves the Integer sort of the context.

Definition at line 139 of file Context.cs.

uint NumProbes
get

The number of supported Probes.

Definition at line 3203 of file Context.cs.

uint NumSMTLIBAssumptions
get

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

Definition at line 2784 of file Context.cs.

uint NumSMTLIBDecls
get

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

Definition at line 2806 of file Context.cs.

uint NumSMTLIBFormulas
get

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

Definition at line 2762 of file Context.cs.

uint NumSMTLIBSorts
get

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

Definition at line 2828 of file Context.cs.

uint NumTactics
get

The number of supported tactics.

Definition at line 2923 of file Context.cs.

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

string [] ProbeNames
get

The names of all supported Probes.

Definition at line 3211 of file Context.cs.

RealSort RealSort
get

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

BoolExpr [] SMTLIBAssumptions
get

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

Definition at line 2790 of file Context.cs.

FuncDecl [] SMTLIBDecls
get

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

Definition at line 2812 of file Context.cs.

BoolExpr [] SMTLIBFormulas
get

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

Definition at line 2768 of file Context.cs.

Sort [] SMTLIBSorts
get

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

Definition at line 2834 of file Context.cs.

string [] TacticNames
get

The names of all supported tactics.

Definition at line 2931 of file Context.cs.