Re: [isabelle] inconsitent correspondence between Isabelle/SMT and z3/SMT.



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.

On 31/01/15 02:05, lyj238 at ios.ac.cn wrote:
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 at ios.ac.cn


________________________________

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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.