% ----------------------------------------------------------------------
% -- the compilation predicates for smodels

lp2sm(Name) :-
        lp2pl(Name),
        pl2sm(Name).
vlp2sm(Name) :-
        vlp2pl(Name),
        pl2sm(Name).

pl2sm(Name) :-
        concatenate(Name,'.pl',FilePL),
        concatenate(Name,'.sm',FileSmodels),
        read_clauses(FilePL,Clauses),
%                     get_flag(variable_names, Mode),
%                     set_flag(variable_names, on),
	domain_atoms(Clauses,DomAtoms),
        apply_to_conjuncts(Clauses,add_domains,Clauses1),
	conjoin(DomAtoms,Clauses1,Clauses2),
        apply_to_conjuncts(Clauses2,replace_variables,PrettyClauses),
        conjoin( (:- false) ,PrettyClauses,ClausesSM),
                     write_program('Smodels Program',ClausesSM),
        write_clauses(FileSmodels,ClausesSM).
%                     set_flag(variable_names, Mode).
%        open(FileSmodels,append,Stream),
%        write(Stream,'compute all {not false}'),
%        close(Stream).

% ----------------------------------------------------------------------
% -- calling smodels from within prolog

sm(Name) :- smodels(Name).
sm(Name,Opts) :- smodels(Name,Opts).

smodels(Name) :-
        smodels(Name,' 0 ').
smodels(Name,nice) :-
	concatenate('/home/torsten/Programming/Prolog/Preferences/Examples/smodels.hiders ',Name,HideFile),
        smodels(HideFile,' 0 ').

smodels(Name,Options) :-
        concatenate(Name,'.sm',FileSM),

%	concatenate('parse ',FileSM,ParseCmd),
	concatenate('lparse ',FileSM,ParseCmd),

	concatenate(' | smodels',Options,SmodelsCmd),

	concatenate(ParseCmd,SmodelsCmd,CMD),
	write('Calling ':CMD),nl,write('--'),
	system(CMD).

% ----------------------------------------------------------------------
% -- caring about hiding internal predicates

:- op(900,fy,hide).

hiders( Hiders ) :-
	Hiders = ( (hide  name(X)   ),

		   (hide      prec(X,Y) ),
		   (hide  neg_prec(X,Y) ),

	           (hide    ok(X)   ),
	           (hide   oko(X,Y) ),
	           (hide    ap(X)   ),
	           (hide    bl(X)   ),

	           (hide sname(X)   ),   % for sets
		   (hide    in(X,Y) ),
	           (hide    ko(X)   ),
	           (hide   apo(X,Y) ),
	           (hide   nap(X)   ),
	           (hide  napo(X,Y) ),
	           (hide nhead(X)   )
	       ).

% ----------------------------------------------------------------------
% -- caring about domain atoms to make 'lparse' happy

domain_atoms( Wff, DomAtoms ) :-
	constants(Wff,Constants),
	names(Wff,Names),
	mysubtract(Constants,Names,Constants1),
	domain_atoms1(Constants1,DomAtoms).

domain_atoms1( [], true ).
domain_atoms1( [N|Ns], NLs ) :-
        domain_atoms1(Ns,NLs1),
        conjoin(NLs1,domain(N),NLs).

add_domains( Wff, Wff1 ) :-
       Wff = (_Head :- name(_),Body) ->
              Wff1=Wff;
       Wff = (false :- Body) ->
              variables(Body,Vars),
	      binding_atoms(Vars,DomAtoms),
	      conjoin(DomAtoms,Body,Body1),
	      flatten_conjunction(Body1,Body2),
	      Wff1 =(false :- Body2);
       % ->
	      Wff1=Wff.

names( Rules, Names ) :-
        Rules = ( Rules1, Rules2 ) ->
	    names(Rules1,Names1),
	    names(Rules2,Names2),
	    union(Names1,Names2,Names);
	Rules = name(N) ->
	    Names = [N];
	% true ->
	    Names=[].

binding_atoms([],true).
binding_atoms([V|Vars],DomAtoms) :-
	binding_atoms(Vars,DomAtoms1),
	conjoin(domain(V),DomAtoms1,DomAtoms).

% mysubtract(L1, L2, L3)
% L3 = L1 - L2

mysubtract([], _, []).
mysubtract([Head|L1tail], L2, L3) :-
	member(Head, L2),
	!,
	mysubtract(L1tail, L2, L3).
mysubtract([Head|L1tail], L2, [Head|L3tail]) :-
	mysubtract(L1tail, L2, L3tail).