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

#!/bin/bash

#
# runs vampire for symbol eliminating inference discovery, followed by consequence elimination to
# eliminate redundant symbol-eliminating clauses
#
# usage:
# symels vampire_executable problem_file [conseq_el_timeout]
#
# conseq_el_timeout is the time in seconds to be spent in a single call to 
#   consequence elinimation. Default is 20s and four calls with different 
#   strategies are made (see calls to doConseqEl later in this file)
#

VAMPIRE=$1
TMP=`mktemp -d /tmp/symel.XXXXX`
#TMP=aux

if [ "$3" == "" ]; then
    CFTIME=20
else
    CFTIME=$3
fi

function doConseqEl()
{
# <input file> <output file> <additional arguments>
# This function requires the file $TMP/theory to contain theory axioms
    
    rm -rf $TMP/ce
    mkdir $TMP/ce
    local CTMP=$TMP/ce

    cp $1 $CTMP/allInv

#prepare Vampire input
    #cp $TMP/theory $CTMP/consElInp
    cat $CTMP/allInv >> $CTMP/consElInp


#find consequences
#    $VAMPIRE -t $CFTIME $3 --mode consequence_elimination -ptb off -spl off -updr off  <$CTMP/consElInp | awk '
    $VAMPIRE --time_limit $CFTIME $3 --mode consequence_elimination --splitting off --unused_predicate_definition_removal off  <$CTMP/consElInp | awk '

/^Pure cf clause/ { cl=$0; clN=NR }
/^Consequence found/ { print cl }
{ if(NR!=clN) { print; fflush() } }
' | tee $CTMP/consElOut >&2

#select non-consequences
    if grep 'Consequence found' $CTMP/consElOut >/dev/null; then
	cat $CTMP/allInv |egrep -v '('`grep 'Consequence found' $CTMP/consElOut | sed 's/^.*: //' | tr '\n' '|' | sed 's/|/,|/g' | sed 's/|$//'`')' > $2
    else
	cp $CTMP/allInv $2
    fi
    echo "Strategy \"$3\" eliminated" `grep 'Consequence found' $CTMP/consElOut | wc -l` >&2
}

echo "Extracting type information...">&2

grep tff $2 > $TMP/theory


#echo "
#import tptp
#tptp.collect_formulas(\"$2\")
#" | python >>$TMP/theory

#if [ "${PIPESTATUS[1]}" != "0" ]; then
#    echo 'Axiom extraction error!' >&2
#    exit 1
#fi

cat $TMP/theory >&2

echo "Obtaining symbol eliminating inferences...">&2
$VAMPIRE --show_skolemisations on --time_limit 3 < $2 | tee $TMP/out >&2

echo "Prepare consequence elimination task...">&2

#filter symbol eliminating inferences
grep tff $TMP/out > $TMP/symelFof

cat $TMP/symelFof

#cat  $TMP/theory $TMP/symelFof > $TMP/symelAll
cat  $TMP/symelFof $TMP/theory > $TMP/symelAll

echo "Start consequence elimination on SEI...">&2

#several attempts to eliminate consequences

cp $TMP/symelAll $TMP/symel_nonred

doConseqEl $TMP/symel_nonred $TMP/symel_nonred "--selection 1003 --saturation_algorithm discount --backward_subsumption_resolution on --condensation on"
doConseqEl $TMP/symel_nonred $TMP/symel_nonred "--saturation_algorithm discount --forward_literal_rewriting on --backward_subsumption_resolution on --condensation on"
doConseqEl $TMP/symel_nonred $TMP/symel_nonred "--selection 1003 --saturation_algorithm discount"
doConseqEl $TMP/symel_nonred $TMP/symel_nonred "--selection -1 --saturation_algorithm discount --forward_literal_rewriting on"


#print statistics
STAT="% "`grep 'tff(inv.*)\.' $TMP/out | wc -l`" symbol eliminating formulas, "`grep 'tff(inv.*)\.' $TMP/symel_nonred|wc -l`" non-redundant ones"
echo $STAT
echo
echo $STAT >&2

#print info on skolemization as TPTP comment
grep Skolem $TMP/out | sed 's/^/%/'
echo

#print non-consequences
grep 'tff(inv.*)\.' $TMP/symel_nonred

#clean up
rm -rf $TMP

echo "Done." >&2