RawModel Class Reference
[Managed (.NET) API]

Z3 RawModel object. More...

Public Member Functions
array< FuncDeclPtr >	GetModelConstants ()
	Return the constants assigned by the given model.
Dictionary< FuncDeclPtr, RawFunctionGraph^>	GetFunctionGraphs ()
	Return the function interpretations in the given model.
TermPtr	Eval (TermPtr)
	Evaluate the AST node t in the given model.
virtual String	ToString () override
	Convert the given model into a string.
void	Display (System::IO::TextWriter^w)
	Display model to TextWriter.

---

Detailed Description

Z3 RawModel object.

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

---

Member Function Documentation

void Display

(

System::IO::TextWriter^

w

)

Display model to TextWriter.

TermPtr Eval

(

TermPtr

)

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.

• the model m is partial, that is, it doesn't have a complete interpretation for free functions. That is, the option PARTIAL_MODELS=true was used.

• the evaluator doesn't have support for some interpreted operator.

• t is type incorrect (see TypeCheck).

• The result of an intepreted operator in t is undefined (e.g. division by zero).

Dictionary<FuncDeclPtr, RawFunctionGraph^> 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.

array<FuncDeclPtr> GetModelConstants

(

)

Return the constants assigned by the given model.

virtual String ToString

(

)

[override, virtual]

Convert the given model into a string.