Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Static Public Member Functions | Properties
Context Class Reference

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

+ Inheritance diagram for Context:

Public Member Functions

 Context ()
 Constructor.
 Context (Dictionary< string, string > settings)
 Constructor.
IntSymbol MkSymbol (int i)
 Creates a new symbol using an integer.
StringSymbol MkSymbol (string name)
 Create a symbol using a string.
BoolSort MkBoolSort ()
 Create a new Boolean sort.
UninterpretedSort MkUninterpretedSort (Symbol s)
 Create a new uninterpreted sort.
UninterpretedSort MkUninterpretedSort (string str)
 Create a new uninterpreted sort.
IntSort MkIntSort ()
 Create a new integer sort.
RealSort MkRealSort ()
 Create a real sort.
BitVecSort MkBitVecSort (uint size)
 Create a new bit-vector sort.
ArraySort MkArraySort (Sort domain, Sort range)
 Create a new array sort.
TupleSort MkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
 Create a new tuple sort.
EnumSort MkEnumSort (Symbol name, params Symbol[] enumNames)
 Create a new enumeration sort.
EnumSort MkEnumSort (string name, params string[] enumNames)
 Create a new enumeration sort.
ListSort MkListSort (Symbol name, Sort elemSort)
 Create a new list sort.
ListSort MkListSort (string name, Sort elemSort)
 Create a new list sort.
FiniteDomainSort MkFiniteDomainSort (Symbol name, ulong size)
 Create a new finite domain sort.
FiniteDomainSort MkFiniteDomainSort (string name, ulong size)
 Create a new finite domain sort.
Constructor MkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
 Create a datatype constructor.
Constructor MkConstructor (string name, string recognizer, string[] fieldNames=null, Sort[] sorts=null, uint[] sortRefs=null)
 Create a datatype constructor.
DatatypeSort MkDatatypeSort (Symbol name, Constructor[] constructors)
 Create a new datatype sort.
DatatypeSort MkDatatypeSort (string name, Constructor[] constructors)
 Create a new datatype sort.
DatatypeSort[] MkDatatypeSorts (Symbol[] names, Constructor[][] c)
 Create mutually recursive datatypes.
DatatypeSort[] MkDatatypeSorts (string[] names, Constructor[][] c)
 Create mutually recursive data-types.
FuncDecl MkFuncDecl (Symbol name, Sort[] domain, Sort range)
 Creates a new function declaration.
FuncDecl MkFuncDecl (Symbol name, Sort domain, Sort range)
 Creates a new function declaration.
FuncDecl MkFuncDecl (string name, Sort[] domain, Sort range)
 Creates a new function declaration.
FuncDecl MkFuncDecl (string name, Sort domain, Sort range)
 Creates a new function declaration.
FuncDecl MkFreshFuncDecl (string prefix, Sort[] domain, Sort range)
 Creates a fresh function declaration with a name prefixed with prefix .
FuncDecl MkConstDecl (Symbol name, Sort range)
 Creates a new constant function declaration.
FuncDecl MkConstDecl (string name, Sort range)
 Creates a new constant function declaration.
FuncDecl MkFreshConstDecl (string prefix, Sort range)
 Creates a fresh constant function declaration with a name prefixed with prefix .
Expr MkBound (uint index, Sort ty)
 Creates a new bound variable.
Pattern MkPattern (params Expr[] terms)
 Create a quantifier pattern.
Expr MkConst (Symbol name, Sort range)
 Creates a new Constant of sort range and named name .
Expr MkConst (string name, Sort range)
 Creates a new Constant of sort range and named name .
Expr MkFreshConst (string prefix, Sort range)
 Creates a fresh Constant of sort range and a name prefixed with prefix .
Expr MkConst (FuncDecl f)
 Creates a fresh constant from the FuncDecl f .
BoolExpr MkBoolConst (Symbol name)
 Create a Boolean constant.
BoolExpr MkBoolConst (string name)
 Create a Boolean constant.
IntExpr MkIntConst (Symbol name)
 Creates an integer constant.
IntExpr MkIntConst (string name)
 Creates an integer constant.
RealExpr MkRealConst (Symbol name)
 Creates a real constant.
RealExpr MkRealConst (string name)
 Creates a real constant.
BitVecExpr MkBVConst (Symbol name, uint size)
 Creates a bit-vector constant.
BitVecExpr MkBVConst (string name, uint size)
 Creates a bit-vector constant.
Expr MkApp (FuncDecl f, params Expr[] args)
 Create a new function application.
BoolExpr MkTrue ()
 The true Term.
BoolExpr MkFalse ()
 The false Term.
