% refinement operator 
%
%


aleph_get_lit(Lit,[H|Lits]):-
    determination(H,Lit),
    \+(aleph_member2(Lit,[H|Lits])).



auto_refine((H:-B),(H1:-B1)):-
        !,
        goals_to_list((H,B),LitList),
        setting(clauselength,L),
        length(LitList,ClauseLength),
        ClauseLength < L,
        aleph_get_lit(Lit,LitList),
        aleph_append([Lit],LitList,LitList1),
        list_to_goals(LitList1,(H1,B1)),
    \+(prune((H1:-B1))),
    \+(tautology((H1:-B1))).
    
/*    ,
    (setting(language,Lang) ->
        lang_ok(Lang,H1,B1);
        true),
    (setting(newvars,NewVars) ->
        newvars_ok(NewVars,H1,B1);
        true).*/
auto_refine(Head,Clause):-
        auto_refine((Head:-true),Clause).


tautology((false:-Body)):-
    !,
    in(Body,L1,Rest),
    in(Rest,not(L2)),
    L1 == L2.
tautology((Head:-Body)):-
    in(Body,Lit),
    Head == Lit, !.
%----------------

aleph_abolish(Name/Arity):-
    functor(Pred,Name,Arity),
    (predicate_property(Pred,dynamic) ->
        retractall(Pred);
        abolish(Name/Arity)).

%-----------------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%----------------
aleph_append(A,[],A).
aleph_append(A,[H|T],[H|T1]):-
    aleph_append(A,T,T1).


%-----------------
set(Variable,Value):-
    check_setting(Variable,Value),
    (Value = inf -> V is inf;
        (Value = +inf -> V is inf;
            (Value = -inf -> V is -inf; V = Value)
        )
    ),
    retractall('$aleph_global'(Variable,set(Variable,_))),
    assertz('$aleph_global'(Variable,set(Variable,V))).
%    broadcast(set(Variable,V)),
%    special_consideration(Variable,Value).

setting(Variable,Value):-
        nonvar(Variable),
        '$aleph_global'(Variable,set(Variable,Value1)), !,
        Value=Value1.

setting(Variable,Value):-
    default_setting(Variable,Value).


noset(Variable):-
    nonvar(Variable),
        retract('$aleph_global'(Variable,set(Variable,_Value))), !,
    set_default(Variable).
noset(_).

%---------------

set_default(A):-
    default_setting(A,B),
    set(A,B),
    fail.
set_default(_).

default_setting(A,B):-
    set_def(A,_,_,_,B,_),
    B \= ''.




% set_def(Parameter,Class,TextDescr,Type,Default,Flag)
set_def(best, search-search_space,
    'Label to beat',
    prolog_term,'',
    show).
set_def(clauselength, search-search_space,
    'Maximum Clause Length',
    int(1)-int(+inf), 4,
    show).
set_def(i, saturation,
    'bound layers of new variables',
    int(1)-int(+inf), 2,
    show).
set_def(language, search-search_space,
    'Maximum occurrence of any predicate symbol in a clause',
    int(1)-int(+inf), +20,
    show).
set_def(newvars, search-search_space,
    'Existential variables in a clause',
    int(0)-int(+inf), +20,
    show).
set_def(nodes, search-search_space,
    'Nodes to be explored in the search',
    int(1)-int(+inf), 5000,
    show).
set_def(d, search-search_space,
    'Dimension of the beam',
    int(1)-int(+inf), 10,
    show).
    
check_setting(A,B):-
    set_def(A,_,_,Dom,_,_), !,
    (check_legal(Dom,B) -> true;
        err_message(set(A,B))).
check_setting(_,_).

check_legal(int(L)-int(U),X):-
    !,
    number(L,IL),
    number(U,IU),
    number(X,IX),
    IX >= IL,
    IX =< IU.
check_legal(float(L)-float(U),X):-
    !,
    number(L,FL),
    number(U,FU),
    number(X,FX),
    FX >= FL,
    FX =< FU.
check_legal([H|T],X):-
    !,
    aleph_member1(X,[H|T]).
check_legal(read(filename),X):-
    X \= '?',
    !,
    exists(X).
check_legal(_,_).

number(+inf,Inf):-
    Inf is inf, !.
number(-inf,MInf):-
    MInf is -inf, !.
number(X,Y):-
    Y is X, !.



%--------------
aleph_member1(H,[H|_]):- !.
aleph_member1(H,[_|T]):-
    aleph_member1(H,T).

aleph_member2(X,[Y|_]):- X == Y, !.
aleph_member2(X,[_|T]):-
    aleph_member2(X,T).

aleph_member3(A,A-B):- A =< B.
aleph_member3(X,A-B):-
    A < B,
    A1 is A + 1,
    aleph_member3(X,A1-B).

aleph_member(X,[X|_]).
aleph_member(X,[_|T]):-
    aleph_member(X,T).

%----------------
goals_to_list((true,Goals),T):-
    !,
    goals_to_list(Goals,T).
goals_to_list((Goal,Goals),[Goal|T]):-
    !,
    goals_to_list(Goals,T).
goals_to_list(true,[]):- !.
goals_to_list(Goal,[Goal]).

list_to_goals([Goal],Goal):- !.
list_to_goals([Goal|Goals],(Goal,Goals1)):-
    list_to_goals(Goals,Goals1).


prune(_):-fail.

in((Head:-true),Head):- !.
in((Head:-Body),L):-
    !,
    in((Head,Body),L).
in((L1,_),L1).
in((_,R),L):-
    !,
    in(R,L).
in(L,L).

in((L1,L),L1,L).
in((L1,L),L2,(L1,Rest)):-
    !,
    in(L,L2,Rest).
in(L,L,true).


% refinement operator for heads
refine_head((Head,[HLit|RestHeadList]),(NewHead,RestHeadList)):-
    delete(Head,HLit,NewHead).

refine_head((Head,[_HLit|RestHeadList]),(NewHead,NewHeadList)):-
    refine_head((Head,RestHeadList),(NewHead,NewHeadList)).