Lines Matching defs:proof
61 I am hoping that the Z3 proof format will eventually be changed
116 (* FIXME: I am hoping that the Z3 proof format will eventually be
305 (* returns an extended proof; 't' must encode a proofterm *)
306 fun extend_proof proof (id, t) =
309 Option.isSome (Redblackmap.peek (proof, id)) then
314 Redblackmap.insert (proof, id, proofterm_of_term t)
318 definition; returns a (possibly extended) dictionary and proof *)
319 fun parse_definition get_token (tydict, tmdict, proof) =
333 val proof = extend_proof proof (proofterm_id name, t)
335 (tmdict, proof)
340 proof)
344 fun parse_proof get_token (tydict, tmdict, proof) (rpars : int) =
351 val (tmdict, proof) = parse_definition get_token (tydict, tmdict, proof)
353 parse_proof get_token (tydict, tmdict, proof) (rpars + 1)
360 parse_proof get_token (tydict, tmdict, proof) rpars
371 (* Z3 assigns no ID to the final proof step; we use ID 0 *)
372 extend_proof proof (0, t) before Lib.funpow rpars
384 Redblackmap.dict) (instream : TextIO.instream) : proof =
390 Feedback.HOL_MESG "HolSmtLib: parsing Z3 proof"
393 val proof = parse_proof get_token
397 "' (and perhaps others) after proof")
401 proof
405 (get-proof) command (for an unsatisfiable problem, with proofs
411 (cf. 'SmtLib_Parser.parse_file'); and the name of the proof
414 fun parse_file (tydict, tmdict) (path : string) : proof =