BoolExpr MkBool (bool value)
 Creates a Boolean value.
BoolExpr MkEq (Expr x, Expr y)
 Creates the equality x = y .
BoolExpr MkDistinct (params Expr[] args)
 Creates a distinct term.
BoolExpr MkNot (BoolExpr a)
 Mk an expression representing not(a).
Expr MkITE (BoolExpr t1, Expr t2, Expr t3)
 Create an expression representing an if-then-else: ite(t1, t2, t3).
BoolExpr MkIff (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 iff t2.
BoolExpr MkImplies (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 -> t2.
BoolExpr MkXor (BoolExpr t1, BoolExpr t2)
 Create an expression representing t1 xor t2.
BoolExpr MkAnd (params BoolExpr[] t)
 Create an expression representing t[0] and t[1] and ....
BoolExpr MkOr (params BoolExpr[] t)
 Create an expression representing t[0] or t[1] or ....
ArithExpr MkAdd (params ArithExpr[] t)
 Create an expression representing t[0] + t[1] + ....
ArithExpr MkMul (params ArithExpr[] t)
 Create an expression representing t[0] * t[1] * ....
ArithExpr MkSub (params ArithExpr[] t)
 Create an expression representing t[0] - t[1] - ....
ArithExpr MkUnaryMinus (ArithExpr t)
 Create an expression representing -t.
ArithExpr MkDiv (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 / t2.
IntExpr MkMod (IntExpr t1, IntExpr t2)
 Create an expression representing t1 mod t2.
IntExpr MkRem (IntExpr t1, IntExpr t2)
 Create an expression representing t1 rem t2.
ArithExpr MkPower (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 ^ t2.
BoolExpr MkLt (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 < t2
BoolExpr MkLe (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 <= t2
BoolExpr MkGt (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 > t2
BoolExpr MkGe (ArithExpr t1, ArithExpr t2)
 Create an expression representing t1 >= t2
RealExpr MkInt2Real (IntExpr t)
 Coerce an integer to a real.
IntExpr MkReal2Int (RealExpr t)
 Coerce a real to an integer.
BoolExpr MkIsInteger (RealExpr t)
 Creates an expression that checks whether a real number is an integer.
BitVecExpr MkBVNot (BitVecExpr t)
 Bitwise negation.
BitVecExpr MkBVRedAND (BitVecExpr t)
 Take conjunction of bits in a vector, return vector of length 1.
BitVecExpr MkBVRedOR (BitVecExpr t)
 Take disjunction of bits in a vector, return vector of length 1.
BitVecExpr MkBVAND (BitVecExpr t1, BitVecExpr t2)
 Bitwise conjunction.
BitVecExpr MkBVOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise disjunction.
BitVecExpr MkBVXOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise XOR.
BitVecExpr MkBVNAND (BitVecExpr t1, BitVecExpr t2)
 Bitwise NAND.
BitVecExpr MkBVNOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise NOR.
BitVecExpr MkBVXNOR (BitVecExpr t1, BitVecExpr t2)
 Bitwise XNOR.
BitVecExpr MkBVNeg (BitVecExpr t)
 Standard two's complement unary minus.
BitVecExpr MkBVAdd (BitVecExpr t1, BitVecExpr t2)
 Two's complement addition.
BitVecExpr MkBVSub (BitVecExpr t1, BitVecExpr t2)
 Two's complement subtraction.
BitVecExpr MkBVMul (BitVecExpr t1, BitVecExpr t2)
 Two's complement multiplication.
BitVecExpr MkBVUDiv (BitVecExpr t1, BitVecExpr t2)
 Unsigned division.
BitVecExpr MkBVSDiv (BitVecExpr t1, BitVecExpr t2)
 Signed division.
BitVecExpr MkBVURem (BitVecExpr t1, BitVecExpr t2)
 Unsigned remainder.
BitVecExpr MkBVSRem (BitVecExpr t1, BitVecExpr t2)
 Signed remainder.
BitVecExpr MkBVSMod (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed remainder (sign follows divisor).
BoolExpr MkBVULT (BitVecExpr t1, BitVecExpr t2)
 Unsigned less-than.
BoolExpr MkBVSLT (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed less-than.
BoolExpr MkBVULE (BitVecExpr t1, BitVecExpr t2)
 Unsigned less-than or equal to.
BoolExpr MkBVSLE (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed less-than or equal to.
BoolExpr MkBVUGE (BitVecExpr t1, BitVecExpr t2)
 Unsigned greater than or equal to.
BoolExpr MkBVSGE (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed greater than or equal to.
BoolExpr MkBVUGT (BitVecExpr t1, BitVecExpr t2)
 Unsigned greater-than.
BoolExpr MkBVSGT (BitVecExpr t1, BitVecExpr t2)
 Two's complement signed greater-than.
BitVecExpr MkConcat (BitVecExpr t1, BitVecExpr t2)
 Bit-vector concatenation.
BitVecExpr MkExtract (uint high, uint low, BitVecExpr t)
 Bit-vector extraction.
BitVecExpr MkSignExt (uint i, BitVecExpr t)
 Bit-vector sign extension.
BitVecExpr MkZeroExt (uint i, BitVecExpr t)
 Bit-vector zero extension.
BitVecExpr MkRepeat (uint i, BitVecExpr t)
 Bit-vector repetition.
BitVecExpr MkBVSHL (BitVecExpr t1, BitVecExpr t2)
 Shift left.
BitVecExpr MkBVLSHR (BitVecExpr t1, BitVecExpr t2)
 Logical shift right.
BitVecExpr MkBVASHR (BitVecExpr t1, BitVecExpr t2)
 Arithmetic shift right.
BitVecExpr MkBVRotateLeft (uint i, BitVecExpr t)
 Rotate Left.
BitVecExpr MkBVRotateRight (uint i, BitVecExpr t)
 Rotate Right.
BitVecExpr MkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)
 Rotate Left.
BitVecExpr MkBVRotateRight (BitVecExpr t1, BitVecExpr t2)
 Rotate Right.
BitVecExpr MkInt2BV (uint n, IntExpr t)
 Create an n bit bit-vector from the integer argument t .
IntExpr MkBV2Int (BitVecExpr t, bool signed)
 Create an integer from the bit-vector argument t .
BoolExpr MkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
 Create a predicate that checks that the bit-wise addition does not overflow.
BoolExpr MkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise addition does not underflow.
BoolExpr MkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise subtraction does not overflow.
BoolExpr MkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
 Create a predicate that checks that the bit-wise subtraction does not underflow.
BoolExpr MkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise signed division does not overflow.
BoolExpr MkBVNegNoOverflow (BitVecExpr t)
 Create a predicate that checks that the bit-wise negation does not overflow.
BoolExpr MkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, bool isSigned)
 Create a predicate that checks that the bit-wise multiplication does not overflow.
BoolExpr MkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)
 Create a predicate that checks that the bit-wise multiplication does not underflow.
ArrayExpr MkArrayConst (Symbol name, Sort domain, Sort range)
 Create an array constant.
ArrayExpr MkArrayConst (string name, Sort domain, Sort range)
 Create an array constant.
Expr MkSelect (ArrayExpr a, Expr i)
 Array read.
ArrayExpr MkStore (ArrayExpr a, Expr i, Expr v)
 Array update.
ArrayExpr MkConstArray (Sort domain, Expr v)
 Create a constant array.
ArrayExpr MkMap (FuncDecl f, params ArrayExpr[] args)
 Maps f on the argument arrays.
Expr MkTermArray (ArrayExpr array)
 Access the array default value.
SetSort MkSetSort (Sort ty)
 Create a set type.
Expr MkEmptySet (Sort domain)
 Create an empty set.
Expr MkFullSet (Sort domain)
 Create the full set.
Expr MkSetAdd (Expr set, Expr element)
 Add an element to the set.
Expr MkSetDel (Expr set, Expr element)
 Remove an element from a set.
Expr MkSetUnion (params Expr[] args)
 Take the union of a list of sets.
Expr MkSetIntersection (params Expr[] args)
 Take the intersection of a list of sets.
Expr MkSetDifference (Expr arg1, Expr arg2)
 Take the difference between two sets.
Expr MkSetComplement (Expr arg)
 Take the complement of a set.
Expr MkSetMembership (Expr elem, Expr set)
 Check for set membership.
Expr MkSetSubset (Expr arg1, Expr arg2)
 Check for subsetness of sets.
Expr MkNumeral (string v, Sort ty)
 Create a Term of a given sort.
Expr MkNumeral (int v, Sort ty)
 Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Expr MkNumeral (uint v, Sort ty)
 Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Expr MkNumeral (long v, Sort ty)
 Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Expr MkNumeral (ulong v, Sort ty)
 Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
RatNum MkReal (int num, int den)
 Create a real from a fraction.
RatNum MkReal (string v)
 Create a real numeral.
RatNum MkReal (int v)
 Create a real numeral.
RatNum MkReal (uint v)
 Create a real numeral.
RatNum MkReal (long v)
 Create a real numeral.
RatNum MkReal (ulong v)
 Create a real numeral.
IntNum MkInt (string v)
 Create an integer numeral.
IntNum MkInt (int v)
 Create an integer numeral.
IntNum MkInt (uint v)
 Create an integer numeral.
IntNum MkInt (long v)
 Create an integer numeral.
IntNum MkInt (ulong v)
 Create an integer numeral.
BitVecNum MkBV (string v, uint size)
 Create a bit-vector numeral.
BitVecNum MkBV (int v, uint size)
 Create a bit-vector numeral.
BitVecNum MkBV (uint v, uint size)
 Create a bit-vector numeral.
BitVecNum MkBV (long v, uint size)
 Create a bit-vector numeral.
BitVecNum MkBV (ulong v, uint size)
 Create a bit-vector numeral.
Quantifier MkForall (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
 Create a universal Quantifier.
Quantifier MkForall (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
 Create a universal Quantifier.
Quantifier MkExists (Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
 Create an existential Quantifier.
Quantifier MkExists (Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
 Create an existential Quantifier.
Quantifier MkQuantifier (bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
 Create a Quantifier.
Quantifier MkQuantifier (bool universal, Expr[] boundConstants, Expr body, uint weight=1, Pattern[] patterns=null, Expr[] noPatterns=null, Symbol quantifierID=null, Symbol skolemID=null)
 Create a Quantifier.
string BenchmarkToSMTString (string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
 Convert a benchmark into an SMT-LIB formatted string.
void ParseSMTLIBString (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
 Parse the given string using the SMT-LIB parser.
void ParseSMTLIBFile (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
 Parse the given file using the SMT-LIB parser.
BoolExpr ParseSMTLIB2String (string str, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
 Parse the given string using the SMT-LIB2 parser.
BoolExpr ParseSMTLIB2File (string fileName, Symbol[] sortNames=null, Sort[] sorts=null, Symbol[] declNames=null, FuncDecl[] decls=null)
 Parse the given file using the SMT-LIB2 parser.
Goal MkGoal (bool models=true, bool unsatCores=false, bool proofs=false)
 Creates a new Goal.
Params MkParams ()
 Creates a new ParameterSet.
string TacticDescription (string name)
 Returns a string containing a description of the tactic with the given name.
Tactic MkTactic (string name)
 Creates a new Tactic.
Tactic AndThen (Tactic t1, Tactic t2, params Tactic[] ts)
 Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Tactic Then (Tactic t1, Tactic t2, params Tactic[] ts)
 Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Tactic OrElse (Tactic t1, Tactic t2)
 Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.
Tactic TryFor (Tactic t, uint ms)
 Create a tactic that applies t to a goal for ms milliseconds.
Tactic When (Probe p, Tactic t)
 Create a tactic that applies t to a given goal if the probe p evaluates to true.
Tactic Cond (Probe p, Tactic t1, Tactic t2)
 Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.
Tactic Repeat (Tactic t, uint max=uint.MaxValue)
 Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
Tactic Skip ()
 Create a tactic that just returns the given goal.
Tactic Fail ()
 Create a tactic always fails.
Tactic FailIf (Probe p)
 Create a tactic that fails if the probe p evaluates to false.
Tactic FailIfNotDecided ()
 Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').
Tactic UsingParams (Tactic t, Params p)
 Create a tactic that applies t using the given set of parameters p .
Tactic With (Tactic t, Params p)
 Create a tactic that applies t using the given set of parameters p .
Tactic ParOr (params Tactic[] t)
 Create a tactic that applies the given tactics in parallel.
Tactic ParAndThen (Tactic t1, Tactic t2)
 Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.
void Interrupt ()
 Interrupt the execution of a Z3 procedure.
string ProbeDescription (string name)
 Returns a string containing a description of the probe with the given name.
Probe MkProbe (string name)
 Creates a new Probe.
Probe ConstProbe (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.
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.

The following parameters can be set:

  • proof (Boolean) Enable proof generation
  • debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
  • trace (Boolean) Tracing support for VCC
  • trace_file_name (String) Trace out file for VCC traces
  • timeout (unsigned) default timeout (in milliseconds) used for solvers
  • well_sorted_check type checker
  • auto_config use heuristics to automatically select solver and configure it
  • model model generation for solvers, this parameter can be overwritten when creating a solver
  • model_validate validate models produced by solvers
  • unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver Note that in previous versions of Z3, this constructor was also used to set global and module parameters. For this purpose we should now use Global.SetParameter

Definition at line 62 of file Context.cs.

            : 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 3333 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 2968 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 2707 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 3065 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 ConstProbe ( double  val) [inline]

Create a probe that always evaluates to val .

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

        {
            // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
            AST_DRQ.Clear(this);
            ASTMap_DRQ.Clear(this);
            ASTVector_DRQ.Clear(this);
            ApplyResult_DRQ.Clear(this);
            FuncEntry_DRQ.Clear(this);
            FuncInterp_DRQ.Clear(this);
            Goal_DRQ.Clear(this);
            Model_DRQ.Clear(this);
            Params_DRQ.Clear(this);
            ParamDescrs_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 3318 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 3104 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 3114 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 3127 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 3303 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));
        }
Probe Gt ( Probe  p1,
Probe  p2 
) [inline]

Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2

Definition at line 3273 of file Context.cs.

        {
            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 3192 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 3288 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 3258 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 927 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Requires(Contract.ForAll(t, a => a != null));
            Contract.Ensures(Contract.Result<ArithExpr>() != null);

            CheckContextMatch(t);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
BoolExpr MkAnd ( params BoolExpr[]  t) [inline]

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

Definition at line 897 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Requires(Contract.ForAll(t, a => a != null));
            Contract.Ensures(Contract.Result<BoolExpr>() != null);

            CheckContextMatch(t);
            return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
Expr MkApp ( FuncDecl  f,
params Expr[]  args 
) [inline]

Create a new function application.

Definition at line 751 of file Context.cs.

        {
            Contract.Requires(f != null);
            Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
            Contract.Ensures(Contract.Result<Expr>() != null);

            CheckContextMatch(f);
            CheckContextMatch(args);
            return Expr.Create(this, f, args);
        }
ArrayExpr MkArrayConst ( Symbol  name,
Sort  domain,
Sort  range 
) [inline]

Create an array constant.

Definition at line 1973 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 1986 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 223 of file Context.cs.

        {
            Contract.Requires(domain != null);
            Contract.Requires(range != null);
            Contract.Ensures(Contract.Result<ArraySort>() != null);

            CheckContextMatch(domain);
            CheckContextMatch(range);
            return new ArraySort(this, domain, range);
        }
BitVecSort MkBitVecSort ( uint  size) [inline]

Create a new bit-vector sort.

Definition at line 213 of file Context.cs.

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

            return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
        }
BoolExpr MkBool ( bool  value) [inline]

Creates a Boolean value.

Definition at line 786 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 664 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 675 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 163 of file Context.cs.

        {
            Contract.Ensures(Contract.Result<BoolSort>() != null);
            return new BoolSort(this);
        }
Expr MkBound ( uint  index,
Sort  ty 
) [inline]

Creates a new bound variable.

Parameters:
indexThe de-Bruijn index of the variable
tyThe sort of the variable

Definition at line 581 of file Context.cs.

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

            return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
        }
BitVecNum MkBV ( string  v,
uint  size 
) [inline]

Create a bit-vector numeral.

Parameters:
vA string representing the value in decimal notation.
sizethe size of the bit-vector

Definition at line 2484 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 2496 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 2508 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 2520 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 2532 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 1825 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 1284 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkBVAddNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
bool  isSigned 
) [inline]

Create a predicate that checks that the bit-wise addition does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1840 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 1857 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 1181 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 1712 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 728 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 739 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 1687 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 1314 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkBVMulNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2,
bool  isSigned 
) [inline]

Create a predicate that checks that the bit-wise multiplication does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1940 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 1957 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 1226 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 1271 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 1925 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 1241 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 1142 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 1196 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 1155 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 1168 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 1730 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 1762 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 1746 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 1780 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 1358 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 1908 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 1518 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 1552 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 1664 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 1484 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkBVSLT ( BitVecExpr  t1,
BitVecExpr  t2 
) [inline]

Two's complement signed less-than.

The arguments must have the same bit-vector sort.

Definition at line 1450 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 1416 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 1398 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 1299 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkBVSubNoOverflow ( BitVecExpr  t1,
BitVecExpr  t2 
) [inline]

Create a predicate that checks that the bit-wise subtraction does not overflow.

The arguments must be of bit-vector sort.

Definition at line 1874 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 1891 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 1334 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 1501 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 1535 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 1467 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkBVULT ( BitVecExpr  t1,
BitVecExpr  t2 
) [inline]

Unsigned less-than.

The arguments must have the same bit-vector sort.

Definition at line 1433 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 1377 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 1256 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 1211 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
        }
BitVecExpr MkConcat ( BitVecExpr  t1,
BitVecExpr  t2 
) [inline]

Bit-vector concatenation.

The arguments must have a bit-vector sort.

Returns:
The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

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

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

            CheckContextMatch(name);
            CheckContextMatch(range);

            return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
        }
Expr MkConst ( string  name,
Sort  range 
) [inline]

Creates a new Constant of sort range and named name .

Definition at line 628 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 653 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 2058 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 537 of file Context.cs.

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

            CheckContextMatch(name);
            CheckContextMatch(range);
            return new FuncDecl(this, name, null, range);
        }
FuncDecl MkConstDecl ( string  name,
Sort  range 
) [inline]

Creates a new constant function declaration.

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

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

            return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
        }
Constructor MkConstructor ( string  name,
string  recognizer,
string[]  fieldNames = null,
Sort[]  sorts = null,
uint[]  sortRefs = null 
) [inline]

Create a datatype constructor.

Parameters:
name
recognizer
fieldNames
sorts
sortRefs
Returns:

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

        {
            Contract.Requires(name != null);
            Contract.Requires(constructors != null);
            Contract.Requires(Contract.ForAll(constructors, c => c != null));

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

            CheckContextMatch(name);
            CheckContextMatch(constructors);
            return new DatatypeSort(this, name, constructors);
        }
DatatypeSort MkDatatypeSort ( string  name,
Constructor[]  constructors 
) [inline]

Create a new datatype sort.

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

        {
            Contract.Requires(names != null);
            Contract.Requires(c != null);
            Contract.Requires(names.Length == c.Length);
            Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
            Contract.Requires(Contract.ForAll(names, name => name != null));
            Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);

            CheckContextMatch(names);
            uint n = (uint)names.Length;
            ConstructorList[] cla = new ConstructorList[n];
            IntPtr[] n_constr = new IntPtr[n];
            for (uint i = 0; i < n; i++)
            {
                Constructor[] 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 440 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 810 of file Context.cs.

        {
            Contract.Requires(args != null);
            Contract.Requires(Contract.ForAll(args, a => a != null));

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

            CheckContextMatch(args);
            return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
        }
ArithExpr MkDiv ( ArithExpr  t1,
ArithExpr  t2 
) [inline]

Create an expression representing t1 / t2.

Definition at line 978 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 2124 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,
params Symbol[]  enumNames 
) [inline]

Create a new enumeration sort.

Definition at line 254 of file Context.cs.

        {
            Contract.Requires(name != null);
            Contract.Requires(enumNames != null);
            Contract.Requires(Contract.ForAll(enumNames, f => f != null));

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

            CheckContextMatch(name);
            CheckContextMatch(enumNames);
            return new EnumSort(this, name, enumNames);
        }
EnumSort MkEnumSort ( string  name,
params string[]  enumNames 
) [inline]

Create a new enumeration sort.

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

        {
            Contract.Requires(x != null);
            Contract.Requires(y != null);
            Contract.Ensures(Contract.Result<BoolExpr>() != null);

            CheckContextMatch(x);
            CheckContextMatch(y);
            return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
        }
Quantifier MkExists ( Sort[]  sorts,
Symbol[]  names,
Expr  body,
uint  weight = 1,
Pattern[]  patterns = null,
Expr[]  noPatterns = null,
Symbol  quantifierID = null,
Symbol  skolemID = null 
) [inline]

Create an existential Quantifier.

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

Definition at line 2598 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 2616 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 1593 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 776 of file Context.cs.

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

            return new BoolExpr(this, Native.Z3_mk_false(nCtx));
        }
FiniteDomainSort MkFiniteDomainSort ( Symbol  name,
ulong  size 
) [inline]

Create a new finite domain sort.

Returns:
The result is a sort
Parameters:
nameThe name used to identify the sort
sizeThe size of the sort

Definition at line 310 of file Context.cs.

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

Returns:
The result is a sort

Elements of the sort are created using

See also:
MkNumeral(ulong, Sort)

, and the elements range from 0 to size-1.

Parameters:
nameThe name used to identify the sort
sizeThe size of the sort

Definition at line 327 of file Context.cs.

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

            return new FiniteDomainSort(this, MkSymbol(name), size);
        }
Fixedpoint MkFixedpoint ( ) [inline]

Create a Fixedpoint context.

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

        {
            Contract.Requires(sorts != null);
            Contract.Requires(names != null);
            Contract.Requires(body != null);
            Contract.Requires(sorts.Length == names.Length);
            Contract.Requires(Contract.ForAll(sorts, s => s != null));
            Contract.Requires(Contract.ForAll(names, n => n != null));
            Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
            Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));

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

            return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
        }
Quantifier MkForall ( Expr[]  boundConstants,
Expr  body,
uint  weight = 1,
Pattern[]  patterns = null,
Expr[]  noPatterns = null,
Symbol  quantifierID = null,
Symbol  skolemID = null 
) [inline]

Create a universal Quantifier.

Definition at line 2582 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 640 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 565 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 523 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 2136 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 459 of file Context.cs.

        {
            Contract.Requires(name != null);
            Contract.Requires(range != null);
            Contract.Requires(Contract.ForAll(domain, d => d != null));
            Contract.Ensures(Contract.Result<FuncDecl>() != null);

            CheckContextMatch(name);
            CheckContextMatch(domain);
            CheckContextMatch(range);
            return new FuncDecl(this, name, domain, range);
        }
FuncDecl MkFuncDecl ( Symbol  name,
Sort  domain,
Sort  range 
) [inline]

Creates a new function declaration.

Definition at line 475 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 492 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 506 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 1078 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
        }
Goal MkGoal ( bool  models = true,
bool  unsatCores = false,
bool  proofs = false 
) [inline]

Creates a new Goal.

Note that the Context must have been created with proof generation support if proofs is set to true here.

Parameters:
modelsIndicates whether model generation should be enabled.
unsatCoresIndicates whether unsat core generation should be enabled.
proofsIndicates whether proof generation should be enabled.

Definition at line 2898 of file Context.cs.

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

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkIff ( BoolExpr  t1,
BoolExpr  t2 
) [inline]

Create an expression representing t1 iff t2.

Definition at line 855 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
        }
BoolExpr MkImplies ( BoolExpr  t1,
BoolExpr  t2 
) [inline]

Create an expression representing t1 -> t2.

Definition at line 869 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
        }
IntNum MkInt ( string  v) [inline]

Create an integer numeral.

Parameters:
vA string representing the Term value in decimal notation.

Definition at line 2422 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 2434 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 2446 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 2458 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 2470 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 1801 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 1099 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 685 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 696 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 194 of file Context.cs.

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

            return new IntSort(this);
        }
BoolExpr MkIsInteger ( RealExpr  t) [inline]

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

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

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            CheckContextMatch(t3);
            return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
        }
