106 views

Skip to first unread message

Oct 9, 2021, 8:15:10 AM10/9/21

to SMT-LIB

Dear SMT community,

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

> (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)

)

(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))

)

(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.

> 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.

> 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?

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.

Thanks.

Best regards,

Siyuan Chen

Oct 9, 2021, 8:37:43 AM10/9/21

to SMT-LIB

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.

Oct 11, 2021, 1:32:15 PM10/11/21

to smt...@googlegroups.com

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

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

Oct 12, 2021, 4:31:31 AM10/12/21

to SMT-LIB

Hi
Jochen,

Thank you for taking the time to answer this question.

Best regards,

Siyuan Chen

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu