OnClause Class Reference

OnClause - clause inference callback More...

Inheritance diagram for OnClause:

Public Member Functions
delegate void	OnClauseEh (Expr proof_hint, ASTVector clause)
	Delegate type for when clauses are inferred. An inference is a pair comprising of More...
	OnClause (Solver s, OnClauseEh onc)
	OnClause constructor More...
virtual void	Dispose ()
	Must be called. The object will not be garbage collected automatically even if the context is disposed More...

Detailed Description

OnClause - clause inference callback

Definition at line 41 of file OnClause.cs.

Constructor & Destructor Documentation

OnClause()

OnClause ( Solver  s, OnClauseEh  onc  )

inline

OnClause constructor

Definition at line 75 of file OnClause.cs.

        {
            gch = GCHandle.Alloc(this);
            solver = s;
            ctx = solver.Context;
            on_clause = onc;
            on_clause_eh = _on_clause;
            Native.Z3_solver_register_on_clause(ctx.nCtx, solver.NativeObject, GCHandle.ToIntPtr(gch), on_clause_eh);
        }

Member Function Documentation

Dispose()

virtual void Dispose ( )

inlinevirtual

Must be called. The object will not be garbage collected automatically even if the context is disposed

Definition at line 96 of file OnClause.cs.

        {
            if (!gch.IsAllocated)
                return;
            gch.Free();
        }

OnClauseEh()

delegate void OnClauseEh	(	Expr	proof_hint,
		ASTVector	clause
	)

Delegate type for when clauses are inferred. An inference is a pair comprising of

• a proof (hint). A partial (or comprehensive) derivation justifying the inference.
• a clause (vector of literals) The life-time of the proof hint and clause vector is limited to the scope of the callback. should the callback want to store hints or clauses it will need to call Dup on the hints and/or extract literals from the clause, respectively.