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.

	OnClause (Solver s, OnClauseEh onc)
	OnClause constructor.

virtual void	Dispose ()
	Must be called. The object will not be garbage collected automatically even if the context is disposed.

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.