Email Gateway (Aug 18 2022 at 20:31): Email Gateway (Aug 18 2022 at 20:31):From: li yongjian <lyj238@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
Email Gateway (Aug 18 2022 at 20:34):From: Sascha Boehme <boehmes@in.tum.de>
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@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 hasI 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_falseThe 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 = QSMT: 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
; -smtSMT: Invoking SMT solver "z3" ...
SMT: Solver:
SMT: Result:
f2 -> S1!val!1
f1 -> S1!val!0
f3 -> S1!val!0
f4 -> S1!val!2
satSMT: Solver z3: Counterexample found (possibly spurious):
P = ??.SMT.term_true
Last updated: Apr 26 2024 at 20:16 UTC