Home • Docs • Download • Mail • FAQ • Awards • Status • MSR

Z3 An Efficient SMT Solver

Microsoft::Z3::RawContext

RawContext Class Reference
[Managed (.NET) API]

Z3 API object. More...


Public Member Functions

 RawContext (Config^config)
 Create a logical context using the given configuration.
Tracing and logging
bool TraceToFile (String^trace_file)
 Enable trace messages to a file.
void TraceToStdErr ()
 Enable trace messages to a standard error.
void TraceToStdOut ()
 Enable trace messages to a standard output.
void TraceOff ()
 Disable trace messages.
void EnableDebugTrace (String^tag)
 Enable debug tracing of tagged log.
bool OpenLog (String^filename)
 Log assertions to a file.
void AppendLog (String^string)
 Append instruction or comment to log with assertion.
void CloseLog ()
 Close file with logged assertions.
void ToggleWarningMessages (bool enabled)
 Enable or disable warning messages sent to the console out/error.
Symbols
Symbol MkSymbol (int i)
 Create a Z3 symbol using an intege or a string.
Symbol MkSymbol (String^s)
Types
SortPtr MkSort (Symbol^s)
 Create a free (uninterpreted) type using the given name (symbol).
SortPtr MkSort (String^s)
SortPtr MkSort (int i)
SortPtr MkBoolSort ()
 Create the boolean type.
SortPtr MkIntSort ()
 Create an integer type.
SortPtr MkRealSort ()
 Create a real type.
SortPtr MkBvSort (unsigned sz)
 Create a bit-vector type of the given size.
SortPtr MkArraySort (SortPtr domain, SortPtr range)
 Create an array type.
SortPtr MkTupleSort (Symbol^mk_tuple_name, array< Symbol^>^field_names, array< SortPtr >^field_types,[Runtime::InteropServices::Out] FuncDeclPtr%mk_tuple_decl,[Runtime::InteropServices::In][Runtime::InteropServices::Out] array< FuncDeclPtr >^proj_decl)
 Create a tuple type.
SortPtr MkTupleSort (String^mk_tuple_name, array< String^>^field_names, array< SortPtr >^field_types,[Runtime::InteropServices::Out] FuncDeclPtr%mk_tuple_decl,[Runtime::InteropServices::In][Runtime::InteropServices::Out] array< FuncDeclPtr >^proj_decl)
SortPtr MkEnumerationSort (String^name, array< String^>^enum_names, array< FuncDeclPtr >^enum_consts, array< FuncDeclPtr >^enum_testers)
 create an enumeration type.
SortPtr MkListSort (String^name, SortPtr elem_sort,[Runtime::InteropServices::Out] FuncDeclPtr%nil_decl,[Runtime::InteropServices::Out] FuncDeclPtr%is_nil_decl,[Runtime::InteropServices::Out] FuncDeclPtr%cons_decl,[Runtime::InteropServices::Out] FuncDeclPtr%is_cons_decl,[Runtime::InteropServices::Out] FuncDeclPtr%head_decl,[Runtime::InteropServices::Out] FuncDeclPtr%tail_decl)
 create list sort.
Constructor MkConstructor (String^name, String^tester, array< String^>^field_names, array< SortPtr >^field_sorts, array< unsigned >^field_refs)
 create constructor object for datatype declarations. The object must be disposed with manually.
FuncDeclPtr GetConstructor (Constructor^c)
 retrieve constructor function declaration.
FuncDeclPtr GetTester (Constructor^c)
 retrieve test function for constructor.
array< FuncDeclPtr > GetAccessors (Constructor^c)
 retrieve accessors for datatype.
SortPtr MkDataType (String^name, array< Constructor^>^constructors)
 create datatype sort.
array< SortPtr > MkDataTypes (array< String^>^names, array< array< Constructor^>^>^constructors)
 create datatype sorts.
Constants and Applications
FuncDeclPtr MkFuncDecl (Symbol^s, array< SortPtr >^domain, SortPtr range)
 Declare a constant or function.
FuncDeclPtr MkFuncDecl (String^s, array< SortPtr >^domain, SortPtr range)
FuncDeclPtr MkConstDecl (Symbol^s, SortPtr ty)
FuncDeclPtr MkFuncDecl (Symbol^s, SortPtr domain, SortPtr range)
FuncDeclPtr MkFuncDecl (Symbol^s, SortPtr d1, SortPtr d2, SortPtr range)
FuncDeclPtr MkConstDecl (String^s, SortPtr ty)
FuncDeclPtr MkFuncDecl (String^s, SortPtr domain, SortPtr range)
FuncDeclPtr MkFuncDecl (String^s, SortPtr d1, SortPtr d2, SortPtr range)
AppPtr MkApp (FuncDeclPtr d, array< TermPtr >^args)
 Create a constant or function application.
AppPtr MkApp (FuncDeclPtr d, TermPtr arg)
AppPtr MkApp (FuncDeclPtr d, TermPtr arg1, TermPtr arg2)
AppPtr MkApp (FuncDeclPtr d, TermPtr arg1, TermPtr arg2, TermPtr arg3)
AppPtr MkConst (FuncDeclPtr d)
 Declare and create a constant.
AppPtr MkConst (String^s, SortPtr ty)
AppPtr MkConst (Symbol^s, SortPtr ty)
FuncDeclPtr MkFreshFuncDecl (String^prefix, array< SortPtr >^domain, SortPtr range)
 Declare a fresh constant or function.
TermPtr MkFreshConst (String^prefix, SortPtr ty)
 Declare and create a fresh constant.
TermPtr MkLabel (Symbol^name, bool pos, TermPtr fml)
 Create labeled formula.
TermPtr MkTrue ()
 Create an AST node representing true.
TermPtr MkFalse ()
 Create an AST node representing false.
TermPtr MkEq (TermPtr l, TermPtr r)
 Create an AST node representing l = r.
TermPtr MkDistinct (array< TermPtr >^args)
 Create an AST node representing distinct(args[0], ..., args[args.Length-1]).
virtual TermPtr MkNot (TermPtr arg)
 Create an AST node representing not(a).
TermPtr MkIte (TermPtr t1, TermPtr t2, TermPtr t3)
 Create an AST node representing an if-then-else: ite(t1, t2, t3).
TermPtr MkIff (TermPtr t1, TermPtr t2)
 Create an AST node representing t1 iff t2.
TermPtr MkImplies (TermPtr t1, TermPtr t2)
 Create an AST node representing t1 implies t2.
TermPtr MkXor (TermPtr t1, TermPtr t2)
 Create an AST node representing t1 xor t2.
TermPtr MkAnd (array< TermPtr >^args)
 Create an AST node representing args[0] and ... and args[args.Length-1].
TermPtr MkAnd (TermPtr arg1, TermPtr arg2)
TermPtr MkOr (array< TermPtr >^args)
 Create an AST node representing args[0] or ... or args[args.Length-1].
TermPtr MkOr (TermPtr arg1, TermPtr arg2)
TermPtr MkAdd (array< TermPtr >^args)
 Create an AST node representing args[0] + ... + args[args.Length-1].
TermPtr MkAdd (TermPtr arg1, TermPtr arg2)
TermPtr MkMul (array< TermPtr >^args)
 Create an AST node representing args[0] * ... * args[args.Length-1].
TermPtr MkMul (TermPtr arg1, TermPtr arg2)
TermPtr MkSub (array< TermPtr >^args)
 Create an AST node representing args[0] - ... - args[args.Length - 1].
TermPtr MkSub (TermPtr arg1, TermPtr arg2)
TermPtr MkUnaryMinus (TermPtr arg)
 Create an AST node representing - arg.
TermPtr MkDiv (TermPtr arg1, TermPtr arg2)
 Create integer or real division.
TermPtr MkMod (TermPtr arg1, TermPtr arg2)
 Create integer modulus.
TermPtr MkRem (TermPtr arg1, TermPtr arg2)
 Create integer remainder.
TermPtr MkLt (TermPtr arg1, TermPtr arg2)
 Create less than.
TermPtr MkLe (TermPtr arg1, TermPtr arg2)
 Create less than or equal to.
TermPtr MkGt (TermPtr arg1, TermPtr arg2)
 Create greater than.
TermPtr MkGe (TermPtr arg1, TermPtr arg2)
 Create greater than or equal to.
TermPtr MkInt2Real (TermPtr arg)
 Coerce integer term to real type.
