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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

#!/bin/sh
# run some basic problems with Vampire, check if it behaves as expected or not
# Problems/, Axioms/ is for files from TPTP because of the include() scheme
# anything else can be in a convenient folder
# try and keep it minimal, reasonably clean to help debugging inevitable CI failures :-)
# new rule: no portfolio modes! hard to debug if they fail

# where is Vampire? passed by CI
vampire="`pwd`/$1 --traceback on"

run_vampire() {
	echo $vampire $@
	(cd checks; $vampire $@ > vampire-stdout 2> vampire-stderr)
	errors=`grep -E 'SIG|viola|error' checks/vampire-stderr`
	if test -n "$errors"
	then
		echo "run failed: contains errors"
		cat checks/vampire-stderr
		exit 1
	fi
}

# check the output is exactly what we expect: quite fragile by nature, be careful
check_exact_output() {
	expected=checks/$1
	shift
	run_vampire $@
	diff=`diff $expected checks/vampire-stdout`
	if test -n "$diff"
	then
		echo "check against $expected failed: diff follows"
		echo "$diff"
		exit 1
	fi
}

# check SZS status
check_szs_status() {
	status=$1
	shift
	run_vampire $@
	szs=`grep -E "^% SZS status $status for .+$" checks/vampire-stdout`
	if test -z "$szs"
	then
		echo "SZS check failed: should have been SZS $status"
		cat checks/vampire-stdout checks/vampire-stderr
		exit 1
	fi
}

# check SMT status
check_smtcomp_status() {
	status=$1
	shift
	run_vampire $@
	result=`grep -E "^$status$" checks/vampire-stdout`
	if test -z "$result"
	then
		echo "$SMT check failed: should have been $status"
		cat checks/vampire-stdout checks/vampire-stderr
		exit 1
	fi
}

# Some simple problems: fail early!
check_szs_status Theorem Problems/PUZ/PUZ001+1.p

# simple polymorphic problems
check_szs_status Theorem Problems/PUZ/PUZ139_1.p

# Unsat core problems
# disabled until we have a known strategy
# check_smtcomp_status unsat --mode smtcomp ucore/test1.smt2
check_exact_output ucore/test2.out --input_syntax smtlib2 -om ucore ucore/test2.smt2

# Term algebra problems
check_szs_status Unsatisfiable term-algebra/terms_distinct.smt2
check_szs_status Unsatisfiable -tac axiom term-algebra/terms_acyclic.smt2

# FOOL
check_szs_status Theorem fool/let-function.p
check_szs_status Theorem -newcnf on fool/let-function.p
check_szs_status Theorem -newcnf on fool/let-tuple.p
check_szs_status Theorem -newcnf on fool/let-tuple-bool.p
check_szs_status Theorem -newcnf on -ile off fool/let-function.p
check_szs_status Theorem -newcnf on -ile off fool/let-tuple.p
check_szs_status Theorem -newcnf on -ile off fool/let-tuple-bool.p

# Integer induction problems
check_szs_status Unsatisfiable -ind int induction/int_invariant_infinite_geq3_val3.smt2
check_szs_status Unsatisfiable -ind int induction/int_invariant_finite_a_to_b.smt2
# disabled until we have a known strategy
#check_szs_status Unsatisfiable --mode portfolio --schedule integer_induction --slowness 0.5 induction/int_power_0_all_0.smt2
#check_szs_status Unsatisfiable --mode portfolio --schedule integer_induction --slowness 0.5 induction/int_sum_y_geq_0.smt2

# Structural induction problems
check_szs_status Unsatisfiable -ind struct -sik one -nui on induction/mem_append_poly.smt2
check_szs_status Unsatisfiable -ind struct -sik two -nui on -to lpo induction/mem_append_poly.smt2
# TODO get rid of -tac axiom
check_szs_status Unsatisfiable -ind struct -sik three -nui on -tac axiom -to lpo induction/mem_append_poly.smt2
check_szs_status Unsatisfiable -ind struct -sik recursion -nui on -newcnf on induction/mem_append_poly.smt2
check_szs_status Unsatisfiable -ind struct -sik recursion -to lpo -newcnf on induction/qreva_len.smt2
check_szs_status Unsatisfiable -ind struct -sik one -indstrhyp on induction/qreva_len.smt2
check_szs_status Unsatisfiable -ind struct -nui on -indgo off -newcnf on induction/prefix-given-suffix.smt2

# Parser
check_szs_status Unsatisfiable parse/types-funs.smt2
check_szs_status Unsatisfiable -newcnf on parse/types-funs.smt2
check_szs_status Unsatisfiable -t 1 parse/smtlib2-parametric-datatypes.smt2
check_szs_status Unsatisfiable -newcnf on -t 1 parse/smtlib2-parametric-datatypes.smt2
check_szs_status Unsatisfiable parse/smtlib2-mutual-recursion.smt2
check_szs_status Unsatisfiable -newcnf on parse/let-bind-variable.smt2
check_szs_status Unsatisfiable -qa synthesis parse/assert-synth-max5.smt2

