Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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.
 
 Context (Dictionary< string, string > settings)
 Constructor.
 
IntSymbol MkSymbol (int i)
 Creates a new symbol using an integer.
 
StringSymbol MkSymbol (string name)
 Create a symbol using a string.
 
BoolSort MkBoolSort ()
 Create a new Boolean sort.
 
UninterpretedSort MkUninterpretedSort (Symbol s)
 Create a new uninterpreted sort.
 
UninterpretedSort MkUninterpretedSort (string str)
 Create a new uninterpreted sort.
 
IntSort MkIntSort ()
 Create a new integer sort.
 
RealSort MkRealSort ()
 Create a real sort.
 
BitVecSort MkBitVecSort (uint size)
 Create a new bit-vector sort.
 
ArraySort MkArraySort (Sort domain, Sort range)
 Create a new array sort.
 
TupleSort MkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 Create a new tuple sort.
 
EnumSort MkEnumSort (Symbol name, Symbol[] enumNames)
 Create a new enumeration sort.
 
EnumSort MkEnumSort (string name, string[] enumNames)
 Create a new enumeration sort.
 
ListSort MkListSort (Symbol name, Sort elemSort)
 Create a new list sort.
 
ListSort MkListSort (string name, Sort elemSort)
 Create a new list sort.
 
FiniteDomainSort MkFiniteDomainSort (Symbol name, ulong size)
 Create a new finite domain sort.
 
FiniteDomainSort MkFiniteDomainSort (string name, ulong size)
 Create a new finite domain sort.
 
Constructor MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
 Create a datatype constructor.
 
Constructor MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
 Create a datatype constructor.
 
DatatypeSort MkDatatypeSort (Symbol name, Constructor[] constructors)
 Create a new datatype sort.
 
DatatypeSort MkDatatypeSort (string name, Constructor[] constructors)
 Create a new datatype sort.
 
DatatypeSort[] MkDatatypeSorts (Symbol[] names, Constructor[][] c)
 Create mutually recursive datatypes.
 
DatatypeSort[] MkDatatypeSorts (string[] names, Constructor[][] c)
 Create mutually recursive data-types.
 
FuncDecl MkFuncDecl (Symbol name, Sort[] domain, Sort range)
 Creates a new function declaration.
 
FuncDecl MkFuncDecl (Symbol name, Sort domain, Sort range)
 Creates a new function declaration.
 
FuncDecl MkFuncDecl (string name, Sort[] domain, Sort range)
 Creates a new function declaration.
 
FuncDecl MkFuncDecl (string name, Sort domain, Sort range)
 Creates a new function declaration.
 
FuncDecl MkFreshFuncDecl (string prefix, Sort[] domain, Sort range)
 Creates a fresh function declaration with a name prefixed with prefix .
 
FuncDecl MkConstDecl (Symbol name, Sort range)
 Creates a new constant function declaration.
 
FuncDecl MkConstDecl (string name, Sort range)
 Creates a new constant function declaration.
 
FuncDecl MkFreshConstDecl (string prefix, Sort range)
 Creates a fresh constant function declaration with a name prefixed with prefix .
 
Expr MkBound (uint index, Sort ty)
 Creates a new bound variable.
 
Pattern MkPattern (params Expr[] terms)
 Create a quantifier pattern.
 
Expr MkConst (Symbol name, Sort range)
 Creates a new Constant of sort range and named name .
 
Expr MkConst (string name, Sort range)
 Creates a new Constant of sort range and named name .
 
Expr MkFreshConst (string prefix, Sort range)
 Creates a fresh Constant of sort range and a name prefixed with prefix .
 
Expr MkConst (FuncDecl f)
 Creates a fresh constant from the FuncDecl f .
 
BoolExpr MkBoolConst (Symbol name)
 Create a Boolean constant.
 
BoolExpr MkBoolConst (string name)
 Create a Boolean constant.
 
IntExpr MkIntConst (Symbol name)
 Creates an integer constant.
 
IntExpr MkIntConst (string name)
 Creates an integer constant.
 
RealExpr MkRealConst (Symbol name)
 Creates a real constant.
 
RealExpr MkRealConst (string name)
 Creates a real constant.
 
BitVecExpr MkBVConst (Symbol name, uint size)
 Creates a bit-vector constant.
 
BitVecExpr MkBVConst (string name, uint size)
 Creates a bit-vector constant.
 
Expr MkApp (FuncDecl f, params Expr[] args)
 Create a new function application.
 
BoolExpr MkTrue ()
 The true Term.
 
BoolExpr MkFalse ()
 The false Term.
 
BoolExpr MkBool (bool value)
 Creates a Boolean value.
 
BoolExpr MkEq (Expr x, Expr y)
 Creates the equality x = y .
 
BoolExpr MkDistinct (params Expr[] args)
 Creates a distinct term.
 
BoolExpr MkNot (BoolExpr a)
 Mk an expression representing not(a).
 
Expr MkITE (BoolExpr t1, Expr t2, Expr t3)
 Create an expression representing an if-then-else: ite(t1, t2, t3).
 
BoolExpr MkIff (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 iff t2.
 
BoolExpr MkImplies (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 -> t2.
 
BoolExpr MkXor (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 xor t2.
 
BoolExpr MkAnd (params BoolExpr[] t)
 Create an expression representing t[0] and t[1] and ....
 
BoolExpr MkOr (params BoolExpr[] t)
 Create an expression representing t[0] or t[1] or ....
 
ArithExpr MkAdd (params ArithExpr[] t)
 Create an expression representing t[0] + t[1] + ....
 
ArithExpr MkMul (params ArithExpr[] t)
 Create an expression representing t[0] * t[1] * ....
 
ArithExpr MkSub (params ArithExpr[] t)
 Create an expression representing t[0] - t[1] - ....
 
ArithExpr MkUnaryMinus (ArithExpr t)
 Create an expression representing -t.
 
ArithExpr MkDiv (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 / t2.
 
IntExpr MkMod (IntExpr t1, IntExpr t2)
 Create an expression representing t1 mod t2.
 
IntExpr MkRem (IntExpr t1, IntExpr t2)
 Create an expression representing t1 rem t2.
 
ArithExpr MkPower (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 ^ t2.
 
BoolExpr MkLt (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 < t2
 
BoolExpr MkLe (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 <= t2
 
BoolExpr MkGt (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 > t2
 
BoolExpr MkGe (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 >= t2
 
RealExpr MkInt2Real (IntExpr t)
 Coerce an integer to a real.
 
IntExpr MkReal2Int (RealExpr t)
 Coerce a real to an integer.
 
BoolExpr MkIsInteger (RealExpr t)
 Creates an expression that checks whether a real number is an integer.
 
BitVecExpr MkBVNot (BitVecExpr t)
 Bitwise negation.
 
BitVecExpr MkBVRedAND (BitVecExpr t)
 Take conjunction of bits in a vector, return vector of length 1.
 
BitVecExpr MkBVRedOR (BitVecExpr t)
 Take disjunction of bits in a vector, return vector of length 1.
 
BitVecExpr MkBVAND (BitVecExpr t1, BitVecExpr t2)
 Bitwise conjunction.
 
BitVecExpr MkBVOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise disjunction.
 
BitVecExpr MkBVXOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise XOR.
 
BitVecExpr MkBVNAND (BitVecExpr t1, BitVecExpr t2)
 Bitwise NAND.
 
BitVecExpr MkBVNOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise NOR.
 
BitVecExpr MkBVXNOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise XNOR.
 
BitVecExpr MkBVNeg (BitVecExpr t)
 Standard two's complement unary minus.
 
BitVecExpr MkBVAdd (BitVecExpr t1, BitVecExpr t2)
 Two's complement addition.
 
BitVecExpr MkBVSub (BitVecExpr t1, BitVecExpr t2)
 Two's complement subtraction.
 
BitVecExpr MkBVMul (BitVecExpr t1, BitVecExpr t2)
 Two's complement multiplication.
 
BitVecExpr MkBVUDiv (BitVecExpr t1, BitVecExpr t2)
 Unsigned division.
 
BitVecExpr MkBVSDiv (BitVecExpr t1, BitVecExpr t2)
 Signed division.
 
BitVecExpr MkBVURem (BitVecExpr t1, BitVecExpr t2)
 Unsigned remainder.
 
BitVecExpr MkBVSRem (BitVecExpr t1, BitVecExpr t2)
 Signed remainder.
 
BitVecExpr MkBVSMod (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed remainder (sign follows divisor).
 
BoolExpr MkBVULT (BitVecExpr t1, BitVecExpr t2)
 Unsigned less-than
 
BoolExpr MkBVSLT (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed less-than
 
BoolExpr MkBVULE (BitVecExpr t1, BitVecExpr t2)
 Unsigned less-than or equal to.
 
BoolExpr MkBVSLE (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed less-than or equal to.
 
BoolExpr MkBVUGE (BitVecExpr t1, BitVecExpr t2)
 Unsigned greater than or equal to.
 
BoolExpr MkBVSGE (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed greater than or equal to.
 
BoolExpr MkBVUGT (BitVecExpr t1, BitVecExpr t2)
 Unsigned greater-than.
 
BoolExpr MkBVSGT (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed greater-than.
 
BitVecExpr MkConcat (BitVecExpr t1, BitVecExpr t2)
 Bit-vector concatenation.
 
BitVecExpr MkExtract (uint high, uint low, BitVecExpr t)
 Bit-vector extraction.
 
BitVecExpr MkSignExt (uint i, BitVecExpr t)
 Bit-vector sign extension.
 
BitVecExpr MkZeroExt (uint i, BitVecExpr t)
 Bit-vector zero extension.
 
BitVecExpr MkRepeat (uint i, BitVecExpr t)
 Bit-vector repetition.
 
BitVecExpr MkBVSHL (BitVecExpr t1, BitVecExpr t2)
 Shift left.
 
BitVecExpr MkBVLSHR (BitVecExpr t1, BitVecExpr t2)
 Logical shift right
 
BitVecExpr MkBVASHR (BitVecExpr t1, BitVecExpr t2)
 Arithmetic shift right
 
BitVecExpr MkBVRotateLeft (uint i, BitVecExpr t)
 Rotate Left.
 
BitVecExpr MkBVRotateRight (uint i, BitVecExpr t)
 Rotate Right.
 
BitVecExpr MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
 Rotate Left.
 
BitVecExpr MkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
 Rotate Right.
 
BitVecExpr MkInt2BV (uint n, IntExpr t)
 Create an n bit bit-vector from the integer argument t .
 
IntExpr MkBV2Int (BitVecExpr t, bool signed)
 Create an integer from the bit-vector argument t .
 
BoolExpr MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
 Create a predicate that checks that the bit-wise addition does not overflow.
 
BoolExpr MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise addition does not underflow.
 
BoolExpr MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise subtraction does not overflow.
 
BoolExpr MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
 Create a predicate that checks that the bit-wise subtraction does not underflow.
 
BoolExpr MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise signed division does not overflow.
 
BoolExpr MkBVNegNoOverflow (BitVecExpr t)
 Create a predicate that checks that the bit-wise negation does not overflow.
 
BoolExpr MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
 Create a predicate that checks that the bit-wise multiplication does not overflow.
 
BoolExpr MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise multiplication does not underflow.
 
ArrayExpr MkArrayConst (Symbol name, Sort domain, Sort range)
 Create an array constant.
 
ArrayExpr MkArrayConst (string name, Sort domain, Sort range)
 Create an array constant.
 
Expr MkSelect (ArrayExpr a, Expr i)
 Array read.
 
ArrayExpr MkStore (ArrayExpr a, Expr i, Expr v)
 Array update.
 
ArrayExpr MkConstArray (Sort domain, Expr v)
 Create a constant array.
 
ArrayExpr MkMap (FuncDecl f, params ArrayExpr[] args)
 Maps f on the argument arrays.
 
Expr MkTermArray (ArrayExpr array)
 Access the array default value.
 
SetSort MkSetSort (Sort ty)
 Create a set type.
 
Expr MkEmptySet (Sort domain)
 Create an empty set.
 
Expr MkFullSet (Sort domain)
 Create the full set.
 
Expr MkSetAdd (Expr set, Expr element)
 Add an element to the set.
 
Expr MkSetDel (Expr set, Expr element)
 Remove an element from a set.
 
Expr MkSetUnion (params Expr[] args)
 Take the union of a list of sets.
 
Expr MkSetIntersection (params Expr[] args)
 Take the intersection of a list of sets.
 
Expr MkSetDifference (Expr arg1, Expr arg2)
 Take the difference between two sets.
 
Expr MkSetComplement (Expr arg)
 Take the complement of a set.
 
Expr MkSetMembership (Expr elem, Expr set)
 Check for set membership.
 
Expr MkSetSubset (Expr arg1, Expr arg2)
 Check for subsetness of sets.
 
Expr MkNumeral (string v, Sort ty)
 Create a Term of a given sort.
 
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.
 
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.
 
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.
 
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.
 
RatNum MkReal (int num, int den)
 Create a real from a fraction.
 
RatNum MkReal (string v)
 Create a real numeral.
 
RatNum MkReal (int v)
 Create a real numeral.
 
RatNum MkReal (uint v)
 Create a real numeral.
 
RatNum MkReal (long v)
 Create a real numeral.
 
RatNum MkReal (ulong v)
 Create a real numeral.
 
IntNum MkInt (string v)
 Create an integer numeral.
 
IntNum MkInt (int v)
 Create an integer numeral.
 
IntNum MkInt (uint v)
 Create an integer numeral.
 
IntNum MkInt (long v)
 Create an integer numeral.
 
IntNum MkInt (ulong v)
 Create an integer numeral.
 
BitVecNum MkBV (string v, uint size)
 Create a bit-vector numeral.
 
BitVecNum MkBV (int v, uint size)
 Create a bit-vector numeral.
 
BitVecNum MkBV (uint v, uint size)
 Create a bit-vector numeral.
 
BitVecNum MkBV (long v, uint size)
 Create a bit-vector numeral.
 
BitVecNum MkBV (ulong v, uint size)
 Create a bit-vector numeral.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
string BenchmarkToSMTString (string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
 Convert a benchmark into an SMT-LIB formatted string.
 
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.
 
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.
 
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.
 
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.
 
Goal MkGoal (bool models=true, bool unsatCores=false, bool proofs=false)
 Creates a new Goal.
 
Params MkParams ()
 Creates a new ParameterSet.
 
string TacticDescription (string name)
 Returns a string containing a description of the tactic with the given name.
 
Tactic MkTactic (string name)
 Creates a new Tactic.
 
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 .
 
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 .
 
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.
 
Tactic TryFor (Tactic t, uint ms)
 Create a tactic that applies t to a goal for ms milliseconds.
 
Tactic When (Probe p, Tactic t)
 Create a tactic that applies t to a given goal if the probe p evaluates to true.
 
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.
 
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.
 
Tactic Skip ()
 Create a tactic that just returns the given goal.
 
Tactic Fail ()
 Create a tactic always fails.
 
Tactic FailIf (Probe p)
 Create a tactic that fails if the probe p evaluates to false.
 
Tactic FailIfNotDecided ()
 Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').
 
Tactic UsingParams (Tactic t, Params p)
 Create a tactic that applies t using the given set of parameters p .
 
Tactic With (Tactic t, Params p)
 Create a tactic that applies t using the given set of parameters p .
 
Tactic ParOr (params Tactic[] t)
 Create a tactic that applies the given tactics in parallel.
 
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.
 
void Interrupt ()
 Interrupt the execution of a Z3 procedure.
 
string ProbeDescription (string name)
 Returns a string containing a description of the probe with the given name.
 
Probe MkProbe (string name)
 Creates a new Probe.
 
Probe Const (double val)
 Create a probe that always evaluates to val .
 
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
 
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
 
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
 
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
 
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
 
Probe And (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
 
Probe Or (Probe p1, Probe p2)
 Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
 
Probe Not (Probe p)
 Create a probe that evaluates to "true" when the value p does not evaluate to "true".
 
Solver MkSolver (Symbol logic=null)
 Creates a new (incremental) solver.
 
Solver MkSolver (string logic)
 Creates a new (incremental) solver.
 
Solver MkSimpleSolver ()
 Creates a new (incremental) solver.
 
Solver MkSolver (Tactic t)
 Creates a solver that is implemented using the given tactic.
 
Fixedpoint MkFixedpoint ()
 Create a Fixedpoint context.
 
AST WrapAST (IntPtr nativeObject)
 Wraps an AST.
 
IntPtr UnwrapAST (AST a)
 Unwraps an AST.
 
string SimplifyHelp ()
 Return a string describing all available parameters to Expr.Simplify.
 
void UpdateParamValue (string id, string value)
 Update a mutable configuration parameter.
 
string GetParamValue (string id)
 Get a configuration parameter.
 
void Dispose ()
 Disposes of the context.
 

Static Public Member Functions

static void ToggleWarningMessages (bool enabled)
 Enable/disable printing of warning messages to the console.
 

Properties

BoolSort BoolSort [get]
 Retrieves the Boolean sort of the context.
 
IntSort IntSort [get]
 Retrieves the Integer sort of the context.
 
RealSort RealSort [get]
 Retrieves the Real sort of the context.
 
Z3_ast_print_mode PrintMode [set]
 Selects the format used for pretty-printing expressions.
 
uint NumSMTLIBFormulas [get]
 The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
BoolExpr[] SMTLIBFormulas [get]
 The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
uint NumSMTLIBAssumptions [get]
 The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
BoolExpr[] SMTLIBAssumptions [get]
 The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
uint NumSMTLIBDecls [get]
 The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
FuncDecl[] SMTLIBDecls [get]
 The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
uint NumSMTLIBSorts [get]
 The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
Sort[] SMTLIBSorts [get]
 The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
 
uint NumTactics [get]
 The number of supported tactics.
 
string[] TacticNames [get]
 The names of all supported tactics.
 
uint NumProbes [get]
 The number of supported Probes.
 
string[] ProbeNames [get]
 The names of all supported Probes.
 
ParamDescrs SimplifyParameterDescriptions [get]
 Retrieves parameter descriptions for simplifier.
 

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.

: base()
{
m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
InitContext();
}
Context ( Dictionary< string, string >  settings)
inline

Constructor.

Definition at line 47 of file Context.cs.

: base()
{
Contract.Requires(settings != null);
IntPtr cfg = Native.Z3_mk_config();
foreach (KeyValuePair<string, string> kv in settings)
Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
m_ctx = Native.Z3_mk_context_rc(cfg);
Native.Z3_del_config(cfg);
InitContext();
}

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

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
}
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 2937 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
CheckContextMatch(ts);
IntPtr last = IntPtr.Zero;
if (ts != null && ts.Length > 0)
{
last = ts[ts.Length - 1].NativeObject;
for (int i = ts.Length - 2; i >= 0; i--)
last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
}
if (last != IntPtr.Zero)
{
last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
}
else
return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
}
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 2676 of file Context.cs.

{
Contract.Requires(assumptions != null);
Contract.Requires(formula != null);
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
formula.NativeObject);
}
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 3034 of file Context.cs.

{
Contract.Requires(p != null);
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(p);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
}
Probe Const ( double  val)
inline

Create a probe that always evaluates to val .

Definition at line 3216 of file Context.cs.

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

Disposes of the context.

Definition at line 3642 of file Context.cs.

{
// Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
AST_DRQ.Clear(this);
ASTMap_DRQ.Clear(this);
ASTVector_DRQ.Clear(this);
ApplyResult_DRQ.Clear(this);
FuncEntry_DRQ.Clear(this);
FuncInterp_DRQ.Clear(this);
Goal_DRQ.Clear(this);
Model_DRQ.Clear(this);
Params_DRQ.Clear(this);
Probe_DRQ.Clear(this);
Solver_DRQ.Clear(this);
Statistics_DRQ.Clear(this);
Tactic_DRQ.Clear(this);
Fixedpoint_DRQ.Clear(this);
m_boolSort = null;
m_intSort = null;
m_realSort = null;
}
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 3287 of file Context.cs.

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
}
Tactic Fail ( )
inline

Create a tactic always fails.

Definition at line 3073 of file Context.cs.

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

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

Definition at line 3083 of file Context.cs.

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

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

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
}
string GetParamValue ( string  id)
inline

Get a configuration parameter.

Returns null if the parameter value does not exist.

See Also
UpdateParamValue

Definition at line 3512 of file Context.cs.

{
IntPtr res = IntPtr.Zero;
int r = Native.Z3_get_param_value(nCtx, id, out res);
if (r == (int)Z3_lbool.Z3_L_FALSE)
return null;
else
return Marshal.PtrToStringAnsi(res);
}
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 3242 of file Context.cs.

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
}
void Interrupt ( )
inline

Interrupt the execution of a Z3 procedure.

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

Definition at line 3161 of file Context.cs.

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

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
}
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 3227 of file Context.cs.

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
}
ArithExpr MkAdd ( params ArithExpr[]  t)
inline

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

Definition at line 896 of file Context.cs.

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

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

Definition at line 868 of file Context.cs.

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

Create a new function application.

Definition at line 722 of file Context.cs.

{
Contract.Requires(f != null);
Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(f);
CheckContextMatch(args);
return Expr.Create(this, f, args);
}
ArrayExpr MkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1942 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<ArrayExpr>() != null);
return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
}
ArrayExpr MkArrayConst ( string  name,
Sort  domain,
Sort  range 
)
inline

Create an array constant.

Definition at line 1955 of file Context.cs.

{
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<ArrayExpr>() != null);
return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
}
ArraySort MkArraySort ( Sort  domain,
Sort  range 
)
inline

Create a new array sort.

Definition at line 202 of file Context.cs.

{
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<ArraySort>() != null);
CheckContextMatch(domain);
CheckContextMatch(range);
return new ArraySort(this, domain, range);
}
BitVecSort MkBitVecSort ( uint  size)
inline

Create a new bit-vector sort.

Definition at line 192 of file Context.cs.

{
Contract.Ensures(Contract.Result<BitVecSort>() != null);
return new BitVecSort(this, size);
}
BoolExpr MkBool ( bool  value)
inline

Creates a Boolean value.

Definition at line 757 of file Context.cs.

{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
return value ? MkTrue() : MkFalse();
}
BoolExpr MkBoolConst ( Symbol  name)
inline

Create a Boolean constant.

Definition at line 635 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
return (BoolExpr)MkConst(name, BoolSort);
}
BoolExpr MkBoolConst ( string  name)
inline

Create a Boolean constant.

Definition at line 646 of file Context.cs.

{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
}
BoolSort MkBoolSort ( )
inline

Create a new Boolean sort.

Definition at line 142 of file Context.cs.

{
Contract.Ensures(Contract.Result<BoolSort>() != null);
return new BoolSort(this);
}
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 552 of file Context.cs.

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

{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
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 2465 of file Context.cs.

{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
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 2477 of file Context.cs.

{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
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 2489 of file Context.cs.

{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
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 2501 of file Context.cs.

{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
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 1794 of file Context.cs.

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

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1253 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1809 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
}
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 1826 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise conjunction.

The arguments must have a bit-vector sort.

Definition at line 1150 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1681 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVConst ( Symbol  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 699 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
return (BitVecExpr)MkConst(name, MkBitVecSort(size));
}
BitVecExpr MkBVConst ( string  name,
uint  size 
)
inline

Creates a bit-vector constant.

Definition at line 710 of file Context.cs.

{
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
return (BitVecExpr)MkConst(name, MkBitVecSort(size));
}
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 1656 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVMul ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement multiplication.

The arguments must have the same bit-vector sort.

Definition at line 1283 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1909 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
}
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 1926 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVNAND ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise NAND.

The arguments must have a bit-vector sort.

Definition at line 1195 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVNeg ( BitVecExpr  t)
inline

Standard two's complement unary minus.

The arguments must have a bit-vector sort.

Definition at line 1240 of file Context.cs.

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

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

Bitwise NOR.

The arguments must have a bit-vector sort.

Definition at line 1210 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVNot ( BitVecExpr  t)
inline

Bitwise negation.

The argument must have a bit-vector sort.

Definition at line 1111 of file Context.cs.

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

Bitwise disjunction.

The arguments must have a bit-vector sort.

Definition at line 1165 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1124 of file Context.cs.

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

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

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

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1715 of file Context.cs.

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

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1327 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1877 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1487 of file Context.cs.

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

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1633 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1453 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1419 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1385 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1367 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVSub ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Two's complement subtraction.

The arguments must have the same bit-vector sort.

Definition at line 1268 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1843 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1860 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
}
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 1303 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1470 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
}
BoolExpr MkBVUGT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned greater-than.

The arguments must have the same bit-vector sort.

Definition at line 1504 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1436 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
}
BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Unsigned less-than

The arguments must have the same bit-vector sort.

Definition at line 1402 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1346 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVXNOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XNOR.

The arguments must have a bit-vector sort.

Definition at line 1225 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkBVXOR ( BitVecExpr  t1,
BitVecExpr  t2 
)
inline

Bitwise XOR.

The arguments must have a bit-vector sort.

Definition at line 1180 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1542 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
}
Expr MkConst ( Symbol  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 584 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(name);
CheckContextMatch(range);
return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
}
Expr MkConst ( string  name,
Sort  range 
)
inline

Creates a new Constant of sort range and named name .

Definition at line 599 of file Context.cs.

{
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<Expr>() != null);
return MkConst(MkSymbol(name), range);
}
Expr MkConst ( FuncDecl  f)
inline

Creates a fresh constant from the FuncDecl f .

Parameters
fA decl of a 0-arity function

Definition at line 624 of file Context.cs.

{
Contract.Requires(f != null);
Contract.Ensures(Contract.Result<Expr>() != null);
return MkApp(f);
}
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 2027 of file Context.cs.

{
Contract.Requires(domain != null);
Contract.Requires(v != null);
Contract.Ensures(Contract.Result<ArrayExpr>() != null);
CheckContextMatch(domain);
CheckContextMatch(v);
return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
}
FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 508 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(name);
CheckContextMatch(range);
return new FuncDecl(this, name, null, range);
}
FuncDecl MkConstDecl ( string  name,
Sort  range 
)
inline

Creates a new constant function declaration.

Definition at line 522 of file Context.cs.

{
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(range);
return new FuncDecl(this, MkSymbol(name), null, range);
}
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 317 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(recognizer != null);
Contract.Ensures(Contract.Result<Constructor>() != null);
return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
}
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 335 of file Context.cs.

{
Contract.Ensures(Contract.Result<Constructor>() != null);
return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
}
DatatypeSort MkDatatypeSort ( Symbol  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 345 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(constructors != null);
Contract.Requires(Contract.ForAll(constructors, c => c != null));
Contract.Ensures(Contract.Result<DatatypeSort>() != null);
CheckContextMatch(name);
CheckContextMatch(constructors);
return new DatatypeSort(this, name, constructors);
}
DatatypeSort MkDatatypeSort ( string  name,
Constructor[]  constructors 
)
inline

Create a new datatype sort.

Definition at line 361 of file Context.cs.

{
Contract.Requires(constructors != null);
Contract.Requires(Contract.ForAll(constructors, c => c != null));
Contract.Ensures(Contract.Result<DatatypeSort>() != null);
CheckContextMatch(constructors);
return new DatatypeSort(this, MkSymbol(name), constructors);
}
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 376 of file Context.cs.

{
Contract.Requires(names != null);
Contract.Requires(c != null);
Contract.Requires(names.Length == c.Length);
Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
Contract.Requires(Contract.ForAll(names, name => name != null));
Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
CheckContextMatch(names);
uint n = (uint)names.Length;
ConstructorList[] cla = new ConstructorList[n];
IntPtr[] n_constr = new IntPtr[n];
for (uint i = 0; i < n; i++)
{
var constructor = c[i];
Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
CheckContextMatch(constructor);
cla[i] = new ConstructorList(this, constructor);
n_constr[i] = cla[i].NativeObject;
}
IntPtr[] n_res = new IntPtr[n];
Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
DatatypeSort[] res = new DatatypeSort[n];
for (uint i = 0; i < n; i++)
res[i] = new DatatypeSort(this, n_res[i]);
return res;
}
DatatypeSort [] MkDatatypeSorts ( string[]  names,
Constructor  c[][] 
)
inline

