%
% logic.pl -- the Knight/Knave identifier...
%
% Author:
%
% Comments:
%



% some "nice" prolog settings...  see assignment 8's
% description for the details on what these do
% -- but it's not crucial to know the details of these Prolog internals
:- set_prolog_flag( prompt_alternatives_on, groundness ).
:- set_prolog_flag(toplevel_print_options, [quoted(true),
     portray(true), attributes(portray), max_depth(999), priority(699)]).






%
% noVars( X ) is true if X is an expression that does not
%       contain any logical variables, that is, no
%       integers. (The expressions will not hold any
%       Prolog variables in any case... .)
%
noVars( t ).
noVars( f ).
noVars( [_, L, R] ) :- noVars( L ), noVars( R ).
noVars( [_, S] ) :- noVars( S ).


% The following tests can be run by typing:
% run_tests(noVars)
:- begin_tests(noVars).
test(noVarsT1, [nondet]) :- noVars( t ), !.
test(noVarsT2, [nondet]) :- noVars( f ), !.
test(noVarsT3, [nondet]) :- noVars( [ifthen,t,[ifthen,t,f]] ), !.
test(noVarsT4, [nondet]) :- \+noVars( [and,f,1] ), !.
test(noVarsT5, [nondet]) :- \+noVars( [not,2] ), !.
% no extra tests needed here...
% ... and be sure to actually test it!


:- end_tests(noVars).


%
% getVar( Expr, N ) is true if Expr is an expression with a
%       logical variable, that is, an integer
%       Then, N should be bound to one of those
%       available variables (again, an integer)
%
getVar( N, N ) :- number( N ).
getVar( [_, Sub], N ) :- getVar( Sub, N ).
getVar( [_, L, R], N ) :- getVar( L, N ); (noVars(L), getVar( R, N )).



% The following tests can be run by typing:
% run_tests(getVar)
:- begin_tests(getVar).
test(getVarT1, [nondet]) :- getVar( 1, 1 ), !.
test(getVarT2, [nondet]) :- getVar( [or,f,[not,2]], 2 ), !.
test(getVarT3, [nondet]) :- \+getVar( [ifthen,t,[ifthen,t,f]], _ ), !.
test(getVarT4, [nondet]) :- getVar( [and,1,2], 1 ), !.
test(getVarT5, [nondet]) :- getVar( [and,f,2], 2 ), !.
% no extra tests needed here...
:- end_tests(getVar).





%
% subst



  
  
% The following tests can be run by typing:
% run_tests(subst)
:- begin_tests(subst).
test(substT1, [nondet]) :- subst( 1, t, 1, t ), !.
test(substT2, [nondet]) :- subst( 1, t, 2, 2 ), !.
test(substT3, [nondet]) :- subst( 1, t, [ifthen,f,t], [ifthen,f,t] ), !.
test(substT4, [nondet]) :- subst( 2, t, [not,2], [not,t] ), !.
test(substT5, [nondet]) :- subst( 2, f, [or,[and,1,2],2], [or,[and,1,f],f] ), !.
% place at least one additional test here
% ... and be sure to test it!


:- end_tests(subst).  
  
  
  




%
% eval




% The following tests can be run by typing:
% run_tests(eval)
:- begin_tests(eval).
test(evalT1, [nondet]) :- eval( [ifthen, f, t], t ), !.
test(evalT2, [nondet]) :- eval( [and, f, t], f ), !.
test(evalT3, [nondet]) :- eval( [or, f, t], t ), !.
test(evalT4, [nondet]) :- eval( [not,[not,[not,f]]], t ), !.
test(evalT5, [nondet]) :- \+eval( [ifthen, f, f], f ), !.
% place at least one additional test here
% ... and be sure to test it!


:- end_tests(eval). 








%
% taut




% The following tests can be run by typing:
% run_tests(taut)
:- begin_tests(taut).
test(tautT1, [nondet]) :- taut( [ifthen, f, 1] ), !.
test(tautT2, [nondet]) :- taut( [iff, 2, 2] ), !.
test(tautT3, [nondet]) :- taut( [ifthen, 1, [ifthen, 2, 1]] ), !.
test(tautT4, [nondet]) :- \+taut( [not,1] ), !.
test(tautT5, [nondet]) :- taut( [iff, [ifthen, [and, 1, 2], 3], [ifthen, 1, [ifthen, 2, 3]]] ), !.
% place at least one additional test here
% ... and be sure to test it!


:- end_tests(taut). 







%
% unsat





% The following tests can be run by typing:
% run_tests(unsat)
:- begin_tests(unsat).
test(unsatT1, [nondet]) :- unsat( [not,[ifthen, f, 1]] ), !.
test(unsatT2, [nondet]) :- unsat( [not,[iff, 2, 2]] ), !.
test(unsatT3, [nondet]) :- unsat( [not,[ifthen, 1, [ifthen, 2, 1]]] ), !.
test(unsatT4, [nondet]) :- \+unsat( [not,1] ), !.
test(unsatT5, [nondet]) :- unsat( [not,[iff, [ifthen, [and, 1, 2], 3], [ifthen, 1, [ifthen, 2, 3]]]] ), !.
% place at least one additional test here
% ... and be sure to test it!


:- end_tests(unsat).  





%
% id





% The following tests can be run by typing:
% run_tests(id)
:- begin_tests(id).
test(idT1, [nondet]) :- id( [not,[ifthen, f, 1]], knave ), !.
test(idT2, [nondet]) :- id( [ifthen, f, 1], knight ), !.
test(idT3, [nondet]) :- id( [not,[ifthen, 1, [ifthen, 2, 1]]], knave ), !.
test(idT4, [nondet]) :- id( [not,1], human ), !.
test(idT5, [nondet]) :- \+id( [not,1], knight ), !.
test(idT6, [nondet]) :- \+id( [not,1], knave ), !.
% place at least one additional test here
% ... and be sure to test it!


:- end_tests(id).