Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] inconsitent correspondence between Isabelle/SM...

Email Gateway (Aug 19 2022 at 17:02):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:
I am confused on an inconsitent correspondence between Isabelle SMT and z3 SMT.
It is really annonying, and I look forward to an answer.

I have a Isabelle theory:

datatype locationType= m| e| s| i

type_synonym state="nat ⇒ locationType"

lemma test1:"~(if ((st::state) 1 = e) then s
else (if ((st::state) 1 = m) then s
else (if ((st::state) 1 = i) then i
else s))) = m"
by (metis locationType.distinct(3))

In Isabelle, it is tautology

But accordingly, I have a z3 theory:

(declare-datatypes () ((locationType m e s i )))

(declare-fun state (Int) locationType)
( assert (not (=> true (= (ite (= (state 1) e)
s (ite (= (state 1) m) s (ite (= (state 1) i) i s ) ) ) m) ) ))
(check-sat)

In z3, I get a counterExample:
sat (model (define-fun state ((x!1 Int)) locationType (ite (= x!1 1) e e)) )

regards

lyj238@ios.ac.cn

Email Gateway (Aug 19 2022 at 17:02):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:
I am confused on an inconsitent correspondence between Isabelle SMT and z3 SMT.
It is really annonying, and I look forward to an answer.

I have a Isabelle theory:

datatype locationType= m| e| s| i

type_synonym state="nat ⇒ locationType"

lemma test1:"~(if ((st::state) 1 = e) then s
else (if ((st::state) 1 = m) then s
else (if ((st::state) 1 = i) then i
else s))) = m"
by (metis locationType.distinct(3))

In Isabelle, it is tautology

But accordingly, I have a z3 theory:

(declare-datatypes () ((locationType m e s i )))

(declare-fun state (Int) locationType)
( assert (not (=> true (= (ite (= (state 1) e)
s (ite (= (state 1) m) s (ite (= (state 1) i) i s ) ) ) m) ) ))
(check-sat)

In z3, I get a counterExample:
sat (model (define-fun state ((x!1 Int)) locationType (ite (= x!1 1) e e)) )

regards

lyj238@ios.ac.cn

Email Gateway (Aug 19 2022 at 17:09):

From: Thomas Sewell <thomas.sewell@nicta.com.au>
Dear lyj238.

You have your SMT sat/unsat cases around the wrong way.

In short, to "prove" a fact in SMT-land, you must assert its negation
and observe unsatisfiability.

If you assert a true fact, this changes nothing, the world is still
satisfiable, and any model will do. That's what you've done here.

Your equality ((if-then-else expression) = m) is always false. Thus its
negation is a tautology in Isabelle.

In SMT-land, it is always false, thus (not (=> true (= (ite-expression) m)))
is equal to (not (=> true false))
and to (true).

Cheers,
Thomas.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Last updated: Nov 21 2024 at 12:39 UTC