Create mutually recursive data-types.

Parameters
names
c
Returns

Definition at line 411 of file Context.cs.

{
Contract.Requires(names != null);
Contract.Requires(c != null);
Contract.Requires(names.Length == c.Length);
Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
Contract.Requires(Contract.ForAll(names, name => name != null));
Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
return MkDatatypeSorts(MkSymbols(names), c);
}
BoolExpr MkDistinct ( params Expr[]  args)
inline

Creates a distinct term.

Definition at line 781 of file Context.cs.

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

Create an expression representing t1 / t2.

Definition at line 947 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<ArithExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
}
Expr MkEmptySet ( Sort  domain)
inline

Create an empty set.

Definition at line 2093 of file Context.cs.

{
Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain);
return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
}
EnumSort MkEnumSort ( Symbol  name,
Symbol[]  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 233 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(enumNames != null);
Contract.Requires(Contract.ForAll(enumNames, f => f != null));
Contract.Ensures(Contract.Result<EnumSort>() != null);
CheckContextMatch(name);
CheckContextMatch(enumNames);
return new EnumSort(this, name, enumNames);
}
EnumSort MkEnumSort ( string  name,
string[]  enumNames 
)
inline

Create a new enumeration sort.

Definition at line 249 of file Context.cs.

{
Contract.Requires(enumNames != null);
Contract.Ensures(Contract.Result<EnumSort>() != null);
return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
}
BoolExpr MkEq ( Expr  x,
Expr  y 
)
inline