BoolExpr MkLe ( ArithExpr  t1,
ArithExpr  t2 
) [inline]

Create an expression representing t1 <= t2

Definition at line 1050 of file Context.cs.

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
        }
ListSort MkListSort ( Symbol  name,
Sort  elemSort 
) [inline]

Create a new list sort.

Definition at line 281 of file Context.cs.

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

            CheckContextMatch(name);
            CheckContextMatch(elemSort);
            return new ListSort(this, name, elemSort);
        }
ListSort MkListSort ( string  name,
Sort  elemSort 
) [inline]

Create a new list sort.

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

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
        }
ArrayExpr MkMap ( FuncDecl  f,
params ArrayExpr[]  args 
) [inline]

Maps f on the argument arrays.

Eeach element of args must be of an array sort [domain_i -> range_i]. The function declaration f must have type range_1 .. range_n -> range. v must have sort range. The sort of the result is [domain_i -> range].

See also:
MkArraySort, MkSelect, MkStore

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

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
        }
ArithExpr MkMul ( params ArithExpr[]  t) [inline]

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

Definition at line 940 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Requires(Contract.ForAll(t, a => a != null));
            Contract.Ensures(Contract.Result<ArithExpr>() != null);

            CheckContextMatch(t);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
BoolExpr MkNot ( BoolExpr  a) [inline]

