An Efficient SMT Solver| Home | • | Docs | • | Download | • | • | FAQ | • | Awards | • | Status | • | MSR |
|---|
An Efficient SMT Solver
Public Member Functions | |
| array< ConstDeclAstPtr > | GetModelConstants () |
| Return the constants assigned by the given model. | |
| ValuePtr | GetValue (ConstDeclAstPtr decl) |
| Return the value of the given constant or application in the given model. | |
| TypeAstPtr | GetValueType (ValuePtr v) |
| Return the value type. | |
| ValueKind | GetValueKind (ValuePtr v) |
| Return the value kind (numeral, array, tuple, etc). | |
| String | GetNumeralValueString (ValuePtr v) |
| Return a numeral value as a string. The representation is stored in decimal notation. | |
| int | GetNumeralValueInt (ValuePtr v) |
| Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine int. Throw InvalidArgument if the call fails. | |
| unsigned int | GetNumeralValueUInt (ValuePtr v) |
| Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine unsigned int. Throw InvalidArgument if the call fails. | |
| unsigned __int64 | GetNumeralValueUInt64 (ValuePtr v) |
| Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine unsigned long long int. Throw InvalidArgument if the call fails. | |
| __int64 | GetNumeralValueInt64 (ValuePtr v) |
| Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine long long int. Throw InvalidArgument if the call fails. | |
| bool | GetBoolValueBool (ValuePtr v) |
Return the value of v as a Boolean value. | |
| TupleValue | GetTupleValue (ValuePtr v) |
| Return the elements of a tuple value. | |
| ArrayValue | GetArrayValue (ValuePtr v) |
| An array values is represented as a dictionary plus a default (else) value. This function returns a value encapsulating these values. | |
| Dictionary < ConstDeclAstPtr, FunctionGraph^> | GetFunctionGraphs () |
| Return the function interpretations in the given model. | |
| ValuePtr | Eval (TermAstPtr) |
Evaluate the AST node t in the given model. | |
| bool | IsEq (ValuePtr v1, ValuePtr v2) |
| Check whether two values are the same. | |
| unsigned | GetValueHash (ValuePtr v) |
| Retrieve hash of value. | |
| virtual String | ToString () override |
| Convert the given model into a string. | |
| void | Display (System::IO::TextWriter^w) |
| Display model to TextWriter. | |
| String | ToString (ValuePtr v) |
| Convert the given (model) value into a string. | |
| void | Display (System::IO::TextWriter^w, ValuePtr v) |
| Display model value to TextWriter. | |
Data Fields | |
| Z3_context | m_context |
| Z3_model | m_model |
|
Dictionary < ConstDeclAstPtr, FunctionGraph^> | m_graphs |
Package Functions | |
| Model (Z3_context c, Z3_model m) | |
Definition at line 491 of file Microsoft.Z3.h.
| array<ConstDeclAstPtr> GetModelConstants | ( | ) |
| ValuePtr GetValue | ( | ConstDeclAstPtr | decl | ) |
Return the value of the given constant or application in the given model.
Referenced by TypeSafeModel::GetValue().
| TypeAstPtr GetValueType | ( | ValuePtr | v | ) |
| ValueKind GetValueKind | ( | ValuePtr | v | ) |
Return the value kind (numeral, array, tuple, etc).
ValueKind.Numeral stores the value of different types (int, real, bv, and uninterpreted).
Referenced by TypeSafeModel::GetValueKind().
| String GetNumeralValueString | ( | ValuePtr | v | ) |
Return a numeral value as a string. The representation is stored in decimal notation.
Referenced by TypeSafeModel::GetNumeralValueString().
| int GetNumeralValueInt | ( | ValuePtr | v | ) |
Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine int. Throw InvalidArgument if the call fails.
Referenced by TypeSafeModel::GetNumeralValueInt(), and TypeSafeModel::GetNumeralValueUInt().
| unsigned int GetNumeralValueUInt | ( | ValuePtr | v | ) |
Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine unsigned int. Throw InvalidArgument if the call fails.
Referenced by TypeSafeModel::GetNumeralValueUInt().
| unsigned __int64 GetNumeralValueUInt64 | ( | ValuePtr | v | ) |
Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine unsigned long long int. Throw InvalidArgument if the call fails.
Referenced by TypeSafeModel::GetNumeralValueUInt64().
| __int64 GetNumeralValueInt64 | ( | ValuePtr | v | ) |
Similar to GetNumeralValueString, but only succeeds if the value can fit in a machine long long int. Throw InvalidArgument if the call fails.
Referenced by TypeSafeModel::GetNumeralValueInt64().
| bool GetBoolValueBool | ( | ValuePtr | v | ) |
Return the value of v as a Boolean value.
Referenced by TypeSafeModel::GetBoolValueBool().
| TupleValue GetTupleValue | ( | ValuePtr | v | ) |
Return the elements of a tuple value.
Referenced by TypeSafeModel::GetTupleValue().
| ArrayValue GetArrayValue | ( | ValuePtr | v | ) |
An array values is represented as a dictionary plus a default (else) value. This function returns a value encapsulating these values.
Referenced by TypeSafeModel::GetArrayValue().
| Dictionary<ConstDeclAstPtr, FunctionGraph^> GetFunctionGraphs | ( | ) |
Return the function interpretations in the given model.
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.
Referenced by TypeSafeModel::GetFunctionGraphs().
| ValuePtr Eval | ( | TermAstPtr | ) |
Evaluate the AST node t in the given model.
Return the result as a non-zero value. The returned value is null if the term does not evaluate to a fixed value in the current model. term to a value.
The evaluation may fail for the following reasons:
t contains a quantifier or bound variable.
m is partial, that is, it doesn't have a complete interpretation for free functions. That is, the option PARTIAL_MODELS=true was used.
t is type incorrect (see TypeCheck).
t is undefined (e.g. division by zero). Referenced by TypeSafeModel::Eval().
| bool IsEq | ( | ValuePtr | v1, | |
| ValuePtr | v2 | |||
| ) |
| unsigned GetValueHash | ( | ValuePtr | v | ) |
| virtual String ToString | ( | ) | [override, virtual] |
| void Display | ( | System::IO::TextWriter^ | w | ) |
Display model to TextWriter.
Referenced by TypeSafeModel::Display(), TestManaged::eval_example1(), and TestManaged::eval_example2().
| String ToString | ( | ValuePtr | v | ) |
Convert the given (model) value into a string.
| void Display | ( | System::IO::TextWriter^ | w, | |
| ValuePtr | v | |||
| ) |
Display model value to TextWriter.
Last modified Wed Sep 3 08:54:20 2008