Z3 Microsoft Research
Public Member Functions | Static Public Member Functions | Properties
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:
nameName of the benchmark. The argument is optional.
logicThe benchmark logic.
statusThe status string (sat, unsat, or unknown)
attributesOther attributes, such as source, difficulty or category.
assumptionsAuxiliary assumptions.
formulaFormula to be checked for consistency in conjunction with assumptions.
Returns:
A string representation of the benchmark.

Definition at line 2676 of file Context.cs.

        {
            Contract.Requires(assumptions != null);
            Contract.Requires(formula != null);
            Contract.Ensures(Contract.Result<string>() != null);

            return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
                                            (uint)assumptions.Length, AST.ArrayToNative(assumptions),
                                            formula.NativeObject);
        }
Tactic Cond ( Probe  p,
Tactic  t1,
Tactic  t2 
) [inline]

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

Definition at line 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:
indexThe de-Bruijn index of the variable
tyThe 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:
vA string representing the value in decimal notation.
sizethe size of the bit-vector

Definition at line 2453 of file Context.cs.

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

            return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
        }
BitVecNum MkBV ( int  v,
uint  size 
) [inline]

Create a bit-vector numeral.

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

Definition at line 2465 of file Context.cs.

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

            return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
        }
BitVecNum MkBV ( uint  v,
uint  size 
) [inline]

Create a bit-vector numeral.

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

Definition at line 2477 of file Context.cs.

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

            return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
        }
BitVecNum MkBV ( long  v,
uint  size 
) [inline]

Create a bit-vector numeral.

Parameters:
vvalue of the numeral.

/

Parameters:
sizethe size of the bit-vector

Definition at line 2489 of file Context.cs.

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

            return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
        }
BitVecNum MkBV ( ulong  v,
uint  size 
) [inline]

Create a bit-vector numeral.

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

Definition at line 2501 of file Context.cs.

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

            return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
        }
IntExpr MkBV2Int ( BitVecExpr  t,
bool  signed 
) [inline]

Create an integer from the bit-vector argument t .

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

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

The argument must be of bit-vector sort.

Definition at line 1794 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<IntExpr>() != null);

            CheckContextMatch(t);
            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
        }
BitVecExpr MkBVAdd ( BitVecExpr  t1,
BitVecExpr  t2 
) [inline]

Two's complement addition.

The arguments must have the same bit-vector sort.

Definition at line 1253 of file Context.cs.

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:
fA decl of a 0-arity function

Definition at line 624 of file Context.cs.

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

            return MkApp(f);
        }
ArrayExpr MkConstArray ( Sort  domain,
Expr  v 
) [inline]

Create a constant array.

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

See also:
MkArraySort, MkSelect

Definition at line 2027 of file Context.cs.

        {
            Contract.Requires(domain != null);
            Contract.Requires(v != null);
            Contract.Ensures(Contract.Result<ArrayExpr>() != null);

            CheckContextMatch(domain);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
        }
FuncDecl MkConstDecl ( Symbol  name,
Sort  range 
) [inline]

Creates a new constant function declaration.

Definition at line 508 of file Context.cs.

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

Definition at line 317 of file Context.cs.

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:
namesnames of datatype sorts
clist 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:
sortsthe sorts of the bound variables.
namesnames of the bound variables
bodythe body of the quantifier.
weightquantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patternsarray containing the patterns created using MkPattern.
noPatternsarray containing the anti-patterns created using MkPattern.
quantifierIDoptional symbol to track quantifier.
skolemIDoptional symbol to track skolem constants.

Definition at line 2531 of file Context.cs.

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:
modelsIndicates whether model generation should be enabled.
unsatCoresIndicates whether unsat core generation should be enabled.
proofsIndicates whether proof generation should be enabled.

Definition at line 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:
vA string representing the Term value in decimal notation.

Definition at line 2391 of file Context.cs.

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

            return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
        }
IntNum MkInt ( int  v) [inline]

Create an integer numeral.

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

Definition at line 2403 of file Context.cs.

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

            return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
        }
IntNum MkInt ( uint  v) [inline]

Create an integer numeral.

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

Definition at line 2415 of file Context.cs.

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

            return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
        }
IntNum MkInt ( long  v) [inline]

Create an integer numeral.

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

Definition at line 2427 of file Context.cs.

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

            return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
        }
IntNum MkInt ( ulong  v) [inline]

Create an integer numeral.

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

Definition at line 2439 of file Context.cs.

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

            return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
        }
BitVecExpr MkInt2BV ( uint  n,
IntExpr  t 
) [inline]

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

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

The argument must be of integer sort.

Definition at line 1770 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<BitVecExpr>() != null);

            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
        }
RealExpr MkInt2Real ( IntExpr  t) [inline]

