SRI-CSL / yices2 / 27026975493

69%

Build Type

push

github

Committed by web-flow

Commit Message

Add wide (truth-invariant) model generalization mode (#630)

* Add wide (truth-invariant) model generalization mode

Implements a new model-generalization algorithm that walks the Boolean
structure of the input formula and unions per-disjunct projections,
producing a generalization that is truth-invariant for the formula
rather than sign-invariant for a single literal implicant.

The wide algorithm is now the default behaviour of YICES_GEN_BY_PROJ
and YICES_GEN_DEFAULT (for arithmetic-variable elimination). The
legacy implicant-then-project pipeline remains available under the
new YICES_GEN_BY_PROJ_LOCAL mode.

Algorithm:
  1. Walk each top-level f[i] enumerating cubes true at the model.
     - OR_TERM positive : pick all satisfied disjuncts, union their
       cube sets.
     - OR_TERM negative : conjunction-of-negations via De Morgan,
       Cartesian-product the cube sets of each negated arg.
     - Boolean-typed ITE_TERM : decompose as (cond AND branch).
     - Otherwise : emit a singleton cube containing the literal.
  2. Cartesian-product per-formula cube sets to obtain joint cubes
     (this preserves coupling of shared elimination variables).
  3. Project each joint cube via the legacy implicant+project
     pipeline, then OR the results.

Output shape:
  - Single-cube case (purely conjunctive input) : projected literals
    are emitted flat, exactly matching the legacy YICES_GEN_BY_PROJ
    output shape. Backwards-compatible with existing callers.
  - Multi-cube case : v contains a single OR-of-AND term.

Fallback: if the cube-set Cartesian product would exceed an internal
budget (WIDE_CUBE_BUDGET = 1024), the routine transparently falls
back to the legacy local pipeline.

The internal exists/forall solver (efsolver.c) is unchanged: it has
its own implicant+project pipeline that bypasses this API.

Files changed:
  - src/include/yices_types.h: add YICES_GEN_BY_PROJ_LOCAL enum value.
  - src/include/yices.h: document the new wide and legacy mo... (continued)

Coverage Stats

411 of 531 new or added lines in 2 files covered. (77.4%)

1 existing line in 1 file now uncovered.

88130 of 127715 relevant lines covered (69.01%)

1647051.91 hits per line