Batch Z3 model value requests and validate responses - #9160
Open
chaizhenhua wants to merge 1 commit into
Open
Conversation
The SMT2 backend currently writes one get-value command per identifier. Request the same sorted identifier set in one Z3 command, and consume every identifier/value pair through the existing typed model decoder. Reject malformed pairs, parser errors and omitted requested typed values instead of accepting a partial SAT model. Keep singleton responses, Boolean set_to fallback, UNSAT model errors and other solvers' behavior. Leave the current Z3 use_as_const setting and type encodings unchanged. Add decision-table unit coverage for empty/singleton/multiple requests, escaped identifiers, typed batched responses, invalid/missing responses, and compatibility cases, plus a real Z3 model round trip. Relinking these tests against the parent solver library reproduces the request assertion failure and six malformed-response failures. Validation: clang-format 15 changed-line check and cpplint pass; [smt2] 308 assertions/46 cases; [z3] 27/7; [core] 18,839 assertions/595 cases, including two expected failures. CBMC CORE passes 1,128 tests (67 skipped), and SMT2 solver CORE passes 42 (2 skipped). The wider Z3 CORE run passes 1,102 (92 skipped); complex2 times out at 20 seconds on both parent and candidate and at 60 seconds on candidate. Its generated formula is identical except for get-value grouping. On one generated 1,000-scalar SAT fixture with Z3 4.15.4, requests fall from 10,006 to 1, SMT input from 1,733,249 to 1,593,179 bytes and model output from 324,598 to 314,593 bytes. Seven alternating Z3 runs have median wall times 49.44/41.78 ms; five CBMC runs have medians 308.03/294.30 ms. Model assignments and decoded traces match exactly. These local sample measurements do not establish a general speedup.
chaizhenhua
requested review from
TGWDB,
kroening,
martin-cs,
peterschrammel and
tautschnig
as code owners
September 10, 2026 00:53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The SMT2 backend currently sends one
get-valuecommand per model identifier.Z3 accepts one command containing the same sorted identifier set, so this change
batches that request and consumes every returned identifier/value pair through
the existing typed decoder. It also rejects malformed pairs, parser errors, and
missing requested values instead of accepting a partial SAT model.
This PR only changes the Z3 model request/response path. Singleton responses,
Boolean
set_tofallback, UNSAT model errors, other solvers,use_as_const, andthe existing type encodings keep their current behavior.
Validation includes failing parent-linked unit regressions, SMT2/Z3/CORE unit
tests,
cbmc-CORE, andsmt2_solver-CORE. The wider Z3 run passed 1,102 caseswith 92 existing skips;
complex2exceeded 20 seconds on both the parent andcandidate and also exceeded 60 seconds on the candidate. On one 1,000-scalar
fixture, requests fell from 10,006 to 1 and seven alternating Z3 runs had median
wall times of 49.44 ms before and 41.78 ms after; this sample is not a general
performance claim.