Coerce an integer to a real.

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

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

Definition at line 1068 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<RealExpr>() != null);

            CheckContextMatch(t);
            return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
        }
IntExpr MkIntConst ( Symbol  name) [inline]

Creates an integer constant.

Definition at line 656 of file Context.cs.

        {
            Contract.Requires(name != null);
            Contract.Ensures(Contract.Result<IntExpr>() != null);

            return (IntExpr)MkConst(name, IntSort);
        }
IntExpr MkIntConst ( string  name) [inline]

Creates an integer constant.

Definition at line 667 of file Context.cs.

        {
            Contract.Requires(name != null);
            Contract.Ensures(Contract.Result<IntExpr>() != null);

            return (IntExpr)MkConst(name, IntSort);
        }
IntSort MkIntSort ( ) [inline]

Create a new integer sort.

Definition at line 173 of file Context.cs.

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:
t1An expression with Boolean sort
t2An expression
t3An 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:
vA string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*.
tyThe sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
Returns:
A Term with value v and sort ty

Definition at line 2232 of file Context.cs.

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:
vValue of the numeral
tySort of the numeral
Returns:
A Term with value v and type ty

Definition at line 2248 of file Context.cs.

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

            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
        }
Expr MkNumeral ( uint  v,
Sort  ty 
) [inline]

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

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

Definition at line 2264 of file Context.cs.

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

            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
        }
Expr MkNumeral ( long  v,
Sort  ty 
) [inline]

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

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

Definition at line 2280 of file Context.cs.

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

            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
        }
Expr MkNumeral ( ulong  v,
Sort  ty 
) [inline]

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

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

Definition at line 2296 of file Context.cs.

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

            CheckContextMatch(ty);
            return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
        }
BoolExpr MkOr ( params BoolExpr[]  t) [inline]

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

Definition at line 881 of file Context.cs.

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:
numnumerator of rational.
dendenominator of rational.
Returns:
A Term with value num /den and sort Real
See also:
MkNumeral(string, Sort)

Definition at line 2314 of file Context.cs.

        {
            if (den == 0)
                throw new Z3Exception("Denominator is zero");

            Contract.Ensures(Contract.Result<RatNum>() != null);
            Contract.EndContractBlock();

            return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
        }
RatNum MkReal ( string  v) [inline]

Create a real numeral.

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

Definition at line 2330 of file Context.cs.

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

            return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
        }
RatNum MkReal ( int  v) [inline]

Create a real numeral.

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

Definition at line 2342 of file Context.cs.

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

            return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
        }
RatNum MkReal ( uint  v) [inline]

Create a real numeral.

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

Definition at line 2354 of file Context.cs.

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

            return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
        }
RatNum MkReal ( long  v) [inline]

Create a real numeral.

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

Definition at line 2366 of file Context.cs.

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

            return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
        }
RatNum MkReal ( ulong  v) [inline]

Create a real numeral.

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

Definition at line 2378 of file Context.cs.

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

            return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
        }
IntExpr MkReal2Int ( RealExpr  t) [inline]

Coerce a real to an integer.

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

Definition at line 1084 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<IntExpr>() != null);

            CheckContextMatch(t);
            return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
        }
RealExpr MkRealConst ( Symbol  name) [inline]

Creates a real constant.

Definition at line 678 of file Context.cs.

        {
            Contract.Requires(name != null);
            Contract.Ensures(Contract.Result<RealExpr>() != null);

            return (RealExpr)MkConst(name, RealSort);
        }
RealExpr MkRealConst ( string  name) [inline]

Creates a real constant.

Definition at line 689 of file Context.cs.

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

            return (RealExpr)MkConst(name, RealSort);
        }
RealSort MkRealSort ( ) [inline]

Create a real sort.

Definition at line 183 of file Context.cs.

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

Create an expression representing t1 rem t2.

The arguments must have int type.

Definition at line 977 of file Context.cs.

        {
            Contract.Requires(t1 != null);
            Contract.Requires(t2 != null);
            Contract.Ensures(Contract.Result<IntExpr>() != null);

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
        }
BitVecExpr MkRepeat ( uint  i,
BitVecExpr  t 
) [inline]

Bit-vector repetition.

The argument t must have a bit-vector sort.

Definition at line 1612 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<BitVecExpr>() != null);

            CheckContextMatch(t);
            return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
        }
Expr MkSelect ( ArrayExpr  a,
Expr  i 
) [inline]

Array read.

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

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

See also:
MkArraySort, MkStore

Definition at line 1977 of file Context.cs.

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:
aThe 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:
nativeObjectThe 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

Retrieves the Boolean sort of the context.

Definition at line 112 of file Context.cs.

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.

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.

Last modified Fri Oct 5 2012 11:32:39