Module items 

Parsing items, e.g. terms, proof steps, quantifiers; and related objects or functions.

Macros

idx

Structs

Assignment

Assignment to a literal.

BitVec

Blame

Explains how a term in a pattern was matched. It will always start with an enode and then have some sequence of equalities used to rewrite distinct subexpressions of the enode.

BoundVars

Cdcl

CdclBacklink

CdclIdx

Conflict

ENode

ENodeIdx

EqGivenIdx

EqTransIdx

Equality

Fingerprint

An identifier for a Z3 quantifier instantiation (called “fingerprint” in the original Axiom Profiler). Represented as a 16-digit hexadecimal number in log files.

GraphIdx

InstIdx

Instantiation

A Z3 instantiation.

Justification

LitIdx

Literal

A boolean term which has been assigned either true or false.

Match

MatchIdx

PatVec

PatternIdx

ProofIdx

ProofStep

A Z3 proof step and associated data. Represents a single step where z3 proved a boolean expression. These steps have dependencies which combine to build up a proof tree. Parts of this tree may be under hypotheses in which case the solver tries to do a proof by contradiction (and the proved terms are only valid under these hypotheses).

ProofStepKindIter

An iterator over the variants of ProofStepKind

QuantIdx

QuantPat

QuantPatVec

Quantifier

A Z3 quantifier and associated data.

StackFrame

StackIdx

Term

A Z3 term and associated data.

TermId

Represents an ID string of the form name#id or name#.

TermIdToIdxMap

Remapping from TermId to TermIdx. We want to have a single flat vector of terms but TermIds don’t map to this nicely, additionally the TermIds may repeat and so we want to map to the latest current TermIdx. Has a special fast path for the common empty namespace case.

TermIdx

TimeRange

TransitiveExpl

TransitiveExplSegment

Enums

CdclKind

Coupling

ENodeBlame

EqualityExpl

A Z3 equality explanation. Root represents a term that is a root of its equivalence class. All other variants represent an equality between two terms and where it came from.

InstProofLink

A Z3 instantiation.

InstantiationKind

JustificationKind

The reason for an assignment.

MatchKind

Meaning

ProofStepKind

Taken from z3-sys. Update from there if more cases are added. A few marked cases were renamed to match z3’s ast.cpp.

QuantKind

Represents an ID string of the form name!id.

TermKind

TermKindInner

TheoryKind

See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.h#L78-L88 and https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.cpp#L1330-L1336 These define the basic family IDs, we get them either as a number (e.g. in [assign] lines) or names (e.g. in [eq-expl] th lines). Other family IDs may be defined, which are represented as either Other or Unknown, depending on if we got a name or a number.

TimeRangeStatus

TransitiveExplIter

TransitiveExplSegmentKind

VarNames

Type Aliases

EqGivenUse