Context Class Reference
[Managed (.NET) API]

Type safe contexts. More...

Public Member Functions
	Context (Config^config)
	Create a type safe version of a context.
	~Context ()
	Dispose method for type safe contexts.
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 out.
void	TraceOff ()
	Disable trace messages.
bool	OpenLog (String^filename)
	Log assertions to a file.
void	AppendLog (String^s)
	Append instruction or comment to log with assertion.
void	CloseLog ()
	Close file with logged assertions.
void	EnableDebugTrace (String^tag)
	Enable or disable warning messages sent to the console out/error.
String	BenchmarkToSmtlib (String^name, String^logic, String^status, String^attributes, array< Term^>^assumptions, Term^formula)
	Convert the given benchmark into SMT-LIB formatted string.
Sort	MkDataType (String^name, array< Constructor^>^constructors)
	create datatype sort.
array< Sort^>	MkDataTypes (array< String^>^names, array< array< Constructor^>^>^constructors)
	create datatype sort.
Symbols
Symbol	MkSymbol (int i)
Symbol	MkSymbol (String^s)
Constraints
void	Push ()
void	Pop (unsigned num_scopes)
void	Pop ()
void	PersistTerm (Term^t, unsigned num_scopes)
LBool	Check ()
LBool	CheckAndGetModel ([Runtime::InteropServices::Out] Model^%m)
LBool	CheckAssumptions ([Runtime::InteropServices::Out] Model^%m,[Runtime::InteropServices::In] array< Term^>^assumptions,[Runtime::InteropServices::Out] Term^%proof,[Runtime::InteropServices::Out] array< Term^>^%core)
LBool	GetImpliedEqualities ([Runtime::InteropServices::In] array< Term^>^terms,[Runtime::InteropServices::Out] array< unsigned >^%class_ids)
SearchFailureExplanation	GetSearchFailureExplanation ()
LabeledLiterals	GetRelevantLabels ()
LabeledLiterals	GetRelevantLiterals ()
LabeledLiterals	GetGuessedLiterals ()
void	BlockLiterals (LabeledLiterals^lbls)
Term	GetLiteral (LabeledLiterals^lbls, unsigned idx)
Term	Simplify (Term^a)
void	AssertCnstr (Term^a)

---

Detailed Description

Type safe contexts.

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

---

Constructor & Destructor Documentation

Context

(

Config^

config

)

[inline]

Create a type safe version of a context.

Terms and models created using the type safe context are wrapped within objects. The object wrappers prevent confusing the IntPtr type used for terms, sorts and values with arbitrary instances.

Each method in Context is paired with a corresponding method in Context.

See also:

Context.

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

: m_ctx(gcnew RawContext(config)) {}

~Context

(

)

[inline]

Dispose method for type safe contexts.

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

{ m_ctx->Reset(); }

---

Member Function Documentation

void AppendLog

(

String^

s

)

[inline]

Append instruction or comment to log with assertion.

See also:

OpenLog

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

{ m_ctx->AppendLog(s); }

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

Convert the given benchmark into SMT-LIB formatted string.

void CloseLog

(

)

[inline]

Close file with logged assertions.

See also:

OpenLog

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

{ m_ctx->CloseLog(); }

void EnableDebugTrace

(

String^

tag

)

[inline]

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.

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

{ m_ctx->EnableDebugTrace(tag); }

Sort MkDataType	(	String^	name,
		array< Constructor^>^	constructors
	)			[inline]

create datatype sort.

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

              {
            return gcnew Sort(m_ctx, m_ctx->MkDataType(name, constructors));
        }

array<Sort^> MkDataTypes	(	array< String^>^	names,
		array< array< Constructor^>^>^	constructors
	)			[inline]

create datatype sort.

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

              {
            return CopySortArray(m_ctx->MkDataTypes(names, constructors));
        }

bool OpenLog

(

String^

filename

)

[inline]

Log assertions to a file.

See also:

CloseLog

Returns true if the open succeeds, otherwise false.

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

Referenced by TestManaged::array_example2().

{ return m_ctx->OpenLog(filename); }

void TraceOff

(

)

[inline]

Disable trace messages.

See also:

TraceToFile

TraceToStdOut

TraceToStdErr

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

{ m_ctx->TraceOff(); }

bool TraceToFile

(

String^

trace_file

)

[inline]

Enable trace messages to a file.

See also:

TraceToFile

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

{ return m_ctx->TraceToFile(trace_file); }

void TraceToStdErr

(

)

[inline]

Enable trace messages to a standard error.

See also:

TraceToStdOut

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

{ m_ctx->TraceToStdErr(); }

void TraceToStdOut

(

)

[inline]

Enable trace messages to a standard out.

See also:

TraceToStdErr

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

{ m_ctx->TraceToStdOut(); }