Skip to content

Commit 54748a7

Browse files
jhoenickejhoenicke
authored
New single-query processor. (#6)
The new logic is: - Take the first line containing the single word sat, unsat, or unknown - all other lines are ignored ("success", warnings, error messages) - if the line is sat or unsat this is the status - if no such line exists, the status is unknown. Added test cases (some from the competition test runs)
1 parent eb9f7a1 commit 54748a7

32 files changed

+528
-14
lines changed

‎single-query-track/process

Lines changed: 17 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,28 @@
11
#!/bin/bash
22

3-
# Aaron Stump, Tjark Weber
4-
# A simple post-processor for SMT.
5-
6-
set -e
7-
set -u
3+
# Jochen Hoenicke
84

9-
# if the output file ($1) does not contain the word "sat", set SAT to 0
10-
SAT=1
11-
grep -qsw sat "$1" || SAT=0
5+
# A simple post-processor for SMT.
6+
# The logic is:
7+
# - take the first line containing the single word sat, unsat, or unknown
8+
# - all other lines before are ignored ("success", warnings, error messages)
9+
# - if the line is sat, unsat, or unknown this is the status
10+
# - if no such line exists, the status is unknown.
11+
# - all lines after the result are ignored.
1212

13-
UNSAT=1
14-
grep -qsw unsat "$1" || UNSAT=0
1513

16-
UNKNOWN=1
17-
grep -qsw unknown "$1" || UNKNOWN=0
14+
STATUS=$(
15+
# remove the StarExec timing information from each line of the solver output
16+
sed 's/^[0-9]*\.[0-9]*\/[0-9]*.[0-9]*\t//g' "$1" | \
17+
# filter out lines containing only sat, unsat, or unknown
18+
egrep -e '^\s*(sat|unsat|unknown)\s*$' | \
19+
# the first answer wins
20+
head -1 | egrep -o '(sat|unsat|unknown)')
1821

19-
if [[ "$SAT" -eq 1 && "$UNSAT" -eq 0 && "$UNKNOWN" -eq 0 ]]; then
22+
if [[ "$STATUS" == "sat" ]]; then
2023
# the output contains only the word "sat"
2124
echo "starexec-result=sat"
22-
elif [[ "$SAT" -eq 0 && "$UNSAT" -eq 1 && "$UNKNOWN" -eq 0 ]]; then
25+
elif [[ "$STATUS" == "unsat" ]]; then
2326
# the output contains only the word "unsat"
2427
echo "starexec-result=unsat"
2528
else

‎single-query-track/run_tests.sh

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#!/bin/sh
2+
#
3+
# check if the test files in test/sat, test/unsat, test/starexec-unknown
4+
# produce the corresponding expected results.
5+
6+
for result in sat unsat starexec-unknown; do
7+
echo "starexec-result=$result" > expected.txt
8+
for file in test/$result/*; do
9+
./process "$file" | diff expected.txt - || echo "... in $file"
10+
done
11+
rm expected.txt
12+
done

‎single-query-track/test/sat/481866107.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
18.26/18.29 sat
2+
20.64/20.71 EOF

‎single-query-track/test/sat/481870398.txt

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
0.00/0.23 success
2+
0.00/0.23 success
3+
0.00/0.23 success
4+
0.00/0.23 success
5+
0.00/0.23 success
6+
0.00/0.23 success
7+
0.00/0.23 success
8+
0.00/0.23 success
9+
0.00/0.23 success
10+
0.00/0.23 success
11+
0.00/0.23 success
12+
0.00/0.23 success
13+
0.00/0.24 success
14+
0.00/0.24 success
15+
0.00/0.24 success
16+
0.00/0.24 success
17+
0.00/0.24 success
18+
0.00/0.24 success
19+
0.00/0.24 success
20+
0.00/0.24 success
21+
0.00/0.24 success
22+
0.00/0.24 success
23+
0.00/0.24 success
24+
0.00/0.24 success
25+
0.00/0.24 success
26+
0.00/0.24 success
27+
0.00/0.24 success
28+
0.00/0.24 success
29+
0.00/0.24 success
30+
0.00/0.24 success
31+
0.00/0.24 success
32+
0.00/0.24 success
33+
0.00/0.24 success
34+
0.00/0.24 success
35+
0.00/0.24 success
36+
0.00/0.24 success
37+
0.00/0.24 success
38+
0.00/0.24 success
39+
0.00/0.24 success
40+
0.00/0.24 success
41+
0.00/0.24 success
42+
0.00/0.24 success
43+
0.00/0.24 success
44+
0.00/0.24 success
45+
0.00/0.24 success
46+
0.00/0.24 success
47+
0.00/0.24 success
48+
0.00/0.24 success
49+
0.00/0.24 success
50+
0.00/0.24 success
51+
0.00/0.24 success
52+
0.00/0.24 success
53+
0.00/0.24 success
54+
0.00/0.24 success
55+
0.00/0.24 success
56+
0.00/0.24 success
57+
0.00/0.24 success
58+
0.00/0.24 success
59+
0.00/0.24 success
60+
0.00/0.24 success
61+
0.00/0.24 success
62+
0.00/0.24 success
63+
0.00/0.24 success
64+
0.00/0.24 success
65+
0.00/0.24 success
66+
4.50/1.62 success
67+
44.52/27.12 sat
68+
44.55/27.17 EOF

‎single-query-track/test/sat/481870579.txt

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
12.62/12.71 sat
2+
12.62/12.71 STAT: nb_atomes=0
3+
12.62/12.71 STAT: nb_functions=425
4+
12.62/12.71 STAT: nb_predicates=0
5+
12.62/12.71 STAT: nb_axiomes=0
6+
12.62/12.71 STAT: nb_instances_EnumTrig=0
7+
12.62/12.71 STAT: nb_conflicting_instances=0
8+
12.62/12.71 EOF

‎single-query-track/test/sat/481873944.txt

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
0.00/0.23 success
2+
0.00/0.24 success
3+
0.00/0.24 success
4+
0.00/0.24 success
5+
0.00/0.24 success
6+
0.00/0.24 success
7+
0.00/0.24 success
8+
0.00/0.24 success
9+
0.00/0.24 success
10+
0.00/0.24 success
11+
0.00/0.24 success
12+
0.00/0.24 success
13+
0.00/0.24 success
14+
0.00/0.24 success
15+
0.00/0.24 success
16+
0.00/0.24 success
17+
0.00/0.24 success
18+
0.00/0.24 success
19+
0.00/0.24 success
20+
0.00/0.24 success
21+
0.00/0.24 success
22+
0.00/0.24 success
23+
0.00/0.24 success
24+
0.00/0.24 success
25+
0.00/0.24 success
26+
0.00/0.24 success
27+
0.00/0.49 success
28+
1.36/0.56 sat
29+
1.36/0.60 EOF

‎single-query-track/test/sat/dummy1.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
18.26/18.29 sat
2+
20.64/20.71 EOF

‎single-query-track/test/sat/dummy2.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
18.26/18.29 sat
2+
20.64/20.71 EOF

‎single-query-track/test/starexec-unknown/481859873.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
0.00/0.01 unknown
2+
0.00/0.01 EOF

‎single-query-track/test/starexec-unknown/481859874.txt

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
2.85/1.37 success
2+
2.97/1.38 success
3+
2.97/1.38 success
4+
2.97/1.38 success
5+
2.97/1.41 success
6+
2.97/1.41 success
7+
2.97/1.41 success
8+
2.97/1.41 success
9+
2.97/1.42 success
10+
2.97/1.42 success
11+
2.97/1.42 success
12+
2.97/1.42 success
13+
2.97/1.43 Unexpected Exception: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /export/starexec/sandbox2/benchmark/theBenchmark.smt2:13:13: Arrays with Bool as argument are not supported
14+
2.97/1.43 de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /export/starexec/sandbox2/benchmark/theBenchmark.smt2:13:13: Arrays with Bool as argument are not supported
15+
2.97/1.43 de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.ExceptionThrowingParseEnvironment.printError(ExceptionThrowingParseEnvironment.java:51)
16+
2.97/1.43 de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.ExceptionThrowingSMTLIB2Parser.run(ExceptionThrowingSMTLIB2Parser.java:58)
17+
2.97/1.43 de.uni_freiburg.informatik.ultimate.controller.eliminator.UltimateEliminatorController.init(UltimateEliminatorController.java:215)
18+
2.97/1.43 de.uni_freiburg.informatik.ultimate.core.coreplugin.UltimateCore.activateController(UltimateCore.java:242)
19+
2.97/1.43 de.uni_freiburg.informatik.ultimate.core.coreplugin.UltimateCore.start(UltimateCore.java:184)
20+
2.97/1.43 org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
21+
2.97/1.43 org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
22+
2.97/1.43 org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
23+
2.97/1.43 org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)
24+
2.97/1.43 org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)
25+
2.97/1.43 sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
26+
2.97/1.43 sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
27+
2.97/1.43 sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
28+
2.97/1.43 java.lang.reflect.Method.invoke(Method.java:498)
29+
2.97/1.43 org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669)
30+
2.97/1.43 org.eclipse.equinox.launcher.Main.basicRun(Main.java:608)
31+
2.97/1.43 org.eclipse.equinox.launcher.Main.run(Main.java:1515)
32+
2.97/1.43 org.eclipse.equinox.launcher.Main.main(Main.java:1488)
33+
2.97/1.43
34+
3.23/2.09 EOF

‎single-query-track/test/starexec-unknown/481860154.txt

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
0.00/0.02 unknown
2+
0.01/0.03 unknown
3+
0.01/0.04 unknown
4+
0.01/0.06 unknown
5+
0.01/0.07 unknown
6+
0.01/0.08 unknown
7+
0.01/0.10 unknown
8+
0.01/0.11 unknown
9+
0.10/0.12 unknown
10+
0.10/0.14 unknown
11+
0.10/0.15 unknown
12+
0.10/0.16 unknown
13+
0.10/0.17 unknown
14+
0.16/0.19 unknown
15+
0.16/0.20 unknown
16+
0.16/0.21 unknown
17+
0.16/0.22 unknown
18+
0.16/0.23 unknown
19+
0.16/0.24 unknown
20+
0.16/0.25 unknown
21+
0.16/0.26 unknown
22+
0.25/0.27 unknown
23+
0.26/0.28 unknown
24+
0.26/0.28 EOF

‎single-query-track/test/starexec-unknown/481860777.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
59.97/60.01 /export/starexec/sandbox/solver/bin/starexec_run_default: line 1: 3916 Alarm clock ./alt-ergo --no-locs-in-answers $1
2+
59.97/60.01 EOF

0 commit comments

Comments
 (0)