Converting examples to higher order predicates - roboguy13/suslik GitHub Wiki
Symbol | Meaning |
---|---|
:clock9: | Ongoing implementation |
:heavy_check_mark: | Implemented |
:heavy_check_mark: :eight_spoked_asterisk: | Partially implemented |
:large_blue_diamond: | Not applicable |
:question: | Should higher-order predicates be used here? |
:x: | Not working due to a likely bug |
src/test/resources/synthesis
directory:
In the Name | Status |
---|---|
abduct |
:heavy_check_mark: :eight_spoked_asterisk: |
account |
:large_blue_diamond: |
all-benchmarks/avl |
:question: |
all-benchmarks/bst |
:question: |
all-benchmarks/dll |
:heavy_check_mark: |
all-benchmarks/ints |
:large_blue_diamond: |
all-benchmarks/multi-list |
:clock9: |
all-benchmarks/packed |
:question: |
all-benchmarks/rbt |
:question: |
all-benchmarks/rose-tree |
:question: |
all-benchmarks/sll |
:heavy_check_mark: :eight_spoked_asterisk: |
all-benchmarks/srtl |
:x: |
all-benchmarks/tree |
:heavy_check_mark: :eight_spoked_asterisk: |
cardio |
:question: |
certification-benchmarks-advanced/* |
:clock9: |
certification-benchmarks/* |
:clock9: |
certification/* |
:clock9: |
copy-len |
:large_blue_diamond: |
copy |
:large_blue_diamond: |
cyclic-benchmarks/* |
:clock9: |
dllist |
:heavy_check_mark: :eight_spoked_asterisk: |
entail |
:large_blue_diamond: |
flatten |
:question: |
ints |
:large_blue_diamond: |
llist |
:x: |
overloaded-ops |
:large_blue_diamond: |
packed-tree |
:clock9: |
paper-benchmarks/* |
:clock9: |
paper-examples |
:clock9: |
proofs |
:large_blue_diamond: |
regression |
:large_blue_diamond: |
sets |
:large_blue_diamond: |
smallfoot |
:large_blue_diamond: |
syntax |
:large_blue_diamond: |
tree |
:heavy_check_mark: :eight_spoked_asterisk: |
Representative examples
sll
and dll
predicate dll(loc x, loc z, set s) {
| x == 0 => { s =i {} ; emp }
| not (x == 0) =>
{ s =i {v} ++ s1 ; [x, 3] ** x :-> v ** (x + 1) :-> w ** (x + 2) :-> z ** dll(w, x, s1) }
}
predicate sll(loc x, set s) {
| x == 0 => { s =i {} ; emp }
| not (x == 0) => { s =i {v} ++ s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
}
generalized to
predicate g_list(loc x, loc z, set s, pred pz, pred sp) {
| x == 0 => { s =i {} ; emp }
| not (x == 0) => {
pz(x, z, y) && s =i {v} ++ s1
;
sp(x, z) ** x :-> v ** (x + 1) :-> w ** g_list(w, y, s1, pz, sp) }
}
synonym dll(loc x, loc z, set s) {
g_list(x, z, s, pred(x0, z, y) => y == x0, pred(p, q) => [p, 3] ** (p+2) :-> q)
}
synonym sll(loc x, set s) {
g_list(x, 0, s, pred(x0, z, y) => z == y, pred(r, t) => [r, 2])
}
tree
and treeN
predicate tree(loc x, set s) {
| x == 0 => {s == {} ; emp}
| not (x == 0) => {
s == {v} ++ s1 ++ s2
;
[x, 3] ** x :-> v ** (x + 1) :-> l ** (x + 2) :-> r ** tree(l, s1) ** tree(r, s2)}
}
predicate treeN(loc x, int n) {
| x == 0 => { n == 0 ; emp }
| not (x == 0) => {
n == 1 + n1 + n2 /\ 0 <= n1 /\ 0 <= n2
;
[x, 3] ** x :-> v ** (x + 1) :-> l ** (x + 2) :-> r ** treeN(l, n1) ** treeN(r, n2)}
}
generalized to
predicate g_tree(loc x, any s, pred emptyP, pred nodeP) {
| x == 0 => {emptyP(s) ; emp}
| not (x == 0) => {
nodeP(s, v, s1, s2)
;
[x, 3] ** x :-> v ** (x + 1) :-> l ** (x + 2) :-> r **
g_tree(l, s1, emptyP, nodeP) ** g_tree(r, s2, emptyP, nodeP)}
}
synonym tree(loc x, set s) {
g_tree(x, s,
pred(currS) => currS == {},
pred(currS, v, s1, s2) => currS == {v} ++ s1 ++ s2)
}
synonym treeN(loc x, int n) {
g_tree(x, n,
pred(currN) => currN == 0,
pred(currN, v, n1, n2) => currN == 1 + n1 + n2 /\ 0 <= n1 /\ 0 <= n2)
}
sll
and ulist
predicate sll(loc x, set s) {
| x == 0 => { s == {} ; emp }
| not (x == 0) => { s == {v} ++ s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
}
predicate ulist(loc x, set s) {
| x == 0 => { s == {} ; emp }
| not (x == 0) => {
s == {v} ++ s1 /\ not (v in s1)
;
[x, 2] ** x :-> v ** (x + 1) :-> nxt ** ulist(nxt, s1) }
}
generalizes to
predicate g_sll(loc x, set s, pred accNil, pred accCons, pred p) {
| x == 0 => { accNil(x, s) ; emp }
| not (x == 0) => {
accCons(v, s, s1) /\ p(v, s1)
;
[x, 2] ** x :-> v ** (x + 1) :-> nxt ** g_sll(nxt, s1, accNil, accCons, p) }
}
synonym sll(loc x, set s) {
g_sll(x, s,
pred(currX, currS) => currS == {},
pred(v, currS, s1) => currS == {v} ++ s1,
pred(v, nextS) => true)
}
synonym ulist(loc x, set s) {
g_sll(x, s,
pred(ignore1, currS) => currS == {},
pred(v, currS, s1) => currS == {v} ++ s1,
pred(v, nextS) => not (v in nextS))
}
TODO: Try to use this generalization to also implement sll_bounded
and len_interval
.
sll
and srtl
The example here is not currently working.
predicate sll(loc x, interval s, int len) {
| x == 0 => { len == 0 && s == [] ; emp }
| not (x == 0) => { len == len1 + 1 && len1 >= 0 &&
s == [v] + s1 ;
[x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1, len1) }
}
predicate srtl(loc x, interval s, int len) {
| x == 0 => { len == 0 && s == [] ; emp }
| not (x == 0) => { len == len1 + 1 && len1 >= 0 &&
s == [v] + s1 && lower s == v ;
[x, 2] ** x :-> v ** (x + 1) :-> nxt ** srtl(nxt, s1, len1) }
}
should generalize to
predicate g_sll(loc x, interval s, int len, pred p) {
| x == 0 => { len == 0 && s == [] ; emp }
| not (x == 0) => { len == len1 + 1 && len1 >= 0 &&
s == [v] + s1 && p(s, v) ;
[x, 2] ** x :-> v ** (x + 1) :-> nxt ** g_sll(nxt, s1, len1, p) }
}
synonym sll(loc x, interval s, int len) {
g_sll(x, s, len, pred(ignore1, ignore2) => true)
}
synonym srtl(loc x, interval s, int len) {
g_sll(x, s, len, pred(currS, v) => lower currS == v)
}
"Optional" argument used in recursive application
Unclear how to implement a generalization of this currently:
predicate lseg(loc x, loc y, set s) {
| x == y => { s =i {} ; emp }
| not (x == y) => { s =i {v} ++ s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
}
predicate lseg2(loc x, set s) {
| x == 0 => { s =i {} ; emp }
| not (x == 0) => {
s =i {v} ++ s1
;
[x, 3] ** x :-> v ** (x + 1) :-> v + 1 ** (x + 2) :-> nxt ** lseg2(nxt, s1) }
}