Re: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer



On 16/05/2019 10:03, Mathias Fleury wrote:
> 
> I think I have found the problem for Z3, but I cannot explain why it would appear now.
> 
> SMT (directly or via Sledgehammer) starts z3 with a timeout of XXs. However, SMT sees the answer "timeout" (as given by Z3) an error. So basically, it a timing issue: if SMT kills the call to the solver, everything is fine. Otherwise, it fails.
> 
> I don't know what happens for CVC4, I have not managed to reproduce the issue.
> 
> Can you try the attached patch?

I have experimented with the included session definition for SMT_Test,
with and without the changeset supprt_timeout (e.g. against
Isabelle2019-RC3). The results are as follows:

  * On my pretty fast home machine (8 cores, fast RAW, fast SSD/MVMe) it
works fine in both situations: there are occasional z3 timeouts but no
errors.

  * On my Sony Vaio from 2013 there are sporadic prover errors, with the
patch they become regular timeouts.

I am unsure what to do now (approx. 2 weeks before the final launch of
the release).

Are these prover errors more than just odd noise in the output?


	Makarius
session SMT_Test = "HOL-Word" +
  options [quick_and_dirty]
  theories Test
theory Test
   imports "HOL-Word.More_Word"
begin

lemma " n < 2 ^ (LENGTH('l::len) - Suc 0) \<Longrightarrow> msb (word_of_int (int n)) \<Longrightarrow> False"
  supply [[smt_trace]]
  sledgehammer unlearn
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sledgehammer [provers=z3]
  sorry

end
# HG changeset patch
# Parent  8feae28e5c449b43a4c0131d1aca8386b788779b
support timeouts as return code

diff -r 8feae28e5c44 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri May 03 20:35:19 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu May 16 09:36:50 2019 +0200
@@ -7,7 +7,7 @@
 signature SMT_SOLVER =
 sig
   (*configuration*)
-  datatype outcome = Unsat | Sat | Unknown
+  datatype outcome = Unsat | Sat | Unknown | Time_Out
 
   type parsed_proof =
     {outcome: SMT_Failure.failure option,
@@ -138,7 +138,7 @@
 
 (* configuration *)
 
-datatype outcome = Unsat | Sat | Unknown
+datatype outcome = Unsat | Sat | Unknown | Time_Out
 
 type parsed_proof =
   {outcome: SMT_Failure.failure option,
@@ -198,6 +198,7 @@
         (case parse_proof0 of
           SOME pp => pp outer_ctxt replay_data xfacts prems concl lines
         | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []})
+    | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   fun replay outcome replay0 oracle outer_ctxt
@@ -211,6 +212,7 @@
             SOME replay => replay outer_ctxt replay_data lines
           | NONE => error "No proof reconstruction for solver -- \
             \declare [[smt_oracle]] to allow oracle")
+    | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   val cfalse = Thm.cterm_of \<^context> \<^prop>\<open>False\<close>
diff -r 8feae28e5c44 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Fri May 03 20:35:19 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu May 16 09:36:50 2019 +0200
@@ -19,10 +19,11 @@
 
 fun make_command name () = [getenv (name ^ "_SOLVER")]
 
-fun outcome_of unsat sat unknown solver_name line =
+fun outcome_of unsat sat unknown timeout solver_name line =
   if String.isPrefix unsat line then SMT_Solver.Unsat
   else if String.isPrefix sat line then SMT_Solver.Sat
   else if String.isPrefix unknown line then SMT_Solver.Unknown
+  else if String.isPrefix timeout line then SMT_Solver.Time_Out
   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
     " option for details"))
@@ -56,7 +57,7 @@
   options = cvc3_options,
   smt_options = [],
   default_max_relevant = 400 (* FUDGE *),
-  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = NONE,
   replay = NONE }
 
@@ -96,7 +97,7 @@
   options = cvc4_options,
   smt_options = [(":produce-unsat-cores", "true")],
   default_max_relevant = 400 (* FUDGE *),
-  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
   replay = NONE }
 
@@ -127,7 +128,7 @@
     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
-  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }
 
@@ -157,7 +158,7 @@
   options = z3_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 350 (* FUDGE *),
-  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME Z3_Replay.parse_proof,
   replay = SOME Z3_Replay.replay }
 


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