new configurations for competition

gaperez64 · May 19, 2016 · 6e89180 · 6e89180
1 parent 036d398
commit 6e89180
Show file tree

Hide file tree

Showing 7 changed files with 36 additions and 7 deletions.
diff --git a/par_conf3.sh b/par_conf3.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+DIR=`dirname $0`/
+# $1 contains the input filename (the name of the AIGER-file).
+COMMAND="${DIR}binary/abssynthe -a -p -s $1"
+$COMMAND
+res=$?
+if [[ $res == 10 ]]; then
+    echo "REALIZABLE"
+else
+    echo "UNREALIZABLE"
+fi
+exit $res
diff --git a/par_synth_conf3.sh b/par_synth_conf3.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+DIR=`dirname $0`/
+# $1 contains the input filename (the name of the AIGER-file).
+COMMAND="${DIR}binary/abssynthe -a -p -s $1 -o $1-result.aag"
+$COMMAND
+res=$?
+if [[ $res == 10 ]]; then
+    cat "$1-result.aag"
+else
+    echo "UNREALIZABLE"
+fi
+exit $res
diff --git a/seq_conf2.sh b/seq_conf2.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 DIR=`dirname $0`/
 # $1 contains the input filename (the name of the AIGER-file).
-COMMAND="${DIR}binary/abssynthe -c 1 $1"
+COMMAND="${DIR}binary/abssynthe -a $1"
 $COMMAND
 res=$?
 if [[ $res == 10 ]]; then

diff --git a/seq_conf3.sh b/seq_conf3.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 DIR=`dirname $0`/
 # $1 contains the input filename (the name of the AIGER-file).
-COMMAND="${DIR}binary/abssynthe -c 2 $1"
+COMMAND="${DIR}binary/abssynthe -a2048 -c 1 $1"
 $COMMAND
 res=$?
 if [[ $res == 10 ]]; then

diff --git a/seq_synth_conf2.sh b/seq_synth_conf2.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 DIR=`dirname $0`/
 # $1 contains the input filename (the name of the AIGER-file).
-COMMAND="${DIR}binary/abssynthe -c 1 $1 -o $1-result.aag"
+COMMAND="${DIR}binary/abssynthe -a $1 -o $1-result.aag"
 $COMMAND
 res=$?
 if [[ $res == 10 ]]; then

diff --git a/seq_synth_conf3.sh b/seq_synth_conf3.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 DIR=`dirname $0`/
 # $1 contains the input filename (the name of the AIGER-file).
-COMMAND="${DIR}binary/abssynthe -c 2 $1 -o $1-result.aag"
+COMMAND="${DIR}binary/abssynthe -a2048 -c 1 $1 -o $1-result.aag"
 $COMMAND
 res=$?
 if [[ $res == 10 ]]; then

diff --git a/source/algos.cpp b/source/algos.cpp
@@ -1239,13 +1239,18 @@ static void pWorker(AIG* spec_base, int solver) {
             result = solve(spec_base);
             break;
         case 1:
-            result = compSolve1(spec_base);
+            settings.use_abs = true;
+            result = solve(spec_base);
             break;
         case 2:
-            result = compSolve2(spec_base);
+            settings.use_abs = true;
+            settings.abs_threshold = 2048;
+            result = compSolve1(spec_base);
             break;
         case 3:
-            result = compSolve3(spec_base);
+            settings.use_abs = true;
+            settings.abs_threshold = 2048;
+            result = compSolve2(spec_base);
             break;
         case 4:
             result = solve(spec_base, CUDD_REORDER_SIFT);