1#!/bin/bash 2 3# Copyright (C) 2020 Mate Soos 4# 5# This program is free software; you can redistribute it and/or 6# modify it under the terms of the GNU General Public License 7# as published by the Free Software Foundation; version 2 8# of the License. 9# 10# This program is distributed in the hope that it will be useful, 11# but WITHOUT ANY WARRANTY; without even the implied warranty of 12# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13# GNU General Public License for more details. 14# 15# You should have received a copy of the GNU General Public License 16# along with this program; if not, write to the Free Software 17# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 18# 02110-1301, USA. 19 20# This file wraps CMake invocation for TravisCI 21# so we can set different configurations via environment variables. 22 23set -e 24set -x 25 26function run_tmp { 27 # cp stuff.cnf tmp 28 ./cryptominisat5 --zero-exit-status --dumpdecformodel b tmp drat.out > out.sat 29 grep "c conflicts" out.sat 30 set +e 31 a=$(grep "s SATIS" out.sat) 32 retval=$? 33 set -e 34 if [[ retval -eq 1 ]]; then 35 echo "-> UNSAT" 36 ../utils/cnf-utils/xor_to_cnf.py tmp final.cnf 37 ./tests/drat-trim/drat-trim final.cnf drat.out |tee out.drat 38 grep "VERIFIED" out.drat 39 grep "resol.*steps" out.drat 40 continue 41 fi 42 echo "-> SAT" 43 44 #cat out.sat 45 rm final.cnf 46 touch final.cnf 47 cat tmp >> final.cnf 48 cat b >> final.cnf 49 cp final.cnf final_without_ban.cnf 50 ../utils/cnf-utils/xor_to_cnf.py final_without_ban.cnf final_without_ban.cnf2 51 mv final_without_ban.cnf2 final_without_ban.cnf 52 grep ^v out.sat | sed "s/v//" | tr -d "\n" | sed "s/ / /g" | sed -e "s/ -/X/g" -e "s/ /Y/g" | sed "s/X/ /g" | sed -E "s/Y([1-9])/ -\1/g" | sed "s/Y0/ 0\n/" >> final.cnf 53 ../utils/cnf-utils/xor_to_cnf.py final.cnf final2.cnf 54 mv final2.cnf final.cnf 55 ./cryptominisat5 --zero-exit-status --verb 0 final.cnf | tee out.unsat 56 set +e 57 a=$(grep "s UNSATIS" out.unsat) 58 retval=$? 59 set -e 60 if [[ retval -eq 1 ]]; then 61 echo "GRAVE ERROR!" 62 exit -1 63 fi 64 65 ./tests/drat-trim/drat-trim final.cnf drat.out |tee out.drat 66 grep "VERIFIED" out.drat || exit -1 67 grep "resol.*steps" out.drat 68} 69 70if [[ $1 == "" ]]; then 71 echo "No arguments, standard run" 72 for(( c=1; c < 10000; c++ )) 73 do 74 r=$((1 + RANDOM % 999999)) 75 echo "" 76 echo "------ Run $c random $r -----------" 77 # ../utils/cnf-utils/cnf-fuzz-brummayer.py -s $r -l 3 -i 90 -I 180 > tmp 78 ../utils/cnf-utils/cnf-fuzz-brummayer.py -s $r > tmp 79 run_tmp 80 done 81else 82 if [[ $1 == "--file" ]]; then 83 echo "Using file $2" 84 rm -f tmp.gz 85 rm -f tmp 86 cp $2 tmp.gz 87 gunzip tmp.gz 88 run_tmp 89 else 90 echo "Seed run" 91 ../utils/cnf-utils/cnf-fuzz-brummayer.py -s $1 -l 3 -i 90 -I 180 > tmp 92 run_tmp 93 exit 0 94 fi 95fi 96