SRI-CSL / yices2
69%

DEFAULT BRANCH: master
Repo Added
Files 486
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

LAST BUILD ON BRANCH master
branch: SELECT
CHANGE BRANCH
x

coverage: 68.793% (+0.007%) from 68.786%
26546352364

push

github

web-flow 
smt2 array model display format (#633)

* smt2: emit Array-declared constants as SMT-LIB store/const in models

Symbols declared via the SMT-LIB Array sort are currently rendered in
(get-model) as

  (define-fun a ((x!0 K)) V (ite ...))

which has the wrong arity and signature: the user wrote
(declare-fun a () (Array K V)), so the model must read

  (define-fun a () (Array K V) (store ... ((as const (Array K V)) d) ...))

This is required by the SMT-COMP 2026 Model Validation Track.

Root cause: once interned, Yices' type system represents both
(declare-fun a () (Array K V)) and (declare-fun f (K) V) as an
UNINTERPRETED_TERM of internal function type (-> K V), so the SMT-LIB
sort information is gone by the time print_smt2_model runs. The fix
records the missing bit ("this name was declared as an Array
constant") in the SMT2 frontend at parse time and consults it in the
model printer.

Implementation, scoped to src/frontend/smt2/:

* smt2_globals_t gains an int_hmap_t array_const_terms mapping term ids
  declared via 0-arity Array sort to a non-zero marker. It is populated
  in smt2_declare_fun whenever the declaration is 0-arity and the
  resulting type is a unary function type (which under SMT-LIB syntax
  can only originate from the Array sort, directly or via define-sort).
  declare-const is automatically covered: the parser reduces it to
  SMT2_DECLARE_FUN.

* The map is kept consistent across (push)/(pop) via a hook in
  smt2_pop_term_names that erases markers for popped term ids before
  the names are removed. (reset-assertions) clears the map alongside
  yices_reset_tables() when global_decls is off (term ids get
  recycled); with global_decls the map is preserved. (reset) is
  covered automatically because smt2_reset_all already destroys and
  re-inits all globals.

* smt2_pp_def gains a bool array_const parameter. When set, the printer
  emits the 0-arity (define-fun name () tau ...) form regardless of
  the value's internal representation, d... (continued)

21 of 21 new or added lines in 2 files covered. (100.0%)

87488 of 127176 relevant lines covered (68.79%)

1621496.52 hits per line

Relevant lines Covered
127176 RELEVANT LINES 87488 COVERED LINES
1621496.52 HITS PER LINE
Source Files on master

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
26546352364 master smt2 array model display format (#633) * smt2: emit Array-declared constants as SMT-LIB store/const in models Symbols declared via the SMT-LIB Array sort are currently rendered in (get-model) as (define-fun a ((x!0 K)) V (ite ...)) which has... push web-flow github
68.79
26491292477 fix/smt2-array-model-format tests: update array model gold files Commit supported by Codex/GPT5.5. Pull #633 disteph github
68.79
26473630241 feature/wide-model-projection Wide projection: address second review pass Two cleanup items raised by review: 1. tests/api/test_generalize_model.c: remove the unused helper run_both_modes_quiet. It was a leftover from an earlier iteration that printed less per-test det... Pull #630 disteph github
68.99
26473629702 feature/wide-model-projection Merge 8b09c89fe into 2137d2aaf Pull #630 web-flow github
68.99
26471293823 feature/wide-model-projection Wide projection: skip-and-continue on projection error; document model pruning Two changes prompted by review: 1. Per-cube projection errors no longer break the SAT-guided loop. project_one_cube_into can fail on cubes whose literals contain ... push disteph github
69.0
26471292351 feature/wide-model-projection Merge 4292db101 into 2137d2aaf Pull #630 web-flow github
69.0
26470694967 feature/wide-model-projection Merge 3fb2be356 into 2137d2aaf Pull #630 web-flow github
69.0
26470694687 feature/wide-model-projection Wide model projection: assert on bug paths, expose cube_budget, drop overclaim Four small changes prompted by review of the SAT-guided enumerator: 1. Assert on SAT-engine bugs. nsat_solve is documented to return only STAT_SAT or STAT_UNSAT (s... Pull #630 disteph github
69.0
26469917215 feature/wide-model-projection Remove the eager Cartesian wide projection path gen_model_by_proj_sat_guided semantically subsumes gen_model_by_proj_wide: every joint cube the syntactic walker would emit is also an implicant of the polarity-aware Boolean abstraction the SAT-gui... Pull #630 disteph github
69.0
26468262109 feature/wide-model-projection Add SAT-guided wide model projection; commit supported by Codex/GPT5.5 Pull #630 disteph github
68.89
See All Builds (2002)