Creates the equality x = y .

Definition at line 767 of file Context.cs.

{
Contract.Requires(x != null);
Contract.Requires(y != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(x);
CheckContextMatch(y);
return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
}
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 2567 of file Context.cs.

{
Contract.Requires(sorts != null);
Contract.Requires(names != null);
Contract.Requires(body != null);
Contract.Requires(sorts.Length == names.Length);
Contract.Requires(Contract.ForAll(sorts, s => s != null));
Contract.Requires(Contract.ForAll(names, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
}
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 2585 of file Context.cs.

{
Contract.Requires(body != null);
Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
}
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 1562 of file Context.cs.

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

The false Term.

Definition at line 747 of file Context.cs.

{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
return new BoolExpr(this, Native.Z3_mk_false(nCtx));
}
FiniteDomainSort MkFiniteDomainSort ( Symbol  name,
ulong  size 
)
inline

Create a new finite domain sort.

Definition at line 286 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
CheckContextMatch(name);
return new FiniteDomainSort(this, name, size);
}
FiniteDomainSort MkFiniteDomainSort ( string  name,
ulong  size 
)
inline

Create a new finite domain sort.

Definition at line 298 of file Context.cs.

{
Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
return new FiniteDomainSort(this, MkSymbol(name), size);
}
Fixedpoint MkFixedpoint ( )
inline

Create a Fixedpoint context.

Definition at line 3402 of file Context.cs.

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

{
Contract.Requires(sorts != null);
Contract.Requires(names != null);
Contract.Requires(body != null);
Contract.Requires(sorts.Length == names.Length);
Contract.Requires(Contract.ForAll(sorts, s => s != null));
Contract.Requires(Contract.ForAll(names, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
}
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 2551 of file Context.cs.

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

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

Definition at line 611 of file Context.cs.

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

{
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(range);
return new FuncDecl(this, prefix, null, range);
}
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 494 of file Context.cs.

{
Contract.Requires(range != null);
Contract.Requires(Contract.ForAll(domain, d => d != null));
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(domain);
CheckContextMatch(range);
return new FuncDecl(this, prefix, domain, range);
}
Expr MkFullSet ( Sort  domain)
inline

Create the full set.

Definition at line 2105 of file Context.cs.

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

Creates a new function declaration.

Definition at line 430 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(range != null);
Contract.Requires(Contract.ForAll(domain, d => d != null));
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(name);
CheckContextMatch(domain);
CheckContextMatch(range);
return new FuncDecl(this, name, domain, range);
}
FuncDecl MkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 446 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(name);
CheckContextMatch(domain);
CheckContextMatch(range);
Sort[] q = new Sort[] { domain };
return new FuncDecl(this, name, q, range);
}
FuncDecl MkFuncDecl ( string  name,
Sort[]  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 463 of file Context.cs.

{
Contract.Requires(range != null);
Contract.Requires(Contract.ForAll(domain, d => d != null));
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(domain);
CheckContextMatch(range);
return new FuncDecl(this, MkSymbol(name), domain, range);
}
FuncDecl MkFuncDecl ( string  name,
Sort  domain,
Sort  range 
)
inline

Creates a new function declaration.

Definition at line 477 of file Context.cs.

{
Contract.Requires(range != null);
Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<FuncDecl>() != null);
CheckContextMatch(domain);
CheckContextMatch(range);
Sort[] q = new Sort[] { domain };
return new FuncDecl(this, MkSymbol(name), q, range);
}
BoolExpr MkGe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 >= t2

Definition at line 1047 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
}
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 2867 of file Context.cs.

Referenced by Goal.Simplify().

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

Create an expression representing t1 > t2

Definition at line 1033 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
}
BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 iff t2.