TermPtr MkBvNot (TermPtr t1)
 Bitwise negation.
TermPtr MkBvAnd (TermPtr t1, TermPtr t2)
 Bitwise and.
TermPtr MkBvOr (TermPtr t1, TermPtr t2)
 Bitwise or.
TermPtr MkBvXor (TermPtr t1, TermPtr t2)
 Bitwise exclusive-or.
TermPtr MkBvNand (TermPtr t1, TermPtr t2)
 Bitwise nand.
TermPtr MkBvNor (TermPtr t1, TermPtr t2)
 Bitwise nor.
TermPtr MkBvXnor (TermPtr t1, TermPtr t2)
 Bitwise xnor.
TermPtr MkBvNeg (TermPtr t1)
 Standard two's complement unary minus.
TermPtr MkBvAdd (TermPtr t1, TermPtr t2)
 Standard two's complement addition.
TermPtr MkBvSub (TermPtr t1, TermPtr t2)
 Standard two's complement subtraction.
TermPtr MkBvMul (TermPtr t1, TermPtr t2)
 Standard two's complement multiplication.
TermPtr MkBvUdiv (TermPtr t1, TermPtr t2)
 Unsigned division.
TermPtr MkBvSdiv (TermPtr t1, TermPtr t2)
 Two's complement signed division.
TermPtr MkBvUrem (TermPtr t1, TermPtr t2)
 Unsigned remainder.
TermPtr MkBvSrem (TermPtr t1, TermPtr t2)
 Two's complement signed remainder (sign follows dividend).
TermPtr MkBvSmod (TermPtr t1, TermPtr t2)
 Two's complement signed remainder (sign follows divisor).
TermPtr MkBvUlt (TermPtr t1, TermPtr t2)
 Unsigned less than.
TermPtr MkBvSlt (TermPtr t1, TermPtr t2)
 Two's complement signed less than.
TermPtr MkBvUle (TermPtr t1, TermPtr t2)
 Unsigned less than or equal to.
TermPtr MkBvSle (TermPtr t1, TermPtr t2)
 Two's complement signed less than or equal to.
TermPtr MkBvUge (TermPtr t1, TermPtr t2)
 Unsigned greater than or equal to.
TermPtr MkBvSge (TermPtr t1, TermPtr t2)
 Two's complement signed greater than or equal to.
TermPtr MkBvUgt (TermPtr t1, TermPtr t2)
 Unsigned greater than.
TermPtr MkBvSgt (TermPtr t1, TermPtr t2)
 Two's complement signed greater than.
TermPtr MkBvConcat (TermPtr t1, TermPtr t2)
 Concatenate the given bit-vectors.
TermPtr MkBvExtract (unsigned high, unsigned low, TermPtr t)
 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.
TermPtr MkBvSignExt (unsigned i, TermPtr t)
 Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
TermPtr MkBvZeroExt (unsigned i, TermPtr t)
 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.
TermPtr MkBvShl (TermPtr t1, TermPtr t2)
 Shift left.
TermPtr MkBvLshr (TermPtr t1, TermPtr t2)
 Logical shift right.
TermPtr MkBvAshr (TermPtr t1, TermPtr t2)
 Arithmetic shift right.
TermPtr MkBvRotateLeft (unsigned i, TermPtr t1)
 Rotate bits of t1 to the left i times.
TermPtr MkBvRotateRight (unsigned i, TermPtr t1)
 Rotate bits of t1 to the right i times.
TermPtr MkBv2Int (TermPtr t1, bool is_signed)
 Convert bit vector to integer.
TermPtr MkInt2Bv (unsigned size, TermPtr t1)
 Convert integer to bit vector.
TermPtr MkBvAddNoOverflow (TermPtr t1, TermPtr t2, bool is_signed)
 Check that addition does not overflow.
TermPtr MkBvAddNoUnderflow (TermPtr t1, TermPtr t2)
 Check that addition does not underflow.
TermPtr MkBvSubNoOverflow (TermPtr t1, TermPtr t2)
 Check that subtraction does not overflow.
TermPtr MkBvSubNoUnderflow (TermPtr t1, TermPtr t2, bool is_signed)
 Check that subtraction does not underflow.
TermPtr MkBvSDivNoOverflow (TermPtr t1, TermPtr t2)
 Check that division does not overflow.
TermPtr MkBvNegNoOverflow (TermPtr t1)
 Check that negation does not overflow.
TermPtr MkBvMulNoOverflow (TermPtr t1, TermPtr t2, bool is_signed)
 Check that multiplication does not overflow.
TermPtr MkBvMulNoUnderflow (TermPtr t1, TermPtr t2)
 Check that multiplication does not underflow.
TermPtr MkArraySelect (TermPtr a, TermPtr i)
 Array read.
TermPtr MkArrayStore (TermPtr a, TermPtr i, TermPtr v)
 Array update.
TermPtr MkArrayMap (FuncDeclPtr d, array< TermPtr >^args)
 Array map.
TermPtr MkArrayConst (SortPtr domain, TermPtr v)
 Constant array.
TermPtr MkArrayDefault (TermPtr a)
 Access the array default.
Sets
SortPtr MkSetSort (SortPtr ty)
 Create Set type.
TermPtr MkEmptySet (SortPtr ty)
 Create the empty set.
TermPtr MkFullSet (SortPtr ty)
 Create the full set.
TermPtr MkSetAdd (TermPtr set, TermPtr elem)
 Add an element to a set.
TermPtr MkSetDel (TermPtr set, TermPtr elem)
 Remove an element to a set.
TermPtr MkSetUnion (array< TermPtr >^sets)
 Take the union of a arrays of sets.
TermPtr MkSetUnion (TermPtr set1, TermPtr set2)
TermPtr MkSetIntersect (array< TermPtr >^sets)
 Take the intersection of a arrays of sets.
TermPtr MkSetIntersect (TermPtr set1, TermPtr set2)
TermPtr MkSetDifference (TermPtr arg1, TermPtr arg2)
 Take the set difference between two sets.
TermPtr MkSetComplement (TermPtr arg)
 Take the complement of a set.
TermPtr MkSetMember (TermPtr elem, TermPtr set)
 Check for set membership.
TermPtr MkSetSubset (TermPtr arg1, TermPtr arg2)
 Check for subsetness of sets.
Injective functions
FuncDeclPtr MkInjectiveFunction (String^name, array< SortPtr >^domain, SortPtr range)
 Create injective function.
FuncDeclPtr MkInjectiveFunction (Symbol^name, array< SortPtr >^domain, SortPtr range)
Numerals
TermPtr MkNumeral (String^numeral, SortPtr ty)
 Create a numeral of a given type.
TermPtr MkNumeral (int n, SortPtr ty)
TermPtr MkNumeral (unsigned n, SortPtr ty)
TermPtr MkNumeral (__int64 n, SortPtr ty)
TermPtr MkNumeral (unsigned __int64 n, SortPtr ty)
Quantifiers
PatternPtr MkPattern (array< TermPtr >^terms)
 Create a pattern for quantifier instantiation.
TermPtr MkBound (unsigned index, SortPtr ty)
 Create a bound variable.
TermPtr MkForall (unsigned weight, array< PatternPtr >^patterns, array< SortPtr >^types, array< Symbol^>^names, TermPtr body)
 Create a forall formula.
TermPtr MkForall (unsigned weight, array< PatternPtr >^patterns, array< SortPtr >^types, array< String^>^names, TermPtr body)
 Create a forall formula.
TermPtr MkForall (unsigned weight, array< AppPtr >^bound, array< PatternPtr >^patterns, TermPtr body)
 Create a forall formula.
TermPtr MkExists (unsigned weight, array< PatternPtr >^patterns, array< SortPtr >^types, array< Symbol^>^names, TermPtr body)
 Create an exists formula. Similar to MkForall.
TermPtr MkExists (unsigned weight, array< PatternPtr >^patterns, array< SortPtr >^types, array< String^>^names, TermPtr body)
TermPtr MkExists (unsigned weight, array< AppPtr >^bound, array< PatternPtr >^patterns, TermPtr body)
TermPtr MkQuantifier (bool is_forall, unsigned weight, array< PatternPtr >^patterns, array< TermPtr >^no_patterns, array< SortPtr >^types, array< Symbol^>^names, TermPtr body)
 Create a quantifier with no-pattern directives.
Accessors
SymbolKind GetSymbolKind (Symbol^s)
 Return SymbolKind.Int if the symbol was constructed using MkIntSymbol, and SymbolKind.String if the symbol was constructed using MkStringSymbol.
