Converting examples to higher order predicates

Symbol	Meaning
🕘	Ongoing implementation
✔️	Implemented
✔️ ✳️	Partially implemented
🔷	Not applicable
❓	Should higher-order predicates be used here?
❌	Not working due to a likely bug

In the src/test/resources/synthesis directory:

Name	Status
abduct	✔️ ✳️
account	🔷
all-benchmarks/avl	❓
all-benchmarks/bst	❓
all-benchmarks/dll	✔️
all-benchmarks/ints	🔷
all-benchmarks/multi-list	🕘
all-benchmarks/packed	❓
all-benchmarks/rbt	❓
all-benchmarks/rose-tree	❓
all-benchmarks/sll	✔️ ✳️
all-benchmarks/srtl	❌
all-benchmarks/tree	✔️ ✳️
cardio	❓
certification-benchmarks-advanced/*	🕘
certification-benchmarks/*	🕘
certification/*	🕘
copy-len	🔷
copy	🔷
cyclic-benchmarks/*	🕘
dllist	✔️ ✳️
entail	🔷
flatten	❓
ints	🔷
llist	❌
overloaded-ops	🔷
packed-tree	🕘
paper-benchmarks/*	🕘
paper-examples	🕘
proofs	🔷
regression	🔷
sets	🔷
smallfoot	🔷
syntax	🔷
tree	✔️ ✳️

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) }
}