[isabelle] SMT completeness issue: Failure to prove a tru... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] SMT completeness issue: Failure to prove a tru...

Email Gateway (Apr 11 2025 at 14:38):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

yesterday I had a proof obligation that boils down to a LIRA problem
(linear integer/real arithmetic). Usually "linarith" can solve these
just fine, but in this case it couldn't (at least not in a single step),
but I know "linarith" is incomplete for mixed integer/real problems. I
then turned to the "smt" method instead and to my surprise found that it
couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤ x +
1 / 2"
shows   "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
    using assms by linarith
thus ?thesis
    using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and
"linarith" can solve it in two steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))" all
fail, and Z3 even claims there's a (possibly spurious) counterexample.

Looking at the generated smtlib problem, I found to my surprise that
both the division on the reals and the type conversion "real_of_int" are
translated to uninterpreted functions, so it's not surprising that the
SMT solvers fail to prove it. It's easy to get rid of the division, of
course, but that doesn't make it work either (presumable because the
"of_int" UF is still there).

I would have expected an encoding like the following:

(set-logic AUFLIRA)
(set-option :produce-proofs true)
(declare-fun x () Real)
(declare-fun m () Int)
(assert (and (<= 0 x) (<= x (/ 1 2)) (<= x m) (<= m (+ x (/ 1 2)))))
(assert (not (= m (* 2 x))))
(check-sat)
(get-proof)

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some
unresolved difficulty in replaying LIRA proofs?

Manuel

Email Gateway (Apr 12 2025 at 05:47):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Manuel,

SMT was developed by Sascha Böhme, so I'm only partly qualified to answer.

The fragment SMT solvers can decide is linear. Some SMT solvers also support division and have nonlinear solvers, but these are very slow. As a result, native division is not used, even when it's between constants like 1 and 2, apparently.

As for "real_of_int", the uninterpreted symbol is definitely suboptimal. I'm not sure it's safe to just omit it everywhere and rely on implicit cast or subtyping. SMT-LIB seems to support overloading, so this is all rather scary.

In "smt_real.ML", I'm seeing code like this:

fun abstract abs t =
(case t of
(c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
| (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ t =>
abs t #>> (fn u => SOME (c $ u))
| _ => pair NONE)

It seems to want to do something about division and Int.of_int, but maybe this setup is somehow bit-rotten or insufficient.

I'm CC:ing Martin. Maybe he and I could look into both issues together, if he has time.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 11. Apr 2025, at 16:29, Manuel Eberl <manuel@pruvisto.org> wrote:

Hello,

yesterday I had a proof obligation that boils down to a LIRA problem (linear integer/real arithmetic). Usually "linarith" can solve these just fine, but in this case it couldn't (at least not in a single step), but I know "linarith" is incomplete for mixed integer/real problems. I then turned to the "smt" method instead and to my surprise found that it couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤ x + 1 / 2"
shows "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
using assms by linarith
thus ?thesis
using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and "linarith" can solve it in two steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))" all fail, and Z3 even claims there's a (possibly spurious) counterexample.

Looking at the generated smtlib problem, I found to my surprise that both the division on the reals and the type conversion "real_of_int" are translated to uninterpreted functions, so it's not surprising that the SMT solvers fail to prove it. It's easy to get rid of the division, of course, but that doesn't make it work either (presumable because the "of_int" UF is still there).

I would have expected an encoding like the following:

(set-logic AUFLIRA)
(set-option :produce-proofs true)
(declare-fun x () Real)
(declare-fun m () Int)
(assert (and (<= 0 x) (<= x (/ 1 2)) (<= x m) (<= m (+ x (/ 1 2)))))
(assert (not (= m (* 2 x))))
(check-sat)
(get-proof)

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some unresolved difficulty in replaying LIRA proofs?

Manuel

smime.p7s

Email Gateway (Apr 12 2025 at 06:34):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Jasmin, Manuel and all,

On 4/12/25 07:47, Jasmin Blanchette wrote:

Hi Manuel,