Mk an expression representing not(a).

Definition at line 824 of file Context.cs.

        {
            Contract.Requires(a != null);
            Contract.Ensures(Contract.Result<BoolExpr>() != null);

            CheckContextMatch(a);
            return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
        }
Expr MkNumeral ( string  v,
Sort  ty 
) [inline]

Create a Term of a given sort.

Parameters:
vA string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*.
tyThe sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
Returns:
A Term with value v and sort ty

Definition at line 2263 of file Context.cs.

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

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

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

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

Definition at line 2279 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 2295 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 2311 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 2327 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 910 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Requires(Contract.ForAll(t, a => a != null));
            Contract.Ensures(Contract.Result<BoolExpr>() != null);

            CheckContextMatch(t);
            return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
Params MkParams ( ) [inline]

Creates a new ParameterSet.

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

        {
            Contract.Requires(terms != null);
            if (terms.Length == 0)
                throw new Z3Exception("Cannot create a pattern from zero terms");

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

            Contract.EndContractBlock();

            IntPtr[] termsNative = AST.ArrayToNative(terms);
            return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
        }
ArithExpr MkPower ( ArithExpr  t1,
ArithExpr  t2 
) [inline]

Create an expression representing t1 ^ t2.

Definition at line 1022 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 3237 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 2631 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 2654 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 2345 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 2361 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 2373 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 2385 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 2397 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 2409 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 1115 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 707 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 718 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 204 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 1008 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 1643 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 2008 of file Context.cs.

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

            CheckContextMatch(a);
            CheckContextMatch(i);
            return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
        }
