Skip to content

Commit

Permalink
V1.4.2 (#8)
Browse files Browse the repository at this point in the history
* fix: vamp_proof_line assigned vampire's output in the case of refutation

* Makefile clean recipe doesn't delete all contents in build directory; only athena-specific files

* bump minor version

* fix vamp_proof_line
  • Loading branch information
WilfredTA authored Oct 15, 2022
1 parent 0122c40 commit 13bd4b9
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions topenv_part2.sml
100755 → 100644
Original file line number Diff line number Diff line change
Expand Up @@ -1957,7 +1957,7 @@ fun getFlotterIndex() = let val cv = !flotter_counter
end

val spass_proof_line = "SPASS beiseite: Proof found.\n"
val vamp_proof_line = "Satisfiable!\n"
val vamp_proof_line = "% Refutation found. Thanks to Tanya!\n"
val e_proof_line = "# Proof found!\n"
val paradox_proof_line = "== Model ==================================================================="

Expand Down Expand Up @@ -2842,8 +2842,8 @@ fun vProve(goal_val, premise_vals,env,ab,max_seconds) =
val vamp_answer_stream = TextIO.openIn(vamp_out_fname)
val answer_bit = findLine(vamp_answer_stream,vamp_proof_line)
val _ = TextIO.closeIn(vamp_answer_stream)
val _ = deleteFile(vamp_in_fname)
val _ = deleteFile(vamp_out_fname)
(* val _ = deleteFile(vamp_in_fname)
val _ = deleteFile(vamp_out_fname) *)
in
(answer_bit,desired_conc)
end
Expand Down Expand Up @@ -2901,8 +2901,8 @@ fun unLimVampireProvePrimMethod([v,listVal(hyp_vals)],env,ab) =
val vamp_answer_stream = TextIO.openIn(vamp_out_fname)
val answer_bit = findLine(vamp_answer_stream,vamp_proof_line)
val _ = TextIO.closeIn(vamp_answer_stream)
val _ = deleteFile(vamp_in_fname)
val _ = deleteFile(vamp_out_fname)
(* val _ = deleteFile(vamp_in_fname)
val _ = deleteFile(vamp_out_fname) *)
in
if answer_bit then propVal(desired_conc) else primError("Failed application of "^N.vpfPrimMethod_name^
":\nUnable to derive the conclusion "^
Expand Down Expand Up @@ -2955,8 +2955,8 @@ fun polyVProve(goal, premises,env,ab,max_seconds,mono:bool,subsorting:bool) =
| loop(i::more,res) = loop(more,(Array.sub(premise_array,i-1))::res)
in SOME(loop(used_premise_indices,[])) end handle _ => NONE
val _ = TextIO.closeIn(vamp_answer_stream)
val _ = deleteFile(vamp_in_fname)
val _ = deleteFile(vamp_out_fname)
(* val _ = deleteFile(vamp_in_fname)
val _ = deleteFile(vamp_out_fname) *)
val _ = List.app (fn (_,f') => Data.removeFSymByName(f')) syms_and_new_syms
in
(answer_bit,goal,used_premises)
Expand Down

0 comments on commit 13bd4b9

Please sign in to comment.