/* A converter that converts DIMACS format into CLP(FD) 
   Neng-Fa Zhou, 2004

Input format:

The common data format for GRASP is conjunctive normal form (CNF). A CNF formula f on n binary variables x1,..., xn is the conjunction (AND) of m clauses w1,...,wm each of which is the disjunction (OR) of one or more literals, where a literal is the occurrence of a variable or its complement. A formula f denotes a unique n-variable Boolean function f(x1,...,xn) and each of its clauses corresponds to an implicate f. 
The GRASP engine reads input in DIMACS format. The following is an example of a data file in DIMACS format: 

   c Example SAT format file in DIMACS format
   c It contains a formula in cnf formulation.
   c
   c
   p cnf 4 3
   2 3 -4 0
   -4 0
   2 3 4 0

A line starting with 'c' indicates a comment. The line represented as 'p cnf #var #cl' indicates the number of variables and clauses in the CNF formula. A single number '0' at the end of the line identifies the end of the clause. 

Output format:

go:-
    [V1,V2,...,Vn] :: 0..1, % declaration of Boolean variables,

    a sequence of constraints in the format X1 #\/ X2 #\/ ... #\/ Xn #= 1
    where Xi is a literal (either a Boolean variable V or the complement 
    of a Boolean variable in the form #\ V),
    labeling([V1,V2,...,Vn]),
    write([V1,V2,...,Vn]),nl.
go:-
    write(unsatisfiable),nl.			   
*/
cnf2pl(File):-
     atom_codes(File,String),
     (append(MainString,".cnf",String)->
      InFile=File,
      append(MainString,".pl",OutString),
      atom_codes(OutFile,OutString);
      append(String,".cnf",InString),
      append(String,".pl",OutString),
      atom_codes(InFile,InString),
      atom_codes(OutFile,OutString)),
      cnf2pl(InFile,OutFile).

cnf2pl(File,OutFile):-
    format("cnf2pl(~q,~q)~n",[File,OutFile]),
    see(File),			   
    tell(OutFile),
    format("go:-top.~n",[]),
    format("top:-cputime(X),top(X).~n",[]),
    readUntilPLine(N), %N is the declared number of variables

    functor(VarVect,vars,N),
    fillVarNames(VarVect,1,N),
    format("top(Start):-~n",[]),
    VarVect=..[_|VarList],
    format("~t~w :: 0..1,~n",[VarList]),
    readTrimLine(ClauseLine),
    readWriteClauses(ClauseLine,VarVect),
    seen,
    format("~t~w,nl,~n",[labeling_ffc(VarList)]),
    format("~t~w,nl,~n",[write(VarList)]),
%    format("~tcputime(End),T is End-Start,write(T),write(milliseconds),nl,~n",[]),

    format("~tfail.~n",[]),
    format("top(Start):-~n",[]),
    format("~twrite(unsatisfiable),nl,~n",[]),
    format("~tcputime(End),T is End-Start,write(T),write(milliseconds),nl.~n",[]),
    told.