SMT was developed by Sascha Böhme, so I'm only partly qualified to answer.

The fragment SMT solvers can decide is linear. Some SMT solvers also
support division and have nonlinear solvers, but these are very slow.
As a result, native division is not used, even when it's between
constants like 1 and 2, apparently.

Getting the divide operator translated is easy to add actually.

As for "real_of_int", the uninterpreted symbol is definitely
suboptimal. I'm not sure it's safe to just omit it everywhere and rely
on implicit cast or subtyping. SMT-LIB seems to support overloading,
so this is all rather scary.

My understanding is that you cannot omit it due to equality requiring to
variables of the same sort. But SMT-Lib has the constant to_real for
casting. Some SMT solvers allow it.

In "smt_real.ML", I'm seeing code like this:

fun abstract abs t =
(case t of
(c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
| (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ t =>
abs t #>> (fn u => SOME (c $ u))
| _ => pair NONE)

It seems to want to do something about division and Int.of_int, but
maybe this setup is somehow bit-rotten or insufficient.

That code is to abstract over division to stay in the LIRA fragment,
e.g., if you have a = 1 / b then you need to get rid of the 1/b.

The better solution is to add a translation of division:

fun mk_divides ts = Term.list_comb (\<^Const>‹divide \<^Type>‹real››, ts)
fun divides _ _ (ts as [a,b]) =
     if SMT_Util.is_number a andalso SMT_Util.is_number b
     then SOME ("/", 2, ts, mk_divides) else NONE
    | divides _ _ _ = NONE

val setup_builtins =
(*the current things followed by *) #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
    (Term.dest_Const \<^Const>‹divide \<^Type>‹real››, divides) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC)
    [(\<^Const>‹of_int \<^Type>‹real››, "to_real"),
     (\<^Const>‹of_nat \<^Type>‹real››, "to_real")]

Division seems to work but the to_real currently breaks the
reconstruction of proofs: on the Isabelle side, of_int is ambiguous
without looking at the rest of the term. I will look into it.

I'm CC:ing Martin. Maybe he and I could look into both issues
together, if he has time.

In all likelihood, Hanna (CC-ed) and I have looked more recently at that
code (for the BV translation -- even if our changes are all out of
tree). But feel free to do looking into it with Martin if you prefer.

Mathias

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 11. Apr 2025, at 16:29, Manuel Eberl <manuel@pruvisto.org> wrote:

Hello,

yesterday I had a proof obligation that boils down to a LIRA problem
(linear integer/real arithmetic). Usually "linarith" can solve these
just fine, but in this case it couldn't (at least not in a single
step), but I know "linarith" is incomplete for mixed integer/real
problems. I then turned to the "smt" method instead and to my
surprise found that it couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤ x
+ 1 / 2"
shows   "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
    using assms by linarith
thus ?thesis
    using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and
"linarith" can solve it in two steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))" all
fail, and Z3 even claims there's a (possibly spurious) counterexample.

Looking at the generated smtlib problem, I found to my surprise that
both the division on the reals and the type conversion "real_of_int"
are translated to uninterpreted functions, so it's not surprising
that the SMT solvers fail to prove it. It's easy to get rid of the
division, of course, but that doesn't make it work either (presumable
because the "of_int" UF is still there).

I would have expected an encoding like the following:

(set-logic AUFLIRA)
(set-option :produce-proofs true)
(declare-fun x () Real)
(declare-fun m () Int)
(assert (and (<= 0 x) (<= x (/ 1 2)) (<= x m) (<= m (+ x (/ 1 2)))))
(assert (not (= m (* 2 x))))
(check-sat)
(get-proof)

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some
unresolved difficulty in replaying LIRA proofs?

Manuel

Email Gateway (Apr 12 2025 at 06:39):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Mathias,

In all likelihood, Hanna (CC-ed) and I have looked more recently at that code (for the BV translation -- even if our changes are all out of tree). But feel free to do looking into it with Martin if you prefer.

By all means, you go ahead! Thank you so much. I knew you worked on reconstruction, but I didn't realize you had such extensive knowledge of the translation.

