Context Class Reference

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

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.
Expr	ParseZ3String (string str)
	Parse the given string using the Z3 native parser.
Expr	ParseZ3File (string fileName)
	Parse the given file using the Z3 native 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 3326 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 2961 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:

name	Name of the benchmark. The argument is optional.
logic	The benchmark logic.
status	The status string (sat, unsat, or unknown)
attributes	Other attributes, such as source, difficulty or category.
assumptions	Auxiliary assumptions.
formula	Formula 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 3058 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 3240 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 3670 of file Context.cs.

Referenced by TestManaged.mk_context(), TestManaged.quantifier_example1(), TestManaged.quantifier_example1_abs(), and TestManaged.unsat_core_and_proof_example().

        {
            // 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 3311 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 3097 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 3107 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 3120 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 3296 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 3540 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 3266 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 3185 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 3281 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 3251 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.

Referenced by TestManaged.eval_example1(), TestManaged.find_model_example2(), TestManaged.prove_example2(), TestManaged.simplifier_example(), and Solver.ToZ3Term().

        {
            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.

Referenced by Solver.ToZ3Formula(), and TestManaged.unsat_core_and_proof_example().

        {
            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.

Referenced by TestManaged.enum_example(), TestManaged.eval_example2(), TestManaged.forest_example(), TestManaged.list_example(), and TestManaged.tree_example().

        {
            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.

Referenced by TestManaged.array_example1(), and TestManaged.array_example2().

        {
            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.

Referenced by TestManaged.bitvector_example1(), TestManaged.bitvector_example2(), and TestManaged.mk_bv_type().

        {
            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.

Referenced by TestManaged.array_example2(), and TestManaged.mk_bool_var().

        {
            Contract.Ensures(Contract.Result<BoolSort>() != null);
            return new BoolSort(this);
        }

Expr MkBound	(	uint	index,
		Sort	ty
	)		[inline]

Creates a new bound variable.

Parameters:

index	The de-Bruijn index of the variable
ty	The sort of the variable

Definition at line 552 of file Context.cs.

Referenced by TestManaged.assert_inj_axiom().

        {
            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:

v	A string representing the value in decimal notation.
size	the 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:

v	value of the numeral.
size	the 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:

v	value of the numeral.
size	the 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:

v	value of the numeral.

/

Parameters:

size	the 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:

v	value of the numeral.
size	the 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.

Referenced by TestManaged.find_small_model_example().

        {
            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.

Referenced by TestManaged.bitvector_example2().

        {
            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.

Referenced by TestManaged.bitvector_example1().

        {
            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.

Referenced by TestManaged.bitvector_example1(), and TestManaged.bitvector_example2().

        {
            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.

Referenced by TestManaged.check_small(), and TestManaged.find_small_model_example().

        {
            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.

Referenced by TestManaged.bitvector_example2().

        {
            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.

Referenced by TestManaged.array_example2(), TestManaged.assert_inj_axiom_abs(), TestManaged.enum_example(), TestManaged.eval_example2(), TestManaged.forest_example(), TestManaged.list_example(), TestManaged.mk_var(), TestManaged.prove_example1(), Solver.ToZ3Formula(), TestManaged.tree_example(), and TestManaged.tuple_example().

        {
            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:

f	A 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.

Referenced by TestManaged.parser_example2().

        {
            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:

name	constructor name
recognizer	name of recognizer function.
fieldNames	names of the constructor fields.
sorts	field sorts, 0 if the field sort refers to a recursive sort.
sortRefs	reference 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.

Referenced by TestManaged.forest_example(), and TestManaged.tree_example().

        {
            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.

Referenced by TestManaged.tree_example().

        {
            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:

names	names of datatype sorts
c	list of constructors, one list per sort.

Definition at line 376 of file Context.cs.

Referenced by TestManaged.forest_example().

        {
            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.

Referenced by TestManaged.array_example2().

        {
            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.

Referenced by TestManaged.enum_example().

        {
            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.

Referenced by TestManaged.array_example1(), TestManaged.assert_inj_axiom(), TestManaged.assert_inj_axiom_abs(), TestManaged.bitvector_example2(), TestManaged.enum_example(), TestManaged.eval_example2(), TestManaged.find_model_example2(), TestManaged.forest_example(), TestManaged.list_example(), TestManaged.prove_example1(), TestManaged.prove_example2(), TestManaged.quantifier_example1(), TestManaged.quantifier_example1_abs(), Solver.ToZ3Formula(), TestManaged.tree_example(), and TestManaged.tuple_example().

        {
            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.

Referenced by TestManaged.ite_example().

        {
            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 3426 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:

sorts	the sorts of the bound variables.
names	names of the bound variables
body	the body of the quantifier.
weight	quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patterns	array containing the patterns created using MkPattern.
noPatterns	array containing the anti-patterns created using MkPattern.
quantifierID	optional symbol to track quantifier.
skolemID	optional symbol to track skolem constants.

Definition at line 2531 of file Context.cs.

Referenced by TestManaged.assert_inj_axiom(), and TestManaged.assert_inj_axiom_abs().

        {
            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.

Referenced by TestManaged.assert_inj_axiom(), TestManaged.assert_inj_axiom_abs(), TestManaged.parser_example3(), TestManaged.prove_example1(), TestManaged.prove_example2(), TestManaged.quantifier_example1(), and TestManaged.quantifier_example1_abs().

        {
            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.

Referenced by TestManaged.push_pop_example1().

        {
            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:

models	Indicates whether model generation should be enabled.
unsatCores	Indicates whether unsat core generation should be enabled.
proofs	Indicates whether proof generation should be enabled.

Definition at line 2891 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.

Referenced by TestManaged.eval_example1(), TestManaged.find_model_example2(), and TestManaged.push_pop_example1().

        {
            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.

Referenced by TestManaged.bitvector_example1().

        {
            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.

Referenced by TestManaged.array_example1(), TestManaged.forest_example(), TestManaged.list_example(), TestManaged.prove_example1(), and TestManaged.tree_example().

        {
            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:

v	A 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:

v	value 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:

v	value 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:

v	value 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:

v	value 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.

Referenced by TestManaged.list_example(), TestManaged.mk_int_type(), TestManaged.parser_example2(), TestManaged.parser_example3(), and Solver.Solver().

        {
            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:

t1	An expression with Boolean sort
t2	An expression
t3	An expression with the same sort as t2

Definition at line 810 of file Context.cs.

Referenced by TestManaged.ite_example().

        {
            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.

Referenced by TestManaged.prove_example2(), TestManaged.push_pop_example1(), and Solver.ToZ3Formula().

        {
            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.

Referenced by TestManaged.list_example().

        {
            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.

Referenced by TestManaged.eval_example1(), TestManaged.find_model_example2(), and TestManaged.prove_example2().

        {
            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.

Referenced by Solver.ToZ3Formula().

        {
            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.

Referenced by Solver.ToZ3Term().

        {
            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.

Referenced by TestManaged.enum_example(), TestManaged.eval_example2(), TestManaged.find_model_example2(), TestManaged.forest_example(), TestManaged.list_example(), TestManaged.prove(), TestManaged.prove2(), TestManaged.prove_example1(), TestManaged.prove_example2(), Solver.ToZ3Formula(), TestManaged.tree_example(), and TestManaged.unsat_core_and_proof_example().

        {
            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:

v	A 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]*.
ty	The 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.

Referenced by TestManaged.bitvector_example1(), TestManaged.bitvector_example2(), TestManaged.push_pop_example1(), Solver.Solver(), Solver.ToZ3Formula(), and Solver.ToZ3Term().

        {
            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:

v	Value of the numeral
ty	Sort 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:

v	Value of the numeral
ty	Sort 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:

v	Value of the numeral
ty	Sort 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:

v	Value of the numeral
ty	Sort 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.

Referenced by TestManaged.array_example1(), TestManaged.enum_example(), TestManaged.forest_example(), TestManaged.list_example(), Solver.ToZ3Formula(), TestManaged.tree_example(), and TestManaged.unsat_core_and_proof_example().

        {
            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 2903 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.

Referenced by TestManaged.assert_inj_axiom(), and TestManaged.assert_inj_axiom_abs().

        {
            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 3230 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:

num	numerator of rational.
den	denominator 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:

v	A 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:

v	value 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:

v	value 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:

v	value 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:

v	value 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.

Referenced by TestManaged.array_example1().

        {
            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 3399 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 3375 of file Context.cs.

Referenced by TestManaged.mk_context(), TestManaged.quantifier_example1(), TestManaged.quantifier_example1_abs(), and TestManaged.unsat_core_and_proof_example().

        {
            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 3389 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 3413 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.

Referenced by TestManaged.array_example1().

        {
            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.

Referenced by TestManaged.prove_example2(), and TestManaged.simplifier_example().

        {
            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(), TestManaged.assert_inj_axiom(), TestManaged.enum_example(), TestManaged.eval_example2(), TestManaged.forest_example(), TestManaged.list_example(), TestManaged.parser_example2(), TestManaged.parser_example3(), TestManaged.prove_example1(), and TestManaged.tuple_example().

        {
            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 2950 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.

Referenced by TestManaged.eval_example2(), and TestManaged.tuple_example().

        {
            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.

Referenced by TestManaged.prove_example1().

        {
            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.

Referenced by TestManaged.find_model_example1().

        {
            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 3356 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 3341 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 3010 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 3170 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 3157 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.

Referenced by TestManaged.parser_example1(), TestManaged.parser_example2(), TestManaged.parser_example3(), TestManaged.parser_example4(), and TestManaged.parser_example5().

        {
            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));     
        }

Expr ParseZ3File

(

string

fileName

)

[inline]

Parse the given file using the Z3 native parser.

Returns:

A conjunction of asserts made in the file.

Definition at line 2872 of file Context.cs.

        {
            Contract.Ensures(Contract.Result<Expr>() != null);

            return Expr.Create(this, Native.Z3_parse_z3_file(nCtx, fileName));
        }

Expr ParseZ3String

(

string

str

)

[inline]

Parse the given string using the Z3 native parser.

Returns:

A conjunction of asserts made in str .

Definition at line 2861 of file Context.cs.

        {
            Contract.Ensures(Contract.Result<Expr>() != null);

            return Expr.Create(this, Native.Z3_parse_z3_string(nCtx, str));
        }

string ProbeDescription

(

string

name

)

[inline]

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

Definition at line 3220 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 3075 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 3471 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 3087 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 2940 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 2996 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

)

[inline, static]

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 3495 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 3027 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, WrapAST

).

Parameters:

a	The AST to unwrap.

Definition at line 3463 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 3528 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 3130 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 3043 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 3145 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, UnwrapAST

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

Parameters:

nativeObject

The native pointer to wrap.

Definition at line 3446 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 3196 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 2916 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 3204 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 3482 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.

Referenced by TestManaged.parser_example4().

FuncDecl [] SMTLIBDecls [get]

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

Definition at line 2781 of file Context.cs.

Referenced by TestManaged.parser_example4().

BoolExpr [] SMTLIBFormulas [get]

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

Definition at line 2737 of file Context.cs.

Referenced by TestManaged.parser_example1(), TestManaged.parser_example2(), TestManaged.parser_example3(), and TestManaged.parser_example4().

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