OnClause.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
public class OnClause implements AutoCloseable {
 
    private long javainfo;
    private final Context ctx;
 
    public OnClause(Context ctx, Solver solver) {
        this.ctx = ctx;
        javainfo = Native.onClauseInit(this, ctx.nCtx(), solver.getNativeObject());
    }
 
    public void onClause(Expr<?> proof_hint, int[] deps, ASTVector literals) {}
 
    final void onClauseWrapper(long proofHintPtr, int[] deps, long literalsPtr) {
        Expr<?> proof_hint = proofHintPtr != 0 ? (Expr<?>) Expr.create(ctx, proofHintPtr) : null;
        ASTVector literals = new ASTVector(ctx, literalsPtr);
        onClause(proof_hint, deps, literals);
    }
 
    @Override
    public void close() {
        if (javainfo != 0) {
            Native.onClauseDestroy(javainfo);
            javainfo = 0;
        }
    }
}