probvm_optimize

addWeight([],[]) :- !.

addWeight([I|Irest],[O|Orest]) :- !,
    addWeight(I,O),
    addWeight(Irest,Orest).

addWeight(A = B,1-(A=B)) :- ground(A),!.

addWeight(A = B,1-(A=B)) :- ground(B),!.

addWeight(A = B,2-(A=B)) :- !.

addWeight(I,100-I).

check_unifyable(0,_Det,_ElemA,_ElemB) :- !.

check_unifyable(N,Det,ElemA,ElemB) :-
    arg(N,Det,D),arg(N,ElemA,A),arg(N,ElemB,B),
    check_unifyable2(D,A,B),
    N2 is N-1,
    check_unifyable(N2,Det,ElemA,ElemB).

check_unifyable2(ignore,_,_).

check_unifyable2(same,A,B) :- A==B.

check_unifyable2(unify,A,B) :- A=B.

is_det_statement(apply(same,same,unify)).

is_det_statement(first_of_sequence(same,unify)).

is_det_statement(tail_of_sequence(same,unify)).

is_det_statement(enumerate(same,ignore,same)).

optimize_instructions(In,Out) :-
    NonLocalVars = [],
    optimize_instructions(In,NonLocalVars,Out).

optimize_instructions(In,NonLocalVars,Out) :-
    ( optimize_instructions2(In,NonLocalVars,New), New \== In ->
    optimize_instructions(New,NonLocalVars,Out)
    ; otherwise ->
    In = Out).

optimize_instructions2(In,_NonLocalVars,Out) :-
    select(true,In,Out).

optimize_instructions2(In,_NonLocalVars,Out) :-
    remove_simple_equations(In,Out).

optimize_instructions2(In,NonLocalVars,Out) :-
    term_variables(In,AllVars),
    propagate_equals(In,NonLocalVars,AllVars,Out).

optimize_instructions2(In,_NonLocalVars,Out) :-
    sort_by_weight(In,Out).

optimize_instructions2(In,_NonLocalVars,Out) :-
    unify_duplicate_instructions(In,Out).

optimize_negate(A,B) :- A==pred_true,B=pred_false.

optimize_negate(A,B) :- A==pred_false,B=pred_true.

pick(Elem,[Elem|Rest],Rest) --> [Elem].

pick(Elem,[E|Rest],Tail) --> [E],pick(Elem,Rest,Tail).

propagate_equals([],_,_,[]) :- !.

propagate_equals([I|Irest],NonLocalVars,AllVars,[O|Orest]) :- !,
    propagate_equals(I,NonLocalVars,AllVars,O),
    propagate_equals(Irest,NonLocalVars,AllVars,Orest).

propagate_equals(A=B,NonLocalVars,_AllVars,true) :-
    propagate_equals2(A,B,NonLocalVars),!.

propagate_equals(A=B,NonLocalVars,_AllVars,true) :-
    propagate_equals2(B,A,NonLocalVars),!.

propagate_equals(check_equal(A,B,P),NonLocalVars,_AllVars,true) :-
    P == pred_true,
    propagate_equals2(A,B,NonLocalVars),!.

propagate_equals(check_equal(A,B,P),NonLocalVars,_AllVars,true) :-
    P == pred_true,
    propagate_equals2(B,A,NonLocalVars),!.

propagate_equals(I,_,_,I).

propagate_equals2(A,B,NonLocalVars) :- ground(A),var(B),!,
    \+ exact_member(B,NonLocalVars),
    A=B.

propagate_equals2(A,B,NonLocalVars) :- var(A),var(B),
    \+ exact_member(A,NonLocalVars),
    \+ exact_member(B,NonLocalVars),
    A=B.

removeWeight([],[]) :- !.

removeWeight([I|Irest],[O|Orest]) :- !,
    removeWeight(I,O),
    removeWeight(Irest,Orest).

removeWeight(_-I,I).

remove_simple_equations(In,Out) :-
    remove_simple_equations2(In,Out,[]).

remove_simple_equations2([]) --> [].

remove_simple_equations2([Elem|Rest]) -->
    ( simple_equation(Elem) -> []
    ; {otherwise} -> [Elem]),
    remove_simple_equations2(Rest).

simple_equation(ex) --> [a,b].

simple_equation(check_negate(A,B)) -->
    ( {optimize_negate(A,B)} -> []
    ; {optimize_negate(B,A)} -> []
    ; {nonvar(A),nonvar(B) } -> [fail]).

simple_equation(check_conjunct(A,B,C)) -->
    {C==pred_true,A=pred_true,B=pred_true}.

simple_equation(check_conjunct(A,B,C)) -->
    {nonvar(A),nonvar(B),
    ( A=pred_true,B=pred_true -> C=pred_true
    ; otherwise -> C=pred_false)}.

sort_by_weight(In,Out) :-
    addWeight(In,Weighted),
    keysort(Weighted,Sorted),
    removeWeight(Sorted,Out).

unify_duplicate_instructions(In,Out) :-
    pick(ElemA,In,Inter,Out,Rest),
    functor(ElemA,Name,Arity),
    functor(Det,Name,Arity),
    is_det_statement(Det),
    functor(ElemB,Name,Arity),
    select(ElemB,Inter,Rest),
    check_unifyable(Arity,Det,ElemA,ElemB).