# Arithmetic
check_szs_status Theorem -t 1d -s 32 -tgt ground -sas z3 -tha some -nm 6 Problems/ANA/ANA135_1.p
check_szs_status Theorem -t 1d Problems/ARI/ARI045_1.p # alasca can't!
check_szs_status Theorem --decode dis+1011_1:1_prc=on:drc=off:canc=force_1 Problems/ARI/ARI184_1.p
check_szs_status Theorem -t 1d Problems/ARI/ARI548_1.p
check_szs_status Theorem -t 1d -thi all Problems/ARI/ARI576_1.p
check_szs_status Theorem -t 1d -tgt ground -sas z3 Problems/ARI/ARI633_1.p
check_szs_status Theorem -t 1d -to lpo -sas z3 Problems/ARI/ARI637_1.p
check_szs_status Theorem -t 1d -sas z3 Problems/ARI/ARI700_1.p
check_szs_status Theorem -t 1d -sas z3 Problems/ARI/ARI724_1.p
check_szs_status Theorem -t 1d -sas z3 -nwc 5.0 -br off Problems/DAT/DAT005_1.p
check_szs_status Theorem -t 1d -alasca on -alascai on -thf on Problems/DAT/DAT023_1.p
check_szs_status Theorem -t 1d -tha off Problems/DAT/DAT042_1.p
check_szs_status Theorem -t 1d -s 1010 -thsq on -thsqr 8,1 -thsqc 64 -thsqd 64 -canc force Problems/DAT/DAT043_1.p
check_szs_status Theorem -t 10d -sa discount -s 2 -awr 1:32 -to lpo -s2a on -s2agt 20 -bd all Problems/HWV/HWV087_2.p
check_szs_status Theorem -t 1d -sa discount -awr 1:32 -to lpo -sp const_frequency -sos all -sac on -lma off Problems/ITP/ITP319_1.p
check_szs_status Theorem -t 1d -sa discount -tha off -nwc 5.0 -gtg exists_sym -gtgl 5 Problems/ITP/ITP320_1.p
check_szs_status Theorem -t 1d -to lpo -spb goal_then_units -sp arity Problems/ITP/ITP412_1.p
check_szs_status Theorem -t 1d -gve force -uwa one_side_interpreted -ep R Problems/NUM/NUM919_1.p
check_szs_status ContradictoryAxioms -t 1d -s 1011 -thi all -uwa ground -br off -nwc 1.0 Problems/PLA/PLA046_1.p
check_szs_status Theorem -t 1d -s 1002 -to kbo -kws inv_frequency -sas z3 -nwc 5.0 -gtg exists_all Problems/PLA/PLA050_1.p
check_szs_status Theorem -t 1d -sa discount -s 1002 -to lpo -tha off -canc force -fsr off -fdi 10 -nwc 1.0 Problems/SEV/SEV425_1.p
check_szs_status Theorem -t 1d -isp bottom -to lpo -sas z3 -fd preordered -ev force -bd all -nwc 1.0 -sp arity Problems/SWC/SWC478_1.p
check_szs_status Theorem --decode ott+11_1:1_to=lpo:thi=all:sas=z3:bd=all:fdtod=on:sp=const_max:foolp=on:gtgl=5:asg=cautious:gtg=all:rawr=on_10 -lma off -add on -nwc 1.0  Problems/SWC/SWC482_1.p
check_szs_status Theorem -t 1d -s 1011 -to lpo -sp unary_frequency -tha off -newcnf on -s2a on -doe on Problems/SWW/SWW587_2.p
check_szs_status Theorem -t 3d -s 1011 -tgt full -fde none -nm 0 -bd all -sp arity -lma off -add on -nwc 1.0 Problems/SWW/SWW605_2.p
check_szs_status Theorem --decode ott+10_1:1024_to=kbo:norm_ineq=on:fde=unused:sas=z3:sos=on:tha=off:nm=16_1 Problems/SWW/SWW617_2.p
check_szs_status Theorem -t 1d -sas z3 -fs off -slsq off -s2a on -ep RSTC -fsr off -alasca on Problems/SWW/SWW620_2.p
check_szs_status Theorem -t 1d -to lpo -sos all -doe on Problems/SWW/SWW629_2.p

# Forward ground joinability
check_szs_status Satisfiable -t 5d -fgj on Problems/SWV/SWV021-1.p
check_szs_status Unsatisfiable -t 5d -fgj on -bd all Problems/SWW/SWW436-1.p

# Synthesis without and with uncomputables
check_szs_status Unsatisfiable -qa synthesis synthesis/max2.smt2
check_szs_status Unsatisfiable -qa synthesis synthesis/ex2-inverse_of_ixopiy.smt2