int GetSymbolInt (Symbol^s)
 Return the symbol int value.
String GetSymbolString (Symbol^s)
 Return the symbol name.
bool IsEq (TermPtr t1, TermPtr t2)
 Return true if the two given AST nodes are equal.
TermKind GetTermKind (TermPtr a)
 Return the kind of the given AST.
DeclKind GetDeclKind (FuncDeclPtr d)
 Return the kind of the built-in operator.
array< IRawParameter^> GetDeclParameters (FuncDeclPtr d)
 Return auxiliary parameters associated with the built-in operator. For example, the operator for bit-vector extraction uses two parameters, the upper and lower bit-index for extraction.
FuncDeclPtr GetAppDecl (AppPtr a)
 Return the declaration of a constant or function application.
array< TermPtr > GetAppArgs (AppPtr a)
 Return the arguments of an application. If t is an constant, then array is empty.
String GetNumeralString (TermPtr a)
 Return the number of a numeric ast.
int GetNumeralInt (TermPtr v)
 Similar to GetNumeralString, but only succeeds if the value can fit in a machine int. Throw InvalidArgument if the call fails.
bool TryGetNumeralInt (TermPtr v,[Runtime::InteropServices::Out] int%i)
unsigned int GetNumeralUInt (TermPtr v)
 Similar to GetNumeralString, but only succeeds if the value can fit in a machine unsigned int. Throw InvalidArgument if the call fails.
bool TryGetNumeralUInt (TermPtr v,[Runtime::InteropServices::Out] unsigned int%u)
unsigned __int64 GetNumeralUInt64 (TermPtr v)
 Similar to GetNumeralString, but only succeeds if the value can fit in a machine unsigned long long int. Throw InvalidArgument if the call fails.
bool TryGetNumeralUInt64 (TermPtr v,[Runtime::InteropServices::Out] unsigned __int64%u)
__int64 GetNumeralInt64 (TermPtr v)
 Similar to GetNumeralString, but only succeeds if the value can fit in a machine long long int. Throw InvalidArgument if the call fails.
bool TryGetNumeralInt64 (TermPtr v,[Runtime::InteropServices::Out] __int64%i)
LBool GetBoolValue (TermPtr a)
 Return the Boolean value of a truth constant. Return LBool::Undef if a is not a boolean constant (true or false).
bool TryGetArrayValue (TermPtr a,[Runtime::InteropServices::Out] RawArrayValue^%av)
 Return decomposed sequence of stores as an array value.
unsigned GetVarIndex (TermPtr a)
 Return the index of a de-Brujin bound variable.
RawQuantifier GetQuantifier (TermPtr a)
 Return components of a quantifier.
array< TermPtr > GetPatternTerms (PatternPtr p)
 Return array of terms in the pattern.
Symbol GetDeclName (FuncDeclPtr d)
 Return the constant declaration name as a symbol.
Symbol GetSortName (SortPtr ty)
 Return the type name as a symbol.
SortPtr GetSort (TermPtr a)
 Return the type of an AST node.
array< SortPtr > GetDomain (FuncDeclPtr d)
 Return the domain of a function declaration.
SortPtr GetRange (FuncDeclPtr d)
 Return the range of the given declaration.
SortKind GetSortKind (SortPtr t)
 Return the type kind (e.g., array, tuple, int, bool, etc).
unsigned GetBvSortSize (SortPtr t)
 Return the size of the given bit-vector type.
SortPtr GetArraySortDomain (SortPtr t)
 Return the domain of the given array type.
SortPtr GetArraySortRange (SortPtr t)
 Return the range of the given array type.
FuncDeclPtr GetTupleConstructor (SortPtr t)
 Return the constructor declaration of the given tuple type.
array< FuncDeclPtr > GetTupleFields (SortPtr t)
 Return the field declarations of a given tuple type.
Constraints
void Push ()
 Create a backtracking point.
void Pop (unsigned num_scopes)
 Backtrack.
void Pop ()
void PersistTerm (TermPtr t, unsigned num_scopes)
 Persist a term during num_scopes of pops.
void AssertCnstr (TermPtr a)
 Assert a constraing into the logical context.
LBool CheckAndGetModel ([Runtime::InteropServices::Out] RawModel^%m)
 Check whether the given logical context is consistent or not.
LBool Check ()
 Check whether the given logical context is consistent or not.
LBool CheckAssumptions ([Runtime::InteropServices::Out] RawModel^%m,[Runtime::InteropServices::In] array< TermPtr >^assumptions,[Runtime::InteropServices::Out] TermPtr%proof,[Runtime::InteropServices::Out] array< TermPtr >^%core)
 Check whether the given logical context is consistent or not with respect to auxiliary assumptions.
LBool GetImpliedEqualities ([Runtime::InteropServices::In] array< TermPtr >^terms,[Runtime::InteropServices::Out] array< unsigned >^%class_ids)
 Retrieve congruence class representatives for terms.
SearchFailureExplanation GetSearchFailureExplanation ()
 Obtain explanation for search failure.
TermPtr GetAssignments ()
 Return conjunction of literals and formulas assigned to true in the current state.
LabeledLiterals GetRelevantLabels ()
 Retrieve set of labels set in current satisfying assignment.
LabeledLiterals GetRelevantLiterals ()
 Retrieve set of literals satisfying the current assignment.
LabeledLiterals GetGuessedLiterals ()
 Retrieve set of guessed literals satisfying the current assignment.
void BlockLiterals (LabeledLiterals^labels)
 Block the combination of remaining non-disabled labels.
TermPtr GetLiteral (LabeledLiterals^labels, unsigned idx)
 Obtain literal corresponding to index in list of literals.
TermPtr Simplify (TermPtr a)
 Interface to simplifier.
String conversion
void SetPrintMode (PrintMode mode)
 Select mode for the format used for pretty-printing AST nodes.
String ToString (AstPtr a)
 Convert the given AST node into a string.
void Display (System::IO::TextWriter^w, AstPtr a)
virtual String ToString () override
 Convert the given logical context into a string.
void Display (System::IO::TextWriter^w)
String StatisticsToString ()
 Convert the given logical context into a string.
void DisplayStatistics (System::IO::TextWriter^w)
String BenchmarkToSmtlib (String^name, String^logic, String^status, String^attributes, array< TermPtr >^assumptions, TermPtr formula)
 Convert the given benchmark into SMT-LIB formatted string.
Parser interface
void ParseSmtlibString (String^string,[Runtime::InteropServices::In] array< SortPtr >^sorts,[Runtime::InteropServices::In] array< FuncDeclPtr >^decls,[Runtime::InteropServices::Out] array< TermPtr >^%assumptions,[Runtime::InteropServices::Out] array< TermPtr >^%formulas,[Runtime::InteropServices::Out] array< FuncDeclPtr >^%new_decls,[Runtime::InteropServices::Out] array< SortPtr >^%new_sorts,[Runtime::InteropServices::Out] String^%parser_out)
 Parse the given string using the SMT-LIB parser.
void ParseSmtlibFile (String^file,[Runtime::InteropServices::In] array< SortPtr >^sorts,[Runtime::InteropServices::In] array< FuncDeclPtr >^decls,[Runtime::InteropServices::Out] array< TermPtr >^%assumptions,[Runtime::InteropServices::Out] array< TermPtr >^%formulas,[Runtime::InteropServices::Out] array< FuncDeclPtr >^%new_decls,[Runtime::InteropServices::Out] array< SortPtr >^%new_sorts,[Runtime::InteropServices::Out] String^%parser_out)
 Similar to ParseSmtlibString, but reads the benchmark from a file.
TermPtr ParseZ3String (String^s)
 Parse a string in the native Z3 format.
TermPtr ParseZ3File (String^filename)
 Parse a file containing formulas in the Simplify format.
TermPtr ParseSimplifyString (String^s,[Runtime::InteropServices::Out] String^%parser_out)
 Parse a string in the simplify format.
TermPtr ParseSimplifyFile (String^filename,[Runtime::InteropServices::Out] String^%parser_out)
 Parse a file containing formulas in the Simplify format.
Miscellaneous
void GetVersion ([Runtime::InteropServices::Out] unsigned%major,[Runtime::InteropServices::Out] unsigned%minor,[Runtime::InteropServices::Out] unsigned%build_number,[Runtime::InteropServices::Out] unsigned%revision_number)
 Return Z3 version number information.

