Re: [isabelle] SMT and bound variables.



Hey Lars.

I'm not sure if proof reconstruction is now available for bitvectors. Sascha and I looked at the problem a few years ago, and the conclusion was it was doable but the performance was a tad disappointing.

The tactic we implemented to help discharge the theory-lemmas appearing in bitvector proofs *is* available, and should be in your context under the name word_bitwise. It does the bitwise expansion of your problem and some minor simplification. Together with real simplification it solves both of these problems, although a bit slowly.

Thomas.

On 06/07/13 03:21, Lars Noschinski wrote:
Hi,

I'm getting annoyed by the tediousness required to discharge seemingly trivial problems on words and thought I would try the "smt" method on them.

(BTW: Is proof reconstruction available for Bitvectors?)

I found a strange behaviour (in 2012, 2013 and ffc3f1659a25): Consider the two goals stated below. They are equivalent, the only difference is between free and bound variables. Yet "smt" can only solve the second goal and suggests a possibly spurious counter-example for the first one.

--------------------------------------------------------------------------
theory Scratch imports "~~/src/HOL/Word/Word" begin

lemma "⋀degree k. (degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
  using [[smt_oracle=true]]
  apply smt (* Fails, talks about possibly spurious counter-example *)
  oops

lemma "(degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
  using [[smt_oracle=true]]
  apply smt (* Succeeds *)
  done
--------------------------------------------------------------------------

Is this some known limitation or a bug in the preprocessing?

Best regards,
  Lars






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