#[non_exhaustive]pub struct Stats {Show 29 fields
pub mode: Option<&'static str>,
pub exit_reason: Option<&'static str>,
pub variables: Option<u32>,
pub clauses: Option<u64>,
pub vtree_spec: Option<String>,
pub vtree_candidate: Option<String>,
pub satisfiable: Option<bool>,
pub model_count: Option<String>,
pub weighted_count: Option<String>,
pub weighted_count_log10: Option<f64>,
pub weighted_count_sign: Option<i8>,
pub tdd_nodes: Option<u64>,
pub tdd_pairs: Option<u64>,
pub tdd_width: Option<u64>,
pub peak_pairs: Option<u64>,
pub answered_by: Option<&'static str>,
pub reduction: Option<&'static str>,
pub preprocess_ms: Option<u64>,
pub arjun_ms: Option<u64>,
pub vtree_ms: Option<u64>,
pub compile_ms: Option<u64>,
pub cascade_ms: Option<u64>,
pub backbone_ms: Option<u64>,
pub backbone_found: Option<u64>,
pub backbone_probes: Option<u64>,
pub show_vars: Option<u64>,
pub sat_prune: Option<&'static str>,
pub sat_prune_disabled_by: Option<&'static str>,
pub sat_prune_tallies: BTreeMap<&'static str, u64>,
}Expand description
One run, as a harness or a researcher reads it back: the record the
binary’s --stats writes, as a value.
Field order here is the order the JSON object carries, and the names are a
wire format, the keys of that object. A field is None when the run has
nothing to say about it — no nulls in the JSON, and never a 0 standing for
“not measured”. Counts are decimal strings because they exceed 64 bits;
everything else is a number, a boolean or a token. Serialize it with
serde_json to get the object the binary writes.
The record reference tabulates the fields and which modes carry each.
Fields (Non-exhaustive)§
This struct is marked as non-exhaustive
Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.mode: Option<&'static str>mc, wmc, pmc, pwmc, or compile for a plain compile: the
Mode the run resolved to.
exit_reason: Option<&'static str>How the run ended: solved, or the class of the error that stopped it
(usage, environment, stage, vtree-spec, input, artifact,
incomplete).
variables: Option<u32>Variables in the parsed formula.
clauses: Option<u64>Clauses in the parsed formula.
vtree_spec: Option<String>The vtree construction the run compiles on: the binary’s --vtree, or
portfolio. None when the input is a vitri bundle, which brings its
vtree.
vtree_candidate: Option<String>The portfolio candidate that won selection, when a portfolio ran. In the plain compile it is the vtree the answering compile ran on: the portfolio’s winner, or the retry’s hypergraph bisection. In the model count the primary compile and the stall recompile name theirs as they start, so a run that gives up names the last of them.
satisfiable: Option<bool>Whether the formula has a model, as the run found it.
model_count: Option<String>The integer count, as a decimal string.
weighted_count: Option<String>The weighted count, spelled as the answer line spells it: an exact
rational <n>/<d> in the exact domain, <mantissa>e<exponent> in the
bounded log domain.
weighted_count_log10: Option<f64>log10 of the weighted count’s magnitude, in the log domain only, and
only when it is finite — a zero count has no logarithm and says so
through weighted_count_sign.
weighted_count_sign: Option<i8>Sign of the weighted count in the log domain: -1, 0 or 1.
tdd_nodes: Option<u64>Nodes in the compiled diagram. Only the plain compile path materializes one; the counting paths stream and never build it.
tdd_pairs: Option<u64>Node-pairs in the compiled diagram.
tdd_width: Option<u64>Widest vtree level of the compiled diagram.
peak_pairs: Option<u64>Largest diagram the compile held at once, in node-pairs.
answered_by: Option<&'static str>Which stage produced the answer: of a model count, compile,
preprocessing, stall-recompile, support-enumeration,
no-sbva-retry, unreduced-retry, monotone-reduction or
shannon-split; of a plain compile, compile, preprocessing or
bisect-retry.
reduction: Option<&'static str>What became of Arjun’s reduction on a model count: used, or
unavailable when Arjun ran and no reduction was kept. None when
Arjun did not run.
preprocess_ms: Option<u64>Wall-clock time in preprocessing, in milliseconds. On the model count’s cascade it is the simplify chain alone, since Arjun has its own key.
arjun_ms: Option<u64>Wall-clock time in Arjun, in milliseconds.
vtree_ms: Option<u64>Wall-clock time building vtrees, over the whole run, in milliseconds.
compile_ms: Option<u64>Wall-clock time compiling, in milliseconds, less every phase with its own key: preprocessing, Arjun and vtree construction.
cascade_ms: Option<u64>Wall-clock time in the model count’s cascade on a kept reduction, in milliseconds: the first compile, then any fallbacks and Shannon split, vtree construction inside it included.
backbone_ms: Option<u64>Wall-clock time in backbone detection, in milliseconds.
backbone_found: Option<u64>Backbone literals found.
backbone_probes: Option<u64>SAT probes backbone detection spent.
show_vars: Option<u64>Variables in the show set of the formula the projected count was
answered on, after preprocessing; None without a show set.
sat_prune: Option<&'static str>off when TIDIDI_SAT_PRUNE=off switched the SAT-pruning pass off for
the run, a diagnostic for paired on/off measurements. Absent when the
pass is on, the default.
sat_prune_disabled_by: Option<&'static str>Why the SAT-pruning pass stood down, when it did.
sat_prune_tallies: BTreeMap<&'static str, u64>The SAT-pruning tallies, keyed sat_prune_<tally>, each present only when
it is nonzero. Times end _us and are microseconds, the unit the pass
accumulates them in. The JSON object carries them as top-level keys.