mirror of
https://github.com/Z3Prover/z3
synced 2026-01-21 09:34:43 +00:00
a3d00ce356
* Reworked phantom reference handling. - Replaced IDecRefQueue with a new Z3ReferenceQueue class - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count. - Context now owns a single Z3ReferenceQueue for all types of references. * Made Statistics.Entry a static subclass * Made Context.close idempotent (as recommended) * Update CMakeLists.txt for building the Java API. * Updated CMakeLists.txt again. * Use correct SuppressWarning annotation to silence the compiler * Formatting
75 lines
1.8 KiB
Java
75 lines
1.8 KiB
Java
/**
|
|
Copyright (c) 2012-2014 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
Probe.java
|
|
|
|
Abstract:
|
|
|
|
Author:
|
|
|
|
@author Christoph Wintersteiger (cwinter) 2012-03-15
|
|
|
|
Notes:
|
|
|
|
**/
|
|
|
|
package com.microsoft.z3;
|
|
|
|
import java.lang.ref.ReferenceQueue;
|
|
|
|
/**
|
|
* Probes are used to inspect a goal (aka problem) and collect information that
|
|
* may be used to decide which solver and/or preprocessing step will be used.
|
|
* The complete list of probes may be obtained using the procedures
|
|
* {@code Context.NumProbes} and {@code Context.ProbeNames}. It may
|
|
* also be obtained using the command {@code (help-tactic)} in the SMT 2.0
|
|
* front-end.
|
|
**/
|
|
public class Probe extends Z3Object {
|
|
/**
|
|
* Execute the probe over the goal.
|
|
*
|
|
* @return A probe always produce a double value. "Boolean" probes return
|
|
* 0.0 for false, and a value different from 0.0 for true.
|
|
* @throws Z3Exception
|
|
**/
|
|
public double apply(Goal g)
|
|
{
|
|
getContext().checkContextMatch(g);
|
|
return Native.probeApply(getContext().nCtx(), getNativeObject(),
|
|
g.getNativeObject());
|
|
}
|
|
|
|
Probe(Context ctx, long obj)
|
|
{
|
|
super(ctx, obj);
|
|
}
|
|
|
|
Probe(Context ctx, String name) {
|
|
super(ctx, Native.mkProbe(ctx.nCtx(), name));
|
|
}
|
|
|
|
@Override
|
|
void incRef() {
|
|
Native.probeIncRef(getContext().nCtx(), getNativeObject());
|
|
}
|
|
|
|
@Override
|
|
void addToReferenceQueue() {
|
|
getContext().getReferenceQueue().storeReference(this, ProbeRef::new);
|
|
}
|
|
|
|
private static class ProbeRef extends Z3ReferenceQueue.Reference<Probe> {
|
|
|
|
private ProbeRef(Probe referent, ReferenceQueue<Z3Object> q) {
|
|
super(referent, q);
|
|
}
|
|
|
|
@Override
|
|
void decRef(Context ctx, long z3Obj) {
|
|
Native.probeDecRef(ctx.nCtx(), z3Obj);
|
|
}
|
|
}
|
|
}
|