*To*: li yongjian <lyj238 at gmail.com>*Subject*: Re: [isabelle] ON Isabelle/SMT counter_example*From*: Sascha Boehme <boehmes at in.tum.de>*Date*: Tue, 03 Jul 2012 15:24:10 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CABCjkDp=ju7uF+Wqupj1rzTHuDyvnQ90JUU_eq_AwAOZJAPMoA@mail.gmail.com>*References*: <CABCjkDp=ju7uF+Wqupj1rzTHuDyvnQ90JUU_eq_AwAOZJAPMoA@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.9)

Hi,

The long answer:

And this is what happens in your case. Your goal P --> Q is transformed into (P = term_true) --> (Q = term_true)

term_true ~= term_false

ALL x::term_bool. x = term_true | x = term_false

SMT: Result: f2 -> S1!val!1 f1 -> S1!val!0 f3 -> S1!val!0 f4 -> S1!val!2 sat

SMT: Solver z3: Counterexample found (possibly spurious): P = ??.SMT.term_true

Cheers, Sascha Quoting li yongjian <lyj238 at gmail.com>:

Hi: . I have two questions on Isabelle/SMT. 1) is the intermedia formula which is tranformed from HOL formula, and will be fed into z3. 2) is the counterexample format after z3 checked the formula has I use the following as a running example. lemma "P --> Q" using [[smt_trace]] by smt; by my understanding, The intermediate formula should be a propostion logical formula in SMT format for "~(p-->q)" The counter-ex should say an assignment: P: true; and Q:Flase. but I'm confued about the Isabelle's trace output. Can anyone explain, (see Isabelle's output below): Does the terms f1 f2 make sense? The assignment only says P = ??.SMT.term_true, but this is not complete, Q is False is also needed to specify? regards! f1 = ??.SMT.term_true f2 = ??.SMT.term_false The counterexample output is just as follows: SMT: Assertions: \<not> (P \<longrightarrow> Q) SMT: Names: sorts: S1 = bool functions: f1 = ??.SMT.term_true f2 = ??.SMT.term_false f3 = P f4 = Q SMT: Problem: (benchmark Isabelle :status unknown :logic AUFLIA :extrasorts ( S1) :extrafuns ( (f1 S1) (f2 S1) (f3 S1) (f4 S1) ) :assumption (not (= f1 f2)) :assumption (not (implies (= f3 f1) (= f4 f1))) :formula true) ; solver: z3 ; timeout: 20.0 ; random seed: 1 ; arguments: ; DISPLAY_PROOF=true ; PROOF_MODE=2 ; -rs:1 ; MODEL=true ; -smt SMT: Invoking SMT solver "z3" ... SMT: Solver: SMT: Result: f2 -> S1!val!1 f1 -> S1!val!0 f3 -> S1!val!0 f4 -> S1!val!2 sat SMT: Solver z3: Counterexample found (possibly spurious): P = ??.SMT.term_true

**References**:**[isabelle] ON Isabelle/SMT counter_example***From:*li yongjian

- Previous by Date: [isabelle] The order the elements of set
- Next by Date: Re: [isabelle] The order the elements of set
- Previous by Thread: [isabelle] ON Isabelle/SMT counter_example
- Next by Thread: [isabelle] verilog.thy
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list