Best,
Jasmin
--

Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 12. Apr 2025, at 08:34, Mathias Fleury <mathias.fleury12@gmail.com> wrote:

Hi Jasmin, Manuel and all,

On 4/12/25 07:47, Jasmin Blanchette wrote:

Hi Manuel,

SMT was developed by Sascha Böhme, so I'm only partly qualified to answer.

The fragment SMT solvers can decide is linear. Some SMT solvers also support division and have nonlinear solvers, but these are very slow. As a result, native division is not used, even when it's between constants like 1 and 2, apparently.
Getting the divide operator translated is easy to add actually.

As for "real_of_int", the uninterpreted symbol is definitely suboptimal. I'm not sure it's safe to just omit it everywhere and rely on implicit cast or subtyping. SMT-LIB seems to support overloading, so this is all rather scary.
My understanding is that you cannot omit it due to equality requiring to variables of the same sort. But SMT-Lib has the constant to_real for casting. Some SMT solvers allow it.

In "smt_real.ML", I'm seeing code like this:

fun abstract abs t =
(case t of
(c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
| (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ t =>
abs t #>> (fn u => SOME (c $ u))
| _ => pair NONE)

It seems to want to do something about division and Int.of_int, but maybe this setup is somehow bit-rotten or insufficient.

That code is to abstract over division to stay in the LIRA fragment, e.g., if you have a = 1 / b then you need to get rid of the 1/b.

The better solution is to add a translation of division:

fun mk_divides ts = Term.list_comb (\<^Const>‹divide \<^Type>‹real››, ts)
fun divides _ _ (ts as [a,b]) =
if SMT_Util.is_number a andalso SMT_Util.is_number b
then SOME ("/", 2, ts, mk_divides) else NONE
| divides _ _ _ = NONE

val setup_builtins =
(*the current things followed by *) #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
(Term.dest_Const \<^Const>‹divide \<^Type>‹real››, divides) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC)
[(\<^Const>‹of_int \<^Type>‹real››, "to_real"),
(\<^Const>‹of_nat \<^Type>‹real››, "to_real")]

Division seems to work but the to_real currently breaks the reconstruction of proofs: on the Isabelle side, of_int is ambiguous without looking at the rest of the term. I will look into it.

I'm CC:ing Martin. Maybe he and I could look into both issues together, if he has time.

In all likelihood, Hanna (CC-ed) and I have looked more recently at that code (for the BV translation -- even if our changes are all out of tree). But feel free to do looking into it with Martin if you prefer.

Mathias

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 11. Apr 2025, at 16:29, Manuel Eberl <manuel@pruvisto.org> <mailto:manuel@pruvisto.org> wrote:

Hello,

yesterday I had a proof obligation that boils down to a LIRA problem (linear integer/real arithmetic). Usually "linarith" can solve these just fine, but in this case it couldn't (at least not in a single step), but I know "linarith" is incomplete for mixed integer/real problems. I then turned to the "smt" method instead and to my surprise found that it couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤ x + 1 / 2"
shows "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
using assms by linarith
thus ?thesis
using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and "linarith" can solve it in two steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))" all fail, and Z3 even claims there's a (possibly spurious) counterexample.

Looking at the generated smtlib problem, I found to my surprise that both the division on the reals and the type conversion "real_of_int" are translated to uninterpreted functions, so it's not surprising that the SMT solvers fail to prove it. It's easy to get rid of the division, of course, but that doesn't make it work either (presumable because the "of_int" UF is still there).

I would have expected an encoding like the following:

(set-logic AUFLIRA)
(set-option :produce-proofs true)
(declare-fun x () Real)
(declare-fun m () Int)
(assert (and (<= 0 x) (<= x (/ 1 2)) (<= x m) (<= m (+ x (/ 1 2)))))
(assert (not (= m (* 2 x))))
(check-sat)
(get-proof)

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some unresolved difficulty in replaying LIRA proofs?

Manuel

smime.p7s

Email Gateway (Apr 12 2025 at 13:41):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

