/***************************************************************************/
/* SMT */
/***************************************************************************/

/***************************************************************************/
/* function declaration */
/***************************************************************************/

/* nonvar, flat and preserving respectively denote the indexes 
   in I0, Inv and Inst */
/* see the research report */

function select : [nonvar = [1], flat = [2], preserving = [2] ].
function ord : [flat = [1,2]].
function inf : [nonvar = [1,2]].
function car : [nonvar = [1] ].
function cdr : [nonvar = [1] ].
function prev : [nonvar = [1] ].
function next : [nonvar = [1] ].
function cons : [nonvar = [1,2]].
function enc : [nonvar = [1,2]].
function dec : [nonvar = [1,2]].
function s : [nonvar = [1]].
function p : [nonvar = [1]].
function succ : [nonvar = [1]].
function ia : [nonvar = [1]].
function sa : [nonvar = [1]].
function store : [nonvar = [1,2,3]].

%constants = [nil, true]. % not necessary 

/* The following list contains all the symbols in C */

restricted_symbols = [enc,dec,s,succ,p,sa,ia,eqa,partitioned,bsorteda,beqa,cons,car,cdr,store,next,prev].

/***************************************************************************/
/* some theories */
/***************************************************************************/

/* The syntax is straightforward. */

/* <clause> = <cl_id> : [ <lit_list> ] | [] */
/* <lit_list> = <literal> {, literal}* */
/* <literal> = <atom> | not(<atom>) */
/* <atom> = <term> = <term> */
/* terms are written using Prolog conventions, in particular variables
   start with a capital letter */

/* sets of clauses can be constructed from cl_id or other clause sets */

/* ordering */

o1 : [not(ord(X,Y) = true), not(ord(Y,X) = true)].
o2 : [not(ord(X,Y) = true), not(ord(Y,Z) = true), ord(X,Z) = true].

ord = [o1,o2].

/* natural number */

n1 : [not(0 = succ(_Y))].
n2 : [X = Y, not(succ(X) = succ(Y))].

nat = [n1,n2].

/* inf on nat */

inf1 : [not(inf(X,Y) = true), not(inf(succ(X),succ(Y))= true)].
inf2 : [inf(0,succ(_X)) = true].

inf = [inf1,inf2].

/* integer offset */

i1 : [p(s(X)) = X].
i2 : [s(p(X)) = X].
i3 : [not(s(X) = X)].
i4 : [not(p(X) = X)].

integeroffset = [i1,i2,i3,i4].

/* list */

l1 : [car(cons(X,_Y)) = X].
l2 : [cdr(cons(_X,Y)) = Y].
l3 : [X = nil, cons(car(X),cdr(X)) = X].
l4 : [not(cons(X,Y) = nil)].

list = [l1,l2,l3,l4].

/* encryption */

e1 : [enc(dec(X,Y),Y) = X].
e2 : [dec(enc(X,Y),Y) = X].

encrypt = [e1,e2].

/* linked list */

ll1 : [X = nil, next(X) = nil, prev(next(X)) = X].
ll2 : [X = nil, prev(X) = nil, next(prev(X)) = X].
ll3 : [not(prev(X) = prev(Y)), prev(X) = nil, prev(Y) = nil, X = Y, X = nil, Y = nil].
ll4 : [not(next(X) = next(Y)), next(X) = nil, next(Y) = nil, X = Y, X = nil, Y = nil].

ll = [ll1,ll2,ll3,ll4].

/* array */

array1 : [select(store(_T,I,V),I) = V].
array2 : [I = J, select(store(T,I,_V),J) = select(T,J)].
array3 : [not(sa(T) = true), select(select(T,I),J) = select(select(T,J),I)].
array4 : [not(ia(T) = true), I = J, not(select(T,I) = select(T,J))].
array5 : [not(eqa(T,S) = true), select(T,I) = select(S,I)].
array6 : [not(beqa(T,S,L,U) = true), not(inf(L,I) = true), not(inf(I,U) = true), select(T,I) = select(S,I)].
array7 : [not(bsorteda(T,L,U) = true), not(inf(L,I) = true), not(inf(I,U) = true), inf(select(T,I),select(S,I)) = true].
array8 : [not(bsorteda(T,L,U) = true), not(inf(L,I) = true), not(inf(I,J) = true), not(inf(J,U) = true), inf(select(T,I),select(S,J)) = true].
array9 : [not(partitioned(T,L1,U1,L2,U2) = true), not(inf(L1,I) = true), not(inf(I,U1) = true), not(inf(U1,L2) = true), not(inf(L2,J) = true), not(inf(J,U2) = true), inf(select(T,I),select(S,J)) = true].

array = [array1,array2,array3,array4,array5,array6,array7,array8,array9].

/***************************************************************************/

all = [ord,nat,integeroffset,inf,array,ll,encrypt,list].

/***************************************************************************/
/* Specify the negative literal that should be selected */
/* (ordering is built-in) */

select_lit not(sa(T) = true).
select_lit not(ia(T) = true).
select_lit not(eqa(T,S) = true).
select_lit not(beqa(T,S,L,U) = true).
select_lit not(bsorteda(T,L,U) = true).
select_lit not(partitioned(T,L,U,LL,UU) = true).

/* this command check that a theory is restrained */

controllable(all).