More benchmark cleanup and new suslik numbers

TyGuS · Mar 25, 2021 · 2198ce8 · 2198ce8
1 parent c968196
commit 2198ce8
Show file tree

Hide file tree

Showing 7 changed files with 31 additions and 31 deletions.
diff --git a/gen-table.py b/gen-table.py
@@ -67,36 +67,36 @@ def __init__(self, name, benchmarks):
 
 OLD_BENCHMARKS = [
   BenchmarkGroup("Integers",  [
-    Benchmark('ints/swap', 'swap two', ['suslik'],  stime=0.0, scode=12),
-    Benchmark('ints/min2', 'min of two', ['suslik','jennisys'], stime=0.1, scode=10),
+    Benchmark('ints/swap', 'swap two', ['suslik'],  stime=0.046, scode=12),
+    Benchmark('ints/min2', 'min of two', ['suslik','jennisys'], stime=0.354, scode=10),
     ]),    
   BenchmarkGroup("Singly Linked List", [
-    Benchmark('sll-bounds/len', 'length', ['suslik','natural'], stime=0.4, scode=21),
-    Benchmark('sll-bounds/max', 'max', ['suslik','natural'], stime=0.6, scode=27),
-    Benchmark('sll-bounds/min', 'min', ['suslik','natural'], stime=0.5, scode=27),
-    Benchmark('sll/singleton', 'singleton', ['suslik', 'jennisys'], stime=0.0, scode=11),
-    Benchmark('sll/free', 'dispose', ['suslik'], stime=0.0, scode=11),
-    Benchmark('sll/init', 'initialize', ['suslik'], stime=0.0, scode=13),
-    Benchmark('sll/copy', 'copy', ['suslik','dryad'], stime=0.2, scode=35),
-    Benchmark('sll/append', 'append', ['suslik','dryad'], stime=0.2, scode=19),
-    Benchmark('sll/delete-all', 'delete', ['suslik','dryad'], stime=0.7, scode=44),
+    Benchmark('sll-bounds/len', 'length', ['suslik','natural'], stime=1.112, scode=21),
+    Benchmark('sll-bounds/max', 'max', ['suslik','natural'], stime=0.678, scode=27),
+    Benchmark('sll-bounds/min', 'min', ['suslik','natural'], stime=0.670, scode=27),
+    Benchmark('sll/singleton', 'singleton', ['suslik', 'jennisys'], stime=0.064, scode=11),
+    Benchmark('sll/free', 'dispose', ['suslik'], stime=0.047, scode=11),
+    Benchmark('sll/init', 'initialize', ['suslik'], stime=0.136, scode=13),
+    Benchmark('sll/copy', 'copy', ['suslik','dryad'], stime=0.346, scode=35),
+    Benchmark('sll/append', 'append', ['suslik','dryad'], stime=0.370, scode=19),
+    Benchmark('sll/delete-all', 'delete', ['suslik','dryad'], stime=0.421, scode=44),
     ]),
   BenchmarkGroup("Sorted list", [
-    Benchmark('srtl/prepend', 'prepend', ['suslik','natural'], stime=0.2, scode=11),
-    Benchmark('srtl/insert', 'insert', ['suslik','natural'], stime=4.8, scode=58),
-    Benchmark('srtl/insertion-sort', 'insertion sort', ['suslik','natural'], stime=1.1, scode=28),
+    Benchmark('srtl/prepend', 'prepend', ['suslik','natural'], stime=0.182, scode=11),
+    Benchmark('srtl/insert', 'insert', ['suslik','natural'], stime=5.233, scode=58),
+    Benchmark('srtl/insertion-sort', 'insertion sort', ['suslik','natural'], stime=1.41, scode=28),
     ]),
   BenchmarkGroup("Tree", [
-    Benchmark('tree/size', 'size', ['suslik'], stime=0.2, scode=38),
-    Benchmark('tree/free', 'dispose', ['suslik'], stime=0.0, scode=16),
-    Benchmark('tree/copy', 'copy', ['suslik'], stime=0.4, scode=55),
-    Benchmark('tree/flatten-helper', 'flatten w/append', ['suslik'], stime=0.4, scode=48),
-    Benchmark('tree/flatten-acc', 'flatten w/acc', ['suslik'], stime=0.6, scode=35),
+    Benchmark('tree/size', 'size', ['suslik'], stime=0.326, scode=38),
+    Benchmark('tree/free', 'dispose', ['suslik'], stime=0.086, scode=16),
+    Benchmark('tree/copy', 'copy', ['suslik'], stime=0.716, scode=55),
+    Benchmark('tree/flatten-helper', 'flatten w/append', ['suslik'], stime=0.663, scode=48),
+    Benchmark('tree/flatten-acc', 'flatten w/acc', ['suslik'], stime=0.701, scode=35),
     ]),
   BenchmarkGroup("BST", [
-    Benchmark('bst/insert', 'insert', ['suslik','natural'], stime=31.9, scode=58),
-    Benchmark('bst/left-rotate', 'rotate left', ['suslik','natural'], stime=37.7, scode=15),
-    Benchmark('bst/right-rotate', 'rotate right', ['suslik','natural'], stime=17.2, scode=15),
+    Benchmark('bst/insert', 'insert', ['suslik','natural'], stime=36.875, scode=58),
+    Benchmark('bst/left-rotate', 'rotate left', ['suslik','natural'], stime=23.873, scode=15),
+    Benchmark('bst/right-rotate', 'rotate right', ['suslik','natural'], stime=9.109, scode=15),
     Benchmark('bst/delete-root', 'delete root', ['natural']),
     ]),
   BenchmarkGroup("Doubly Linked List", [

diff --git a/src/test/resources/synthesis/simple-benchmarks/bst/insert.syn b/src/test/resources/synthesis/simple-benchmarks/bst/insert.syn
@@ -5,6 +5,6 @@ binary search tree: insert an element
 
 {0 <= n /\ 0 <= k /\ k <= 7 ; ret :-> k ** bst(x, n, lo, hi) }
 void bst_insert (loc x, loc ret)
-{b == a + 3 /\ n1 == n + 1 /\ lo1 == (k <= lo ? k : lo)  /\ hi1 == (hi <= k ? k : hi) ; ret :-> y ** bst(y, n1, lo1, hi1) }
+{n1 == n + 1 /\ lo1 == (k <= lo ? k : lo)  /\ hi1 == (hi <= k ? k : hi) ; ret :-> y ** bst(y, n1, lo1, hi1) }
 
 #####
diff --git a/src/test/resources/synthesis/simple-benchmarks/bst/left-rotate.syn b/src/test/resources/synthesis/simple-benchmarks/bst/left-rotate.syn
@@ -2,7 +2,7 @@ binary search tree: rotate left
 
 #####
 
-{ not (r == 0) /\ 0 <= sz1 /\  0 <= sz2  /\  0 <= v /\ v <= 7 /\ hi1 <= v /\ v <= lo2 /\ 0 <= a /\ 0 <= b  ;
+{ not (r == 0) /\ 0 <= sz1 /\  0 <= sz2  /\  0 <= v /\ v <= 7 /\ hi1 <= v /\ v <= lo2  ;
   ret :-> unused ** [x, 3] ** x :-> v ** (x + 1) :-> l ** (x + 2) :-> r ** bst(l, sz1, lo1, hi1) ** bst(r, sz2, lo2, hi2) }
 void bst_left_rotate (loc x, loc ret)
 { sz3 + sz4 == sz1 + sz2 /\  0 <= sz3 /\  0 <= sz4  /\  0 <= v3 /\ v3 <= 7 /\ hi3 <= v3 /\ v3 <= lo4 ;

diff --git a/src/test/resources/synthesis/simple-benchmarks/bst/right-rotate.syn b/src/test/resources/synthesis/simple-benchmarks/bst/right-rotate.syn
@@ -2,7 +2,7 @@ binary search tree: rotate right
 
 #####
 
-{ not (l == 0) /\ 0 <= sz1 /\  0 <= sz2  /\  0 <= v /\ v <= 7 /\ hi1 <= v /\ v <= lo2 /\ 0 <= a /\ 0 <= b ;
+{ not (l == 0) /\ 0 <= sz1 /\  0 <= sz2  /\  0 <= v /\ v <= 7 /\ hi1 <= v /\ v <= lo2 ;
   ret :-> unused ** [x, 3] ** x :-> v ** (x + 1) :-> l ** (x + 2) :-> r ** bst(l, sz1, lo1, hi1) ** bst(r, sz2, lo2, hi2) }
 void bst_right_rotate (loc x, loc ret)
 { sz3 + sz4 == sz1 + sz2 /\ 0 <= sz3 /\  0 <= sz4  /\  0 <= v3 /\ v3 <= 7 /\ hi3 <= v3 /\ v3 <= lo4 ;

diff --git a/src/test/resources/synthesis/simple-benchmarks/dll/append.syn b/src/test/resources/synthesis/simple-benchmarks/dll/append.syn
@@ -4,8 +4,8 @@ doubly-linked list: append
 
 #####
 
-{true ; dll(x1, a, s1) ** dll(x2, b, s2) ** ret :-> x2}
+{ dll(x1, a, s1) ** dll(x2, b, s2) ** ret :-> x2 }
 void dll_append (loc x1, loc ret)
-{s =i s1 ++ s2 ; dll(y, c, s) ** ret :-> y }
+{ s == s1 ++ s2 ; dll(y, c, s) ** ret :-> y }
 
 #####
diff --git a/src/test/resources/synthesis/simple-benchmarks/dll/copy.syn b/src/test/resources/synthesis/simple-benchmarks/dll/copy.syn
@@ -4,8 +4,8 @@ doubly-linked list: copy
 
 #####
 
-{true ; r :-> x ** dll(x, a, s)}
+{ r :-> x ** dll(x, a, s)}
 void dll_copy(loc r)
-{true ; r :-> y ** dll(x, a, s) ** dll(y, b, s) }
+{ r :-> y ** dll(x, a, s) ** dll(y, b, s) }
 
 #####
diff --git a/src/test/resources/synthesis/simple-benchmarks/dll/delete-all.syn b/src/test/resources/synthesis/simple-benchmarks/dll/delete-all.syn
@@ -3,8 +3,8 @@ doubly-linked list: delete all occurrences of x
 
 #####
 
-{true ; dll(x, b, s) ** ret :-> a}
+{ dll(x, b, s) ** ret :-> a }
 void dll_delete_all (loc x, loc ret)
-{s1 =i s -- {a} ; dll(y, c, s1) ** ret :-> y }
+{ s1 == s -- {a} ; dll(y, c, s1) ** ret :-> y }
 
 #####