Definition at line 826 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
}
BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 -> t2.

Definition at line 840 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
}
IntNum MkInt ( string  v)
inline

Create an integer numeral.

Parameters
vA string representing the Term value in decimal notation.

Definition at line 2391 of file Context.cs.

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

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

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

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

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

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

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

Creates an integer constant.

Definition at line 656 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<IntExpr>() != null);
return (IntExpr)MkConst(name, IntSort);
}
IntExpr MkIntConst ( string  name)
inline

Creates an integer constant.

Definition at line 667 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<IntExpr>() != null);
return (IntExpr)MkConst(name, IntSort);
}
IntSort MkIntSort ( )
inline

Create a new integer sort.

Definition at line 173 of file Context.cs.

{
Contract.Ensures(Contract.Result<IntSort>() != null);
return new IntSort(this);
}
BoolExpr MkIsInteger ( RealExpr  t)
inline

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

Definition at line 1096 of file Context.cs.

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

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Requires(t3 != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
CheckContextMatch(t3);
return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
}
BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 <= t2

Definition at line 1019 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
}
ListSort MkListSort ( Symbol  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 260 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(elemSort != null);
Contract.Ensures(Contract.Result<ListSort>() != null);
CheckContextMatch(name);
CheckContextMatch(elemSort);
return new ListSort(this, name, elemSort);
}
ListSort MkListSort ( string  name,
Sort  elemSort 
)
inline