Static Public Member Functions

Errors
static void SetErrorHandler (IErrorHandler^h)
 Register a Z3 error handler.
static String GetErrorMessage (ErrorCode err)
 Return a string describing the given error code.
static void ResetMemory ()
 Free all resources allocated for Z3.

Detailed Description

Z3 API object.

Definition at line 731 of file Microsoft.Z3.h.

Constructor & Destructor Documentation

RawContext ( Config^  config  ) 

Create a logical context using the given configuration.

After a context is created, the configuration cannot be changed. All main interaction with Z3 happens in the context of a Context.

All contexts that are created must be disposed (call Dispose). Failure to dispose contexts cause memory leaks. Garbage collection will not free resources allocated in contexts.

Member Function Documentation

void AppendLog ( String^  string  ) 

Append instruction or comment to log with assertion.

See also:
OpenLog

void AssertCnstr ( TermPtr  a  ) 

Assert a constraing into the logical context.

After one assertion, the logical context may become inconsistent.

The functions Check or CheckAndGetModel should be used to check whether the logical context is consistent or not.

See also:
Check

CheckAndGetModel

String BenchmarkToSmtlib ( String^  name,
String^  logic,
String^  status,
String^  attributes,
array< TermPtr >^  assumptions,
TermPtr  formula 
)

Convert the given benchmark into SMT-LIB formatted string.

void BlockLiterals ( LabeledLiterals^  labels  ) 

Block the combination of remaining non-disabled labels.

Subsequent calls to Check will not contain satisfying assignments with the same combination of labels.

LBool Check (  ) 

Check whether the given logical context is consistent or not.

The function GetModel should be used when models are needed.

See also:
GetModel

LBool CheckAndGetModel ( [Runtime::InteropServices::Out] RawModel^%  m  ) 

Check whether the given logical context is consistent or not.

If the logical context is not unsatisfiable (i.e., the return value is different from false) and model construction is enabled (see Config), then a model is stored in m. Otherwise, the value null is stored in m. The caller is responsible for deleting the model using its Dispose method.

Remarks:
Model construction must be enabled using configuration parameters (See, Config).
See also:
Check

LBool CheckAssumptions ( [Runtime::InteropServices::Out] RawModel^%  m,
[Runtime::InteropServices::In] array< TermPtr >^  assumptions,
[Runtime::InteropServices::Out] TermPtr%  proof,
[Runtime::InteropServices::Out] array< TermPtr >^%  core 
)

Check whether the given logical context is consistent or not with respect to auxiliary assumptions.

If the logical context is not unsatisfiable (i.e., the return value is different from false) and model construction is enabled (see Config), then a model is stored in m. Otherwise, the value null is stored in m. The caller is responsible for deleting the model using its Dispose method. If the logical context is unsatisfiable, then a proof object is return and stored in proof. An unsatisfiable core (subset) for the set of supplied assumptions is returned.

Remarks:
Model construction must be enabled using configuration parameters (See, Config).
Parameters:
m returned model.
assumptions array of auxiliary assumptions.
proof proof object. Proofs must be enabled for this value to be returned.
core subset of assumptions that is an unsatisfiable core.
See also:
Check

void CloseLog (  ) 

Close file with logged assertions.

See also:
OpenLog

void EnableDebugTrace ( String^  tag  ) 

Enable debug tracing of tagged log.

array<FuncDeclPtr> GetAccessors ( Constructor^  c  )  [inline]

retrieve accessors for datatype.

Definition at line 1029 of file Microsoft.Z3.h.

01029 { return c->GetAccessors(); }

array<TermPtr> GetAppArgs ( AppPtr  a  ) 

Return the arguments of an application. If t is an constant, then array is empty.

FuncDeclPtr GetAppDecl ( AppPtr  a  ) 

Return the declaration of a constant or function application.

Precondition:
GetTermKind(a) == TermKind.App

SortPtr GetArraySortDomain ( SortPtr  t  ) 

Return the domain of the given array type.

Precondition:
GetSortKind(t) == SortKind.Array
See also:
MkArraySort

GetSortKind

SortPtr GetArraySortRange ( SortPtr  t  ) 

Return the range of the given array type.

Precondition:
GetSortKind(t) == SortKind.Array
See also:
MkArraySort

GetSortKind

TermPtr GetAssignments (  ) 

Return conjunction of literals and formulas assigned to true in the current state.

LBool GetBoolValue ( TermPtr  a  ) 

Return the Boolean value of a truth constant. Return LBool::Undef if a is not a boolean constant (true or false).

Precondition:
GetTermKind(a) == TermKind.App

unsigned GetBvSortSize ( SortPtr  t  ) 

Return the size of the given bit-vector type.

Precondition:
GetSortKind(t) = SortKind.Bv
See also:
MkBvSort

GetSortKind

FuncDeclPtr GetConstructor ( Constructor^  c  )  [inline]

retrieve constructor function declaration.

Definition at line 1019 of file Microsoft.Z3.h.

01019 { return c->GetConstructor(); }

DeclKind GetDeclKind ( FuncDeclPtr  d  ) 

Return the kind of the built-in operator.

Precondition:
GetTermKind(a) == TermKind.App

Symbol GetDeclName ( FuncDeclPtr  d  ) 

Return the constant declaration name as a symbol.

array<IRawParameter^> GetDeclParameters ( FuncDeclPtr  d  ) 

Return auxiliary parameters associated with the built-in operator. For example, the operator for bit-vector extraction uses two parameters, the upper and lower bit-index for extraction.

array<SortPtr> GetDomain ( FuncDeclPtr  d  ) 

Return the domain of a function declaration.

static String GetErrorMessage ( ErrorCode  err  )  [static]

Return a string describing the given error code.

LabeledLiterals GetGuessedLiterals (  ) 

Retrieve set of guessed literals satisfying the current assignment.

LBool GetImpliedEqualities ( [Runtime::InteropServices::In] array< TermPtr >^  terms,
[Runtime::InteropServices::Out] array< unsigned >^%  class_ids 
)

Retrieve congruence class representatives for terms.

The function can be used for relying on Z3 to identify equal terms under the current set of assumptions. The array of terms and array of class identifiers should have the same length. The class identifiers are numerals that are assigned to the same value for their corresponding terms if the current context forces the terms to be equal. You cannot deduce that terms corresponding to different numerals must be different, (especially when using non-convex theories). Also note that not necessarily all implied equalities are returned by this call. Only the set of implied equalities that follow from simple constraint and equality propagation is discovered.

A side-effect of the function is a satisfiability check. The function return LBool.False if the current assertions are not satisfiable.

See also:
Check

TermPtr GetLiteral ( LabeledLiterals^  labels,
unsigned  idx 
) [inline]

Obtain literal corresponding to index in list of literals.

Definition at line 2533 of file Microsoft.Z3.h.

02533                                                                   {
02534             return labels->GetLiteral(idx);
02535         }

int GetNumeralInt ( TermPtr  v  ) 

Similar to GetNumeralString, but only succeeds if the value can fit in a machine int. Throw InvalidArgument if the call fails.

Precondition:
GetTermKind(v) == TermKind.Numeral && IsInt32(v)
See also:
GetNumeralString

__int64 GetNumeralInt64 ( TermPtr  v  ) 

Similar to GetNumeralString, but only succeeds if the value can fit in a machine long long int. Throw InvalidArgument if the call fails.

Precondition:
GetTermKind(v) == TermKind.Numeral
See also:
GetNumeralTermPtrString

String GetNumeralString ( TermPtr  a  ) 

Return the number of a numeric ast.

Precondition:
GetTermKind(a) == TermKind.Numeral

unsigned int GetNumeralUInt ( TermPtr  v  ) 

Similar to GetNumeralString, but only succeeds if the value can fit in a machine unsigned int. Throw InvalidArgument if the call fails.

Precondition:
GetTermKind(v) == TermKind.Numeral
See also:
GetNumeralString

unsigned __int64 GetNumeralUInt64 ( TermPtr  v  ) 

Similar to GetNumeralString, but only succeeds if the value can fit in a machine unsigned long long int. Throw InvalidArgument if the call fails.

Precondition:
GetTermKind(v) == TermKind.Numeral
See also:
GetNumeralString

array<TermPtr> GetPatternTerms ( PatternPtr  p  ) 

Return array of terms in the pattern.

Precondition:
GetTermKind(a) = TermKind.Pattern