Expr MkSetAdd ( Expr  set,
Expr  element 
) [inline]

Add an element to the set.

Definition at line 2148 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 2216 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 2163 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 2202 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 2189 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 2228 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 2112 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 2242 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 2177 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 1610 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 3406 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 3382 of file Context.cs.

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

            if (logic == null)
                return new Solver(this, Native.Z3_mk_solver(nCtx));
            else
                return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
        }
Solver MkSolver ( string  logic) [inline]

Creates a new (incremental) solver.

See also:
MkSolver(Symbol)

Definition at line 3396 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 3420 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 2036 of file Context.cs.

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

            CheckContextMatch(a);
            CheckContextMatch(i);
            CheckContextMatch(v);
            return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
        }
ArithExpr MkSub ( params ArithExpr[]  t) [inline]

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

Definition at line 953 of file Context.cs.

        {
            Contract.Requires(t != null);
            Contract.Requires(Contract.ForAll(t, a => a != null));
            Contract.Ensures(Contract.Result<ArithExpr>() != null);

            CheckContextMatch(t);
            return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
        }
IntSymbol MkSymbol ( int  i) [inline]

Creates a new symbol using an integer.

Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

Definition at line 84 of file Context.cs.

Referenced by Params.Add().

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

            return new IntSymbol(this, i);
        }
