% ex ... file of examples etc.


pred_def( void/0, [], [], [] ).

init_clause(( void :- true )).

ex( void, true ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% List Processing: Membership // 3 ex's is enough if head depth ==1


pred_def( mmember/2, [ -x, +xl ], [ mmember/2 , llast/2 ], [] ).

%ex( mmember( a, []), false).
ex( mmember( a, [ a ] ), true ).

%ex( mmember( b, [ a ] ), false ).
%ex( mmember( a, [ a, b ] ), true ).
%ex( mmember( a, [ a, b, c]), true ).
%ex( mmember( a, [ b ] ), false ).
%ex( mmember( a, [ b, a ] ), true ).
%ex( mmember( a, [ b, c ] ), false). %L.P.
ex( mmember( a, [ b, c, a, d]), true).


% Different constants

%ex( mmember( a, [ a ] ), true ).
%ex( mmember( b, [ c ] ), false ). %orriginaly
%%ex( mmember( d, [ e, d] ), true ).
%%ex( mmember( f, [ g, h, f] ), true ).
/*
ex( mmember( b, [ c, b ] ), true ).
ex( mmember( d, [ e, d ] ), true ).
ex( mmember( d, [ e, b ] ), false).
*/

%ex( mmember( f, [ g, h, f] ), true ).

% Assumptions

%ass( mmember( b, [ c ] ), false ).

%ex(  mmember( b, [ a ] ), false ). % for last/2


%ex( mmember( d, [ e, ch, d] ), true ).

/*
setting 

Max. free variables: 1
Max. goals: 1
Max. goals added in one step: 2
Max. head argument depth: 1
Max. clause length: 999
Search ahead depth: 2
*/

%ex( mmember( b, [b,a] ), false).


%ex( mmember( a, [ b, c ] ), false). %L.P.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  member/2 -- tryinig just 1 positive example, -> mmember(X,[Y,X|Z]):-true.
 
/*
%ex( mmember( a, [ a ] ), true ).
ex( mmember( b, [ a ] ), false ).
ex( mmember( a, [ b, a ] ), true ).
%%ex( mmember( a, [ b, c ] ), false). %L.P.
ex( mmember(1,[2]),false).
ex( mmember(1,[2,3]), false).
*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% List Processing: List concatenation

/*
pred_def( aappend/3, [ +xl, +xl, -xl ], [ aappend/3 ], [] ).

ex( aappend( [], [ a ], [ a ] ), true ).

%ex( aappend( [ a ], [ a ], [ a ] ), false ). %orriginaly

ex( aappend( [ a, b ], [ c, d ], [ a, b, c, d ] ), true ).
%ex( aappend( [ b ], [ c, d ], [ b, c, d ] ), true ).



%ex( aappend([],[],[1]),false). % as a 1st relevant negative(gn used)
*/

/*

% max. number of free variables (additionaly introduced variables)

sys_set( mx_free_vars, 1).   !!! principal: 0 is too small

sys_set( mx_goals, 1 ). %L.P. was 3
sys_set( mx_add_goals, 2). % L.P. was 2
sys_set( mx_arg_depth, 1).  % L.P. was 3
sys_set( mx_clause_length, 999). % L.P. was 999
sys_set( search_ahead_depth, 2 ).



*/


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% List Processing: List concatenation - only positive examples!

/*
pred_def( aappend/3, [ +xl, +xl, -xl ], [ aappend/3 ], [] ).

ex( aappend( [], [ a ], [ a ] ), true ).
ex( aappend( [ a, b ], [ c, d ], [ a, b, c, d ] ), true ).
ex( aappend( [ b ], [ c, d ], [ b, c, d ] ), true ).
*/

/*
 Correct solution found with the following settings

Max. free variables: 1
Max. goals: 1
Max. goals added in one step: 2
Max. head argument depth: 1
Max. clause length: 999

*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% List Processing: List concatenation - not on the same path


pred_def( aappend/3, [ +xl, +xl, -xl ], [ aappend/3 ], [] ).

%ex( aappend( [], [ a ], [ a ] ), true ).
ex( aappend( [  b , c], [  d , e], [ b, c, d, e ] ), true ).
ex( aappend( [ f ], [ g , h ], [f ,g, h ] ), true ).

/*
aappend([a,b],[c,d],[a,c,d]) assumed to be false.

Found predicate after searching 2 clauses (Total = 2) :

    aappend([X|Y],Z,[X|U]):-aappend(Y,Z,U).
    aappend([X],Y,[X|Y]):-true.

under assumption that 

    aappend([a,b],[c,d],[a,c,d]) = false

*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% List Processing: List concatenation !!! using gp/gn/strategy

%!!! no no no nonon NNNOOO


pred_def( aapp/3, [ +xl, +xl, -xl ], [ aapp/3 ], [] ).

ex( aapp([],[],[]), true).
ex( aapp([],[1],[1]), true).
ex( aapp([],[],[1]),false). % as a 1st relevant negative(gn used)
ex( aapp([1],[2],[1,2]), true).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% List Processing: Reverse list

pred_def( rreverse/2, [ +xl, -xl ], [ cconc/3, rreverse/2 ], [] ).
%pred_def( append/3, [ +xl, +xl, -xl ], [ append/3 ], [] ).
 
pred_def( cconc/3, [ +xl, +x, -xl ], [ cconc/3 ], [] ).
 
    cconc([],X,[X]):-true.
    cconc([X|Y],Z,[X|U]):-cconc(Y,Z,U).


sys_set( rreverse/2, clause_promising, exact_with_theory ).
/*
rreverse( [], [] ).
rreverse( [ X|L1 ], L2 ) :-
  rreverse( L1, L3 ),
  cconc( L3, X, L2 ).
*/
%ex( rreverse( [], [] ), true ).	%orriginaly was

%ex( rreverse( [ b, a ], [ b, a ] ), false ).	%orriginaly was

%ex( rreverse( [ a ], [] ), false ). %orriginaly was

ex( rreverse( [ a, b, c ], [ c, b, a ] ), true ).
ex( rreverse( [ d, e], [e, d]), true).

%ex( rreverse( [ a,  c ], [ c, b, a ] ), false).	%orriginaly was

/*
ex( rreverse( [], [] ), true ).
ex( rreverse( [ a, b, c ], [ c, b, a ] ), true ).

Found predicate after searching 2 clauses (Total = 2) :
    rreverse([X|Y],Z):-rreverse(Y,U),cconc(U,X,Z).
    rreverse(X,[]):-true.
with no need of assumption.
*/

/*
Found predicate after searching 2 clauses:
    rreverse([X|Y],Z):-rreverse(Y,U),cconc(U,X,Z).
    rreverse([],[]):-true.

sett:

        System settings
Refinement operator: MIS General
Max. free variables: 1
Max. goals: 2
Max. goals added in one step: 2
Max. head argument depth: 1
Max. clause length: 999
Search ahead depth: 2
Assesing clause to be promising: Exact, using learned theory
Max. recursion depth: 6
Checking: On
Report level: Full
Output file: markus.out
*/


% SKIL - List Processing: Reverse list

pred_def( rv/2, [ +xl, -xl ], [ ssingleton/2, append/3, rv/2  ], [] ).
pred_def( append/3, [ +xl, +xl, -xl ], [ append/3], [] ).

pred_def( ssingleton/2, [+x, -xl],[],[]).
	ssingleton(X,[X]).

ex( rv([1,3,4],[4,3,1]), true ).
ex( rv([2,0],[0,2]),true ).
%ex( rv([7],[7]), true ).
ex( rv( [], []), true).

%ex( rv([2,0],[2,0]), false ).
%ex( rv([2],[1,2]), false ).
%ex( rv([1], [] ), false).

/*
ex( rv([1,3,4],[4,3,1]), true ).
ex( rv([2,0],[0,2]),true ).

with the settings

Max. free variables: 3
Max. goals: 3
Max. goals added in one step: 3
Max. head argument depth: 1
Max. clause length: 999
Search ahead depth: 3

Found predicate after searching 2 clauses:
    rv([X|Y],Z):-ssingleton(X,U),rv(Y,V),append(V,U,Z).
    rv([X|Y],Z):-ssingleton(X,U),append(Y,U,Z).

if ex( rv( [], []), true). added, then the nonrecursive clause replaced by

    rv(X,[]):-true.

*/

/*

Found predicate after searching 4 clauses:
    rv([X|Y],Z):-mmakeList(X,U),rv(Y,V),append(V,U,Z).
    rv([],[]):-true.

*/

/*
huhla(L) :- rv(L, K), write(L), tab(3), write(K), nl, fail.

 %  rv([],[]).
   rv([X|Y],Z):-rv(Y,U),cconc(U,X,Z).
   rv([X|Y],Z):-cconc(Y,X,Z).

*/

/*
pred_def( rv1/3, [ +xl, +x , -xl ], [ append/3, rv1/3 ], [] ).

ex( rv1([1,3,4], [1], [4,3,1]), true ).
ex( rv1([2,0], [2], [0,2]),true ).
ex( rv1([7], [7], [7]), true ).

ex( rv1([2,0], [2], [2,0]), false ).
ex( rv1([2], [2], [1,2]), false ).
 
just a heap of shit
*/

%%%

% List Processing: Last element

pred_def( llast/2, [-x, +xl], [llast/2], []).

/* mplus

ex(llast(a,[a]), true).
ex(llast(b,[c,b]), true).
ex(llast(c,[c,b]), false).

Found predicate after searching 2 clauses:
    llast(X,[Y|Z]):-llast(X,Z).
    llast(X,[X]):-true.
under assumption that 

    llast(c,[c,b]) = false

O.K. ? (y/n) y.   !! and no other solution found !!
*/

/* mplus

Found predicate after searching 2 clauses:
    llast(X,[Y|Z]):-llast(X,Z).
    llast(X,[X|Y]):-true.
under assumption that 

    llast(a,[]) = false

!! == member/2 !!            !! and no other solution found !!


ex(llast(a,[a]), true).
ex(llast(a,[]), false).
ex(llast(b,[c,b]), true).
*/

/* mplus

Found predicate after searching 2 clauses:
    llast(X,[Y,Z|U]):-llast(X,U).
    llast(X,[X]):-true.
under assumption that 

    llast(b,[c,b,a]) = false

ex(llast(a,[a]), true).
ex(llast(a,[c,b,a]), true).
ex(llast(b,[c,b,a]), false).
ex(llast(c,[c,b,a]), false).
*/

/* mplus - no solution

ex(llast(a,[c,b,a]), true).
ex(llast(b,[c,b,a]), false).
ex(llast(c,[c,b,a]), false).
*/


/* mplus - no solution

ex(llast(a,[b,a]), true).
ex(llast(b,[b,a]), false).
*/

/* Stan matwin's == stan.yap

ex(llast(a,[c,a]), true).
ex(llast(b,[x,y,b]), true).
%ex(llast([x,y],[x]), false).

ex( llast( a, [ c ] ), false).

Found predicate after searching 2 clauses:
    llast(X,[Y|Z]):-llast(X,Z).
    llast(X,[Y,X|Z]):-true.
*/

% List Processing: Add at the begining of list

pred_def( aaddbeg/3, [+x, +xl,-xl], [], []).

%ex( aaddbeg(1,[],[1]), true).
%ex( aaddbeg(2,[3],[2,3]), true).
ex( aaddbeg(4,[5,6],[4,5,6]), true).

/* for any of the above examples Markus succeeds

Found predicate after searching 1 clauses:
    aaddbeg(X,Y,[X|Y]):-true.

*/

%%%%
%  compress/2 by Pierre Flener

pred_def( ccompress/2, [+xl, -xl], [ ccompress/2], []).

%pred_def( ccompress/2, [+xl, -xl], [ hhead/2,  cconcInt/3, 
%ssucc/2, 	nnotEqual/2], []).

% ccompress/2, ssingleton/2,

% BK predicate definitions

pred_def( hhead/2, [+xl, -x], [], []).
hhead([X|Y], X).

pred_def( cconcInt/3, [+xl, +x, -xl], [], []).
cconcInt([],X,[X]) :- integer(X).
cconcInt([X|Y],Z,[X|V]) :- integer(Z), cconcInt(Y,Z,V).

pred_def(is / 2,[+ x,+ x],[],[]).
pred_def(integer/1 ,[+ x],[],[]).
pred_def('\='/ 2,[+ x,+ x],[],[]).

pred_def( ssucc/2, [+x,-x], [integer/1, is/2], []).
ssucc(X,Y) :- integer(X), Y is X+1.

pred_def( nnotEqual/2, [+x, -x], ['\='/2], []).
nnotEqual(X,Y) :- X\=Y.

% examples
/* but shit
ex( ccompress([],[]), true).
ex( ccompress( [a],	[a,1] ), true).
ex( ccompress( [z],	[z,1] ), true).
ex( ccompress( [b,b],	[b,2] ), true).
ex( ccompress( [c,d],	[c,1, d,1]), true).

ex( ccompress( [a],	[a,2] ), false).
ex( ccompress( [b,b],	[b,1] ), false).
*/

ex( ccompress([],[]), true).
ex( ccompress( [a],	[a] ), true).
ex( ccompress( [z],	[z] ), true).
ex( ccompress( [b,b],	[b] ), true).
ex( ccompress( [c,d],	[c, d]), true).
ex( ccompress( [f,f,g],	[f,g]), true).
ex( ccompress( [h,i,i], [h,i]), true).
ex( ccompress( [j,k,l],	[j,k,l]), true).

ex( ccompress([a],[]), false).
ex( ccompress( [c,d],	[c]), false).
ex( ccompress( [c,d],	[d]), false).
ex( ccompress( [c,d,e],	[c,d]), false).
ex( ccompress( [c,c,d,d],	[c,d,d]), false).
ex( ccompress( [c,c,d],	[c]), false).




end.