thanks for the answers! The problem is not the least bit urgent for me,
so I don't really have much of a stake in this. I just wanted to know
whether this was a known issue or not, and see if someone is interested
in fixing it.

So if you have the time and energy to do this, that's great – but no
pressure (at least not from me. :) ).

I didn't know equality between integers and reals was a problem in SMT.
I do know that Nelson–Oppen doesn't like things like that, but I don't
know enough about the internals of SMT solvers to understand whether it
is an issue, and I expected SMT solvers to just "abstract away" from
this if need be and insert coercions like "to_real" in a preprocessing
step. I mean, my smtlib problem went through just fine without any
errors or warnings, and I even got a proof (although I don't understand
enough about SMT proof objects to be able to see whether it is actually
a proof that makes sense and proves what I want).

Manuel

On 12/04/2025 08:38, Jasmin Blanchette wrote:

Hi Mathias,

In all likelihood, Hanna (CC-ed) and I have looked more recently at
that code (for the BV translation -- even if our changes are all out
of tree). But feel free to do looking into it with Martin if you prefer.

By all means, you go ahead! Thank you so much. I knew you worked on
reconstruction, but I didn't realize you had such extensive knowledge
of the translation.

Best,
Jasmin

--

Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 12. Apr 2025, at 08:34, Mathias Fleury
<mathias.fleury12@gmail.com> wrote:

Hi Jasmin, Manuel and all,

On 4/12/25 07:47, Jasmin Blanchette wrote:

Hi Manuel,

SMT was developed by Sascha Böhme, so I'm only partly qualified to
answer.

The fragment SMT solvers can decide is linear. Some SMT solvers also
support division and have nonlinear solvers, but these are very
slow. As a result, native division is not used, even when it's
between constants like 1 and 2, apparently.

Getting the divide operator translated is easy to add actually.

As for "real_of_int", the uninterpreted symbol is definitely
suboptimal. I'm not sure it's safe to just omit it everywhere and
rely on implicit cast or subtyping. SMT-LIB seems to support
overloading, so this is all rather scary.

My understanding is that you cannot omit it due to equality requiring
to variables of the same sort. But SMT-Lib has the constant to_real
for casting. Some SMT solvers allow it.

In "smt_real.ML", I'm seeing code like this:

fun abstract abs t =
(case t of
(c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
| (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ t =>
abs t #>> (fn u => SOME (c $ u))
| _ => pair NONE)

It seems to want to do something about division and Int.of_int, but
maybe this setup is somehow bit-rotten or insufficient.

That code is to abstract over division to stay in the LIRA fragment,
e.g., if you have a = 1 / b then you need to get rid of the 1/b.

The better solution is to add a translation of division:

fun mk_divides ts = Term.list_comb (\<^Const>‹divide
\<^Type>‹real››, ts)
fun divides _ _ (ts as [a,b]) =
     if SMT_Util.is_number a andalso SMT_Util.is_number b
     then SOME ("/", 2, ts, mk_divides) else NONE
    | divides _ _ _ = NONE

val setup_builtins =
(*the current things followed by *) #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
    (Term.dest_Const \<^Const>‹divide \<^Type>‹real››, divides) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC)
    [(\<^Const>‹of_int \<^Type>‹real››, "to_real"),
     (\<^Const>‹of_nat \<^Type>‹real››, "to_real")]

Division seems to work but the to_real currently breaks the
reconstruction of proofs: on the Isabelle side, of_int is ambiguous
without looking at the rest of the term. I will look into it.

I'm CC:ing Martin. Maybe he and I could look into both issues
together, if he has time.

In all likelihood, Hanna (CC-ed) and I have looked more recently at
that code (for the BV translation -- even if our changes are all out
of tree). But feel free to do looking into it with Martin if you prefer.

Mathias

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 11. Apr 2025, at 16:29, Manuel Eberl <manuel@pruvisto.org> wrote:

Hello,

yesterday I had a proof obligation that boils down to a LIRA
problem (linear integer/real arithmetic). Usually "linarith" can
solve these just fine, but in this case it couldn't (at least not
in a single step), but I know "linarith" is incomplete for mixed
integer/real problems. I then turned to the "smt" method instead
and to my surprise found that it couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤
x + 1 / 2"
shows   "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
    using assms by linarith