StringSymbol MkSymbol ( string  name) [inline]

Create a symbol using a string.

Definition at line 94 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 2957 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 2098 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 766 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 237 of file Context.cs.

        {
            Contract.Requires(name != null);
            Contract.Requires(fieldNames != null);
            Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
            Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
            Contract.Ensures(Contract.Result<TupleSort>() != null);

            CheckContextMatch(name);
            CheckContextMatch(fieldNames);
            CheckContextMatch(fieldSorts);
            return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
        }
ArithExpr MkUnaryMinus ( ArithExpr  t) [inline]

Create an expression representing -t.

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

        {
            Contract.Requires(s != null);
            Contract.Ensures(Contract.Result<UninterpretedSort>() != null);

            CheckContextMatch(s);
            return new UninterpretedSort(this, s);
        }
UninterpretedSort MkUninterpretedSort ( string  str) [inline]

Create a new uninterpreted sort.

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

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

            CheckContextMatch(t1);
            CheckContextMatch(t2);
            return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
        }
BitVecExpr MkZeroExt ( uint  i,
BitVecExpr  t 
) [inline]

Bit-vector zero extension.

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. The argument t must have a bit-vector sort.

Definition at line 1628 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 3363 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 3348 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 3017 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 3177 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 3164 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 2871 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 2852 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 2746 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 2729 of file Context.cs.

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

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

