Probe Class Reference

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 Context.NumProbes and Context.ProbeNames. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. More...

Inheritance diagram for Probe:

Data Structures
class	DecRefQueue

Public Member Functions
double	Apply (Goal g)
	Execute the probe over the goal. More...
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
double	this[Goal g] [get]
	Apply the probe to a goal. More...

Detailed Description

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 Context.NumProbes and Context.ProbeNames. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end.

Definition at line 33 of file Probe.cs.

Member Function Documentation

Apply()

double Apply ( Goal  g )

inline

Execute the probe over the goal.

Returns

A probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.

Definition at line 40 of file Probe.cs.

        {
            Debug.Assert(g != null);
 
            Context.CheckContextMatch(g);
            return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
        }

Property Documentation

this[Goal g]

double this[Goal g]

get

Apply the probe to a goal.

Definition at line 52 of file Probe.cs.

        {
            get
            {
                Debug.Assert(g != null);
 
                return Apply(g);
            }
        }