vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64

#!/bin/bash

#
# A simple proof checker, not particularly smart, e.g. reports an error in 
# the "negated conjecture" step as result of this step is not a conclusion of
# the premise but rather its negation. However it can still be helpul for 
# debugging...
#
# usage:
# proofcheck <the usual vampire arguments>
#
# The arguments to the script are passed to vampire_rel (which must therefore 
# be present). One should not pass the option "--proof" as the script sets the
# proof output to "proofcheck" which is specially designed to work well with 
# this script.
#

SCRIPT_DIR=`dirname $0`
BASE_DIR="$SCRIPT_DIR/.."


VAMPIRE="$BASE_DIR/vampire_rel"
#EPROVER='/raid/hoder/eprover/PROVER/eprover'
#OTHER_PROVER='/raid/hoder/vampire_old'
OTHER_PROVER="$VAMPIRE --time_limit 10 -ptb off -spl off"

$VAMPIRE --proof proofcheck $* |awk '
BEGIN { finished=0; curr=""; checkedCnt=0 }
END { print "checked steps: " checkedCnt }
{ special=0 }
/^Refutation found/ { special=1 }
/^%#/ {
	special=1
	if( curr!="" ) {
		cmd="echo '\''" curr "'\'' | sed -e \"s/\\\\\\$sk/xXsk/g\" -e \"s/\\\\\\$n/xXn/g\" -e \"s/\\\\\\$\\\\\\$e/xXeqProxy/g\" -e \"s/~!/~ !/g\" | '"$OTHER_PROVER"' /dev/stdin |grep \"^Refutation found\" "
		cmd_out=(cmd | getline)
		#print "============"
		#print cmd
		#print "============"
		#print $0
		#print "------------"
		print "cmd_out: " cmd_out
		#print
		#print
		if( !cmd_out ) {
			print "============"
#				print cmd
#				print "------------"
			print "% '"$*"'"
			print "% failed:"
			print curr
			print ""
		}
		close(cmd)
		checkedCnt++
		curr=""
	} else {
		finished=1
	}
}
special==0 && finished==0 {
	curr = curr "\n" $0
}
'