RawQuantifier GetQuantifier ( TermPtr  a  ) 

Return components of a quantifier.

Precondition:
GetTermKind(a) = TermKind.Quantifier

SortPtr GetRange ( FuncDeclPtr  d  ) 

Return the range of the given declaration.

If d is a constant (i.e., has zero arguments), then this function returns the type of the constant.

LabeledLiterals GetRelevantLabels (  ) 

Retrieve set of labels set in current satisfying assignment.

LabeledLiterals GetRelevantLiterals (  ) 

Retrieve set of literals satisfying the current assignment.

SearchFailureExplanation GetSearchFailureExplanation (  ) 

Obtain explanation for search failure.

See also:
Check()

SortPtr GetSort ( TermPtr  a  ) 

Return the type of an AST node.

The AST node must be a constant, application, numeral, bound variable, or quantifier.

SortKind GetSortKind ( SortPtr  t  ) 

Return the type kind (e.g., array, tuple, int, bool, etc).

See also:
SortKind

Symbol GetSortName ( SortPtr  ty  ) 

Return the type name as a symbol.

int GetSymbolInt ( Symbol^  s  ) 

Return the symbol int value.

Precondition:
GetSymbolKind(s) == SymbolKind.Int
See also:
MkIntSymbol

SymbolKind GetSymbolKind ( Symbol^  s  ) 

Return SymbolKind.Int if the symbol was constructed using MkIntSymbol, and SymbolKind.String if the symbol was constructed using MkStringSymbol.

String GetSymbolString ( Symbol^  s  ) 

Return the symbol name.

Precondition:
GetSymbolKind(s) = SymbolKind.String
See also:
MkStringSymbol

TermKind GetTermKind ( TermPtr  a  ) 

Return the kind of the given AST.

FuncDeclPtr GetTester ( Constructor^  c  )  [inline]

retrieve test function for constructor.

Definition at line 1024 of file Microsoft.Z3.h.

01024 { return c->GetTester(); }

FuncDeclPtr GetTupleConstructor ( SortPtr  t  ) 

Return the constructor declaration of the given tuple type.

Precondition:
GetSortKind(t) == SortKind.Tuple
See also:
MkTupleSort

GetSortKind

array<FuncDeclPtr> GetTupleFields ( SortPtr  t  ) 

Return the field declarations of a given tuple type.

Precondition:
GetSortKind(t) == SortKind.Tuple
See also:
MkTupleSort

GetSortKind

unsigned GetVarIndex ( TermPtr  a  )  [inline]

Return the index of a de-Brujin bound variable.

Precondition:
GetTermKind(a) == TermKind.Var

Definition at line 2225 of file Microsoft.Z3.h.

02225                                         {
02226             return Z3_get_index_value(m_context, get_ast(a));
02227         }

void GetVersion ( [Runtime::InteropServices::Out] unsigned%  major,
[Runtime::InteropServices::Out] unsigned%  minor,
[Runtime::InteropServices::Out] unsigned%  build_number,
[Runtime::InteropServices::Out] unsigned%  revision_number 
)

Return Z3 version number information.

bool IsEq ( TermPtr  t1,
TermPtr  t2 
)

Return true if the two given AST nodes are equal.

TermPtr MkAdd ( array< TermPtr >^  args  ) 

Create an AST node representing args[0] + ... + args[args.Length-1].

All arguments must have int or real type.

Remarks:
The number of arguments must be greater than zero.

TermPtr MkAnd ( array< TermPtr >^  args  ) 

Create an AST node representing args[0] and ... and args[args.Length-1].

All arguments must have Boolean type.

Remarks:
The number of arguments must be greater than zero.

AppPtr MkApp ( FuncDeclPtr  d,
array< TermPtr >^  args 
)

Create a constant or function application.

See also:
MkFuncDecl

TermPtr MkArrayConst ( SortPtr  domain,
TermPtr  v 
)

Constant array.

The node a must have an array type [range], domain indicates the domain of the array. The type of the result is [domain -> range].

See also:
MkArraySort

MkArraySelect

MkArrayStore

TermPtr MkArrayDefault ( TermPtr  a  ) 

Access the array default.

The node a must have an array type [domain -> range]. The type of the result is [range]. The result is a term whose value holds the default array value. That is, models should ensure that the default for a (ElseCase) evaluates to the same value as MkArrayDefault(a).

See also:
MkArraySort

MkArraySelect

MkArrayStore

MkArrayconst

TermPtr MkArrayMap ( FuncDeclPtr  d,
array< TermPtr >^  args 
)

Array map.

The n nodes args must be of array sorts [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

MkArraySelect

MkArrayStore

TermPtr MkArraySelect ( TermPtr  a,
TermPtr  i 
)

Array read.

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

See also:
MkArraySort

MkArrayStore

SortPtr MkArraySort ( SortPtr  domain,
SortPtr  range 
)

Create an array type.

We usually represent the array type as: [domain -> range]. Arrays are usually used to model the heap/memory in software verification.

See also:
MkArraySelect

MkArrayStore

MkArrayMap

MkConstArray

TermPtr MkArrayStore ( TermPtr  a,
TermPtr  i,
TermPtr  v 
)

Array update.

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

See also:
MkArraySort

MkArraySelect

SortPtr MkBoolSort (  ) 

Create the boolean type.

This type is used to create propositional variables and predicates.

TermPtr MkBound ( unsigned  index,
SortPtr  ty 
)

Create a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

           abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
           abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
           abs1(x, x, n) = b_n
           abs1(y, x, n) = y
           abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
           abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Parameters:
index de-Bruijn index
ty type of the bound variable
See also:
MkForall

MkExists

TermPtr MkBv2Int ( TermPtr  t1,
bool  is_signed 
)

Convert bit vector to integer.

The node t1 must have a bit-vector type.

TermPtr MkBvAdd ( TermPtr  t1,
TermPtr  t2 
)

Standard two's complement addition.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvAddNoOverflow ( TermPtr  t1,
TermPtr  t2,
bool  is_signed 
)

Check that addition does not overflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvAddNoUnderflow ( TermPtr  t1,
TermPtr  t2 
)

Check that addition does not underflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvAnd ( TermPtr  t1,
TermPtr  t2 
)

Bitwise and.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvAshr ( TermPtr  t1,
TermPtr  t2 
)

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.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvConcat ( TermPtr  t1,
TermPtr  t2 
)

Concatenate the given bit-vectors.

The nodes t1 and t2 must have (possibly different) bit-vector types

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

TermPtr MkBvExtract ( unsigned  high,
unsigned  low,
TermPtr  t 
)

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 node t must have a bit-vector type.

TermPtr MkBvLshr ( TermPtr  t1,
TermPtr  t2 
)

Logical shift right.

It is equivalent to unsigned division by 2^x where x is the value of the third argument.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvMul ( TermPtr  t1,
TermPtr  t2 
)

Standard two's complement multiplication.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvMulNoOverflow ( TermPtr  t1,
TermPtr  t2,
bool  is_signed 
)

Check that multiplication does not overflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvMulNoUnderflow ( TermPtr  t1,
TermPtr  t2 
)

Check that multiplication does not underflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvNand ( TermPtr  t1,
TermPtr  t2 
)

Bitwise nand.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvNeg ( TermPtr  t1  ) 

Standard two's complement unary minus.

The node t1 must have bit-vector type.

TermPtr MkBvNegNoOverflow ( TermPtr  t1  ) 

Check that negation does not overflow.

TermPtr MkBvNor ( TermPtr  t1,
TermPtr  t2 
)

Bitwise nor.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvNot ( TermPtr  t1  ) 

Bitwise negation.

The node arg1 must have a bit-vector type.

TermPtr MkBvOr ( TermPtr  t1,
TermPtr  t2 
)

Bitwise or.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvRotateLeft ( unsigned  i,
TermPtr  t1 
)

Rotate bits of t1 to the left i times.

The node t1 must have a bit-vector type.

TermPtr MkBvRotateRight ( unsigned  i,
TermPtr  t1 
)

Rotate bits of t1 to the right i times.

The node t1 must have a bit-vector type.

TermPtr MkBvSdiv ( TermPtr  t1,
TermPtr  t2 
)

Two's complement 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 nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSDivNoOverflow ( TermPtr  t1,
TermPtr  t2 
)

Check that division does not overflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSge ( TermPtr  t1,
TermPtr  t2 
)