thus ?thesis
    using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and
"linarith" can solve it in two steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))"
all fail, and Z3 even claims there's a (possibly spurious)
counterexample.

Looking at the generated smtlib problem, I found to my surprise
that both the division on the reals and the type conversion
"real_of_int" are translated to uninterpreted functions, so it's
not surprising that the SMT solvers fail to prove it. It's easy to
get rid of the division, of course, but that doesn't make it work
either (presumable because the "of_int" UF is still there).

I would have expected an encoding like the following:

(set-logic AUFLIRA)
(set-option :produce-proofs true)
(declare-fun x () Real)
(declare-fun m () Int)
(assert (and (<= 0 x) (<= x (/ 1 2)) (<= x m) (<= m (+ x (/ 1 2)))))
(assert (not (= m (* 2 x))))
(check-sat)
(get-proof)

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some
unresolved difficulty in replaying LIRA proofs?

Manuel

Email Gateway (Apr 14 2025 at 13:25):

From: Haniel Barbosa <hbarbosa@dcc.ufmg.br>
Hello,

Manuel Eberl <manuel@pruvisto.org> writes:

I didn't know equality between integers and reals was a problem in SMT. I do know that Nelson–Oppen
doesn't like things like that, but I don't know enough about the internals of SMT solvers to understand
whether it is an issue, and I expected SMT solvers to just "abstract away" from this if need be and insert
coercions like "to_real" in a preprocessing step. I mean, my smtlib problem went through just fine without
any errors or warnings, and I even got a proof (although I don't understand enough about SMT proof objects
to be able to see whether it is actually a proof that makes sense and proves what I want).

To clarify this point, internally SMT solvers do overlead arithmetic
operations to mix ints and reals. They are only (generally...) strict
for the input because SMT-LIB does not allow this overloading. And
some can be strict for the output because otherwise it can lead to
issues with some proof checkers or reconstruction in proof assistants.

As soon as the problem is parsed solvers generally do not care about
mixing these types anymore. Which makes it a pain to undo these
implicit mixing if one wants to output proofs that have the explicit
casts, which are added in post-processing. With cvc5 this is done via
the option --proof-elim-subtypes, for example, which is not on by
default.

Best,

Manuel

On 12/04/2025 08:38, Jasmin Blanchette wrote:

Hi Mathias,

In all likelihood, Hanna (CC-ed) and I have looked more recently at that code (for the BV translation --
even if our changes are all out of tree). But feel free to do looking into it with Martin if you prefer.

By all means, you go ahead! Thank you so much. I knew you worked on reconstruction, but I didn't realize
you had such extensive knowledge of the translation.

Best,
Jasmin

--

Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 12. Apr 2025, at 08:34, Mathias Fleury <mathias.fleury12@gmail.com> wrote:

Hi Jasmin, Manuel and all,

On 4/12/25 07:47, Jasmin Blanchette wrote:

Hi Manuel,

SMT was developed by Sascha Böhme, so I'm only partly qualified to answer.

The fragment SMT solvers can decide is linear. Some SMT solvers also support division and have
nonlinear solvers, but these are very slow. As a result, native division is not used, even when it's
between constants like 1 and 2, apparently.

Getting the divide operator translated is easy to add actually.

As for "real_of_int", the uninterpreted symbol is definitely suboptimal. I'm not sure it's safe to just
omit it everywhere and rely on implicit cast or subtyping. SMT-LIB seems to support overloading,
so this is all rather scary.

My understanding is that you cannot omit it due to equality requiring to variables of the same sort.
But SMT-Lib has the constant to_real for casting. Some SMT solvers allow it.

In "smt_real.ML", I'm seeing code like this:

fun abstract abs t =
(case t of
(c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
| (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ t =>
abs t #>> (fn u => SOME (c $ u))
| _ => pair NONE)

It seems to want to do something about division and Int.of_int, but maybe this setup is somehow
bit-rotten or insufficient.

That code is to abstract over division to stay in the LIRA fragment, e.g., if you have a = 1 / b then
you need to get rid of the 1/b.

The better solution is to add a translation of division:

fun mk_divides ts = Term.list_comb (\<^Const>‹divide \<^Type>‹real››, ts)
fun divides _ _ (ts as [a,b]) =
if SMT_Util.is_number a andalso SMT_Util.is_number b
then SOME ("/", 2, ts, mk_divides) else NONE
| divides _ _ _ = NONE

val setup_builtins =
(*the current things followed by *) #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
(Term.dest_Const \<^Const>‹divide \<^Type>‹real››, divides) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC)
[(\<^Const>‹of_int \<^Type>‹real››, "to_real"),
(\<^Const>‹of_nat \<^Type>‹real››, "to_real")]

Division seems to work but the to_real currently breaks the reconstruction of proofs: on the Isabelle
side, of_int is ambiguous without looking at the rest of the term. I will look into it.

I'm CC:ing Martin. Maybe he and I could look into both issues together, if he has time.

In all likelihood, Hanna (CC-ed) and I have looked more recently at that code (for the BV translation --
even if our changes are all out of tree). But feel free to do looking into it with Martin if you prefer.

Mathias

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 11. Apr 2025, at 16:29, Manuel Eberl <manuel@pruvisto.org> wrote:

Hello,

yesterday I had a proof obligation that boils down to a LIRA problem (linear integer/real
arithmetic). Usually "linarith" can solve these just fine, but in this case it couldn't (at least not
in a single step), but I know "linarith" is incomplete for mixed integer/real problems. I then
turned to the "smt" method instead and to my surprise found that it couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤ x + 1 / 2"
shows "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
using assms by linarith
thus ?thesis
using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and "linarith" can solve it in two
steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))" all fail, and Z3 even claims
there's a (possibly spurious) counterexample.

Looking at the generated smtlib problem, I found to my surprise that both the division on the
reals and the type conversion "real_of_int" are translated to uninterpreted functions, so it's not
surprising that the SMT solvers fail to prove it. It's easy to get rid of the division, of course, but
that doesn't make it work either (presumable because the "of_int" UF is still there).

I would have expected an encoding like the following:

(set-logic AUFLIRA)
(set-option :produce-proofs true)
(declare-fun x () Real)
(declare-fun m () Int)
(assert (and (<= 0 x) (<= x (/ 1 2)) (<= x m) (<= m (+ x (/ 1 2)))))
(assert (not (= m (* 2 x))))
(check-sat)
(get-proof)

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some unresolved difficulty in
replaying LIRA proofs?

Manuel

--
Haniel Barbosa
https://hanielbarbosa.com/

Email Gateway (Apr 14 2025 at 17:46):

From: Hanna Elif Lachnitt <lachnitt@stanford.edu>
Hi everyone,

as Mathias wrote, we have been working on extending the translation of machine word problems to SMT-LIB. Our end goal is to support cvc5's proof certificates including those with bit-vectors. I hope we can make this functionality available soon.

Recently, I have been looking into extending the embedding of natural numbers into integers to include not only constants but also variables and functions, so I have been learning a lot about the translation code.

Thus, if you have any other benchmarks for which the translation is suboptimal, I'd be very grateful if you could send them to me (lachnitt@cs.stanford.edu) or Mathias. Same with anything you think should be solvable by an SMT solver but isn't. The cvc5 team is eager to offer good integration with ITPs.

Best,
Hanna

TL;DR: please sent me your SMT benchmarks so I can add them to my test suite

From: Jasmin Blanchette
Sent: Friday, April 11, 2025 23:38
To: Mathias Fleury
Cc: Manuel Eberl; cl-isabelle-users@lists.cam.ac.uk; Martin Desharnais; Hanna Elif Lachnitt
Subject: Re: [isabelle] SMT completeness issue: Failure to prove a true LIRA formula

