Re: [isabelle] ON Isabelle/SMT counter_example



Hi,

The short answer: Counterexamples produced by SMT solvers might often by spurious, and the corresponding code in Isabelle/HOL is not well tested and currently experimental. You might instead consider Nitpick or Quickcheck for producing counterexamples.

The long answer:

The SMT interface in Isabelle/HOL applies transformations before giving a formula to the SMT solver. These transformations are tuned for proving a goal, but might unfortunately lead to strange counterexamples.

One particular transformation encodes any formula of type bool that is not a Boolean constant nor a Boolean connective into an equation with the constant term_true. The idea is to turn atomic formulas into terms (in the sense of first-order logic). These terms get a new type, called term_bool, to distinguish them from formulas. For the SMT solver, the constant term_true belongs to the type term_bool.

And this is what happens in your case. Your goal

  P --> Q

is transformed into

  (P = term_true) --> (Q = term_true)

where P and Q are now of type term_bool. In addition, the SMT solver gets the fact

  term_true ~= term_false

Hence, it will know that there are at least two distinct values of type term_bool. For the SMT solver, however, there might also be other values of type term_bool. This is because, for technical reasons, the SMT solver does not get an exhaustion rule such as

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

Therefore, an SMT counterexample produced for your goal might refer to further values of type term_bool. And indeed, this is what happens:

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

The names f1 and f2 abbreviate term_true and term_false, whereas f3 and f4 abbreviate P and Q. The value "S1!val!1" is what Z3 assigns to term_false. The above output can thus be read as follows: For P = term_true and Q having some other value, your goal does not hold.

Now, there is some piece of code in Isabelle's SMT integration that parses the above output and tries to turn it into a better readable form. It produces:

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

As you already noted, a value for Q is missing. This is just one indication that currently the parsing code for counterexamples is just experimental and not well tested. You can look at it in your Isabelle distribution at src/HOL/Tools/SMT/z3_model.ML. In case, you desperately need counterexamples from Z3 (or some other SMT solver) instead of relying on Nitpick or Quickcheck, you are invited to extend and modify this code. I suggest to discuss the details privately (not on this list).

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








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