An Efficient SMT Solver| Home | • | Docs | • | Download | • | • | FAQ | • | Awards | • | Status | • | MSR |
|---|
An Efficient SMT Solver
Binary relations | |
| void | EnableBinaryRelations () |
| Enable theory of binary relations. | |
| ConstDeclAstPtr | MkBinaryRelation (String^name, TypeAstPtr domain, RelationProperty p) |
| Create binary relation. | |
| ConstDeclAstPtr | MkBinaryRelation (Symbol^name, TypeAstPtr domain, RelationProperty p) |
Public Member Functions | |
| Context (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 | Log (String^filename) |
| Log assertions to a file. | |
| void | CloseLog () |
| Close file with logged assertions. | |
| void | ToggleWarningMessages (bool enabled) |
| Enable or disable warning messages sent to the console out/error. | |
Theories | |
| void | EnableArithmetic () |
| Enable arithmetic theory in the given logical context. | |
| void | EnableBv () |
| Enable bit-vector theory in the given logical context. | |
| void | EnableArrays () |
| Enable array theory in the given logical context. | |
| void | EnableTuples () |
| Enable tuple theory in the given logical context. | |
Symbols | |
| Symbol | MkSymbol (int i) |
| Create a Z3 symbol using an intege or a string. | |
| Symbol | MkSymbol (String^s) |
Types | |
| TypeAstPtr | MkType (Symbol^s) |
| Create a free (uninterpreted) type using the given name (symbol). | |
| TypeAstPtr | MkType (String^s) |
| TypeAstPtr | MkType (int i) |
| TypeAstPtr | MkBoolType () |
| Create the boolean type. | |
| TypeAstPtr | MkIntType () |
| Create an integer type. | |
| TypeAstPtr | MkRealType () |
| Create a real type. | |
| TypeAstPtr | MkBvType (unsigned sz) |
| Create a bit-vector type of the given size. | |
| TypeAstPtr | MkArrayType (TypeAstPtr domain, TypeAstPtr range) |
| Create an array type. | |
| TypeAstPtr | MkTupleType (Symbol^mk_tuple_name, array< Symbol^>^field_names, array< TypeAstPtr >^field_types, ConstDeclAstPtr%mk_tuple_decl, array< ConstDeclAstPtr >^proj_decl) |
| Create a tuple type. | |
| TypeAstPtr | MkTupleType (String^mk_tuple_name, array< String^>^field_names, array< TypeAstPtr >^field_types, ConstDeclAstPtr%mk_tuple_decl, array< ConstDeclAstPtr >^proj_decl) |
Constants and Applications | |
| ConstDeclAstPtr | MkFuncDecl (Symbol^s, array< TypeAstPtr >^domain, TypeAstPtr range) |
| Declare a constant or function. | |
| ConstDeclAstPtr | MkFuncDecl (String^s, array< TypeAstPtr >^domain, TypeAstPtr range) |
| ConstDeclAstPtr | MkConstDecl (Symbol^s, TypeAstPtr ty) |
| ConstDeclAstPtr | MkFuncDecl (Symbol^s, TypeAstPtr domain, TypeAstPtr range) |
| ConstDeclAstPtr | MkFuncDecl (Symbol^s, TypeAstPtr d1, TypeAstPtr d2, TypeAstPtr range) |
| ConstDeclAstPtr | MkConstDecl (String^s, TypeAstPtr ty) |
| ConstDeclAstPtr | MkFuncDecl (String^s, TypeAstPtr domain, TypeAstPtr range) |
| ConstDeclAstPtr | MkFuncDecl (String^s, TypeAstPtr d1, TypeAstPtr d2, TypeAstPtr range) |
| ConstAstPtr | MkApp (ConstDeclAstPtr d, array< TermAstPtr >^args) |
| Create a constant or function application. | |
| ConstAstPtr | MkApp (ConstDeclAstPtr d, TermAstPtr arg) |
| ConstAstPtr | MkApp (ConstDeclAstPtr d, TermAstPtr arg1, TermAstPtr arg2) |
| ConstAstPtr | MkApp (ConstDeclAstPtr d, TermAstPtr arg1, TermAstPtr arg2, TermAstPtr arg3) |
| ConstAstPtr | MkConst (ConstDeclAstPtr d) |
| Declare and create a constant. | |
| ConstAstPtr | MkConst (String^s, TypeAstPtr ty) |
| ConstAstPtr | MkConst (Symbol^s, TypeAstPtr ty) |
| ConstDeclAstPtr | MkFreshFuncDecl (String^prefix, array< TypeAstPtr >^domain, TypeAstPtr range) |
| Declare a fresh constant or function. | |
| TermAstPtr | MkFreshConst (String^prefix, TypeAstPtr ty) |
| Declare and create a fresh constant. | |
| TermAstPtr | MkLabel (Symbol^name, bool pos, TermAstPtr fml) |
| TermAstPtr | MkTrue () |
Create an AST node representing true. | |
| TermAstPtr | MkFalse () |
Create an AST node representing false. | |
| TermAstPtr | MkEq (TermAstPtr l, TermAstPtr r) |
Create an AST node representing l = r. | |
| TermAstPtr | MkDistinct (array< TermAstPtr >^args) |
Create an AST node representing distinct(args[0], ..., args[args.Length-1]). | |
| virtual TermAstPtr | MkNot (TermAstPtr arg) |
Create an AST node representing not(a). | |
| TermAstPtr | MkIte (TermAstPtr t1, TermAstPtr t2, TermAstPtr t3) |
Create an AST node representing an if-then-else: ite(t1, t2, t3). | |
| TermAstPtr | MkIff (TermAstPtr t1, TermAstPtr t2) |
Create an AST node representing t1 iff t2. | |
| TermAstPtr | MkImplies (TermAstPtr t1, TermAstPtr t2) |
Create an AST node representing t1 implies t2. | |
| TermAstPtr | MkXor (TermAstPtr t1, TermAstPtr t2) |
Create an AST node representing t1 xor t2. | |
| TermAstPtr | MkAnd (array< TermAstPtr >^args) |
Create an AST node representing args[0] and ... and args[args.Length-1]. | |
| TermAstPtr | MkAnd (TermAstPtr arg1, TermAstPtr arg2) |
| TermAstPtr | MkOr (array< TermAstPtr >^args) |
Create an AST node representing args[0] or ... or args[args.Length-1]. | |
| TermAstPtr | MkOr (TermAstPtr arg1, TermAstPtr arg2) |
| TermAstPtr | MkAdd (array< TermAstPtr >^args) |
Create an AST node representing args[0] + ... + args[args.Length-1]. | |
| TermAstPtr | MkAdd (TermAstPtr arg1, TermAstPtr arg2) |
| TermAstPtr | MkMul (array< TermAstPtr >^args) |
Create an AST node representing args[0] * ... * args[args.Length-1]. | |
| TermAstPtr | MkMul (TermAstPtr arg1, TermAstPtr arg2) |
| TermAstPtr | MkSub (array< TermAstPtr >^args) |
Create an AST node representing args[0] - ... - args[args.Length - 1]. | |
| TermAstPtr | MkSub (TermAstPtr arg1, TermAstPtr arg2) |
| TermAstPtr | MkUnaryMinus (TermAstPtr arg) |
Create an AST node representing - arg. | |
| TermAstPtr | MkDiv (TermAstPtr arg1, TermAstPtr arg2) |
| Create integer or real division. | |
| TermAstPtr | MkMod (TermAstPtr arg1, TermAstPtr arg2) |
| Create integer modulus. | |
| TermAstPtr | MkRem (TermAstPtr arg1, TermAstPtr arg2) |
| Create integer remainder. | |
| TermAstPtr | MkLt (TermAstPtr arg1, TermAstPtr arg2) |
| Create less than. | |
| TermAstPtr | MkLe (TermAstPtr arg1, TermAstPtr arg2) |
| Create less than or equal to. | |
| TermAstPtr | MkGt (TermAstPtr arg1, TermAstPtr arg2) |
| Create greater than. | |
| TermAstPtr | MkGe (TermAstPtr arg1, TermAstPtr arg2) |
| Create greater than or equal to. | |
| TermAstPtr | MkBvNot (TermAstPtr t1) |
| Bitwise negation. | |
| TermAstPtr | MkBvAnd (TermAstPtr t1, TermAstPtr t2) |
| Bitwise and. | |
| TermAstPtr | MkBvOr (TermAstPtr t1, TermAstPtr t2) |
| Bitwise or. | |
| TermAstPtr | MkBvXor (TermAstPtr t1, TermAstPtr t2) |
| Bitwise exclusive-or. | |
| TermAstPtr | MkBvNand (TermAstPtr t1, TermAstPtr t2) |
| Bitwise nand. | |
| TermAstPtr | MkBvNor (TermAstPtr t1, TermAstPtr t2) |
| Bitwise nor. | |
| TermAstPtr | MkBvXnor (TermAstPtr t1, TermAstPtr t2) |
| Bitwise xnor. | |
| TermAstPtr | MkBvNeg (TermAstPtr t1) |
| Standard two's complement unary minus. | |
| TermAstPtr | MkBvAdd (TermAstPtr t1, TermAstPtr t2) |
| Standard two's complement addition. | |
| TermAstPtr | MkBvSub (TermAstPtr t1, TermAstPtr t2) |
| Standard two's complement subtraction. | |
| TermAstPtr | MkBvMul (TermAstPtr t1, TermAstPtr t2) |
| Standard two's complement multiplication. | |
| TermAstPtr | MkBvUdiv (TermAstPtr t1, TermAstPtr t2) |
| Unsigned division. | |
| TermAstPtr | MkBvSdiv (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed division. | |
| TermAstPtr | MkBvUrem (TermAstPtr t1, TermAstPtr t2) |
| Unsigned remainder. | |
| TermAstPtr | MkBvSrem (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed remainder (sign follows dividend). | |
| TermAstPtr | MkBvSmod (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed remainder (sign follows divisor). | |
| TermAstPtr | MkBvUlt (TermAstPtr t1, TermAstPtr t2) |
| Unsigned less than. | |
| TermAstPtr | MkBvSlt (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed less than. | |
| TermAstPtr | MkBvUle (TermAstPtr t1, TermAstPtr t2) |
| Unsigned less than or equal to. | |
| TermAstPtr | MkBvSle (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed less than or equal to. | |
| TermAstPtr | MkBvUge (TermAstPtr t1, TermAstPtr t2) |
| Unsigned greater than or equal to. | |
| TermAstPtr | MkBvSge (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed greater than or equal to. | |
| TermAstPtr | MkBvUgt (TermAstPtr t1, TermAstPtr t2) |
| Unsigned greater than. | |
| TermAstPtr | MkBvSgt (TermAstPtr t1, TermAstPtr t2) |
| Two's complement signed greater than. | |
| TermAstPtr | MkBvConcat (TermAstPtr t1, TermAstPtr t2) |
| Concatenate the given bit-vectors. | |
| TermAstPtr | MkBvExtract (unsigned high, unsigned low, TermAstPtr 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. | |
| TermAstPtr | MkBvSignExt (unsigned i, TermAstPtr 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. | |
| TermAstPtr | MkBvZeroExt (unsigned i, TermAstPtr 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. | |
| TermAstPtr | MkBvShl (TermAstPtr t1, TermAstPtr t2) |
| Shift left. | |
| TermAstPtr | MkBvLshr (TermAstPtr t1, TermAstPtr t2) |
| Logical shift right. | |
| TermAstPtr | MkBvAshr (TermAstPtr t1, TermAstPtr t2) |
| Arithmetic shift right. | |
| TermAstPtr | MkBvRotateLeft (unsigned i, TermAstPtr t1) |
Rotate bits of t1 to the left i times. | |
| TermAstPtr | MkBvRotateRight (unsigned i, TermAstPtr t1) |
Rotate bits of t1 to the right i times. | |
| TermAstPtr | MkArraySelect (TermAstPtr a, TermAstPtr i) |
| Array read. | |
| TermAstPtr | MkArrayStore (TermAstPtr a, TermAstPtr i, TermAstPtr v) |
| Array update. | |
| TermAstPtr | MkArrayConst (TypeAstPtr domain, TermAstPtr v) |
| Constant array. | |
| TermAstPtr | MkArrayDefault (TermAstPtr a) |
| Access the array default. | |
Sets | |
| void | EnableSets () |
| Enable set theory. | |
| TypeAstPtr | MkSetType (TypeAstPtr ty) |
| Create Set type. | |
| TermAstPtr | MkEmptySet (TypeAstPtr ty) |
| Create the empty set. | |
| TermAstPtr | MkFullSet (TypeAstPtr ty) |
| Create the full set. | |
| TermAstPtr | MkSetAdd (TermAstPtr set, TermAstPtr elem) |
| Add an element to a set. | |
| TermAstPtr | MkSetDel (TermAstPtr set, TermAstPtr elem) |
| Remove an element to a set. | |
| TermAstPtr | MkSetUnion (array< TermAstPtr >^sets) |
| Take the union of a arrays of sets. | |
| TermAstPtr | MkSetUnion (TermAstPtr set1, TermAstPtr set2) |
| TermAstPtr | MkSetIntersect (array< TermAstPtr >^sets) |
| Take the intersection of a arrays of sets. | |
| TermAstPtr | MkSetIntersect (TermAstPtr set1, TermAstPtr set2) |
| TermAstPtr | MkSetDifference (TermAstPtr arg1, TermAstPtr arg2) |
| Take the set difference between two sets. | |
| TermAstPtr | MkSetComplement (TermAstPtr arg) |
| Take the complement of a set. | |
| TermAstPtr | MkSetMember (TermAstPtr elem, TermAstPtr set) |
| Check for set membership. | |
| TermAstPtr | MkSetSubset (TermAstPtr arg1, TermAstPtr arg2) |
| Check for subsetness of sets. | |
Marbles | |
| void | EnableMarbles () |
| Enable marble theory. | |
| TypeAstPtr | MkMarbleType (String^name) |
| Create marble type. | |
| TermAstPtr | MkColoredMarble (String^name, unsigned partition, TypeAstPtr ty) |
| Create a marble that is pinned to a partition. | |
Injective functions | |
| void | EnableInjectiveFunctions () |
| Enable theory of injective functions. | |
| ConstDeclAstPtr | MkInjectiveFunction (String^name, array< TypeAstPtr >^domain, TypeAstPtr range) |
| Create injective function. | |
| ConstDeclAstPtr | MkInjectiveFunction (Symbol^name, array< TypeAstPtr >^domain, TypeAstPtr range) |
Numerals | |
| TermAstPtr | MkNumeral (String^numeral, TypeAstPtr ty) |
| Create a numeral of a given type. | |
| TermAstPtr | MkNumeral (int n, TypeAstPtr ty) |
| TermAstPtr | MkNumeral (unsigned n, TypeAstPtr ty) |
| TermAstPtr | MkNumeral (__int64 n, TypeAstPtr ty) |
| TermAstPtr | MkNumeral (unsigned __int64 n, TypeAstPtr ty) |
Quantifiers | |
| PatternAstPtr | MkPattern (array< TermAstPtr >^terms) |
| Create a pattern for quantifier instantiation. | |
| TermAstPtr | MkBound (unsigned index, TypeAstPtr ty) |
| Create a bound variable. | |
| TermAstPtr | MkForall (unsigned weight, array< PatternAstPtr >^patterns, array< TypeAstPtr >^types, array< Symbol^>^names, TermAstPtr body) |
| Create a forall formula. | |
| TermAstPtr | MkForall (unsigned weight, array< PatternAstPtr >^patterns, array< TypeAstPtr >^types, array< String^>^names, TermAstPtr body) |
| Create a forall formula. | |
| TermAstPtr | MkForall (unsigned weight, array< ConstAstPtr >^bound, array< PatternAstPtr >^patterns, TermAstPtr body) |
| Create a forall formula. | |
| TermAstPtr | MkExists (unsigned weight, array< PatternAstPtr >^patterns, array< TypeAstPtr >^types, array< Symbol^>^names, TermAstPtr body) |
| Create an exists formula. Similar to MkForall. | |
| TermAstPtr | MkExists (unsigned weight, array< PatternAstPtr >^patterns, array< TypeAstPtr >^types, array< String^>^names, TermAstPtr body) |
| TermAstPtr | MkExists (unsigned weight, array< ConstAstPtr >^bound, array< PatternAstPtr >^patterns, TermAstPtr body) |
| TermAstPtr | MkQuantifier (bool is_forall, unsigned weight, array< PatternAstPtr >^patterns, array< TermAstPtr >^no_patterns, array< TypeAstPtr >^types, array< Symbol^>^names, TermAstPtr 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 (TermAstPtr t1, TermAstPtr t2) |
Return true if the two given AST nodes are equal. | |
| AstKind | GetAstKind (TermAstPtr a) |
| Return the kind of the given AST. | |
| DeclKind | GetDeclKind (ConstDeclAstPtr d) |
| Return the kind of the built-in operator. | |
| ConstDeclAstPtr | GetConstAstDecl (ConstAstPtr a) |
| Return the declaration of a constant or function application. | |
| array< TermAstPtr > | GetConstAstArgs (ConstAstPtr a) |
Return the arguments of an application. If t is an constant, then array is empty. | |
| String | GetNumeralAstValue (TermAstPtr a) |
| Return the number of a numeric ast. | |
| unsigned | GetVarIndex (TermAstPtr a) |
| Return the index of a de-Brujin bound variable. | |
| QuantifierPtr | GetQuantifier (TermAstPtr a) |
| Return components of a quantifier. | |
| array< TermAstPtr > | GetPatternTerms (PatternAstPtr p) |
| Return array of terms in the pattern. | |
| Symbol | GetDeclName (ConstDeclAstPtr d) |
| Return the constant declaration name as a symbol. | |
| Symbol | GetTypeName (TypeAstPtr ty) |
| Return the type name as a symbol. | |
| TypeAstPtr | GetType (TermAstPtr a) |
| Return the type of an AST node. | |
| array< TypeAstPtr > | GetDomain (ConstDeclAstPtr d) |
| Return the domain of a function declaration. | |
| TypeAstPtr | GetRange (ConstDeclAstPtr d) |
| Return the range of the given declaration. | |
| TypeKind | GetTypeKind (TypeAstPtr t) |
| Return the type kind (e.g., array, tuple, int, bool, etc). | |
| unsigned | GetBvTypeSize (TypeAstPtr t) |
| Return the size of the given bit-vector type. | |
| TypeAstPtr | GetArrayTypeDomain (TypeAstPtr t) |
| Return the domain of the given array type. | |
| TypeAstPtr | GetArrayTypeRange (TypeAstPtr t) |
| Return the range of the given array type. | |
| ConstDeclAstPtr | GetTupleConstructor (TypeAstPtr t) |
| Return the constructor declaration of the given tuple type. | |
| array< ConstDeclAstPtr > | GetTupleFields (TypeAstPtr 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 | AssertCnstr (TermAstPtr a) |
| Assert a constraing into the logical context. | |
| LBool | CheckAndGetModel (Model^%m) |
| Check whether the given logical context is consistent or not. | |
| LBool | Check () |
| Check whether the given logical context is consistent or not. | |
| LabeledLiterals | GetRelevantLabels () |
| Retrieve set of labels set in current satisfying assignment. | |
| void | BlockLabels (LabeledLiterals^labels) |
| Block the combination of remaining non-disabled labels. | |
| TermAstPtr | Simplify (TermAstPtr a) |
| Interface to simplifier. | |
Timers | |
| void | SetSoftTimeout (unsigned t) |
| Set a soft timeout in seconds. | |
| void | ResetSoftTimeout () |
| Disable soft timeouts. | |
| bool | CheckSoftTimeout () |
| Check timeout. | |
String conversion | |
| 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) |
Parser interface | |
| void | ParseSmtlibString (String^string, array< TypeAstPtr >^types, array< ConstDeclAstPtr >^decls) |
| Parse the given string using the SMT-LIB parser. | |
| void | ParseSmtlibFile (String^file, array< TypeAstPtr >^types, array< ConstDeclAstPtr >^decls) |
| Similar to ParseSmtlibString, but reads the benchmark from a file. | |
| array< TermAstPtr > | GetSmtlibFormulas () |
| Return the SMTLIB formulas parsed by the last call to ParseSmtlibString or ParseSmtlibFile. | |
| array< TermAstPtr > | GetSmtlibAssumptions () |
| Return SMTLIB assumptions parsed by ParseSmtlibString or ParseSmtlibFile. | |
| array< ConstDeclAstPtr > | GetSmtlibDecls () |
| Return the declarations parsed by ParseSmtlibString or ParseSmtlibFile. | |
| TermAstPtr | ParseZ3String (String^s) |
| Parse a string in the native Z3 format. | |
| TermAstPtr | ParseZ3File (String^filename) |
| Parse a file containing formulas in the native Z3 format. | |
Miscellaneous | |
| void | GetVersion (unsigned%major, unsigned%minor, unsigned%build_number, unsigned%revision_number) |
| Return Z3 version number information. | |
| bool | TypeCheck (TermAstPtr t) |
Return true if t is type correct. | |
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. | |
Data Fields | |
| Z3_context | m_context |
Static Package Attributes | |
| static IErrorHandler | m_error_handler = nullptr |
Definition at line 696 of file Microsoft.Z3.h.
| bool TraceToFile | ( | String^ | trace_file | ) |
| void TraceToStdErr | ( | ) |
| void TraceToStdOut | ( | ) |
| void TraceOff | ( | ) |
| void EnableDebugTrace | ( | String^ | tag | ) |
Enable debug tracing of tagged log.
| bool Log | ( | String^ | filename | ) |
| void CloseLog | ( | ) |
| 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.
| void EnableArithmetic | ( | ) |
Enable arithmetic theory in the given logical context.
| void EnableBv | ( | ) |
Enable bit-vector theory in the given logical context.
| void EnableArrays | ( | ) |
Enable array theory in the given logical context.
| void EnableTuples | ( | ) |
Enable tuple theory in the given logical context.
| Symbol MkSymbol | ( | int | i | ) |
Create a Z3 symbol using an intege or a string.
Symbols are used to name several term and type constructors.
Referenced by TestManaged::assert_inj_axiom(), TestManaged::eval_example2(), and TestManaged::tuple_example().
| TypeAstPtr MkType | ( | 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.
Referenced by TestManaged::prove_example1().
| TypeAstPtr MkBoolType | ( | ) |
Create the boolean type.
This type is used to create propositional variables and predicates.
Referenced by TestManaged::array_example2(), and TestManaged::mk_bool_var().
| TypeAstPtr MkIntType | ( | ) |
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.
Referenced by TestManaged::mk_int_type().
| TypeAstPtr MkRealType | ( | ) |
Create a real type.
This type is not a floating point number. Z3 does not have support for floating point numbers yet.
| TypeAstPtr MkBvType | ( | unsigned | sz | ) |
Create a bit-vector type of the given size.
This type can also be seen as a machine integer.
Referenced by TestManaged::mk_bv_type().
| TypeAstPtr MkArrayType | ( | TypeAstPtr | domain, | |
| TypeAstPtr | 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.
MkConstArray
Referenced by TestManaged::array_example1(), and TestManaged::array_example2().
| TypeAstPtr MkTupleType | ( | Symbol^ | mk_tuple_name, | |
| array< Symbol^>^ | field_names, | |||
| array< TypeAstPtr >^ | field_types, | |||
| ConstDeclAstPtr% | mk_tuple_decl, | |||
| array< ConstDeclAstPtr >^ | 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.
| 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. |
Referenced by TestManaged::eval_example2(), and TestManaged::tuple_example().
| ConstDeclAstPtr MkFuncDecl | ( | Symbol^ | s, | |
| array< TypeAstPtr >^ | domain, | |||
| TypeAstPtr | range | |||
| ) |
Declare a constant or function.
| s | name of the constant or function. | |
| domain_size | number of arguments. It is 0 when declaring a constant. | |
| 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. |
Referenced by TestManaged::assert_inj_axiom(), TestManaged::assert_inj_axiom_abs(), Context::MkConstDecl(), TestManaged::prove_example1(), TestManaged::prove_example2(), TestManaged::quantifier_example1(), and TestManaged::quantifier_example1_abs().
| ConstAstPtr MkApp | ( | ConstDeclAstPtr | d, | |
| array< TermAstPtr >^ | args | |||
| ) |
Create a constant or function application.
Referenced by TestManaged::assert_inj_axiom(), TestManaged::assert_inj_axiom_abs(), TestManaged::eval_example2(), TestManaged::injective_example(), and TestManaged::tuple_example().
| ConstAstPtr MkConst | ( | ConstDeclAstPtr | d | ) |
Declare and create a constant.
Referenced by TestManaged::array_example2(), TestManaged::assert_inj_axiom_abs(), TestManaged::eval_example2(), TestManaged::injective_example(), TestManaged::mk_var(), TestManaged::prove_example1(), TestManaged::push_pop_example1(), and TestManaged::tuple_example().
| ConstDeclAstPtr MkFreshFuncDecl | ( | String^ | prefix, | |
| array< TypeAstPtr >^ | domain, | |||
| TypeAstPtr | range | |||
| ) |
Declare a fresh constant or function.
Z3 will generate an unique name for this function declaration.
| TermAstPtr MkFreshConst | ( | String^ | prefix, | |
| TypeAstPtr | ty | |||
| ) |
| TermAstPtr MkLabel | ( | Symbol^ | name, | |
| bool | pos, | |||
| TermAstPtr | fml | |||
| ) |
Create labeled formula.
| TermAstPtr MkTrue | ( | ) | [inline] |
Create an AST node representing true.
Definition at line 1018 of file Microsoft.Z3.h.
01018 { return TermAstPtr(Z3_mk_true(m_context)); }
| TermAstPtr MkFalse | ( | ) | [inline] |
Create an AST node representing false.
Definition at line 1024 of file Microsoft.Z3.h.
01024 { return TermAstPtr(Z3_mk_false(m_context)); }
| TermAstPtr MkEq | ( | TermAstPtr | l, | |
| TermAstPtr | r | |||
| ) |
Create an AST node representing l = r.
The nodes l and r must have the same type.
Referenced by TestManaged::array_example1(), TestManaged::assert_inj_axiom(), TestManaged::assert_inj_axiom_abs(), TestManaged::eval_example2(), TestManaged::find_model_example2(), TestManaged::injective_example(), TestManaged::prove_example1(), TestManaged::prove_example2(), TestManaged::quantifier_example1(), TestManaged::quantifier_example1_abs(), and TestManaged::tuple_example().