#!/bin/sh # Usage: vallst.sh [problemfile] [vallstoptions] # Repeatedly calls vallst to solve a boolean constraint problem. # Exit values: # 0: A proof of false was found. # 1: A model was found. # 2: The time limit has been exceeded. Not used here. # 3: An interupt signal was received. # 4: Not enough memory could be allocated. # 5: Some file error occurred. # vallstoptions are the usual vallst options, see vallst --help, with the # following exceptions: # * [problemfile], if present, must come before any vallstoptions. # * Any time limit will only affect vallst calls; there is no time limit for # the script itself. You can kill the script in a controlled manner with # ctrl-c (SIGINT) or a term signal (SIGTERM) or SIGXCPU to the vallst # process. It might be better to signal or kill the subprocess vallst # rather than the script ($$) if you want to quit. # * Any time limit will be overridden every $periodth [4th] time vallst is # called. # * These flags will be overridden and will have no effect: # --out-theory-file-name --changing-setting-file-name. # * These flags will only affect the first vallst call: # --first-restart --nr-of-vars-set-at-start-is-zero. #set -x # The directory where temporary files are saved. Any model is also saved here. # Posibly defined previously. #tmpdir="/tmp" if [ -z "$tmpdir" ] then tmpdir="/tmp" fi # Name to evoke vallst with. # Posibly defined previously. #vallstcom=vallst if [ -z "$vallstcom" ] then vallstcom=vallst fi # Time limit for subcalls in seconds. Not used. #timeLimit=600 firstrestart=80 # Every period-th time, we will try evoking the solver with a bit different # options. On those more rare occasions we will focus more on simplification. period=4 # Kill any child. Flawed because it kills its own subprocess!!?? function killchild { ps -o pid= -o ppid= -o comm= | while read pid ppid comm do if [ "$ppid" -eq "$$" ] && [ "$comm" == "vallst" ] then kill -s SIGINT $pid fi done } # Make sure that tmpdir exists. Is this a good practice?? mkdir -p $tmpdir # Find a unique temporary subdirectory name to be used for this call. # Nr of other current simultaneous runs made. The tmp subdir will be named # ${tmpdir}/vallst_sh_tmp_subdir_${d}. d=0 mkdir ${tmpdir}/vallst_sh_tmp_subdir_${d} dres=$? while [ $dres -ne 0 ] do let d+=1 if [ $d -eq 1000 ] then echo "Error: cannot create a new temp dir ${tmpdir}/vallst_sh_tmp_subdir_n" exit 5 fi mkdir ${tmpdir}/vallst_sh_tmp_subdir_${d} dres=$? done # Holds the result of vallst calls. result=3 # Copy files in tmpdir that should be saved to its parent. function copyfiles { if [ $result -eq 3 ] then echo " Interupt; Current theory and settings are copied here:" echo " ${tmpdir}/vallst_sh_out_theory.vnf" echo " ${tmpdir}/vallst_sh_changing_setting.options" wait nice \ cp -f -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ ${tmpdir}/vallst_sh_out_theory.vnf cp -f -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options \ ${tmpdir}/vallst_sh_changing_setting.options fi } # Clean up if the script is terminated ungracefully. # Note that SIGINT, SIGTERM and SIGXCPU are handled also by vallst. # We'll also kill any subprocess. # Handling specific signals isn't working as intended because the script # will wait until any vallst call is finished before dealing with any signal # sent to the script. How to fix this????? The way the code works now, not # trapping any signals except at exit, is perhaps good enough though. The trap # will execute at every exit even though it's only when a signal was sent to # the parent, $$, that it is useful. However, wait isn't working!! Hence the # "sleep 0.3". #trap killchild SIGXCPU #trap killchild SIGINT #trap killchild SIGTERM trap ' killchild; wait; sleep 0.3; wait; copyfiles; \ rm -f -r ${tmpdir}/vallst_sh_tmp_subdir_${d} ' EXIT # Number of vallst calls made, also counting the coming one. n=1 echo "$n:" $vallstcom \ --first-restart=$firstrestart \ --improve-proof-level=0 \ --abort-threshold=60 \ --no-abort-time=300 \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ --nr-of-vars-set-at-start-is-zero=yes \ "$@" \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options result=$? # Used to store the value of n%$period (because I suck at script programming). p=0 # Increment argument list to skip $1 if it is an unflagged file name or '-'. if [ $# -gt 0 ] then if [[ $1 != -* ]] then shift else if [[ $1 == - ]] then shift fi fi fi while [ $result -eq 2 ] do #cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf ${tmpdir}/vallst_sh_out_theory$n.vnf let n+=1 let firstrestart+=40 let p=$n%$period echo echo "$n:" if [ $p -eq 0 ] then $vallstcom \ --improve-proof-level=999999 \ --simp-time-limit-fast=3800 --simp-time-limit-slow=100000 \ --simp-setting 1-1-4294901498-0 --simp-setting 2-1-400-0 \ --simp-setting 2-2-40-0 --simp-setting 3-1-60-0 \ --simp-setting 3-2-8-0 --simp-setting 3-3-6-0 \ --simp-setting-slow 1-1-4294901501-0 \ --simp-setting-slow 2-1-2200-0 --simp-setting-slow 2-2-348-0 \ --simp-setting-slow 3-1-200-0 --simp-setting-slow 3-2-16-0 \ --simp-setting-slow 3-3-7-0 --simp-setting-slow 4-1-14-0 \ --simp-setting-slow 4-2-6-0 --simp-setting-slow 4-3-4-0 \ --simp-setting-slow 4-4-3-0 \ --abort-threshold=50 \ --no-abort-time=240 \ --subst-equs=no \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ "$@" \ --pb=no --atsp=no --tsp=no \ --nr-of-vars-set-at-start-is-zero=no \ --time-limit=360 \ --first-restart=$firstrestart \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options \ --file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ $(head --lines=1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options) result=$? else $vallstcom \ --improve-proof-level=0 \ --abort-threshold=50 \ --no-abort-time=240 \ --subst-equs=no \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ "$@" \ --pb=no --atsp=no --tsp=no \ --nr-of-vars-set-at-start-is-zero=no \ --first-restart=$firstrestart \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options \ --file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ $(head --lines=1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options) result=$? fi done echo "times:" times if [ $result -eq 0 ] then echo " Proof of false found" fi if [ $result -eq 1 ] then #echo " $(cat ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model)" cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ ${tmpdir}/vallst_sh.model echo " Model found (${tmpdir}/vallst_sh.model if no result file was specified explicitly)" fi # Below code is commented away because the exit is always trapped and things # are cleaned up there. If trapping is fixed so that signals are just # propagated (which is the ideal), uncomment below code!! #if [ $result -eq 3 ] #then #copyfiles; #fi #wait #rm -f -r ${tmpdir}/vallst_sh_tmp_subdir_${d} echo "Result: $result" exit $result
Generated on Mon Jul 18 11:34:15 2005 for Vallst by doxygen 1.4.3.