Definition at line 3227 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 3082 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 3478 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 3094 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 2947 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 3003 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 3498 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 3034 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 3470 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 -p Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

Definition at line 3530 of file Context.cs.

        {
            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 3137 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 3050 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 3152 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 3453 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 127 of file Context.cs.

Retrieves the Integer sort of the context.

Definition at line 139 of file Context.cs.

uint NumProbes [get]

The number of supported Probes.

Definition at line 3203 of file Context.cs.

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

Definition at line 2784 of file Context.cs.

uint NumSMTLIBDecls [get]

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

Definition at line 2806 of file Context.cs.

uint NumSMTLIBFormulas [get]

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

Definition at line 2762 of file Context.cs.

uint NumSMTLIBSorts [get]

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

Definition at line 2828 of file Context.cs.

uint NumTactics [get]

The number of supported tactics.

Definition at line 2923 of file Context.cs.

Selects the format used for pretty-printing expressions.

The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.

See also:
AST.ToString(), Pattern.ToString(), FuncDecl.ToString(), Sort.ToString()

Definition at line 2691 of file Context.cs.

string [] ProbeNames [get]

The names of all supported Probes.

Definition at line 3211 of file Context.cs.

Retrieves the Real sort of the context.

Definition at line 152 of file Context.cs.

ParamDescrs SimplifyParameterDescriptions [get]

Retrieves parameter descriptions for simplifier.

Definition at line 3489 of file Context.cs.

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

Definition at line 2790 of file Context.cs.

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

Definition at line 2812 of file Context.cs.

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

Definition at line 2768 of file Context.cs.

Sort [] SMTLIBSorts [get]

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

Definition at line 2834 of file Context.cs.

string [] TacticNames [get]

The names of all supported tactics.

Definition at line 2931 of file Context.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines