#!/bin/ksh
#####################################################
# Script for generating comparison problems         #
#####################################################
INSTANCES="$1"

if test -z "$INSTANCES"
then
    INSTANCES=8
fi

MAINOPT="-lits 4 -all ${INSTANCES}"

echo "GENERATION"

for PROBLEM in qbf qbf-inv qbf-cpdl
do
    echo "   ${PROBLEM}"

     for DEPTH in 4 6
     do
         for CLAUSES in 10 20 30
         do
             for VARS in 4 8 16
             do
 ${PROBLEM} -clauses ${CLAUSES} -vars ${VARS} -depth ${DEPTH} ${MAINOPT}
             done
         done
     done

     for DEPTH in 4 6
     do
         for CLAUSES in 10 20 30 40 50
         do
             for VARS in 4 8 16
             do
 ${PROBLEM} -ladner -clauses ${CLAUSES} -vars ${VARS} -depth ${DEPTH} ${MAINOPT}
 ${PROBLEM} -sss -clauses ${CLAUSES} -vars ${VARS} -depth ${DEPTH} ${MAINOPT}
             done
         done
     done

for OPT in cnf
    do
        tar -cf ${PROBLEM}-${OPT}-tancs.tar p-${PROBLEM}-${OPT}*
        rm -f p-${PROBLEM}-${OPT}*
        gzip ${PROBLEM}-${OPT}-tancs.tar
    done
done


 for PROBLEM in psat psat-inv
 do
     echo "   ${PROBLEM}"

     for DEPTH in 1 2
     do
         for CLAUSES in 20 30 40 50
         do
             for VARS in 4 8
             do
 ${PROBLEM} -clauses ${CLAUSES} -vars ${VARS} -depth ${DEPTH} ${MAINOPT}
             done
         done
     done

 for OPT in cnf
     do
         tar -cf ${PROBLEM}-${OPT}-tancs.tar p-${PROBLEM}-${OPT}*
         rm -f p-${PROBLEM}-${OPT}*
         gzip ${PROBLEM}-${OPT}-tancs.tar
     done
 done