Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Data Structures | Public Member Functions | Properties
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-tactics) 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.
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object.
 

Properties

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

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-tactics) in the SMT 2.0 front-end.

Definition at line 34 of file Probe.cs.

Member Function Documentation

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 41 of file Probe.cs.

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

Property Documentation

double this[Goal g]
get

Apply the probe to a goal.

Definition at line 52 of file Probe.cs.