Added files for TABLEAUX15 release.

README.TABLEAUX15

@@ -0,0 +1,44 @@
+OVERVIEW:
+This file contains instructions about the tool described in
+the TABLEAUX'15 paper
+
+  J. Brotherston and N. Gorogiannis.
+  Disproving Inductive Entailments in Separation Logic 
+  via Base Pair Approximation
+
+If you downloaded the binary release from GitHub a x64 binary
+should be already present in this directory.  If you 
+do not have such a binary, look at the file README.compiling.
+
+Running the executable (sl_disprove.native) without options will produce 
+some help text explaining its usage.
+
+There are three classes of benchmarks described in the paper.  The classes
+SLL and UDP are from the SL-COMP14 competition:
+
+  https://github.com/mihasighi/smtcomp14-sl
+
+The benchmarks for SLL and UDP can be downloaded from the repository above.
+
+The third class (LEM) is included in this tree, in 
+
+  tests/sl_disproof
+
+The definitions are in "all.defs" and the sequents in "seqs".  The "invbench.sh"
+script will execute the LEM benchmark.
+
+================================================================================
+THEORY:
+See papers/TABLEAUX15.{pdf,bib}
+
+================================================================================
+CONTACT:
+Questions and help to get things working: 
+  nikos.gorogiannis+cyclist@gmail.com
+
+Github: 
+  https://github.com/ngorogiannis/cyclist
+
+URL (papers and software): 
+  http://www.cs.mdx.ac.uk/staffpages/nikosgkorogiannis/  
+

tests/sl_disproof/all.defs

