fixing premises in veriT proof reconstruction
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Nov 10 17:49:54 2015 +0100 (2015-11-10)
changeset 61611a9c0572109af
parent 61610 4f54d2759a0b
child 61612 40859aa6d10c
fixing premises in veriT proof reconstruction
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/SMT/verit_proof.ML
     1.1 --- a/src/HOL/SMT.thy	Tue Nov 10 14:43:29 2015 +0000
     1.2 +++ b/src/HOL/SMT.thy	Tue Nov 10 17:49:54 2015 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Sascha Boehme, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
     1.8 +section \<open>Bi ndings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
     1.9  
    1.10  theory SMT
    1.11  imports Divides
     2.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Tue Nov 10 14:43:29 2015 +0000
     2.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Tue Nov 10 17:49:54 2015 +0100
     2.3 @@ -109,7 +109,7 @@
     2.4    smt_options = [(":produce-proofs", "true")],
     2.5    default_max_relevant = 200 (* FUDGE *),
     2.6    outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
     2.7 -    "warning : proof_done: status is still open"),
     2.8 +    "(error \"status is not unsat.\")"),
     2.9    parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
    2.10    replay = NONE }
    2.11  
     3.1 --- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Nov 10 14:43:29 2015 +0000
     3.2 +++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Nov 10 17:49:54 2015 +0100
     3.3 @@ -118,9 +118,12 @@
     3.4    let
     3.5      fun mk_prop_of_term concl =
     3.6        concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
     3.7 +    fun update_prems assumption_id prems =
     3.8 +      map (fn prem => id_of_father_step ^ prem)
     3.9 +          (filter_out (curry (op =) assumption_id) prems)
    3.10      fun inline_assumption assumption assumption_id
    3.11 -        (node as VeriT_Node {id, rule, prems, concl, bounds}) =
    3.12 -      mk_node id rule (filter_out (curry (op =) assumption_id) prems)
    3.13 +        (VeriT_Node {id, rule, prems, concl, bounds}) =
    3.14 +      mk_node id rule (update_prems assumption_id prems)
    3.15          (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
    3.16      fun find_input_steps_and_inline [] last_step = ([], last_step)
    3.17        | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)