optimizations in deduction phase

regression/acdl/Makefile

@@ -1,12 +1,12 @@
 default: tests.log
 
-FLAGS = --verbosity 10 --acdl --decision equality --learning first-uip --propagate chaotic --inline
+FLAGS = --verbosity 10 --acdl --decision ordered --learning first-uip --propagate chaotic --inline
 
 test:
-	@../test.pl -c "/usr/bin/time ../../../src/2ls/2ls $(FLAGS)"
+	@../test.pl -c "/usr/bin/time ../../src/2ls/2ls $(FLAGS)"
 
 tests.log: ../test.pl
-	@../test.pl -c "../../../src/2ls/2ls $(FLAGS)"
+	@../test.pl -c "../../src/2ls/2ls $(FLAGS)"
 
 show:
 	@for dir in *; do \
@@ -17,4 +17,4 @@ show:
 
 clean:
 	@rm -f *.log
-	@for dir in *; do rm -f $$dir/*.out; done;
+	@for dir in *; do rm -f $$dir/*.{sv,dat,log,out,cnf,smt2,aag,aig,v,git,svn,nfs}; rm -f $$dir/*.nfs*; done;

regression/acdl/branch4/main.c

@@ -1,6 +1,5 @@
 int main() {
 int x, y;
-_Bool c;
 if(y<0)
   x=0;
 else

regression/acdl/loop2/main.c

@@ -1,7 +1,7 @@
 int main() {
   int x=0,i;
   for(i=0;i<10;i++)
-    x = x+i;
+   x = x+i;
   assert(x<10);
 }
 

regression/acdl/run-acdls-interval.sh

@@ -0,0 +1,19 @@
+PWD=`pwd`
+TIMEOUT=3600
+TOOL=acdls
+BENCHMARKDIRS=`cat benchmarks-intv.txt`
+PROGRESSLOG=${PWD}/progress.log-intervals-${TOOL}
+FLAGS="--inline --acdl --decision ordered --propagate chaotic --learning first-uip" 
+EXEC=/users/rajdeep/thesis-tool-webpage/acdlp_thesis_version/2ls/src/2ls/2ls
+echo "Starting experiments at `date` on `hostname`" > ${PROGRESSLOG}
+for DIR in $BENCHMARKDIRS
+do
+  echo  ${DIR}
+  cd ${DIR}
+  LOG=${PWD}/logintv-${DIR}
+  filename=main.c
+  echo "Starting to processing $DIR/$filename at `date`" >> ${PROGRESSLOG}
+  runsolver -C $TIMEOUT -W $TIMEOUT -d 1 -M 32768 ${EXEC} ${FLAGS} $filename >> ${LOG}
+  echo "done at `date`" >> ${PROGRESSLOG}
+  cd ../
+done

regression/acdl/run-acdls-octagon.sh

@@ -0,0 +1,19 @@
+PWD=`pwd`
+TIMEOUT=3600
+TOOL=acdls
+BENCHMARKDIRS=`cat benchmarks-octagons.txt`
+PROGRESSLOG=${PWD}/progress.log-oct-${TOOL}
+FLAGS="--inline --acdl --decision ordered --propagate chaotic --learning first-uip --octagons" 
+EXEC=/users/rajdeep/thesis-tool-webpage/acdlp_thesis_version/2ls/src/2ls/2ls
+echo "Starting experiments at `date` on `hostname`" > ${PROGRESSLOG}
+for DIR in $BENCHMARKDIRS
+do
+  echo  ${DIR}
+  cd ${DIR}
+  LOG=${PWD}/logoct-${DIR}
+  filename=main.c
+  echo "Starting to processing $DIR/$filename at `date`" >> ${PROGRESSLOG}
+  runsolver -C $TIMEOUT -W $TIMEOUT -d 1 -M 32768 ${EXEC} ${FLAGS} $filename >> ${LOG}
+  echo "done at `date`" >> ${PROGRESSLOG}
+  cd ../
+done