Basic support for the SMT prover veriT.
authorfleury
Wed Jul 30 14:03:12 2014 +0200 (2014-07-30)
changeset 57704c0da3fc313e3
parent 57703 fefe3ea75289
child 57705 5da48dae7d03
Basic support for the SMT prover veriT.
src/HOL/SMT2.thy
src/HOL/Tools/SMT2/smt2_systems.ML
src/HOL/Tools/SMT2/smtlib2.ML
src/HOL/Tools/SMT2/smtlib2_interface.ML
src/HOL/Tools/SMT2/smtlib2_isar.ML
src/HOL/Tools/SMT2/verit_isar.ML
src/HOL/Tools/SMT2/verit_proof.ML
src/HOL/Tools/SMT2/verit_proof_parse.ML
src/HOL/Tools/SMT2/z3_new_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     1.1 --- a/src/HOL/SMT2.thy	Wed Jul 30 14:03:11 2014 +0200
     1.2 +++ b/src/HOL/SMT2.thy	Wed Jul 30 14:03:12 2014 +0200
     1.3 @@ -108,6 +108,7 @@
     1.4  ML_file "Tools/SMT2/smtlib2.ML"
     1.5  ML_file "Tools/SMT2/smtlib2_interface.ML"
     1.6  ML_file "Tools/SMT2/smtlib2_proof.ML"
     1.7 +ML_file "Tools/SMT2/smtlib2_isar.ML"
     1.8  ML_file "Tools/SMT2/z3_new_proof.ML"
     1.9  ML_file "Tools/SMT2/z3_new_isar.ML"
    1.10  ML_file "Tools/SMT2/smt2_solver.ML"
    1.11 @@ -117,6 +118,9 @@
    1.12  ML_file "Tools/SMT2/z3_new_replay_rules.ML"
    1.13  ML_file "Tools/SMT2/z3_new_replay_methods.ML"
    1.14  ML_file "Tools/SMT2/z3_new_replay.ML"
    1.15 +ML_file "Tools/SMT2/verit_proof.ML"
    1.16 +ML_file "Tools/SMT2/verit_isar.ML"
    1.17 +ML_file "Tools/SMT2/verit_proof_parse.ML"
    1.18  ML_file "Tools/SMT2/smt2_systems.ML"
    1.19  
    1.20  method_setup smt2 = {*
     2.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:11 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:12 2014 +0200
     2.3 @@ -37,6 +37,8 @@
     2.4      val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines))
     2.5    in (test_outcome solver_name l, ls) end
     2.6  
     2.7 +fun on_first_non_unsupported_line test_outcome solver_name lines =
     2.8 +  on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
     2.9  
    2.10  (* CVC3 *)
    2.11  
    2.12 @@ -85,6 +87,26 @@
    2.13  
    2.14  end
    2.15  
    2.16 +(* veriT *)
    2.17 +
    2.18 +val veriT: SMT2_Solver.solver_config = {
    2.19 +  name = "veriT",
    2.20 +  class = K SMTLIB2_Interface.smtlib2C,
    2.21 +  avail = make_avail "VERIT",
    2.22 +  command = make_command "VERIT",
    2.23 +  options = (fn ctxt => [
    2.24 +    "--proof-version=1",
    2.25 +    "--proof=-",
    2.26 +    "--proof-prune",
    2.27 +    "--proof-merge",
    2.28 +    "--disable-print-success",
    2.29 +    "--disable-banner",
    2.30 +    "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]),
    2.31 +  smt_options = [],
    2.32 +  default_max_relevant = 350 (* FUDGE *),
    2.33 +  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"),
    2.34 +  parse_proof = SOME VeriT_Proof_Parse.parse_proof,
    2.35 +  replay = NONE }
    2.36  
    2.37  (* Z3 *)
    2.38  
    2.39 @@ -160,6 +182,7 @@
    2.40  val _ = Theory.setup (
    2.41    SMT2_Solver.add_solver cvc3 #>
    2.42    SMT2_Solver.add_solver cvc4 #>
    2.43 +  SMT2_Solver.add_solver veriT #>
    2.44    SMT2_Solver.add_solver z3)
    2.45  
    2.46  end;
     3.1 --- a/src/HOL/Tools/SMT2/smtlib2.ML	Wed Jul 30 14:03:11 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smtlib2.ML	Wed Jul 30 14:03:12 2014 +0200
     3.3 @@ -118,7 +118,7 @@
     3.4        read l cs None ((S (rev ts1) :: ts2) :: tss)
     3.5    | read l ("#" :: "x" :: cs) None (ts :: tss) =
     3.6        token read_hex l cs ts tss
     3.7 -  | read l ("#" :: cs) None (ts :: tss) =
     3.8 +  | read l ("#" :: "b" :: cs) None (ts :: tss) =
     3.9        token read_bin l cs ts tss
    3.10    | read l (":" :: cs) None (ts :: tss) =
    3.11        token (read_sym Key) l cs ts tss
     4.1 --- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Wed Jul 30 14:03:11 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Wed Jul 30 14:03:12 2014 +0200
     4.3 @@ -11,6 +11,7 @@
     4.4    val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
     4.5    val translate_config: Proof.context -> SMT2_Translate.config
     4.6    val assert_index_of_name: string -> int
     4.7 +  val assert_prefix : string
     4.8  end;
     4.9  
    4.10  structure SMTLIB2_Interface: SMTLIB2_INTERFACE =
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:12 2014 +0200
     5.3 @@ -0,0 +1,99 @@
     5.4 +(*  Title:      HOL/Tools/SMT2/smtlib2_isar.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Author:     Mathias Fleury, ENS Rennes
     5.7 +
     5.8 +General tools for Isar proof reconstruction.
     5.9 +*)
    5.10 +
    5.11 +signature SMTLIB2_ISAR =
    5.12 +sig
    5.13 +  val simplify_bool: term -> term
    5.14 +  val unlift_term: term list -> term -> term
    5.15 +  val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term
    5.16 +  val normalize_prems : Proof.context -> term -> (string * string list) list
    5.17 +  val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
    5.18 +    (''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c
    5.19 +
    5.20 +end;
    5.21 +
    5.22 +structure SMTLIB2_Isar: SMTLIB2_ISAR =
    5.23 +struct
    5.24 +
    5.25 +open ATP_Problem
    5.26 +open ATP_Util
    5.27 +
    5.28 +fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
    5.29 +    let val t' = simplify_bool t in
    5.30 +      if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
    5.31 +    end
    5.32 +  | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
    5.33 +  | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
    5.34 +  | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
    5.35 +  | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
    5.36 +  | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
    5.37 +  | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
    5.38 +    if u aconv v then @{const True} else t
    5.39 +  | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
    5.40 +  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
    5.41 +  | simplify_bool t = t
    5.42 +
    5.43 +fun strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T)
    5.44 +  | strip_alls t = ([], t)
    5.45 +
    5.46 +fun push_skolem_all_under_iff t =
    5.47 +  (case strip_alls t of
    5.48 +    (qs as _ :: _,
    5.49 +     (t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) =>
    5.50 +    t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
    5.51 +  | _ => t)
    5.52 +
    5.53 +(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
    5.54 +val unskolemize_names =
    5.55 +  Term.map_abs_vars (perhaps (try Name.dest_skolem))
    5.56 +  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
    5.57 +
    5.58 +fun unlift_term ll_defs =
    5.59 +  let
    5.60 +    val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
    5.61 +
    5.62 +    fun un_free (t as Free (s, _)) =
    5.63 +       (case AList.lookup (op =) lifted s of
    5.64 +         SOME t => un_term t
    5.65 +       | NONE => t)
    5.66 +     | un_free t = t
    5.67 +    and un_term t = map_aterms un_free t
    5.68 +  in un_term end
    5.69 +
    5.70 +fun postprocess_step_conclusion concl thy rewrite_rules ll_defs =
    5.71 +  concl
    5.72 +  |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    5.73 +  |> Object_Logic.atomize_term thy
    5.74 +  |> simplify_bool
    5.75 +  |> not (null ll_defs) ? unlift_term ll_defs
    5.76 +  |> unskolemize_names
    5.77 +  |> push_skolem_all_under_iff
    5.78 +  |> HOLogic.mk_Trueprop
    5.79 +
    5.80 +fun normalize_prems ctxt concl0 =
    5.81 +  SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
    5.82 +  SMT2_Normalize.abs_min_max_table
    5.83 +  |> map_filter (fn (c, th) =>
    5.84 +    if exists_Const (curry (op =) c o fst) concl0 then
    5.85 +      let val s = short_thm_name ctxt th in SOME (s, [s]) end
    5.86 +    else
    5.87 +      NONE)
    5.88 +
    5.89 +fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t
    5.90 +    t =
    5.91 +  (case ss of
    5.92 +    [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
    5.93 +  | _ =>
    5.94 +    if id = conjecture_id then
    5.95 +      (Conjecture, concl_t)
    5.96 +    else
    5.97 +      (Hypothesis,
    5.98 +       (case find_index (curry (op =) id) prem_ids of
    5.99 +         ~1 => t
   5.100 +       | i => nth hyp_ts i)))
   5.101 +
   5.102 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/SMT2/verit_isar.ML	Wed Jul 30 14:03:12 2014 +0200
     6.3 @@ -0,0 +1,58 @@
     6.4 +(*  Title:      HOL/Tools/SMT2/verit_isar.ML
     6.5 +    Author:     Mathias Fleury, TU Muenchen
     6.6 +    Author:     Jasmin Blanchette, TU Muenchen
     6.7 +
     6.8 +VeriT proofs as generic ATP proofs for Isar proof reconstruction.
     6.9 +*)
    6.10 +
    6.11 +signature VERIT_ISAR =
    6.12 +sig
    6.13 +  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
    6.14 +  val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term ->
    6.15 +    (string * term) list -> int list -> int -> (int * string) list -> VeriT_Proof.veriT_step list ->
    6.16 +    (term, string) ATP_Proof.atp_step list
    6.17 +end;
    6.18 +
    6.19 +structure VeriT_Isar: VERIT_ISAR =
    6.20 +struct
    6.21 +
    6.22 +open ATP_Util
    6.23 +open ATP_Problem
    6.24 +open ATP_Proof
    6.25 +open ATP_Proof_Reconstruct
    6.26 +open SMTLIB2_Isar
    6.27 +open VeriT_Proof
    6.28 +
    6.29 +fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
    6.30 +    conjecture_id fact_helper_ids proof =
    6.31 +  let
    6.32 +    val thy = Proof_Context.theory_of ctxt
    6.33 +
    6.34 +    fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
    6.35 +      let
    6.36 +        val sid = string_of_int id
    6.37 +        val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
    6.38 +        fun standard_step role =
    6.39 +          ((sid, []), role, concl', rule,
    6.40 +           map (fn id => (id, [])) prems)
    6.41 +      in
    6.42 +        if rule = verit_proof_input_rule then
    6.43 +          let
    6.44 +            val ss = the_list (AList.lookup (op =) fact_helper_ids id)
    6.45 +            val name0 = (sid ^ "a", ss)
    6.46 +            val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids
    6.47 +              fact_helper_ts hyp_ts concl_t concl
    6.48 +
    6.49 +            val normalizing_prems = normalize_prems ctxt concl0
    6.50 +          in
    6.51 +            [(name0, role0, concl0, rule, []),
    6.52 +             ((sid, []), Plain, concl', verit_rewrite,
    6.53 +              name0 :: normalizing_prems)] end
    6.54 +        else
    6.55 +          [standard_step Plain]
    6.56 +      end
    6.57 +  in
    6.58 +    maps steps_of proof
    6.59 +  end
    6.60 +
    6.61 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     7.3 @@ -0,0 +1,135 @@
     7.4 +(*  Title:      HOL/Tools/SMT2/verit_proof.ML
     7.5 +    Author:     Mathias Fleury, ENS Rennes
     7.6 +    Author:     Sascha Boehme, TU Muenchen
     7.7 +
     7.8 +VeriT proofs: parsing and abstract syntax tree.
     7.9 +*)
    7.10 +
    7.11 +signature VERIT_PROOF =
    7.12 +sig
    7.13 +  (*proofs*)
    7.14 +  datatype veriT_step = VeriT_Step of {
    7.15 +    id: int,
    7.16 +    rule: string,
    7.17 +    prems: string list,
    7.18 +    concl: term,
    7.19 +    fixes: string list}
    7.20 +
    7.21 +  (*proof parser*)
    7.22 +  val parse: typ Symtab.table -> term Symtab.table -> string list ->
    7.23 +    Proof.context -> veriT_step list * Proof.context
    7.24 +
    7.25 +  val verit_step_prefix : string
    7.26 +  val verit_proof_input_rule: string
    7.27 +  val verit_rewrite : string
    7.28 +end;
    7.29 +
    7.30 +structure VeriT_Proof: VERIT_PROOF =
    7.31 +struct
    7.32 +
    7.33 +open SMTLIB2_Proof
    7.34 +
    7.35 +(* proof rules *)
    7.36 +
    7.37 +datatype veriT_node = VeriT_Node of {
    7.38 +  id: int,
    7.39 +  rule: string,
    7.40 +  prems: string list,
    7.41 +  concl: term,
    7.42 +  bounds: string list}
    7.43 +
    7.44 +fun mk_node id rule prems concl bounds =
    7.45 +  VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
    7.46 +
    7.47 +(*two structures needed*)
    7.48 +datatype veriT_step = VeriT_Step of {
    7.49 +  id: int,
    7.50 +  rule: string,
    7.51 +  prems: string list,
    7.52 +  concl: term,
    7.53 +  fixes: string list}
    7.54 +
    7.55 +fun mk_step id rule prems concl fixes =
    7.56 +  VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
    7.57 +
    7.58 +val verit_step_prefix = ".c"
    7.59 +val verit_proof_input_rule = "input"
    7.60 +val verit_rewrite = "rewrite"
    7.61 +
    7.62 +(* proof parser *)
    7.63 +
    7.64 +fun node_of p cx =
    7.65 +  ([], cx)
    7.66 +  ||>> with_fresh_names (term_of p)
    7.67 +  ||>> next_id
    7.68 +  |>> (fn ((prems, (t, ns)), id) => mk_node id verit_proof_input_rule prems t ns)
    7.69 +
    7.70 +(*in order to get Z3-style quantification*)
    7.71 +fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) =
    7.72 +    let
    7.73 +      val (quantified_vars, t) = split_last (map fix_quantification l)
    7.74 +    in
    7.75 +      SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: [])
    7.76 +    end
    7.77 +  | fix_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) =
    7.78 +    let val (quantified_vars, t) = split_last (map fix_quantification l)
    7.79 +    in
    7.80 +      SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: [])
    7.81 +    end
    7.82 +  | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l)
    7.83 +  | fix_quantification x = x
    7.84 +
    7.85 +fun parse_proof cx =
    7.86 +  let
    7.87 +    fun rotate_pair (a, (b, c)) = ((a, b), c)
    7.88 +    fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l)
    7.89 +      | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t)
    7.90 +    fun change_id_to_number x = (unprefix verit_step_prefix #> Int.fromString #> the) x
    7.91 +    fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l)
    7.92 +    fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) =
    7.93 +        (SOME (map (fn (SMTLIB2.Sym id) => id) source), l)
    7.94 +      | parse_source l = (NONE, l)
    7.95 +    fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l
    7.96 +      | skip_args l = l
    7.97 +
    7.98 +    fun parse_conclusion [SMTLIB2.Key "conclusion", SMTLIB2.S concl] = concl
    7.99 +
   7.100 +    fun make_or_from_clausification l =
   7.101 +      foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => (HOLogic.mk_disj (concl1, concl2),
   7.102 +        bounds1 @ bounds2)) l
   7.103 +    (*the conclusion is empty, ie no false*)
   7.104 +    fun to_node ((((id, rule), prems), ([], cx))) = (mk_node id rule (the_default [] prems)
   7.105 +          @{const False} [], cx)
   7.106 +      | to_node ((((id, rule), prems), (concls, cx))) =
   7.107 +        let val (concl, bounds) = make_or_from_clausification concls in
   7.108 +          (mk_node id rule (the_default [] prems) concl bounds, cx) end
   7.109 +  in
   7.110 +    get_id
   7.111 +    #>> change_id_to_number
   7.112 +    ##> parse_rule
   7.113 +    #> rotate_pair
   7.114 +    ##> parse_source
   7.115 +    #> rotate_pair
   7.116 +    ##> skip_args
   7.117 +    ##> parse_conclusion
   7.118 +    ##> map fix_quantification
   7.119 +    ##> (fn terms => fold_map (fn t => fn cx => node_of t cx) terms cx)
   7.120 +    ##> apfst (map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds)))
   7.121 +    #> to_node
   7.122 +  end
   7.123 +
   7.124 +
   7.125 +(* overall proof parser *)
   7.126 +fun parse typs funs lines ctxt =
   7.127 +  let
   7.128 +    val (u, env) =
   7.129 +     fold_map (fn l => fn cx => parse_proof cx l) (map (fn f => SMTLIB2.parse [f]) lines)
   7.130 +     (empty_context ctxt typs funs)
   7.131 +    val t =
   7.132 +     map (fn (VeriT_Node {id, rule, prems, concl, bounds, ...}) =>
   7.133 +       mk_step id rule prems concl bounds) u
   7.134 +  in
   7.135 +    (t, ctxt_of env)
   7.136 +  end
   7.137 +
   7.138 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML	Wed Jul 30 14:03:12 2014 +0200
     8.3 @@ -0,0 +1,100 @@
     8.4 +(*  Title:      HOL/Tools/SMT2/verit_proof_parse.ML
     8.5 +    Author:     Mathias Fleury, TU Muenchen
     8.6 +    Author:     Jasmin Blanchette, TU Muenchen
     8.7 +
     8.8 +VeriT proof parsing.
     8.9 +*)
    8.10 +
    8.11 +signature VERIT_PROOF_PARSE =
    8.12 +sig
    8.13 +  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
    8.14 +  val parse_proof: Proof.context -> SMT2_Translate.replay_data ->
    8.15 +    ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
    8.16 +    SMT2_Solver.parsed_proof
    8.17 +end;
    8.18 +
    8.19 +structure VeriT_Proof_Parse: VERIT_PROOF_PARSE =
    8.20 +struct
    8.21 +
    8.22 +open ATP_Util
    8.23 +open ATP_Problem
    8.24 +open ATP_Proof
    8.25 +open ATP_Proof_Reconstruct
    8.26 +open VeriT_Isar
    8.27 +open VeriT_Proof
    8.28 +
    8.29 +fun find_and_add_missing_dependances steps assms conjecture_id =
    8.30 +  let
    8.31 +    fun prems_to_theorem_number [] id repl = (([], []), (id, repl))
    8.32 +      | prems_to_theorem_number (x :: ths) id replaced =
    8.33 +        (case Int.fromString (perhaps (try (unprefix SMTLIB2_Interface.assert_prefix)) x) of
    8.34 +          NONE =>
    8.35 +          let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced
    8.36 +          in
    8.37 +            ((perhaps (try (unprefix verit_step_prefix)) x :: prems, iidths), (id', replaced'))
    8.38 +          end
    8.39 +        | SOME th =>
    8.40 +          (case Option.map snd (List.find (fst #> curry (op =) x) replaced) of
    8.41 +            NONE =>
    8.42 +            let
    8.43 +              val id' = if th = conjecture_id then 0 else id - conjecture_id
    8.44 +              val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths
    8.45 +                                                          (if th = 0 then id + 1 else id)
    8.46 +                                                          ((x, string_of_int id') :: replaced)
    8.47 +            in ((string_of_int id' :: prems, (th, (id', th)) :: iidths), (id'', replaced')) end
    8.48 +          | SOME x =>
    8.49 +            let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced
    8.50 +            in ((x :: prems, iidths), (id', replaced')) end))
    8.51 +    fun update_step (VeriT_Proof.VeriT_Step {prems, id = id0, rule = rule0,
    8.52 +        concl = concl0, fixes = fixes0}) (id, replaced) =
    8.53 +      let val ((prems', iidths), (id', replaced)) = prems_to_theorem_number prems id replaced
    8.54 +      in
    8.55 +        ((VeriT_Proof.VeriT_Step {id = id0, rule = rule0, prems = prems', concl = concl0,
    8.56 +           fixes = fixes0}, iidths), (id', replaced))
    8.57 +      end
    8.58 +  in
    8.59 +    fold_map update_step steps (1, [])
    8.60 +    |> fst
    8.61 +    |> `(map snd)
    8.62 +    ||> (map fst)
    8.63 +    |>> flat
    8.64 +    |>> map (fn (_, (id, tm_id)) => let val (i, tm) = nth assms tm_id in (i, (id, tm)) end)
    8.65 +  end
    8.66 +
    8.67 +fun add_missing_steps iidths =
    8.68 +  let
    8.69 +    fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = id, rule = "input",
    8.70 +      prems = [], concl = prop_of th, fixes = []}
    8.71 +  in map add_single_step iidths end
    8.72 +
    8.73 +fun parse_proof _
    8.74 +    ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT2_Translate.replay_data)
    8.75 +    xfacts prems concl output =
    8.76 +  let
    8.77 +    val conjecture_i = length ll_defs
    8.78 +    val (steps, _) = VeriT_Proof.parse typs terms output ctxt
    8.79 +    val (iidths, steps'') = find_and_add_missing_dependances steps assms conjecture_i
    8.80 +    val steps' = add_missing_steps iidths @ steps''
    8.81 +    fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i))
    8.82 +
    8.83 +    val prems_i = 1
    8.84 +    val facts_i = prems_i + length prems
    8.85 +
    8.86 +    val conjecture_id = id_of_index conjecture_i
    8.87 +    val prem_ids = map id_of_index (prems_i upto facts_i - 1)
    8.88 +    val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths
    8.89 +
    8.90 +    val fact_ids = map_filter (fn (i, (id, _)) =>
    8.91 +      (try (apsnd (nth xfacts)) (id, i - facts_i))) iidths
    8.92 +    val fact_helper_ts =
    8.93 +      map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @
    8.94 +      map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids
    8.95 +    val fact_helper_ids =
    8.96 +      map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids
    8.97 +  in
    8.98 +    {outcome = NONE, fact_ids = fact_ids,
    8.99 +     atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
   8.100 +       fact_helper_ts prem_ids conjecture_id fact_helper_ids steps'}
   8.101 +  end
   8.102 +
   8.103 +end;
     9.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Wed Jul 30 14:03:11 2014 +0200
     9.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Wed Jul 30 14:03:12 2014 +0200
     9.3 @@ -18,6 +18,7 @@
     9.4  open ATP_Problem
     9.5  open ATP_Proof
     9.6  open ATP_Proof_Reconstruct
     9.7 +open SMTLIB2_Isar
     9.8  
     9.9  val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def
    9.10  val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis
    9.11 @@ -62,69 +63,16 @@
    9.12            end
    9.13        end
    9.14  
    9.15 -fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
    9.16 -    let val t' = simplify_bool t in
    9.17 -      if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
    9.18 -    end
    9.19 -  | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
    9.20 -  | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
    9.21 -  | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
    9.22 -  | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
    9.23 -  | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
    9.24 -  | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
    9.25 -    if u aconv v then @{const True} else t
    9.26 -  | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
    9.27 -  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
    9.28 -  | simplify_bool t = t
    9.29 -
    9.30 -(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
    9.31 -val unskolemize_names =
    9.32 -  Term.map_abs_vars (perhaps (try Name.dest_skolem))
    9.33 -  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
    9.34 -
    9.35 -fun strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T)
    9.36 -  | strip_alls t = ([], t)
    9.37 -
    9.38 -fun push_skolem_all_under_iff t =
    9.39 -  (case strip_alls t of
    9.40 -    (qs as _ :: _,
    9.41 -     (t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) =>
    9.42 -    t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
    9.43 -  | _ => t)
    9.44 -
    9.45 -fun unlift_term ll_defs =
    9.46 -  let
    9.47 -    val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
    9.48 -
    9.49 -    fun un_free (t as Free (s, _)) =
    9.50 -       (case AList.lookup (op =) lifted s of
    9.51 -         SOME t => un_term t
    9.52 -       | NONE => t)
    9.53 -     | un_free t = t
    9.54 -    and un_term t = map_aterms un_free t
    9.55 -  in un_term end
    9.56 -
    9.57  fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
    9.58      conjecture_id fact_helper_ids proof =
    9.59    let
    9.60      val thy = Proof_Context.theory_of ctxt
    9.61  
    9.62 -    val unlift_term = unlift_term ll_defs
    9.63 -
    9.64      fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    9.65        let
    9.66          val sid = string_of_int id
    9.67  
    9.68 -        val concl' =
    9.69 -          concl
    9.70 -          |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    9.71 -          |> Object_Logic.atomize_term thy
    9.72 -          |> simplify_bool
    9.73 -          |> not (null ll_defs) ? unlift_term
    9.74 -          |> unskolemize_names
    9.75 -          |> push_skolem_all_under_iff
    9.76 -          |> HOLogic.mk_Trueprop
    9.77 -
    9.78 +        val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
    9.79          fun standard_step role =
    9.80            ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
    9.81             map (fn id => (string_of_int id, [])) prems)
    9.82 @@ -136,30 +84,15 @@
    9.83              val name0 = (sid ^ "a", ss)
    9.84  
    9.85              val (role0, concl0) =
    9.86 -              (case ss of
    9.87 -                [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
    9.88 -              | _ =>
    9.89 -                if id = conjecture_id then
    9.90 -                  (Conjecture, concl_t)
    9.91 -                else
    9.92 -                  (Hypothesis,
    9.93 -                   (case find_index (curry (op =) id) prem_ids of
    9.94 -                     ~1 => concl
    9.95 -                   | i => nth hyp_ts i)))
    9.96 +              distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
    9.97 +              hyp_ts concl_t concl
    9.98  
    9.99 -            val normalize_prems =
   9.100 -              SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
   9.101 -              SMT2_Normalize.abs_min_max_table
   9.102 -              |> map_filter (fn (c, th) =>
   9.103 -                if exists_Const (curry (op =) c o fst) concl0 then
   9.104 -                  let val s = short_thm_name ctxt th in SOME (s, [s]) end
   9.105 -                else
   9.106 -                  NONE)
   9.107 +            val normalizing_prems = normalize_prems ctxt concl0
   9.108            in
   9.109              (if role0 = Axiom then []
   9.110               else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
   9.111              [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
   9.112 -              name0 :: normalize_prems)]
   9.113 +              name0 :: normalizing_prems)]
   9.114            end
   9.115          | Z3_New_Proof.Rewrite => [standard_step Lemma]
   9.116          | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:11 2014 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:12 2014 +0200
    10.3 @@ -57,7 +57,7 @@
    10.4  
    10.5  val skolemize_rules =
    10.6    [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
    10.7 -zipperposition_cnf_rule, leo2_extcnf_combined_rule]
    10.8 +zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_skomelisation_rule]
    10.9  
   10.10  val is_skolemize_rule = member (op =) skolemize_rules
   10.11  val is_arith_rule = String.isPrefix z3_th_lemma_rule
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 14:03:11 2014 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 14:03:12 2014 +0200
    11.3 @@ -258,6 +258,7 @@
    11.4  
    11.5  val canonical_isar_supported_prover = eN
    11.6  val z3N = "z3"
    11.7 +val veriT_newN = "veriT"
    11.8  
    11.9  fun isar_supported_prover_of thy name =
   11.10    if is_atp thy name orelse name = z3N then name