Hi Mathias,

In all likelihood, Hanna (CC-ed) and I have looked more recently at that code (for the BV translation -- even if our changes are all out of tree). But feel free to do looking into it with Martin if you prefer.

By all means, you go ahead! Thank you so much. I knew you worked on reconstruction, but I didn't realize you had such extensive knowledge of the translation.

Best,
Jasmin

On 12. Apr 2025, at 08:34, Mathias Fleury <mathias.fleury12@gmail.com> wrote:

Hi Jasmin, Manuel and all,

On 4/12/25 07:47, Jasmin Blanchette wrote:
Hi Manuel,

SMT was developed by Sascha Böhme, so I'm only partly qualified to answer.

Getting the divide operator translated is easy to add actually.

My understanding is that you cannot omit it due to equality requiring to variables of the same sort. But SMT-Lib has the constant to_real for casting. Some SMT solvers allow it.

In "smt_real.ML", I'm seeing code like this:

It seems to want to do something about division and Int.of_int, but maybe this setup is somehow bit-rotten or insufficient.

That code is to abstract over division to stay in the LIRA fragment, e.g., if you have a = 1 / b then you need to get rid of the 1/b.

The better solution is to add a translation of division:

fun mk_divides ts = Term.list_comb (\<^Const>‹divide \<^Type>‹real››, ts)
fun divides _ _ (ts as [a,b]) =
if SMT_Util.is_number a andalso SMT_Util.is_number b
then SOME ("/", 2, ts, mk_divides) else NONE
| divides _ _ _ = NONE

val setup_builtins =
(*the current things followed by *) #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
(Term.dest_Const \<^Const>‹divide \<^Type>‹real››, divides) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC)
[(\<^Const>‹of_int \<^Type>‹real››, "to_real"),
(\<^Const>‹of_nat \<^Type>‹real››, "to_real")]

Division seems to work but the to_real currently breaks the reconstruction of proofs: on the Isabelle side, of_int is ambiguous without looking at the rest of the term. I will look into it.

I'm CC:ing Martin. Maybe he and I could look into both issues together, if he has time.

In all likelihood, Hanna (CC-ed) and I have looked more recently at that code (for the BV translation -- even if our changes are all out of tree). But feel free to do looking into it with Martin if you prefer.

Mathias

Best,
Jasmin

On 11. Apr 2025, at 16:29, Manuel Eberl <manuel@pruvisto.org><mailto:manuel@pruvisto.org> wrote:

Hello,

yesterday I had a proof obligation that boils down to a LIRA problem (linear integer/real arithmetic). Usually "linarith" can solve these just fine, but in this case it couldn't (at least not in a single step), but I know "linarith" is incomplete for mixed integer/real problems. I then turned to the "smt" method instead and to my surprise found that it couldn't do it either.

I boiled it down to the following minimal example:

lemma
assumes "0 ≤ x" "x ≤ 1 / 2" "x ≤ real_of_int m" "real_of_int m ≤ x + 1 / 2"
shows "real_of_int m = 2 * x"
proof -
have "m = 0 ∨ m = 1"
using assms by linarith
thus ?thesis
using assms by linarith
qed

As you can see, it's a LIRA problem, it's a true statement, and "linarith" can solve it in two steps.

However, "apply smt", "apply (smt (cvc5))" and "apply (smt (z3))" all fail, and Z3 even claims there's a (possibly spurious) counterexample.

Looking at the generated smtlib problem, I found to my surprise that both the division on the reals and the type conversion "real_of_int" are translated to uninterpreted functions, so it's not surprising that the SMT solvers fail to prove it. It's easy to get rid of the division, of course, but that doesn't make it work either (presumable because the "of_int" UF is still there).

I would have expected an encoding like the following:

Both CVC5 and Z3 can do this and produce proofs.

So, is this some known limitation of the smt method? Is there some unresolved difficulty in replaying LIRA proofs?

Manuel

Last updated: May 06 2025 at 08:28 UTC