Create a new list sort.

Definition at line 274 of file Context.cs.

{
Contract.Requires(elemSort != null);
Contract.Ensures(Contract.Result<ListSort>() != null);
CheckContextMatch(elemSort);
return new ListSort(this, MkSymbol(name), elemSort);
}
BoolExpr MkLt ( ArithExpr  t1,
ArithExpr  t2 
)
inline

Create an expression representing t1 < t2

Definition at line 1005 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
}
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 2049 of file Context.cs.

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

Create an expression representing t1 mod t2.

The arguments must have int type.

Definition at line 962 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<IntExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
}
ArithExpr MkMul ( params ArithExpr[]  t)
inline

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

Definition at line 909 of file Context.cs.

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

Mk an expression representing not(a).

Definition at line 795 of file Context.cs.

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

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

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

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

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

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

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

Definition at line 881 of file Context.cs.

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

Creates a new ParameterSet.

Definition at line 2879 of file Context.cs.

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

Create a quantifier pattern.

Definition at line 565 of file Context.cs.

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

Create an expression representing t1 ^ t2.

Definition at line 991 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<ArithExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
}
Probe MkProbe ( string  name)
inline

Creates a new Probe.

Definition at line 3206 of file Context.cs.

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

{
Contract.Requires(body != null);
Contract.Requires(names != null);
Contract.Requires(sorts != null);
Contract.Requires(sorts.Length == names.Length);
Contract.Requires(Contract.ForAll(sorts, s => s != null));
Contract.Requires(Contract.ForAll(names, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
if (universal)
return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
else
return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
}
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 2623 of file Context.cs.

{
Contract.Requires(body != null);
Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
if (universal)
return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
else
return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
}
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 2314 of file Context.cs.

{
if (den == 0)
throw new Z3Exception("Denominator is zero");
Contract.Ensures(Contract.Result<RatNum>() != null);
Contract.EndContractBlock();
return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
}
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 2330 of file Context.cs.

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

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

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

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

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

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

Creates a real constant.

Definition at line 678 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Ensures(Contract.Result<RealExpr>() != null);
return (RealExpr)MkConst(name, RealSort);
}
RealExpr MkRealConst ( string  name)
inline

Creates a real constant.

Definition at line 689 of file Context.cs.

{
Contract.Ensures(Contract.Result<RealExpr>() != null);
return (RealExpr)MkConst(name, RealSort);
}
RealSort MkRealSort ( )
inline

Create a real sort.

Definition at line 183 of file Context.cs.

{
Contract.Ensures(Contract.Result<RealSort>() != null);
return new RealSort(this);
}
IntExpr MkRem ( IntExpr  t1,
IntExpr  t2 
)
inline

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 977 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<IntExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
}
BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
)
inline

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1612 of file Context.cs.

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

