contrib/get-lfsc-checker

   1 #!/usr/bin/env bash
   2
   3 # utility function to download a file
   4 function download {
   5   if [ -x "$(command -v wget)" ]; then
   6     wget -c -O "$2" "$1"
   7   elif [ -x "$(command -v curl)" ]; then
   8     curl -L "$1" >"$2"
   9   else
  10     echo "Can't figure out how to download from web.  Please install wget or curl." >&2
  11     exit 1
  12   fi
  13 }
  14
  15 CVC_DIR=$(dirname $(dirname "$0"))
  16 mkdir -p $CVC_DIR/deps
  17 pushd $CVC_DIR/deps
  18
  19 BASE_DIR=`pwd`
  20 mkdir -p $BASE_DIR/tmp/
  21
  22 ##### LFSC
  23 LFSC_DIR="$BASE_DIR/lfsc-checker"
  24 mkdir -p $LFSC_DIR
  25
  26 # download and unpack LFSC
  27 version="15f53d6feb84e4ddb41deaf2b5630f5c1303b06d"
  28 download "https://github.com/CVC4/LFSC/archive/$version.tar.gz" $BASE_DIR/tmp/lfsc.tgz
  29 tar --strip 1 -xzf $BASE_DIR/tmp/lfsc.tgz -C $LFSC_DIR
  30
  31 # build and install LFSC
  32 pushd $LFSC_DIR
  33 mkdir -p build && cd build
  34 cmake -DCMAKE_INSTALL_PREFIX="$BASE_DIR" ..
  35 make install
  36 popd
  37
  38 ##### signatures
  39 SIG_DIR="$BASE_DIR/lfsc-signatures"
  40 mkdir -p $SIG_DIR
  41
  42 # download and unpack signatures
  43 sig_version="5d72dafd48aded21fd717ef77321e1c88f732d28"
  44 download "https://github.com/CVC4/signatures/archive/$sig_version.tar.gz" $BASE_DIR/tmp/signatures.tgz
  45 tar --strip 1 -xzf $BASE_DIR/tmp/signatures.tgz -C $SIG_DIR
  46
  47 # install signatures and scripts
  48 mkdir -p $BASE_DIR/share/lfsc
  49 cp -r $SIG_DIR/lfsc/new/signatures $BASE_DIR/share/lfsc
  50
  51 # based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen_and_check.sh
  52 cat << EOF > $BASE_DIR/bin/cvc5-lfsc-check.sh
  53 #!/bin/bash
  54
  55 echo "=== Generate proof: \$@"
  56 $BASE_DIR/bin/cvc5-proof.sh \$@ > proof.plf
  57
  58 echo "=== Check proof with LFSC"
  59 $BASE_DIR/bin/lfsc-check.sh proof.plf
  60 EOF
  61 chmod +x $BASE_DIR/bin/cvc5-lfsc-check.sh
  62
  63 # based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen.sh
  64 cat << EOF > $BASE_DIR/bin/cvc5-proof.sh
  65 #!/bin/bash
  66
  67 # call cvc5 and remove the first line of the output (should be "unsat")
  68 \$@ --dump-proofs --proof-format=lfsc | tail -n +2
  69 EOF
  70 chmod +x $BASE_DIR/bin/cvc5-proof.sh
  71
  72 # based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/lfsc_check.sh
  73 cat << EOF > $BASE_DIR/bin/lfsc-check.sh
  74 #!/bin/bash
  75
  76 cat \$@ | grep WARNING
  77 CHECK=\$(cat \$@ | grep check)
  78 [ -z "\$CHECK" ] && echo "; WARNING: Empty proof!!!"
  79
  80 SIG_DIR=$BASE_DIR/share/lfsc/signatures
  81 SIGS="\$SIG_DIR/core_defs.plf \\
  82     \$SIG_DIR/util_defs.plf \\
  83     \$SIG_DIR/theory_def.plf \\
  84     \$SIG_DIR/type_checking_programs.plf \\
  85     \$SIG_DIR/nary_programs.plf \\
  86     \$SIG_DIR/boolean_programs.plf \\
  87     \$SIG_DIR/boolean_rules.plf \\
  88     \$SIG_DIR/cnf_rules.plf \\
  89     \$SIG_DIR/equality_rules.plf \\
  90     \$SIG_DIR/arith_programs.plf \\
  91     \$SIG_DIR/arith_rules.plf \\
  92     \$SIG_DIR/strings_programs.plf \\
  93     \$SIG_DIR/strings_rules.plf \\
  94     \$SIG_DIR/quantifiers_rules.plf"
  95 $BASE_DIR/bin/lfscc \$SIGS \$@ >& lfsc.out
  96
  97 # recover macros for applications of arity 1,2,3, and simplify builtin syntax for constants
  98 #sed -i.orig 's/(f_ite [^ \)]*)/f_ite/g' lfsc.out
  99 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
 100
 101 cat lfsc.out
 102 rm lfsc.out
 103 EOF
 104 chmod +x $BASE_DIR/bin/lfsc-check.sh
 105
 106 popd
 107
 108 echo ""
 109 echo "========== How to use LFSC =========="
 110 echo "Generate a LFSC proof with cvc5:"
 111 echo "  $CVC_DIR/deps/bin/cvc5-proof.sh cvc5 <options> <input file>"
 112 echo "Check a generated proof:"
 113 echo "  $CVC_DIR/deps/bin/lfsc-check.sh <proof file>"
 114 echo "Run cvc5 and check the generated proof:"
 115 echo "  $CVC_DIR/deps/bin/cvc5-lfsc-check.sh cvc5 <options> <input file>"