@@ -0,0 +1,225 @@
+BinListFirst {
+  emp => BinListFirst(x) |
+  nil!=x * x->yp',xp' * BinListFirst(yp') => BinListFirst(x)
+} ;
+BinListSecond {
+  emp => BinListSecond(x) |
+  nil!=x * x->yp',xp' * BinListSecond(xp') => BinListSecond(x)
+} ;
+BinPath {
+  x=y => BinPath(x,y) |
+  nil!=x * x->xp',yp' * BinPath(xp',y) => BinPath(x,y) |
+  nil!=x * x->xp',yp' * BinPath(yp',y) => BinPath(x,y)
+} ;
+BinTree {
+  emp => BinTree(x) |
+  nil!=x * x->yp',xp' * BinTree(yp') * BinTree(xp') => BinTree(x)
+} ;
+BinTreeSeg {
+  x=y => BinTreeSeg(x,y) |
+  nil!=x * x->xp',yp' * BinTreeSeg(xp',y) * BinTree(yp') => BinTreeSeg(x,y) |
+  nil!=x * x->xp',yp' * BinTree(xp') * BinTreeSeg(yp',y) => BinTreeSeg(x,y)
+} ;
+BSLL {
+  x=y => BSLL(x,y) |
+  nil!=xp' * xp'->yp',y * BSLL(x,xp') => BSLL(x,y)
+} ;
+clist {
+  in=self_19' * in->p_18' * lseg(p_18',self_19') => clist(in)
+} ;
+DLL1_plus {
+  hd->nil,p => DLL1_plus(hd,p) |
+  hd->x',p * DLL1_plus(x',hd) => DLL1_plus(hd,p)
+} ;
+DLL2_plus {
+  hd=tl * hd->n,p,down_hd' * DLL1_plus(down_hd',hd) => DLL2_plus(hd,p,tl,n) |
+  hd->x',p,down_hd' * DLL1_plus(down_hd',hd) * DLL2_plus(x',hd,tl,n) => DLL2_plus(hd,p,tl,n)
+} ;
+DLL2_plus_rev {
+  hd=tl * hd->n,p,down_hd' * DLL1_plus(down_hd',hd) => DLL2_plus_rev(hd,p,tl,n) |
+  tl->n,x',down_hd' * DLL1_plus(down_hd',tl) * DLL2_plus_rev(hd,p,x',tl) => DLL2_plus_rev(hd,p,tl,n)
+} ;
+DLL {
+  p=tl * hd=n => DLL(hd,p,tl,n) |
+  hd->x',p * DLL(x',hd,tl,n) => DLL(hd,p,tl,n)
+} ;
+dll_e1 {
+  in=s' * q=p1' * dll(q1',s') * in->p1',q1' => dll_e1(in,q)
+} ;
+dll_e2 {
+  n'=q1' * p1'=p2' * in=s' * q=p2' * in->p1',n' * dll(q1',s') => dll_e2(in,q)
+} ;
+dll_e3 {
+  p=q' * dll(in,q') => dll_e3(in,p)
+} ;
+DLL_plus {
+  hd=tl * hd->n,p => DLL_plus(hd,p,tl,n) |
+  hd->x',p * DLL_plus(x',hd,tl,n) => DLL_plus(hd,p,tl,n)
+} ;
+DLL_plus_mid {
+  hd=tl * hd->n,p => DLL_plus_mid(hd,p,tl,n) |
+  hd->tl,p * points_to(tl,n,hd) => DLL_plus_mid(hd,p,tl,n) |
+  x'->y',z' * DLL_plus(y',x',tl,n) * DLL_plus_rev(hd,p,z',x') => DLL_plus_mid(hd,p,tl,n)
+} ;
+DLL_plus_rev {
+  hd=tl * hd->n,p => DLL_plus_rev(hd,p,tl,n) |
+  tl->n,x' * DLL_plus_rev(hd,p,x',tl) => DLL_plus_rev(hd,p,tl,n)
+} ;
+elseg {
+  in=p => elseg(in,p) |
+  in->a' * a'->b' * elseg(b',p) => elseg(in,p)
+} ;
+enode {
+  p=p0' * l=l0' * r=r0' * n=n0' * in->p0',l0',r0',n0' => enode(in,p,l,r,n)
+} ;
+eright_nil {
+  p0'=p1' * l0'=l1' * r0'=r1' * n0'=n1' * nil=r1' * in->p0',l0',r0',n0' => eright_nil(in)
+} ;
+eright_nnil {
+  p0'=p1' * l0'=l1' * r0'=r1' * n0'=n1' * nil=r1' * in->p0',l0',r0',n0' * tree(l1') * tree(r1') => eright_nnil(in)
+} ;
+etll {
+  p=p1' * t=t1' * tll(in,p1',r,t1') => etll(in,p,t,r)
+} ;
+List {
+  nil!=x * x->y => List(x,y) |
+  nil!=x * x->xp' * List(xp',y) => List(x,y)
+} ;
+ListE {
+  nil!=x * x->xp' * ListO(xp',y) => ListE(x,y)
+} ;
+ListO {
+  nil!=x * x->y => ListO(x,y) |
+  nil!=x * x->xp' * ListE(xp',y) => ListO(x,y)
+} ;
+ListX {
+  ListO(x,y) => ListX(x,y) |
+  ListE(x,y) => ListX(x,y)
+} ;
+ll {
+  nil=in => ll(in) |
+  in->q_18' * ll(q_18') => ll(in)
+} ;
+ll_e1 {
+  in->q' * ll(q') => ll_e1(in)
+} ;
+ll_e2 {
+  p'=q' * in->p' * ll(q') => ll_e2(in)
+} ;
+ls {
+  x=y => ls(x,y) |
+  nil!=x * x!=y * x->xp' * ls(xp',y) => ls(x,y)
+} ;
+lseg {
+  in=p => lseg(in,p) |
+  in->a' * lseg(a',p) => lseg(in,p)
+} ;
+lseg_e1 {
+  p=q' * lseg(in,p) => lseg_e1(in,p)
+} ;
+lso {
+  in=out => lso(in,out) |
+  in!=out * in->u' * lso(u',out) => lso(in,out)
+} ;
+lsso {
+  in=out => lsso(in,out) |
+  in->u',u' * lsso(u',out) => lsso(in,out)
+} ;
+ltll {
+  in->p,l,r,D * tll(l,in,v,l1') * tll(r,in,l1',t) => ltll(in,p,l,r,D,v,t)
+} ;
+nll {
+  in=out => nll(in,out,boundary) |
+  in!=out * in->u',Z1' * lso(Z1',boundary) * nll(u',out,boundary) => nll(in,out,boundary)
+} ;
+node2_e1 {
+  p=p1' * q=n1' * in->p1',n1' => node2_e1(in,p,q)
+} ;
+node_e1 {
+  q=p' * in->p' => node_e1(in,q)
+} ;
+olseg {
+  in->p => olseg(in,p) |
+  in->a' * a'->b' * olseg(b',p) => olseg(in,p)
+} ;
+points_to {
+  a->b,c => points_to(a,b,c)
+} ;
+right1 {
+  lseg(in,u') * u'->p => right1(in,p)
+} ;
+right2 {
+  lseg(in,u') * lseg(u',p) => right2(in,p)
+} ;
+right3 {
+  lseg(in,u') * lseg(u',u2') * lseg(u2',p) => right3(in,p)
+} ;
+right4 {
+  lseg(in,u') * lseg(u',w') => right4(in)
+} ;
+right5 {
+  lseg(in,w') => right5(in)
+} ;
+right {
+  elseg(in,u') * elseg(u',p) => right(in,p)
+} ;
+right_nil {
+  nil=r' * in->p',l',r',n' => right_nil(in)
+} ;
+right_nnil {
+  nil!=r' * in->p',l',r',n' * tree(l') * tree(r') => right_nnil(in)
+} ;
+RList {
+  nil!=x * x->y => RList(x,y) |
+  nil!=xp' * xp'->y * RList(x,xp') => RList(x,y)
+} ;
+skl1 {
+  hd=ex => skl1(hd,ex) |
+  hd!=ex * hd->nil,tl' * skl1(tl',ex) => skl1(hd,ex)
+} ;
+skl2 {
+  hd=ex => skl2(hd,ex) |
+  hd!=ex * hd->tl',Z1' * skl1(Z1',tl') * skl2(tl',ex) => skl2(hd,ex)
+} ;
+skl3 {
+  hd=ex => skl3(hd,ex) |
+  hd!=ex * hd->tl',Z2',Z1' * skl1(Z1',Z2') * skl2(Z2',tl') * skl3(tl',ex) => skl3(hd,ex)
+} ;
+SLL {
+  x=y => SLL(x,y) |
+  nil!=x * x->xp',yp' * SLL(xp',y) => SLL(x,y)
+} ;
+TLL_aux {
+  x->back,r',up',nil * TLL_aux(up',p,lr',x,top,mright) * TLL_plus(r',x,z,lr') => TLL_aux(x,p,z,back,top,mright) |
+  x=top * x->back,r',p,nil * TLL_plus(r',x,z,mright) => TLL_aux(x,p,z,back,top,mright)
+} ;
+tll {
+  nil=l_23' * in=ll * lr=lr_28' * in->p_21',D1_22',l_23',lr_28' => tll(in,p,ll,lr) |
+  nil!=r_25' * p=p_29' * in=self_30' * ll=ll_31' * in=self_32' * z_33'=z_27' * lr=lr_34' * in->p_29',l_24',r_25',D2_26' * tll(l_24',self_30',ll_31',z_27') * tll(r_25',self_32',z_33',lr_34') => tll(in,p,ll,lr)
+} ;
+TLL_plus {
+  root=ll * root->nil,nil,par,lr => TLL_plus(root,par,ll,lr) |
+  root->l',r',par,nil * TLL_plus(l',root,ll,z') * TLL_plus(r',root,z',lr) => TLL_plus(root,par,ll,lr)
+} ;
+TLL_plus_rev {
+  top=mleft * top->nil,nil,p,mright => TLL_plus_rev(top,p,mleft,mright) |
+  mleft=x' * x'->nil,nil,up',lr' * TLL_aux(up',p,lr',x',top,mright) => TLL_plus_rev(top,p,mleft,mright)
+} ;
+TLL_tail {
+  root=ll * root=tr * root->nil,nil,par,lr => TLL_tail(root,par,ll,tr,lr) |
+  root->l',r',par,nil * TLL_plus(l',root,ll,z') * TLL_tail(r',root,z',tr,lr) => TLL_tail(root,par,ll,tr,lr)
+} ;
+TPP_aux {
+  x->down,right',up' * TPP_plus(right',x) * TPP_aux(up',x,top,b) => TPP_aux(x,down,top,b) |
+  x->left',down,up' * TPP_plus(left',x) * TPP_aux(up',x,top,b) => TPP_aux(x,down,top,b) |
+  x=top * x->down,right',b * TPP_plus(right',x) => TPP_aux(x,down,top,b) |
+  x=top * x->left',down,b * TPP_plus(left',x) => TPP_aux(x,down,top,b)
+} ;
+TPP_plus {
+  x->nil,nil,back => TPP_plus(x,back) |
+  x->y',z',back * TPP_plus(y',x) * TPP_plus(z',x) => TPP_plus(x,back)
+} ;
+TPP_plus_rev {
+  top->nil,nil,b => TPP_plus_rev(top,b) |
+  x'->nil,nil,up' * TPP_aux(up',x',top,b) => TPP_plus_rev(top,b)
+} 

tests/sl_disproof/invbench.sh

@@ -0,0 +1,3 @@
+#!/bin/bash
+
+cat seqs | tr '\n' '\0' | nice xargs -n 1 -P 4 -0 ./run-inv-test.sh

tests/sl_disproof/run-inv-test.sh

@@ -0,0 +1,30 @@
+#!/bin/bash
+
+CMD=../../sl_disprove.native
+QUERY=$1
+NAME=$(echo "$QUERY" | md5sum | cut -f1 -d' ')
+LOG="results/${NAME}.log"
+OUT="results/${NAME}.out"
+DEFS=all.defs
+
+exec > "$LOG"
+exec 2>&1
+
+export OCAMLRUNPARAM=b
+"$CMD" -s -t 60 -IP -D "$DEFS" -S "$QUERY" > "$OUT" 2>&1
+
+STATUS=$?
+if [ $STATUS -eq 0 ]; then 
+  PROVER_STATUS="unsat"
+elif [ $STATUS -eq 255 ]; then
+  PROVER_STATUS="sat"
+else
+  PROVER_STATUS="unknown"
+fi
+
+echo ============
+echo -e "Query: $QUERY" 
+echo ============
+echo -e "Status: ${PROVER_STATUS}"
+echo ============
+