:- use_module(library(clpfd)).
:- use_module(library(lists)).

%%%%%%%%%%%%%%%%
% some test cases
%%%%%%%%%%%%%%%%
test1 :- solve1([[a,not(b),c],[b,not(c)]]).
test2 :- solve2([[a,not(b),c],[b,not(c)]]).
test3 :- solve1([[a,not(b),c],[b,not(c)],[a,d,e],[not(a),g,e],[not(g),f,not(e)],[not(b),not(c),not(d)],[not(c),g,not(d)],[not(f),not(g)],[a,b],[not(a),not(b)]]).
test4 :- solve2([[a,not(b),c],[b,not(c)],[a,d,e],[not(a),g,e],[not(g),f,not(e)],[not(b),not(c),not(d)],[not(c),g,not(d)],[not(f),not(g)],[a,b],[not(a),not(b)]]).
test5 :- solve1([[a,not(b),c],[not(a),b,not(c)],[a]]).
test6 :- solve2([[a,not(b),c],[not(a),b,not(c)],[a]]).
test7 :- solve1([[d],[f,g,not(e),not(b),a],[c,not(d)],[not(a),c],[a,not(b),c],[b,not(c)],[a,d,e],[not(a),g,e],[not(g),f,not(e)],[not(b),not(c),not(d)],[not(c),g,not(d)],[not(f),not(g)],[a,b],[not(a),not(b)]]).
test8 :- solve2([[d],[f,g,not(e),not(b),a],[c,not(d)],[not(a),c],[a,not(b),c],[b,not(c)],[a,d,e],[not(a),g,e],[not(g),f,not(e)],[not(b),not(c),not(d)],[not(c),g,not(d)],[not(f),not(g)],[a,b],[not(a),not(b)]]).



%%%%%%%%%%%%%%%%
% solveN(+Expr)
%
% finds a set of truth assignments that satisfy the input expression +Expr
% prints it and then backtracks to find more. solve1 uses constraint
% logic and solve2 uses exhaustive generation of all possible values
%%%%%%%%%%%%%%%%
solve1(Expr) :- ((findtruth1(Expr,PropBind),print(PropBind),nl,fail);true).
solve2(Expr) :- ((findtruth2(Expr,PropBind),print(PropBind),nl,fail);true).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% findvars(+Expr,-PropNames)
%
% unpacks the expression Expr to return the elementary proposition names
% uniquely in list PropNames
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
findvars(Expr,PropNames) :- myfindvars(Expr,[],PropNames).

%%%%%%%%%%%%%%%%
% myfindvars(+Expr,+NamesSoFar,-NamesToReturn)
%
% adds any remaining elementary proposition names in Expr to those
% in NamesSoFar, returning result in NamesToReturn
%%%%%%%%%%%%%%%%
myfindvars([],PropNames,PropNames).
myfindvars([Disj|Rest],InPropNames,PropNames) :-
  disjnames(Disj,InPropNames,DisjPropNames), % unpack the first disjunction
  myfindvars(Rest,DisjPropNames,PropNames). % recurse on rest

%%%%%%%%%%%%%%%%
% disjnames(+Expr,+NamesSoFar,-NamesToReturn)
%
% adds any remaining elementary proposition names in the disjunction Expr
% to those in NamesSoFar, returning result in NamesToReturn
%%%%%%%%%%%%%%%%
disjnames([],PropNames,PropNames).
disjnames([X|Rest],SoFar,PropNames) :-
  atom(X),                              % use if an atom
  \+member(X,SoFar),!,                  % and not used so far
  disjnames(Rest,[X|SoFar],PropNames).  
disjnames([not(X)|Rest],SoFar,PropNames) :-
  \+member(X,SoFar),!,                  % use if atom not used so far
  disjnames(Rest,[X|SoFar],PropNames).
disjnames([_|Rest],SoFar,PropNames) :-  % otherwise just skip
  disjnames(Rest,SoFar,PropNames).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% findtruth1(+Expr,-PropBind)
%
% solution with CLPFD. Finds a set of proposition value bindings 
% PropBind that make expression Expr true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
findtruth1(Expr,PropBind) :- 
 findvars(Expr,PropNames),             % get prop names
 makeconstraints1(PropNames,PropBind,Vars),  % construct CL constraints
 evalexpr1(Expr,PropBind,Result),               % evaluate expression
 Result,
 labeling([],Vars).                     % search for remaining
