Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Vampire update #14

Merged
merged 2 commits into from
Jul 27, 2024
Merged

Vampire update #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d10bd41
Updated to a more recent version of Vampire
konstantine4096 Jul 27, 2024
98388d2
WIP
konstantine4096 Jul 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion names.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1133,7 +1133,7 @@ val spass_windows_binary = (case Paths.findFileWithPossibleSuffix("SPASS",".exe"

val spass_binary = if (Paths.is_unix) then Paths.findIterated(["spass","SPASS"],"./SPASS") else spass_windows_binary

val vampire_linux_binary = Paths.findIterated(["vampire","vampire_linux64","vampire_lin64"],"./vampire")
val vampire_linux_binary = Paths.findIterated(["vampire_z3_rel_static_sledge_5980"],"./vampire_z3_rel_static_sledge_5980")

val vampire_binary = (case Paths.findFileWithPossibleSuffix("vampire",".exe") of
SOME(str) => str
Expand Down
6 changes: 3 additions & 3 deletions topenv_part2.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1881,7 +1881,7 @@ fun findLine(in_stream,l) = let fun loop() =
in
if line = "" then false
else
if line = l then true else loop()
if (String.isSubstring l line) then true else loop()
end
in
loop()
Expand Down Expand Up @@ -2915,7 +2915,7 @@ fun unLimVampireProvePrimMethod([v,listVal(hyp_vals)],env,ab) =

fun polyVProve(goal, premises,env,ab,max_seconds,mono:bool,subsorting:bool) =
let val vi = getVampIndex()
val (vamp_in_fname,vamp_out_fname) = (Paths.vampireInName(vi),Paths.vampireOutName(vi))
val (vamp_in_fname,vamp_out_fname,vamp_error_fname) = (Paths.vampireInName(vi),Paths.vampireOutName(vi),Paths.vampireErrorName(vi))
val ax_index = ref(0)
val premise_array = Array.fromList(premises)
fun getAxNum() = (Basic.inc(ax_index);"ax"^(Int.toString(!ax_index)))
Expand Down Expand Up @@ -2946,7 +2946,7 @@ fun polyVProve(goal, premises,env,ab,max_seconds,mono:bool,subsorting:bool) =
fun write(str) = TextIO.output(vamp_problem_stream,str)
val _ = (List.app write hyps;write conc)
val _ = TextIO.closeOut(vamp_problem_stream)
val cmd = Names.vampire_binary ^ " --proof tptp --show_skolemisations on --time_limit "^max_seconds^" --input_file "^vamp_in_fname^" > "^vamp_out_fname
val cmd = Names.vampire_binary ^ " --proof tptp --mode casc --show_skolemisations on --time_limit "^max_seconds^" --input_file "^vamp_in_fname^" > "^vamp_out_fname ^ " 2> " ^ vamp_error_fname
val _ = OS.Process.system(cmd)
val vamp_answer_stream = TextIO.openIn(vamp_out_fname)
val answer_bit = findLine(vamp_answer_stream,vamp_proof_line)
Expand Down
Loading