blob: 45ae432f6d096702ccc9ffc92c4dd8f80bfabf23 (
plain)
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
|
#!/usr/bin/env bash
# utility function to download a file
function download {
if [ -x "$(command -v wget)" ]; then
wget -c -O "$2" "$1"
elif [ -x "$(command -v curl)" ]; then
curl -L "$1" >"$2"
else
echo "Can't figure out how to download from web. Please install wget or curl." >&2
exit 1
fi
}
CVC_DIR=$(dirname $(dirname "$0"))
mkdir -p $CVC_DIR/deps
pushd $CVC_DIR/deps
BASE_DIR=`pwd`
mkdir -p $BASE_DIR/tmp/
##### LFSC
LFSC_DIR="$BASE_DIR/lfsc-checker"
mkdir -p $LFSC_DIR
# download and unpack LFSC
version="15f53d6feb84e4ddb41deaf2b5630f5c1303b06d"
download "https://github.com/CVC4/LFSC/archive/$version.tar.gz" $BASE_DIR/tmp/lfsc.tgz
tar --strip 1 -xzf $BASE_DIR/tmp/lfsc.tgz -C $LFSC_DIR
# build and install LFSC
pushd $LFSC_DIR
mkdir -p build && cd build
cmake -DCMAKE_INSTALL_PREFIX="$BASE_DIR" ..
make install
popd
##### signatures
SIG_DIR="$BASE_DIR/lfsc-signatures"
mkdir -p $SIG_DIR
# download and unpack signatures
sig_version="5d72dafd48aded21fd717ef77321e1c88f732d28"
download "https://github.com/CVC4/signatures/archive/$sig_version.tar.gz" $BASE_DIR/tmp/signatures.tgz
tar --strip 1 -xzf $BASE_DIR/tmp/signatures.tgz -C $SIG_DIR
# install signatures and scripts
mkdir -p $BASE_DIR/share/lfsc
cp -r $SIG_DIR/lfsc/new/signatures $BASE_DIR/share/lfsc
# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen_and_check.sh
cat << EOF > $BASE_DIR/bin/cvc4-lfsc-check.sh
#!/bin/bash
echo "=== Generate proof: \$@"
$BASE_DIR/bin/cvc4-proof.sh \$@ > proof.plf
echo "=== Check proof with LFSC"
$BASE_DIR/bin/lfsc-check.sh proof.plf
EOF
chmod +x $BASE_DIR/bin/cvc4-lfsc-check.sh
# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen.sh
cat << EOF > $BASE_DIR/bin/cvc4-proof.sh
#!/bin/bash
# call cvc4 and remove the first line of the output (should be "unsat")
\$@ --dump-proofs --proof-format=lfsc | tail -n +2
EOF
chmod +x $BASE_DIR/bin/cvc4-proof.sh
# based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/lfsc_check.sh
cat << EOF > $BASE_DIR/bin/lfsc-check.sh
#!/bin/bash
cat \$@ | grep WARNING
CHECK=\$(cat \$@ | grep check)
[ -z "\$CHECK" ] && echo "; WARNING: Empty proof!!!"
SIG_DIR=$BASE_DIR/share/lfsc/signatures
SIGS="\$SIG_DIR/core_defs.plf \\
\$SIG_DIR/util_defs.plf \\
\$SIG_DIR/theory_def.plf \\
\$SIG_DIR/type_checking_programs.plf \\
\$SIG_DIR/nary_programs.plf \\
\$SIG_DIR/boolean_programs.plf \\
\$SIG_DIR/boolean_rules.plf \\
\$SIG_DIR/cnf_rules.plf \\
\$SIG_DIR/equality_rules.plf \\
\$SIG_DIR/arith_programs.plf \\
\$SIG_DIR/arith_rules.plf \\
\$SIG_DIR/strings_programs.plf \\
\$SIG_DIR/strings_rules.plf \\
\$SIG_DIR/quantifiers_rules.plf"
$BASE_DIR/bin/lfscc \$SIGS \$@ >& lfsc.out
# recover macros for applications of arity 1,2,3, and simplify builtin syntax for constants
#sed -i.orig 's/(f_ite [^ \)]*)/f_ite/g' lfsc.out
sed -i.orig 's/(\\ [^ ]* (\\ [^ ]* (\\ [^ ]* (apply (apply (apply f_\([^ ]*\) [^ ]*) [^ ]*) [^ ]*))))/\1/g; s/(\\ [^ ]* (\\ [^ ]* (apply (apply f_\([^ ]*\) [^ ]*) [^ ]*)))/\1/g; s/(\\ [^ ]* (apply f_\([^ ]*\) [^ ]*))/\1/g; s/(var \([^ ]*\) [^ \)]*)/var_\1/g; s/(int \([^ \)]*\))/\1/g; s/emptystr/""/g; s/int\.//g' lfsc.out
cat lfsc.out
rm lfsc.out
EOF
chmod +x $BASE_DIR/bin/lfsc-check.sh
popd
echo ""
echo "========== How to use LFSC =========="
echo "Generate a LFSC proof with CVC4:"
echo " $CVC_DIR/deps/bin/cvc4-proof.sh cvc4 <options> <input file>"
echo "Check a generated proof:"
echo " $CVC_DIR/deps/bin/lfsc-check.sh <proof file>"
echo "Run CVC4 and check the generated proof:"
echo " $CVC_DIR/deps/bin/cvc4-lfsc-check.sh cvc4 <options> <input file>"
|