fillVarNames(VarVect,N0,N):-N0>N,!.
fillVarNames(VarVect,N0,N):-
    number_codes(N0,N0Codes),
    atom_codes(VarName,[0'V|N0Codes]),
    arg(N0,VarVect,VarName),
    N1 is N0+1,
    fillVarNames(VarVect,N1,N).
    			   
readUntilPLine(N):-
   readTrimLine(Line),
   (Line==[]->throw(mailformatedCNFFile);true),
   (Line=[0'p|_]->
       append("p cnf ",LineRest,Line),
       append(NCodes,[0' |_],LineRest),!,
       number_codes(N,NCodes);
       readUntilPLine(N)).

readTrimLine(Line):-
    readLine(Line1),
    trimSpaces(Line1,Line2),
    (Line2=[0'%|_]->readTrimLine(Line);

     Line2=[0'0|_]->readTrimLine(Line);
     Line=Line2).

trimSpaces([0' |Line],Line1):-!,
   trimSpaces(Line,Line1).
trimSpaces(Line,Line1):-Line1=Line.

readWriteClauses([],VarVect):-!. % end of file

readWriteClauses(Line,VarVect):-
   extractLiterals(Line,Signs,[],Literals,[],VarVect),
   length(Literals,Len),
/*
%   (Len=<15->

      append(Signs,Literals,Args),
      Propagator=..[$bc_clause|Args],
      format("~t~w,~n",[Propagator]);
      constructConstrExp(Signs,Literals,Exp),
      format("~t~w#=1,~n",[Exp])),
*/
   constructConstrExp(Signs,Literals,Exp),
   format("~t(~w)#=1,~n",[Exp]),
   readTrimLine(NextLine),
   readWriteClauses(NextLine,VarVect).
       
extractLiterals([],Signs,SignsR,Literals,LiteralsR,VarVect):-!,%no 0 in the previous line

    readTrimLine(Line),
    extractLiterals(Line,Signs,SignsR,Literals,LiteralsR,VarVect).
extractLiterals(Line,Signs,SignsR,Literals,LiteralsR,VarVect):-
   (append(VNCodes,[0' |LineRest],Line);
    VNCodes=Line,LineRest=[]),!,
   number_codes(Vn,VNCodes),
   (Vn==0->Literals=LiteralsR,Signs=SignsR;
    trimSpaces(LineRest,LineRest1),
    extractLiterals(LineRest1,Signs1,SignsR,Literals1,LiteralsR,VarVect),
    (Vn>0->arg(Vn,VarVect,V),Signs=[1|Signs1],Literals=[V|Literals1];
     Vm is -Vn, arg(Vm,VarVect,V),
     Signs=[0|Signs1],
     Literals=[V|Literals1])).

constructConstrExp([],[],0):-!.
constructConstrExp([Sign],[V],Exp):-(Sign==1->Exp=V;Exp=(#\ V)).
constructConstrExp([Sign|Signs],[V|Vs],Exp):-
     Exp=(L #\/ Exp1),
     (Sign==1->L=V;L=(#\ V)),
     constructConstrExp(Signs,Vs,Exp1).


labeling_c(VarList):-
     get_constraints_numbers(VarList,PairsList),
     sort(0,>=,PairsList,SortedList),
     labeling_c_extract_vars(SortedList,Vars),
     clpb_labeling(Vars).

get_constraints_numbers([],[]).
get_constraints_numbers([V|Vs],[(N,V)|PairsList]):-
     constraints_number(V,N),
     get_constraints_numbers(Vs,PairsList).

labeling_c_extract_vars([],[]).
labeling_c_extract_vars([(N,V)|Vs],[V|VarList]):-
     labeling_c_extract_vars(Vs,VarList).

clpb_labeling([]):-true : true.
clpb_labeling([Var|Vars]):-integer(Var) :
    clpb_labeling(Vars).
clpb_labeling([Var|Vars]):-true :
    (Var=1;Var=0),
    clpb_labeling(Vars).


/*
test([X,Y,Z]):-
    [X,Y,Z] :: 0..1,
    $bc_clause(0,1,1,X,Y,Z),
    labeling([X,Y,Z]).

%generate action rules for Boolean constraints
gen_bcp(N0,N):-N0>N,!.
gen_bcp(N0,N):-
    Arity is 2*N0,
    functor(Head,$bc_clause,Arity),
    number_vars(Head,0,_),
    format("~w,~n",[Head]),
    format("~t{",[]),
    I is N0+1,
    gen_bcp_events(I,Arity,Head),
    format("}~n",[]),
    format("~t=>'_$bcp'(~w).~n",[N0]),
    N1 is N0+1,
    gen_bcp(N1,N).
    
gen_bcp_events(I0,I,Head):-I0=:=I,!,
    arg(I0,Head,X),
    format("ins(~w)",X).
gen_bcp_events(I0,I,Head):-
    arg(I0,Head,X),
    format("ins(~w),",X),
    I1 is I0+1,
    gen_bcp_events(I1,I,Head).


$clpb_negation(X,Y),var(X),var(Y),{ins(X),ins(Y)}=>true.
$clpb_negation(X,Y),var(X)=>(Y==1->X=0;X=1).
$clpb_negation(X,Y)=>(X==1->Y=0;Y=1).
*/
main:-
    get_main_args(L),
    sat(L).

sat([File]):-!,
    write('=>sat'),nl,
    cnf2pl(File,'temp.pl'),
    compile(temp),
    load(temp),
    go.
sat(_):-format("Usage: sat cnf-file~n",[]).