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