SRI-CSL / yices2 / 26546352364

69%

push

github

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