Click a stage for a summary of it.
Nothing in the diagram is a separate program or a separate traversal of the input from scratch: the formula is one hash-consed multigraph throughout, and each stage rewrites it in place. The node factory is already simplifying as the parser builds the multigraph, so the formula reaching the first stage has had the cheap local rewrites applied to it. A session that has engaged the incremental driver does not come this way at all. The driver keeps one SAT solver and one encoding alive across queries and preprocesses what each ``check-sat`` added rather than the whole formula, so the sequence above describes only the solves that precede engagement, and those the driver declines to take. It engages on the 32nd solve of a pure ``QF_BV`` or ``QF_ABV`` session and the third of any other, or from the first with ``--incremental=on``, and never with ``--incremental=off``. :doc:`incremental-solving` describes what it does instead. The stages in detail -------------------- Each box above links here. The stages are listed in the order the pipeline runs them. .. raw:: htmlThe front end parses the query into a directed acyclic multigraph, hash-consed so that two identical subterms are one node and every later pass can compare subterms by pointer. It is a multigraph because a node can take the same child more than once, as bvadd x x does. Nodes are not built verbatim: SimplifyingNodeFactory rewrites each one as it is created, so constant folding and the cheap local identities have already been applied by the time the first pass below runs.
Reached only by a query that uses one of the floating-point theories. It makes the partial operations total, canonicalises the indexes of float-indexed arrays, and pins every rounding mode the formula names to one of the five legal encodings, before the formula is used for anything else. The test is per query rather than per session, so a float term that was popped, or built and never asserted, does not drag a later pure bit-vector query through a floating-point pass.
An equality between two whole arrays is built as a single opaque node that survives function, let and query substitution unchanged. Here, at the complete-query boundary, each one still reachable is replaced by a fresh Boolean variable and its witness constraints are conjoined, which is what puts it into the refinement loop at the bottom of the pipeline. Two passes deliberately run just before the replacement, equality propagation and unconstrained elimination, because an equality that defines a symbol, or one with an unconstrained operand, is far cheaper to eliminate outright than to abstract and then refine. See Array extensionality.
When fewer than ten array reads are reachable, or fifty if --ackermannisation was asked for, the reads are rewritten away here rather than left to the refinement loop. The bit-vector simplifications are more thorough than the array ones, so a formula with no arrays left in it gets a better pass than one that keeps them: nothing below eliminates unconstrained arrays, for instance, but everything eliminates unconstrained bit-vectors. Above that threshold the axioms are left to abstraction refinement, which adds only the ones a candidate model actually violates.
The first of three runs, on the formula roughly as written. Every node carries a vector of bits known to be zero, known to be one, or not yet known, and the transfer functions push that knowledge both from a node's children to the node and from the node back to its children: knowing that the result of bvand is all ones tells you that both operands are too. This is where the pipeline learns most of what it knows about individual bits. A worklist holds the nodes whose neighbours changed and each run drains it, so a run ends at its own fixed point rather than after a set number of sweeps. Fully determined nodes are replaced by their constant, with a fact conjoined to pin the node down so the constraint is not lost, and a contradiction found on the way — a bit required to be both zero and one — decides the query unsatisfiable without reaching the SAT solver. --disable-cbitp turns all three runs off.
A sequence chosen so that no pass in it can make the multigraph bigger. Each one can expose work for the others — eliminating an unconstrained variable can make an equality propagatable, which can fix more bits — so the sequence runs once and is then repeated until a round changes nothing. Rebuilding the analysis state each round is what makes the repeat expensive, so it is entered only for a formula with no array operations and fewer nodes than --size-reducing-fixed-point-limit; passing -1 drops the size condition.
Floating-point operations become circuits over packed bits. This sits after the size-reducing passes rather than before them because those passes want to see a float symbol rather than its exposed bits, unconstrained elimination in particular. Symbols, constants and reads keep their sort metadata so that a model can be reconstructed afterwards. The only floating-point operations that survive are the predicates, which the bit-blaster encodes natively over the packed bits.
The main simplification loop: equality propagation, then the general simplifier, then the linear bit-vector equation solver, repeated until a round returns the formula it started with. Because the multigraph is hash-consed that comparison is a pointer comparison, not a traversal. Unlike the size-reducing sequence above this loop is not guarded by a size limit, its passes being the ones that shrink formulas most reliably.
The second run. Repeating the analysis pays here because the loop above has rewritten the formula enough that bits which were not derivable the first time often are: substituted equalities and solved linear equations both expose constants the first run could not see.
Passes that use what the analyses now know, or that restructure the formula in ways the earlier passes cannot. Strength reduction reads the fixed bits and the unsigned intervals together and swaps operations for cheaper ones rather than for constants: a signed division whose operands are known to share a sign bit becomes an unsigned division, an arithmetic right shift whose sign bit is known to be zero becomes a logical one, and a sign-extension whose sign bit is fixed becomes a concatenation with a constant. The rest work on the Boolean structure — pure literals, if-then-else context, and a propositional core simplified through an AIG.
Simplification does not always help, so the estimated cost of the formula is compared against the estimate taken before the loops ran. Unless it fell by at least a fifth the whole simplification is discarded and the earlier formula is used instead. Constants discovered along the way are kept and re-applied, since assigning a variable a constant cannot make the problem harder. The estimator is calibrated against the number of AIG nodes the bit-blaster really builds.
Reads are rewritten through the writes above them, so a read of a written array becomes an if-then-else on whether the two indexes are equal, and array terms disappear from the formula handed to the bit-blaster. The axioms relating two reads of the same array at possibly-equal indexes are not emitted here: that is what the refinement loop at the bottom is for.
The third run differs from the other two in that it does not rewrite the formula at all. Its fixed-bit map is handed to the bit-blaster, which emits no gates for the bits already known — the same information spent on making the encoding smaller rather than on making the formula smaller. Because that map has to describe exactly the tree the bit-blaster receives, no pass may run between this point and bit-blasting.
Each bit-vector operation becomes a circuit of and-gates and inverters. ABC builds and structurally hashes that graph, so equal subcircuits are built once however many times they appear, and then converts it to CNF. --cnf-generation-effort chooses how hard the conversion works at finding a smaller clause set.
The clauses go to whichever backend the build has and the command line selects. If the formula still contains array operations the encoding is deliberately incomplete: it omits the axioms saying that two reads at equal indexes return equal values. A satisfiable answer is therefore checked against those axioms, and any the candidate model violates are added to the live solver before it is asked again, until a model satisfies all of them. An unsatisfiable answer needs no check, since adding axioms can only remove models.