Two's complement signed greater than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSgt ( TermPtr  t1,
TermPtr  t2 
)

Two's complement signed greater than.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvShl ( TermPtr  t1,
TermPtr  t2 
)

Shift left.

It is equivalent to multiplication by 2^x where x is the value of the third argument.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSignExt ( unsigned  i,
TermPtr  t 
)

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

The node t must have a bit-vector type.

TermPtr MkBvSle ( TermPtr  t1,
TermPtr  t2 
)

Two's complement signed less than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSlt ( TermPtr  t1,
TermPtr  t2 
)

Two's complement signed less than.

It abbreviates: 

           (or (and (= (extract[|m-1|:|m-1|] s) bit1)
                    (= (extract[|m-1|:|m-1|] t) bit0))
               (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
                    (bvult s t)))

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSmod ( TermPtr  t1,
TermPtr  t2 
)

Two's complement signed remainder (sign follows divisor).

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector type.

See also:
MkBvSrem

SortPtr MkBvSort ( unsigned  sz  ) 

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

Remarks:
The size of the bitvector type must be greater than zero.

TermPtr MkBvSrem ( TermPtr  t1,
TermPtr  t2 
)

Two's complement signed remainder (sign follows dividend).

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 nodes t1 and t2 must have the same bit-vector type.

See also:
MkBvSmod

TermPtr MkBvSub ( TermPtr  t1,
TermPtr  t2 
)

Standard two's complement subtraction.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSubNoOverflow ( TermPtr  t1,
TermPtr  t2 
)

Check that subtraction does not overflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvSubNoUnderflow ( TermPtr  t1,
TermPtr  t2,
bool  is_signed 
)

Check that subtraction does not underflow.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvUdiv ( TermPtr  t1,
TermPtr  t2 
)

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 nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvUge ( TermPtr  t1,
TermPtr  t2 
)

Unsigned greater than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvUgt ( TermPtr  t1,
TermPtr  t2 
)

Unsigned greater than.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvUle ( TermPtr  t1,
TermPtr  t2 
)

Unsigned less than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvUlt ( TermPtr  t1,
TermPtr  t2 
)

Unsigned less than.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvUrem ( TermPtr  t1,
TermPtr  t2 
)

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 nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvXnor ( TermPtr  t1,
TermPtr  t2 
)

Bitwise xnor.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvXor ( TermPtr  t1,
TermPtr  t2 
)

Bitwise exclusive-or.

The nodes t1 and t2 must have the same bit-vector type.

TermPtr MkBvZeroExt ( unsigned  i,
TermPtr  t 
)

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 node t1 must have a bit-vector type.

AppPtr MkConst ( FuncDeclPtr  d  ) 

Declare and create a constant.

See also:
MkApp

MkFuncDecl

Constructor MkConstructor ( String^  name,
String^  tester,
array< String^>^  field_names,
array< SortPtr >^  field_sorts,
array< unsigned >^  field_refs 
)

create constructor object for datatype declarations. The object must be disposed with manually.

Use the methods GetConstructor, GetTester, and GetAccessors to retrieve the function declarations for constructors, tester and accessors after the datatype has been declared.

A field_ref is the index of the (mutually) recursive datatype. For example, if you declare a single recursive datatype, then a reference to the recursive datatype that is being declared is the number 0. If you declare two mutually recursive datatypes, then the reference to the second recursive datatype is 1.

SortPtr MkDataType ( String^  name,
array< Constructor^>^  constructors 
)

create datatype sort.

array<SortPtr> MkDataTypes ( array< String^>^  names,
array< array< Constructor^>^>^  constructors 
)

create datatype sorts.

Parameters:
names array of names for the recursive datatypes.
constructors array of arrays of constructors.

TermPtr MkDistinct ( array< TermPtr >^  args  ) 

Create an AST node representing distinct(args[0], ..., args[args.Length-1]).

The distinct construct is used for declaring the arguments pairwise distinct. That is, Forall 0 <= i < j < args.Length. not args[i] = args[j].

All arguments must have the same type.

Remarks:
The number of arguments of a distinct construct must be greater than one.

TermPtr MkDiv ( TermPtr  arg1,
TermPtr  arg2 
)

Create integer or real division.

The nodes arg1 and arg2 must have the same type, and must be int or real.

TermPtr MkEmptySet ( SortPtr  ty  )  [inline]

Create the empty set.

Definition at line 1759 of file Microsoft.Z3.h.

01759 { return TermPtr(Z3_mk_empty_set(m_context, get_sort_ast(ty))); }

SortPtr MkEnumerationSort ( String^  name,
array< String^>^  enum_names,
array< FuncDeclPtr >^  enum_consts,
array< FuncDeclPtr >^  enum_testers 
)

create an enumeration type.

Parameters:
name - name of enumeration sort.
enum_names - names of enumerated elements.
enum_consts - output function declarations for enumerated elements.
enum_testers - output function declarations for enumeration testers.

TermPtr MkEq ( TermPtr  l,
TermPtr  r 
)

Create an AST node representing l = r.

The nodes l and r must have the same type.

TermPtr MkExists ( unsigned  weight,
array< PatternPtr >^  patterns,
array< SortPtr >^  types,
array< Symbol^>^  names,
TermPtr  body 
)

Create an exists formula. Similar to MkForall.

See also:
MkPattern

MkBound

MkForall

TermPtr MkFalse (  )  [inline]

Create an AST node representing false.

Definition at line 1145 of file Microsoft.Z3.h.

01145 { return TermPtr(Z3_mk_false(m_context)); }

TermPtr MkForall ( unsigned  weight,
array< AppPtr >^  bound,
array< PatternPtr >^  patterns,
TermPtr  body 
)

Create a forall formula.

This function allows creating a forall without using de-Bruijn indices in the body or patterns. It is sometimes convenient to create the body of a quantifier without de-Bruijn indices, but instead use constants. These constants have to be replaced by de-Bruijn indices for the internal representation. This function allows the caller to hand over the task to Z3 of abstracting the constants into bound variables, so that each occurrence of the variables in the array bound gets replaced by a de-Bruijn index.

Parameters:
weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
bound array containing the constants to be abstracted as bound variables.
patterns array containing the patterns created using MkPattern.
body the body of the quantifier.
See also:
MkPattern

MkExists

TermPtr MkForall ( unsigned  weight,
array< PatternPtr >^  patterns,
array< SortPtr >^  types,
array< String^>^  names,
TermPtr  body 
)

Create a forall formula.

Parameters:
weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patterns array containing the patterns created using MkPattern.
types array containing the types of the bound variables.
names array containing the names as strings of the bound variables.
body the body of the quantifier.
See also:
MkPattern

MkBound

MkExists

TermPtr MkForall ( unsigned  weight,
array< PatternPtr >^  patterns,
array< SortPtr >^  types,
array< Symbol^>^  names,
TermPtr  body 
)

Create a forall formula.

Parameters:
weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
patterns array containing the patterns created using MkPattern.
types array containing the types of the bound variables.
names array containing the names as symbols of the bound variables.
body the body of the quantifier.
See also:
MkPattern

MkBound

MkExists

TermPtr MkFreshConst ( String^  prefix,
SortPtr  ty 
)

Declare and create a fresh constant.

See also:
MkFuncDecl

MkApp

FuncDeclPtr MkFreshFuncDecl ( String^  prefix,
array< SortPtr >^  domain,
SortPtr  range 
)

Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration.

See also:
MkFuncDecl

TermPtr MkFullSet ( SortPtr  ty  )  [inline]

Create the full set.

Definition at line 1764 of file Microsoft.Z3.h.

01764 { return TermPtr(Z3_mk_full_set(m_context, get_sort_ast(ty))); }

FuncDeclPtr MkFuncDecl ( Symbol^  s,
array< SortPtr >^  domain,
SortPtr  range 
)

Declare a constant or function.

Parameters:
s name of the constant or function.
domain array containing the type of each argument. The array must contain domain_size elements. It is 0 whe declaring a constant.
range type of the constant or the return type of the function.
After declaring a constant or function, the function MkApp can be used to create a constant or function application.

See also:
MkApp

TermPtr MkGe ( TermPtr  arg1,
TermPtr  arg2 
)

Create greater than or equal to.

The nodes arg1 and arg2 must have the same type, and must be int or real.

TermPtr MkGt ( TermPtr  arg1,
TermPtr  arg2 
)

Create greater than.

The nodes arg1 and arg2 must have the same type, and must be int or real.

