# HG changeset patch
# User blanchet
# Date 1406915058 -7200
# Node ID 1649841f3b383de83daf5daea314d01a9ceb2fd5
# Parent  dafecf8fa26613653e4f9011f1e61cf323a77aa3
tuning

diff -r dafecf8fa266 -r 1649841f3b38 src/HOL/Tools/SMT2/verit_proof.ML
--- a/src/HOL/Tools/SMT2/verit_proof.ML	Fri Aug 01 19:36:23 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Fri Aug 01 19:44:18 2014 +0200
@@ -21,9 +21,11 @@
 
   val veriT_step_prefix : string
   val veriT_input_rule: string
+  val veriT_la_generic_rule : string
   val veriT_rewrite_rule : string
+  val veriT_simp_arith_rule : string
+  val veriT_tmp_ite_elim_rule : string
   val veriT_tmp_skolemize_rule : string
-  val veriT_tmp_ite_elim_rule : string
 end;
 
 structure VeriT_Proof: VERIT_PROOF =
@@ -52,11 +54,13 @@
   VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
 
 val veriT_step_prefix = ".c"
+val veriT_alpha_conv_rule = "tmp_alphaconv"
 val veriT_input_rule = "input"
-val veriT_rewrite_rule = "__rewrite" (*arbitrary*)
+val veriT_la_generic_rule = "la_generic"
+val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
+val veriT_simp_arith_rule = "simp_arith"
 val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
 val veriT_tmp_skolemize_rule = "tmp_skolemize"
-val veriT_alpha_conv_rule = "tmp_alphaconv"
 
 (* proof parser *)
 
@@ -66,18 +70,18 @@
   |>> snd
 
 (*in order to get Z3-style quantification*)
-fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) =
-    let val (quantified_vars, t) = split_last (map fix_quantification l)
+fun repair_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) =
+    let val (quantified_vars, t) = split_last (map repair_quantification l)
     in
       SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: [])
     end
-  | fix_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) =
-    let val (quantified_vars, t) = split_last (map fix_quantification l)
+  | repair_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) =
+    let val (quantified_vars, t) = split_last (map repair_quantification l)
     in
       SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: [])
     end
-  | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l)
-  | fix_quantification x = x
+  | repair_quantification (SMTLIB2.S l) = SMTLIB2.S (map repair_quantification l)
+  | repair_quantification x = x
 
 fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var =
     (case List.find (fn v => String.isPrefix v var) free_var of
@@ -188,21 +192,16 @@
     #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub))
     #> rotate_pair
     ##> parse_conclusion
-    ##> map fix_quantification
+    ##> map repair_quantification
     #> (fn ((((id, rule), prems), (subproof, cx)), terms) =>
          (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx)))
-    (*the conclusion is the empty list, ie no false is written, we have to add it.*)
-    ##> (apfst (fn [] => (@{const False}, [])
-                 | concls => make_or_from_clausification concls))
+    ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls)
     #> fix_subproof_steps
     ##> to_node
     #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
-    #-> (fold_map update_step_and_cx)
+    #-> fold_map update_step_and_cx
   end
 
-
-(*function related to parsing and general transformation*)
-
 (*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are
 unbalanced on each line*)
 fun seperate_into_steps lines =
@@ -222,9 +221,8 @@
     seperate lines "" 0
   end
 
- (*VeriT adds @ before every variable.*)
-fun remove_all_at (SMTLIB2.Sym v :: l) =
-    SMTLIB2.Sym (if nth_string v 0 = "@" then String.extract (v, 1, NONE) else v) :: remove_all_at l
+ (* VeriT adds @ before every variable. *)
+fun remove_all_at (SMTLIB2.Sym v :: l) = SMTLIB2.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
   | remove_all_at (SMTLIB2.S l :: l') = SMTLIB2.S (remove_all_at l) :: remove_all_at l'
   | remove_all_at (SMTLIB2.Key v :: l) = SMTLIB2.Key v :: remove_all_at l
   | remove_all_at (v :: l) = v :: remove_all_at l
@@ -278,12 +276,10 @@
   | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
   | find_ite_var_in_term _ = NONE
 
-
 fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) =
   if rule = veriT_tmp_ite_elim_rule then
     if bounds = [] then
-      (*if the introduced var has already been defined,
-        adding the definition as a dependency*)
+      (*if the introduced var has already been defined, adding the definition as a dependency*)
       let
         val new_prems =
           (case find_ite_var_in_term concl of
@@ -302,7 +298,6 @@
   else
     st
 
-(*remove alpha conversion step, that just renames the variables*)
 fun remove_alpha_conversion _ [] = []
   | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
     let
@@ -323,7 +318,6 @@
   |> map (correct_veriT_step steps)
   |> remove_alpha_conversion Symtab.empty
 
-(* overall proof parser *)
 fun parse typs funs lines ctxt =
   let
     val smtlib2_lines_without_at =
diff -r dafecf8fa266 -r 1649841f3b38 src/HOL/Tools/SMT2/z3_new_proof.ML
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Aug 01 19:36:23 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Fri Aug 01 19:44:18 2014 +0200
@@ -100,7 +100,7 @@
     SOME rule => rule
   | NONE => error ("unknown Z3 proof rule " ^ quote name))
 
-fun string_of_rule (Th_Lemma kind) = "th-lemma " ^ kind
+fun string_of_rule (Th_Lemma kind) = "th-lemma" ^ (if kind = "" then "" else " " ^ kind)
   | string_of_rule r =
       let fun eq_rule (s, r') = if r = r' then SOME s else NONE
       in the (Symtab.get_first eq_rule rule_names) end
diff -r dafecf8fa266 -r 1649841f3b38 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 19:36:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 19:44:18 2014 +0200
@@ -56,7 +56,7 @@
 val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
 val veriT_tmp_skolemize_rule = "tmp_skolemize"
 val z3_skolemize_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Skolemize
-val z3_th_lemma_rule = "th-lemma"
+val z3_th_lemma_rule_prefix = Z3_New_Proof.string_of_rule (Z3_New_Proof.Th_Lemma "")
 val zipperposition_cnf_rule = "cnf"
 
 val skolemize_rules =
@@ -66,7 +66,7 @@
 
 val is_skolemize_rule = member (op =) skolemize_rules
 fun is_arith_rule rule =
-  String.isPrefix z3_th_lemma_rule rule orelse rule = veriT_simp_arith_rule orelse
+  String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
   rule = veriT_la_generic_rule
 val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule