#!/bin/bash

mkdir -p generated_comp

echo "Identifying variables" >&2
#obtaining integer variables
for i in results/*.kind-ai.result; do 
    tmp=`basename $i kind-ai.result`; 
    kind-ai -print-vars lustre/`basename $i .kind-ai.result`.lus| grep integer| sed "s/.*://;s/F2L_state//g" > generated_comp/`basename $i .kind-ai.result`.vars;done

# Generate files for comparison 
echo "Generating headers" >&2
# header
for i in results/*.kind-ai.result; do tmp=`basename $i kind-ai.result`;  
#  echo `basename $i .fst.lus.kind-ai.result` >&2;  
  bench=`cd results; ls \`basename $i .kind-ai.result\`*.result | sed "s/$tmp//;s/.result//"| grep -v kind-ai | grep -v vars`; 
  echo $i benchs $bench
  for m in $bench; do   
      file1=$tmp$m\_kind-ai.yices;
      file2=${tmp}kind-ai\_$m.yices;
      echo "(set-evidence! true)" > generated_comp/$file1;  
      echo "(set-evidence! true)" > generated_comp/$file2;  
      for v in $(eval cat generated_comp/${tmp}vars); do echo "(define $v::int)" >> generated_comp/$file1; echo "(define $v::int)" >> generated_comp/$file2; done;  
      for v in $(eval cat fst/${tmp}fst | grep states | sed "s/states //;s/;//;s/,/ /g"); do echo "(define $v::bool)" >> generated_comp/$file1; echo "(define $v::bool)" >> generated_comp/$file2; done;  
  done ;  
done;

# lines from results
# with prenex
echo "Translating properties into prenex form" >&2
cd generated_comp;
for i in *.yices; do  
    echo $i >&2 
    prefix=`echo $i | sed "s/\..*//"`; 
#echo prefix $prefix
    benchs=`echo $i | sed "s/^[^\.]*\.//;s/.yices//;s/_/ /"`; 
#echo benchs $benchs
    for m in $benchs; do  
#	echo prefix $prefix
#	echo m $m
#	echo "../tools/arith < ../results/$prefix.$m.result"
        ../tools/arith < ../results/$prefix.$m.result > tmp;  
      awk '{print NR,$0}' tmp | sed "s/^\([0-9]*\) \(.*\)$/(define ${m}_\1::bool \2)/" >> $i; 
    done;
done;



# add the main variables and the final check
echo "Adding challenge ann1 => ann2" >&2
for i in *.yices; do  
    # echo $i;  
    prefix=`echo $i | sed "s/\..*//"`; 
    benchs=`echo $i | sed "s/^[^\.]*\.//;s/.yices//;s/_/ /"`; 
    for m in $benchs; do  
	nb_lines=`wc -l ../results/$prefix.$m.result |sed "s/ .*//"`;  
	props=`for i in $(eval echo "{1..$nb_lines}"); do echo $m\_$i;done |xargs`;  
     echo "(define $m::bool (and $props))" >> $i;  
    done; 
    echo "(assert (not (=> $benchs)))" >> $i; 
    echo "(check)" >> $i;  
done;


