Can SMT-LIB standard allow `(get-model)` to return a list of definition that is not user-declared function symbols, even formulas?

[Siyuan Chen]

Dear SMT community,

I have some confusion about `get-model` and `abstract value`.

Following the smt-lib-reference-v2.6-r2021-05-12.pdf p.65, it says that

> (get-model) returns a list (d1 ... dk) of definitions specifying all and only the current user-declared function symbols {g1, ..., gm} in the current model A.

Noticed that the standard uses "all and only". However, I found that many implementations do not conform with the standard.

For example,

```

$ z3 -in
(set-logic ALL)
(declare-const _v10 Int)
(declare-const _v11 Int)
(assert (= 2 (div _v10 _v11)))
(assert (not (= _v11 0)))
(check-sat)
sat
(get-model)
(
  (define-fun _v10 () Int
    2)
  (define-fun _v11 () Int
    1)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    2)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    0)
)

```

I did not declare `div0` and `div0` in the script, but z3 returned the unexpected symbols (A related issue https://github.com/Z3Prover/z3/issues/5565#issuecomment-927141253).

For the 2nd example (slight different ...),

```

$ z3 -in
(set-logic ALL)
(declare-sort Type 0)
(declare-fun subtype (Type Type) Bool)
(declare-const root-type Type)
(assert (forall ((x Type)) (subtype x root-type)))
(check-sat)
sat
(get-model)
(
  ;; universe for Type:
  ;;   Type!val!1 Type!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Type!val!1 () Type)
  (declare-fun Type!val!0 () Type)
  ;; cardinality constraint:
  (forall ((x Type)) (or (= x Type!val!1) (= x Type!val!0)))
  ;; -----------
  (define-fun root-type () Type
    Type!val!0)
  (define-fun subtype ((x!0 Type) (x!1 Type)) Bool
    (= x!1 Type!val!0))
)

```

I did not declare `Type!val!1` and `Type!val!0` in the script, but z3 returned the unexpected symbols. Noticed that Z3 even returned a formula in the list.

Can I think that both two examples above violate the SMT-LIB standard? Or they are different?

It seems that the 1st example violates the SMTLIB standard, but the 2nd example doesn't, because they are abstract values. Is that right?

The following are some of my analysis:

The `Type!val!1` and `Type!val!0` could be abstract values, because

1.  In p.24, it says 

   > Simple symbols starting with the character @ or . are reserved for solver use. Solvers can use them respectively as identifiers for abstract values and solver-generated function symbols other than abstract values.

   Noticed that the standard uses "can", so `@` is not mandatory.

2. In p.83, it says that

   > Note that the requirements on Vσ can be always trivially satisfied by L by making sure that the signature Ω above contains a distinguished set of infinitely many additional free constant symbols of sort σ, and defining Vσ to be that set. We call these constant symbols abstract values

   The `Type!val!1` and `Type!val!0` are additional free constant symbols in a distinguished set of Ω. PS. I assumed the "additional free constant symbols" here refer to the "free sort symbols" (in p.82) of the combined theory 𝓣.

   So z3 just dumps all the definitions of function symbols, even including these  constant symbols in the distinguished set of Ω, even including some formulas involving these constant symbols.

All in all, the questions are that

1. Is my analysis above correct?

2. Should we treat the z3 behaviors as standard violations (because it returns unexpected symbols)? Or we make the standard more precise?

Thanks.

Best regards,

Siyuan Chen

[Siyuan Chen]

Sorry, there are some typo in my previous post.

>   The `Type!val!1` and `Type!val!0` are additional free constant symbols in a distinguished set of Ω. PS. I assumed the "additional free constant symbols" here refer to the "free sort symbols" (in p.82) of the combined theory 𝓣.

I mean "free function symbols", not "free sort symbols".

Thanks.

[Jochen Hoenicke]

Hello,

The current definition of get-model in the SMT-LIB standard does not
have a syntax to specify everything that you may want in every logic.
When we added the model validation track to SMT-COMP, we only
supported theories where the model can be fully expressed using the
syntax in the SMT-LIB standard. And we would need to solve these
problems when extending the track to more theories/logics. So to
answer your question: z3 behavior contradicts the standard, but there
is no standard conform way to give a model in certain logics, in
particular for the first example.

ad 1st example. Your first point is mainly for "undefined" parts of
theory-defined functions. There is no standard syntax in get-model to
specify what something like (div 5 0) should be. The SMT-LIB theory
for integers/real specifically says that division by 0 should be
treated as if it was an uninterpreted function, i.e. the solver should
search for an interpretation of the function that satisfies the
formula. But there is no way to communicate the found interpretation
back to the user/application.

This not only affects division by 0 in non-linear arithmetic, but also
some floating point operations and selector functions in the theory of
datatypes like "(car (as nil (List Int)))". Even the "select" function
in the array theory is uninterpreted, if you use model values (or is
this the array model value that is uninterpreted?).

Without giving these additional definitions, it would require an SMT
solver just to check that the "model" given by the solver can be
satisfied by choosing the right interpretation for the "theory-defined
functions".

ad 2nd example. My interpretation of the "can" in "Solvers can use
them respectively as identifiers for abstract values" is that the
solver doesn't have to use abstract values. But since there is no
other way to specify a value in the case of uninterpreted sorts, the
only standard conforming way would be to use them. In particular the
standard doesn't support "declare-fun" in the answer to the get-model
command that z3 currently gives.

There is another area where the SMT-LIB standard for models is
currently lacking: specify constraints on user-defined sorts or array
sorts. You cannot specify a cardinality constraint on uninterpreted
sorts, which are necessary to satisfy certain quantified formulas.
Likewise the formula "(assert (forall ((a (Array Int Int))) (exists
((x Int)) (not (= (select a x) 0)))))" is satisfiable but only if the
"constant 0" array is not an element of the array sort domain. Of
course, checking whether a quantified formula is satisfied by a
concrete model needs a kind of solver anyways and is undecidable in
some logics like NIA.

I'm not sure if a solver may answer "sat" if you give it a Gödel-sentence...

Regards,
Jochen

> --
> You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/c43f781a-dffb-455c-8c2f-ff89718e3a71n%40googlegroups.com.



--
Jochen Hoenicke,
Email: hoen...@informatik.uni-freiburg.de Tel: +49 761 203 8243

[Siyuan Chen]

Hi Jochen,

Thank you for taking the time to answer this question.

Best regards,

Siyuan Chen