Re: [isabelle] inconsitent correspondence between Isabelle/SMT and z3/SMT.
- To: <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] inconsitent correspondence between Isabelle/SMT and z3/SMT.
- From: Thomas Sewell <thomas.sewell at nicta.com.au>
- Date: Mon, 2 Feb 2015 11:38:42 +1100
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0
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).
On 31/01/15 02:05, lyj238 at ios.ac.cn wrote:
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) ) ))
In z3, I get a counterExample:
sat (model (define-fun state ((x!1 Int)) locationType (ite (= x!1 1) e e)) )
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