TermPtr MkIff ( TermPtr  t1,
TermPtr  t2 
)

Create an AST node representing t1 iff t2.

The nodes t1 and t2 must have Boolean type.

TermPtr MkImplies ( TermPtr  t1,
TermPtr  t2 
)

Create an AST node representing t1 implies t2.

The nodes t1 and t2 must have Boolean type.

FuncDeclPtr MkInjectiveFunction ( String^  name,
array< SortPtr >^  domain,
SortPtr  range 
)

Create injective function.

TermPtr MkInt2Bv ( unsigned  size,
TermPtr  t1 
)

Convert integer to bit vector.

The node t1 must have a integer type.

TermPtr MkInt2Real ( TermPtr  arg  ) 

Coerce integer term to real type.

There is no converse operation exposed, but you can take the floor of a real by creating an auxiliary integer constant k and and asserting MkInt2Real(k) <= t1 < MkInt2Real(k)+1.

The node arg must have type int.

SortPtr MkIntSort (  ) 

Create an integer type.

This type is not the int type found in programming languages. A machine integer can be represented using bit-vectors. The function MkBvType creates a bit-vector type.

See also:
MkBvType

TermPtr MkIte ( TermPtr  t1,
TermPtr  t2,
TermPtr  t3 
)

Create an AST node representing an if-then-else: ite(t1, t2, t3).

The node t1 must have Boolean type, t2 and t3 must have the same type. The type of the new node is equal to the type of t2 and t3.

TermPtr MkLabel ( Symbol^  name,
bool  pos,
TermPtr  fml 
)

Create labeled formula.

TermPtr MkLe ( TermPtr  arg1,
TermPtr  arg2 
)

Create less than or equal to.

The nodes arg1 and arg2 must have the same type, and must be int or real.

SortPtr MkListSort ( String^  name,
SortPtr  elem_sort,
[Runtime::InteropServices::Out] FuncDeclPtr%  nil_decl,
[Runtime::InteropServices::Out] FuncDeclPtr%  is_nil_decl,
[Runtime::InteropServices::Out] FuncDeclPtr%  cons_decl,
[Runtime::InteropServices::Out] FuncDeclPtr%  is_cons_decl,
[Runtime::InteropServices::Out] FuncDeclPtr%  head_decl,
[Runtime::InteropServices::Out] FuncDeclPtr%  tail_decl 
)

create list sort.

Parameters:
name of resulting list type.
elem_sort sort of elements.
nil_decl function declaration for nil.
is_nil_decl function declaration for nil tester.
cons_decl function declaration for cons constructor.
is_cons_decl function declaration for cons tester.
head_decl function declaration for head accessor.
tail_decl function declaration for tail accessor.

TermPtr MkLt ( TermPtr  arg1,
TermPtr  arg2 
)

Create less than.

The nodes arg1 and arg2 must have the same type, and must be int or real.

TermPtr MkMod ( TermPtr  arg1,
TermPtr  arg2 
)

Create integer modulus.

The nodes arg1 and arg2 must have integer type.

TermPtr MkMul ( array< TermPtr >^  args  ) 

Create an AST node representing args[0] * ... * args[args.Length-1].

All arguments must have int or real type.

Remarks:
Z3 has limited support for non-linear arithmetic.

The number of arguments must be greater than zero.

virtual TermPtr MkNot ( TermPtr  arg  )  [virtual]

Create an AST node representing not(a).

The node a must have Boolean type.

TermPtr MkNumeral ( String^  numeral,
SortPtr  ty 
)

Create a numeral of a given type.

Parameters:
numeral An integer, or a string representing the numeral value in decimal notation. If the given type is a real, then the numeral can be a rational, that is, a string of the form [num]* / [num]*.
ty The type of the numeral. In the current implementation, the given type can be an int, real, or bit-vectors of arbitrary size.

TermPtr MkOr ( array< TermPtr >^  args  ) 

Create an AST node representing args[0] or ... or args[args.Length-1].

All arguments must have Boolean type.

Remarks:
The number of arguments must be greater than zero.

PatternPtr MkPattern ( array< TermPtr >^  terms  ) 

Create a pattern for quantifier instantiation.

Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.

Patterns comprise an array of terms. The array of terms passed to MkPattern should be non-empty. If the array comprises of more than one term, it is a called a multi-pattern.

In general, one can pass in an array of (multi-)patterns in the quantifier constructor.

To summarize, each quantifier takes an array of alternative multi-patterns. The quantifier is instantiated for every multi-pattern that is matched. Each multi-pattern is an array of terms. All terms must match for the multi-pattern to trigger instantiation. Create a multi-pattern using MkPattern. Create an array of multi-patterns and pass it to the quantifier constructor. If you just want a multi-pattern with a single term, then pass in the singleton array

For example, if you want to create the multi-pattern consisting of the two terms: (store A I V) and (select A J) where A, I, J, V are bound variables, create the pattern

           pattern1 = context.MkPattern(new TermPtr[]{ 
                             context.MkArrayStore(A,I,V),
                             context.MkArraySelect(A,J)
                                      })
Then form the array 
 
                 new PatternPtr[]{ pattern1 }
and pass it to the function MkForall or MkExists. Suppose you also want to have the quantifier be instantiated if the pattern (select (store A I V) J) is matched, then create the pattern: 
           pattern2 = context.MkPattern(new TermPtr[] {
                                         context.MkArraySelect(context.MkArrayStore(A,I,V),J) })
Then form the array: 
                 new PatternPtr[] { pattern1, pattern2 }

See also:
MkForall

MkExists

TermPtr MkQuantifier ( bool  is_forall,
unsigned  weight,
array< PatternPtr >^  patterns,
array< TermPtr >^  no_patterns,
array< SortPtr >^  types,
array< Symbol^>^  names,
TermPtr  body 
)

Create a quantifier with no-pattern directives.

See also:
MkPattern

MkBound

MkForall

MkExists

SortPtr MkRealSort (  ) 

Create a real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

TermPtr MkRem ( TermPtr  arg1,
TermPtr  arg2 
)

Create integer remainder.

The nodes arg1 and arg2 must have integer type.

TermPtr MkSetAdd ( TermPtr  set,
TermPtr  elem 
) [inline]

Add an element to a set.

The first argument must be a set, the second an element.

Definition at line 1771 of file Microsoft.Z3.h.

01771                                                     {
01772             return TermPtr(Z3_mk_set_add(m_context, get_ast(set), get_ast(elem)));
01773         }

TermPtr MkSetComplement ( TermPtr  arg  )  [inline]

Take the complement of a set.

Definition at line 1807 of file Microsoft.Z3.h.

01807                                              {
01808             return TermPtr(Z3_mk_set_complement(m_context, get_ast(arg)));
01809         }

TermPtr MkSetDel ( TermPtr  set,
TermPtr  elem 
) [inline]

Remove an element to a set.

The first argument must be a set, the second an element.

Definition at line 1780 of file Microsoft.Z3.h.

01780                                                     {
01781             return TermPtr(Z3_mk_set_del(m_context, get_ast(set), get_ast(elem)));
01782         }

TermPtr MkSetDifference ( TermPtr  arg1,
TermPtr  arg2 
) [inline]

Take the set difference between two sets.

Definition at line 1801 of file Microsoft.Z3.h.

01801                                                             {
01802             return TermPtr(Z3_mk_set_difference(m_context, get_ast(arg1), get_ast(arg2)));
01803         }

TermPtr MkSetIntersect ( array< TermPtr >^  sets  ) 

Take the intersection of a arrays of sets.

TermPtr MkSetMember ( TermPtr  elem,
TermPtr  set 
) [inline]

Check for set membership.

The first argument should be an element type of the set.

Definition at line 1816 of file Microsoft.Z3.h.

01816                                                        {
01817             return TermPtr(Z3_mk_set_member(m_context, get_ast(elem), get_ast(set)));
01818         }

SortPtr MkSetSort ( SortPtr  ty  )  [inline]

Create Set type.

Definition at line 1754 of file Microsoft.Z3.h.

01754 { return SortPtr(Z3_mk_set_sort(m_context, get_sort_ast(ty))); }

TermPtr MkSetSubset ( TermPtr  arg1,
TermPtr  arg2 
) [inline]

Check for subsetness of sets.

Definition at line 1823 of file Microsoft.Z3.h.

01823                                                         {
01824             return TermPtr(Z3_mk_set_subset(m_context, get_ast(arg1), get_ast(arg2)));
01825         }

TermPtr MkSetUnion ( array< TermPtr >^  sets  ) 

Take the union of a arrays of sets.

The arguments must all be of the same type and all be of set types.

SortPtr MkSort ( Symbol^  s  ) 

Create a free (uninterpreted) type using the given name (symbol).

Two free types are considered the same iff the have the same name.

TermPtr MkSub ( array< TermPtr >^  args  ) 

Create an AST node representing args[0] - ... - args[args.Length - 1].

All arguments must have int or real type.

Remarks:
The number of arguments must be greater than zero.

Symbol MkSymbol ( int  i  ) 

Create a Z3 symbol using an intege or a string.

Symbols are used to name several term and type constructors.

TermPtr MkTrue (  )  [inline]

Create an AST node representing true.

Definition at line 1139 of file Microsoft.Z3.h.

01139 { return TermPtr(Z3_mk_true(m_context)); }

SortPtr MkTupleSort ( Symbol^  mk_tuple_name,
array< Symbol^>^  field_names,
array< SortPtr >^  field_types,
[Runtime::InteropServices::Out] FuncDeclPtr%  mk_tuple_decl,
[Runtime::InteropServices::Out] array< FuncDeclPtr >^  proj_decl 
)

Create a tuple type.

A tuple with n fields has a constructor and n projections. This function will also declare the constructor and projection functions.

Parameters:
mk_tuple_name name of the constructor function associated with the tuple type.
field_names name of the projection functions.
field_types type of the tuple fields.
mk_tuple_decl output parameter that will contain the constructor declaration.
proj_decl output parameter that will contain the projection function declarations. This field must be a buffer of size num_fields allocated by the user.

TermPtr MkUnaryMinus ( TermPtr  arg  ) 

Create an AST node representing - arg.

The argument must have int or real type.

TermPtr MkXor ( TermPtr  t1,
TermPtr  t2 
)

Create an AST node representing t1 xor t2.

The nodes t1 and t2 must have Boolean type.

bool OpenLog ( String^  filename  ) 

Log assertions to a file.

See also:
CloseLog
Returns true if the open succeeds, otherwise false.

TermPtr ParseSimplifyFile ( String^  filename,
[Runtime::InteropServices::Out] String^%  parser_out 
)

Parse a file containing formulas in the Simplify format.

Return conjunction of Asserts occurring in the file.

TermPtr ParseSimplifyString ( String^  s,
[Runtime::InteropServices::Out] String^%  parser_out 
)

Parse a string in the simplify format.

Return conjunction of Asserts occurring in the string.

void ParseSmtlibFile ( String^  file,
[Runtime::InteropServices::In] array< SortPtr >^  sorts,
[Runtime::InteropServices::In] array< FuncDeclPtr >^  decls,
[Runtime::InteropServices::Out] array< TermPtr >^%  assumptions,
[Runtime::InteropServices::Out] array< TermPtr >^%  formulas,
[Runtime::InteropServices::Out] array< FuncDeclPtr >^%  new_decls,
[Runtime::InteropServices::Out] array< SortPtr >^%  new_sorts,
[Runtime::InteropServices::Out] String^%  parser_out 
)

Similar to ParseSmtlibString, but reads the benchmark from a file.

void ParseSmtlibString ( String^  string,
[Runtime::InteropServices::In] array< SortPtr >^  sorts,
[Runtime::InteropServices::In] array< FuncDeclPtr >^  decls,
[Runtime::InteropServices::Out] array< TermPtr >^%  assumptions,
[Runtime::InteropServices::Out] array< TermPtr >^%  formulas,
[Runtime::InteropServices::Out] array< FuncDeclPtr >^%  new_decls,
[Runtime::InteropServices::Out] array< SortPtr >^%  new_sorts,
[Runtime::InteropServices::Out] String^%  parser_out 
)

Parse the given string using the SMT-LIB parser.

The symbol table of the parser can be initialized using the given types and declarations. The symbols in the arrays type_names and decl_names don't need to match the names of the types and declarations in the arrays types and decls. This is an useful feature since we can use arbitrary names to reference types and declarations defined using the C API.

The formulas, assumptions and declarations defined in str.

Parameters:
string The string contianing the SMT-LIB benchmark
sorts List of auxiliary sorts used in SMT-LIB benchmark.
decls List of declarations to be used for parsing the SMT-LIB string.
assumptions Returned set of assumptions.
formulas Returned set of formulas.
new_decls Additional declarations from the SMT-LIB benchmark.
new_sorts Additional sorts fromt he SMT-LIB benchmark.
parser_out String containing error messages from parsing.

TermPtr ParseZ3File ( String^  filename  ) 

Parse a file containing formulas in the Simplify format.

Return conjunction of Asserts occurring in the file.

TermPtr ParseZ3String ( String^  s  ) 

Parse a string in the native Z3 format.

Return conjunction of Asserts occurring in the string.

void PersistTerm ( TermPtr  t,
unsigned  num_scopes 
)

Persist a term during num_scopes of pops.

Normally, references to terms are no longer valid when popping scopes beyond the level where the terms are created. If you want to reference a term below the scope where it was created, use this method to specify how many pops the term should survive. The current scope level is given as the current total number of calls to push subtracted by the total number of calls to pop. If num_scopes is larger or equal to the current scope level, then the term pointer persists throughout the life-time of the context.

Example usage:

context.Push(); context.Push(); Term t = context.MkNumeral(1, context.MkIntSort()); context.PersistTerm(t, 1); context.Pop(); reference to t is valid. context.Pop(); reference to t is not valid.

void Pop ( unsigned  num_scopes  ) 

Backtrack.

Restores the context from the top of the stack, and pops it off the stack. Any changes to the logical context (by AssertCnstr or other functions) between the matching Push and Pop operators are flushed, and the context is completely restored to what it was right before the Push.

Parameters:
num_scopes number of scopes to pop. Default value is 1.
See also:
Push

PersistTerm

void Push (  ) 

Create a backtracking point.

The logical context can be viewed as a stack of contexts. The scope level is the number of elements on this stack. The stack of contexts is simulated using trail (undo) stacks.

See also:
Pop

PersistTerm

static void ResetMemory (  )  [static]

Free all resources allocated for Z3.

static void SetErrorHandler ( IErrorHandler^  h  )  [static]

Register a Z3 error handler.

A call to a Z3 function throw Z3Error when it is not used correctly. An error handler can be registered and will be called in this case prior to throwing Z3Error.

void SetPrintMode ( PrintMode  mode  ) 

Select mode for the format used for pretty-printing AST nodes.

The default mode for pretty printing AST nodes is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called PrintMode.SmtlibFull. To print shared common subexpressions only once, use the PrintMode.LowLevel mode.

TermPtr Simplify ( TermPtr  a  ) 

Interface to simplifier.

Provides an interface to the AST simplifier used by Z3. It allows clients to piggyback on top of the AST simplifier for their own term manipulation.

String StatisticsToString (  )  [inline]

Convert the given logical context into a string.

This function is mainly used for debugging purposes. It displays the internal structure of a logical context.

Definition at line 2590 of file Microsoft.Z3.h.

02590                                      {
02591             return gcnew String(Z3_statistics_to_string(m_context));
02592         }

void ToggleWarningMessages ( bool  enabled  ) 

Enable or disable warning messages sent to the console out/error.

Warnings are printed after passing true, warning messages are suppressed after calling this method with false.

virtual String ToString (  )  [override, virtual]

Convert the given logical context into a string.

This function is mainly used for debugging purposes. It displays the internal structure of a logical context.

String ToString ( AstPtr  a  ) 

Convert the given AST node into a string.

void TraceOff (  ) 

Disable trace messages.

See also:
TraceToFile

TraceToStdOut

TraceToStdErr

bool TraceToFile ( String^  trace_file  ) 

Enable trace messages to a file.

When trace messages are enabled, Z3 will record the operations performed on a context in the given file file.

Return true if the file was opened successfully, and false otherwise.

See also:
TraceOff

void TraceToStdErr (  ) 

Enable trace messages to a standard error.

See also:
TraceOff

void TraceToStdOut (  ) 

Enable trace messages to a standard output.

See also:
TraceOff

bool TryGetArrayValue ( TermPtr  a,
[Runtime::InteropServices::Out] RawArrayValue^%  av 
)

Return decomposed sequence of stores as an array value.

Last modified Thu Nov 12 16:35:57 2009