OnClause Class Reference

Inheritance diagram for OnClause:

Public Member Functions
	OnClause (Context ctx, Solver solver)
void	onClause (Expr<?> proof_hint, int[] deps, ASTVector literals)
void	close ()

Detailed Description

Clause inference callback.

Allows users to observe clauses learned during solving. Useful for custom learning strategies, clause sharing in parallel solvers, debugging, and proof extraction.

Usage: create an instance, override onClause(Expr, int[], ASTVector), and close the instance when done.

Definition at line 34 of file OnClause.java.

Constructor & Destructor Documentation

OnClause()

OnClause ( Context  ctx, Solver  solver  )

inline

Creates an on-clause callback for the given solver.

Parameters

ctx	The Z3 context
solver	The solver to register the callback with

Exceptions

Z3Exception

Definition at line 46 of file OnClause.java.

                                                {
        this.ctx = ctx;
        javainfo = Native.onClauseInit(this, ctx.nCtx(), solver.getNativeObject());
    }

Member Function Documentation

close()

void close ( )

inline

Unregisters the callback and frees associated resources. Must be called when the callback is no longer needed.

Definition at line 79 of file OnClause.java.

                        {
        if (javainfo != 0) {
            Native.onClauseDestroy(javainfo);
            javainfo = 0;
        }
    }

onClause()

void onClause ( Expr<?>  proof_hint, int[]  deps, ASTVector  literals  )

inline

Called when a clause is inferred during solving.

The life-time of proof_hint and literals is limited to the scope of this callback. If you want to store them, you must duplicate the expressions or extract the literals before returning.

Parameters

proof_hint	A partial or comprehensive derivation justifying the inference (may be null)
deps	Dependency indices
literals	The inferred clause as a vector of literals

Definition at line 63 of file OnClause.java.

{}