SRI-CSL / yices2 / 25364583433

67%

master: 67%

Build Type

Pull #606

github

Committed by disteph

Commit Message

mcsat: zero-copy peek variant of tuple_blast_get (L3)

Many call sites inside tuple_blast_term_body only read the blasted
leaves of a sub-term. They currently pay a malloc + memcpy per sub-term
by construction:

  init_ivector(&v, 0);
  tuple_blast_get(pre, x, &v);
  use v.data, v.size;
  delete_ivector(&v);

Add tuple_blast_peek, which returns (data_ptr, size) pointing directly
into tuple_blast_data. The pointer is live only until the next
operation that can grow tuple_blast_data -- most notably a subsequent
tuple_blast_term call; this invariant is spelled out in the helper's
doc-comment and repeated at every use site.

Convert the three hot read-only sites called out in the review:
  * tuple_blast_collect_arg  (called from APP / UPDATE / composites)
  * ITE                      (three leaf vectors per ITE sub-term)
  * DISTINCT                 (two leaf vectors per (i,j) pair, O(n^2))
  * EQ                       (two leaf vectors per equality)

Also tighten tuple_blast_eq_vector's signature to take (a, b, n)
directly so it can consume peek output without re-wrapping in an
ivector.

Call sites that call tuple_blast_term AGAIN after getting the leaves
(APP/UPDATE scan loops, composite/pprod/poly child loops) still use
the copying tuple_blast_get; peek would be unsafe there and rewriting
those to defer the tuple_blast_term calls would balloon the diff.

All three build modes (debug, sanitize, release) still pass the 31
api tests, and all eight tuple .ys regressions (the four pre-existing
plus the four added in M6) still match their gold output. Addresses
review item L3.

Pull Request Pull Request #606: MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

Coverage Stats

730 of 965 new or added lines in 3 files covered. (75.65%)

1 existing line in 1 file now uncovered.

84340 of 126083 relevant lines covered (66.89%)

1634423.76 hits per line