#!/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=`echo $i | sed "s/results\/\(.*\)kind-ai.*\.result/\1/"`;\
  idx=`echo $i | sed "s/.*kind-ai\(.*\)\.result/\1/;s/\.$//"`;\
#  echo `basename $i .fst.lus.kind-ai.result` >&2;  
  echo test; \
     echo $i | sed "s/results\/\(.*\)\.kind-ai.*\.result/\1/" ; \
echo $tmp $i $idx; \
echo test2; 
  bench=`cd results; ls \`echo $i | sed "s/results\/\(.*\)\.kind-ai.*\.result/\1/"\`*.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${idx}.yices;
      file2=${tmp}kind-ai${idx}\_$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;