{
Contract.Requires(a != null);
Contract.Requires(i != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(a);
CheckContextMatch(i);
return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
}
Expr MkSetAdd ( Expr  set,
Expr  element 
)
inline

Add an element to the set.

Definition at line 2117 of file Context.cs.

{
Contract.Requires(set != null);
Contract.Requires(element != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(set);
CheckContextMatch(element);
return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
}
Expr MkSetComplement ( Expr  arg)
inline

Take the complement of a set.

Definition at line 2185 of file Context.cs.

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

Remove an element from a set.

Definition at line 2132 of file Context.cs.

{
Contract.Requires(set != null);
Contract.Requires(element != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(set);
CheckContextMatch(element);
return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
}
Expr MkSetDifference ( Expr  arg1,
Expr  arg2 
)
inline

Take the difference between two sets.

Definition at line 2171 of file Context.cs.

{
Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(arg1);
CheckContextMatch(arg2);
return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
}
Expr MkSetIntersection ( params Expr[]  args)
inline

Take the intersection of a list of sets.

Definition at line 2158 of file Context.cs.

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

Check for set membership.

Definition at line 2197 of file Context.cs.

{
Contract.Requires(elem != null);
Contract.Requires(set != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(elem);
CheckContextMatch(set);
return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
}
SetSort MkSetSort ( Sort  ty)
inline

Create a set type.

Definition at line 2081 of file Context.cs.

{
Contract.Requires(ty != null);
Contract.Ensures(Contract.Result<SetSort>() != null);
CheckContextMatch(ty);
return new SetSort(this, ty);
}
Expr MkSetSubset ( Expr  arg1,
Expr  arg2 
)
inline

Check for subsetness of sets.

Definition at line 2211 of file Context.cs.

{
Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(arg1);
CheckContextMatch(arg2);
return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
}
Expr MkSetUnion ( params Expr[]  args)
inline

Take the union of a list of sets.

Definition at line 2146 of file Context.cs.

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

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

Creates a new (incremental) solver.

Definition at line 3375 of file Context.cs.

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

{
Contract.Ensures(Contract.Result<Solver>() != null);
if (logic == null)
return new Solver(this, Native.Z3_mk_solver(nCtx));
else
return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
}
Solver MkSolver ( string  logic)
inline

Creates a new (incremental) solver.

See Also
MkSolver(Symbol)

Definition at line 3365 of file Context.cs.

{
Contract.Ensures(Contract.Result<Solver>() != null);
return MkSolver(MkSymbol(logic));
}
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 3389 of file Context.cs.

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

{
Contract.Requires(a != null);
Contract.Requires(i != null);
Contract.Requires(v != null);
Contract.Ensures(Contract.Result<ArrayExpr>() != null);
CheckContextMatch(a);
CheckContextMatch(i);
CheckContextMatch(v);
return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
}
ArithExpr MkSub ( params ArithExpr[]  t)
inline

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

Definition at line 922 of file Context.cs.

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

Referenced by Params.Add().

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

Create a symbol using a string.

Definition at line 79 of file Context.cs.

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

Creates a new Tactic.

Definition at line 2926 of file Context.cs.

Referenced by Goal.Simplify().

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

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

The true Term.

Definition at line 737 of file Context.cs.

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

Create a new tuple sort.

Definition at line 216 of file Context.cs.

{
Contract.Requires(name != null);
Contract.Requires(fieldNames != null);
Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
Contract.Ensures(Contract.Result<TupleSort>() != null);
CheckContextMatch(name);
CheckContextMatch(fieldNames);
CheckContextMatch(fieldSorts);
return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
}
ArithExpr MkUnaryMinus ( ArithExpr  t)
inline

Create an expression representing -t.

Definition at line 935 of file Context.cs.

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

Create a new uninterpreted sort.

Definition at line 151 of file Context.cs.

{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
CheckContextMatch(s);
return new UninterpretedSort(this, s);
}
UninterpretedSort MkUninterpretedSort ( string  str)
inline

Create a new uninterpreted sort.

Definition at line 163 of file Context.cs.

{
Contract.Ensures(Contract.Result<UninterpretedSort>() != null);
return MkUninterpretedSort(MkSymbol(str));
}
BoolExpr MkXor ( BoolExpr  t1,
BoolExpr  t2 
)
inline

Create an expression representing t1 xor t2.

Definition at line 854 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
}
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 1597 of file Context.cs.

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

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

Definition at line 3332 of file Context.cs.

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

{
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
}
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 2986 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
}
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 3146 of file Context.cs.

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
}
Tactic ParOr ( params Tactic[]  t)
inline

Create a tactic that applies the given tactics in parallel.

Definition at line 3133 of file Context.cs.

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

{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
uint csn = Symbol.ArrayLength(sortNames);
uint cs = Sort.ArrayLength(sorts);
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
}
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 2821 of file Context.cs.

{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
uint csn = Symbol.ArrayLength(sortNames);
uint cs = Sort.ArrayLength(sorts);
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
}
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 2715 of file Context.cs.

{
uint csn = Symbol.ArrayLength(sortNames);
uint cs = Sort.ArrayLength(sorts);
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
Native.Z3_parse_smtlib_file(nCtx, fileName,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
}
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 2698 of file Context.cs.

{
uint csn = Symbol.ArrayLength(sortNames);
uint cs = Sort.ArrayLength(sorts);
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
Native.Z3_parse_smtlib_string(nCtx, str,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
}
string ProbeDescription ( string  name)
inline

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

Definition at line 3196 of file Context.cs.

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

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

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

Definition at line 3447 of file Context.cs.

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

Create a tactic that just returns the given goal.

Definition at line 3063 of file Context.cs.

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

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

Definition at line 2916 of file Context.cs.

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

{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
Contract.Ensures(Contract.Result<Tactic>() != null);
return AndThen(t1, t2, ts);
}
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 3467 of file Context.cs.

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

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

{
return a.NativeObject;
}
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 -ini? Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

See Also
GetParamValue

Definition at line 3500 of file Context.cs.

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

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

Definition at line 3106 of file Context.cs.

{
Contract.Requires(t != null);
Contract.Requires(p != null);
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(t);
CheckContextMatch(p);
return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
}
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 3019 of file Context.cs.

{
Contract.Requires(p != null);
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(t);
CheckContextMatch(p);
return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
}
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 3121 of file Context.cs.

{
Contract.Requires(t != null);
Contract.Requires(p != null);
Contract.Ensures(Contract.Result<Tactic>() != null);
return UsingParams(t, p);
}
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 3422 of file Context.cs.

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

Property Documentation

BoolSort BoolSort
get

Retrieves the Boolean sort of the context.

Definition at line 112 of file Context.cs.

IntSort IntSort
get

Retrieves the Integer sort of the context.

Definition at line 125 of file Context.cs.

uint NumProbes
get

The number of supported Probes.

Definition at line 3172 of file Context.cs.

uint NumSMTLIBAssumptions
get

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

Definition at line 2753 of file Context.cs.

uint NumSMTLIBDecls
get

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

Definition at line 2775 of file Context.cs.

uint NumSMTLIBFormulas
get

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

Definition at line 2731 of file Context.cs.

uint NumSMTLIBSorts
get

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

Definition at line 2797 of file Context.cs.

uint NumTactics
get

The number of supported tactics.

Definition at line 2892 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 2660 of file Context.cs.

string [] ProbeNames
get

The names of all supported Probes.

Definition at line 3180 of file Context.cs.

RealSort RealSort
get

Retrieves the Real sort of the context.

Definition at line 137 of file Context.cs.

ParamDescrs SimplifyParameterDescriptions
get

Retrieves parameter descriptions for simplifier.

Definition at line 3458 of file Context.cs.

BoolExpr [] SMTLIBAssumptions
get

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

Definition at line 2759 of file Context.cs.

FuncDecl [] SMTLIBDecls
get

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

Definition at line 2781 of file Context.cs.

BoolExpr [] SMTLIBFormulas
get

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

Definition at line 2737 of file Context.cs.

Sort [] SMTLIBSorts
get

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

Definition at line 2803 of file Context.cs.

string [] TacticNames
get

The names of all supported tactics.

Definition at line 2900 of file Context.cs.

Generated on Thu Nov 22 2012 18:37:21 for Z3 by   doxygen 1.8.2