%%%%%%%%%%%%%%%%
% makeconstraints1(+Names,-Bindings,-Variables)
%
% turns a list of names Names=[n1, n2, ... nx] into a list Bindings of pairings
% between the names and the unbound truth values
% [[n1,V1], [n2,V2], ... [nx, Vx]] and a list Variables of the 
% variables [V1, V2, ... Vx]
%%%%%%%%%%%%%%%%
makeconstraints1([],[],[]).
makeconstraints1([Name|RestNames],[[Name,Var]|RestBind],[Var|RestVars]) :-
  Var in 0..1,
  makeconstraints1(RestNames,RestBind,RestVars).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% evalexpr1(+Expr,+Bindings,-Formula)
%
% Constructs conjunction of logical formulas with the variables in
% the same structure as Expr, using the given atom->Variable pairs
% as in Bindings.
% It assumes that Expr is a conjunction of disjunctions.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
evalexpr1([],_,1) :- !.
evalexpr1([Conj|Rest],PropBind,ConjResult #/\SubResult) :-
  evaldisj1(Conj,PropBind,ConjResult),  % construct the 1st conjunction
  evalexpr1(Rest,PropBind,SubResult).   % construct rest

%%%%%%%%%%%%%%%%
% evaldisj1(+Expr,+Bindings,-Formula)
%
% succeeds if expression Expr is true with the bindings given in Bindings
% It assumes that Expr is a disjunction of either elementary proposition 
% names or their negations, so is true if any of term is true.
%%%%%%%%%%%%%%%%
evaldisj1([not(X)],PropBind,(#\ Val)) :- % base case is a not
    member([X,Val],PropBind).            % extract var
evaldisj1([X],PropBind,Val) :-           % base case is atom
    atom(X),
    member([X,Val],PropBind).            % extract var
evaldisj1([not(X)|Rest],PropBind,(#\ Val) #\/ SubResult) :- % neg head term
    member([X,Val],PropBind),            % extract var
    evaldisj1(Rest,PropBind,SubResult).  % get expression for rest
evaldisj1([X|Rest],PropBind,Val #\/ SubResult) :- 
    atom(X),
    member([X,Val],PropBind),            % extract var
    evaldisj1(Rest,PropBind,SubResult).  % get expression for rest

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% findtruth2(+Expr,-PropBind)
%
% solution with exhaustive value generation. Finds a set of proposition 
% value bindings PropBind that make expression Expr true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% solution with exhaustive search
findtruth2(Expr,PropBind) :- 
  findvars(Expr,PropNames),            % get prop names
  makeconstraints2(PropNames,PropBind), % construct bindings
  evalexpr2(Expr,PropBind).              % evaluate expression
%%%%%%%%%%%%%%%%
% makeconstraints2(+Names,-Bindings)
%
% turns a list of names [n1, n2, ... nx] into a list Bindings of pairings
% between the names and truth values [[n1,T1], [n2,T2], ... [nx, Tx]] 
%%%%%%%%%%%%%%%%
makeconstraints2([],[]) :-!.
makeconstraints2([Name|RestNames],[[Name,1]|RestBind]) :-  % treat as true
  makeconstraints2(RestNames,RestBind).
makeconstraints2([Name|RestNames],[[Name,0]|RestBind]) :-  % treat as false
  makeconstraints2(RestNames,RestBind).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% evalexpr2(+Expr,+Bindings)
%
% succeeds if expression Expr is true with the bindings given in Bindings
% It assumes that Expr is a conjunction of disjunctions.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% evaluate conjunctions
evalexpr2([],_) :- !.
evalexpr2([Conj|Rest],PropBind) :-
  evaldisj2(Conj,PropBind),  % can be true only if each disjunction is true
  evalexpr2(Rest,PropBind).
%%%%%%%%%%%%%%%%
% evaldisj2(+Expr,+Bindings)
%
% succeeds if expression Expr is true with the bindings given in Bindings
% It assumes that Expr is a disjunction of either elementary proposition 
% names or their negations, so is true if any of term is true.
%%%%%%%%%%%%%%%%
evaldisj2([X|_],PropBind) :- 
    atom(X),
    member([X,1],PropBind).        % true if prop is assigned true->success
evaldisj2([X|Rest],PropBind) :- 
    atom(X),
    member([X,0],PropBind),        % false if prop is assigned false
    evaldisj2(Rest,PropBind).       % so check rest of terms
evaldisj2([not(X)|_],PropBind) :-   % negation case
    member([X,0],PropBind).        % true if prop is assigned false->success
evaldisj2([not(X)|Rest],PropBind) :- % negation case
    member([X,1],PropBind),        % false if prop is assigned true
    evaldisj2(Rest,PropBind).       % so check rest of terms
