/*************************************************************************

         name: modelCheckerDRT1.pl (Volume 2, Chapter 1)
      version: July 10, 2001
  description: The basic model checker for DRT
      authors: Patrick Blackburn & Johan Bos
 
*************************************************************************/

:- module(modelCheckerDRT1,[evaluate/0,
			    evaluate/2,
			    evaluate/3,
			    satisfyDrs/4]).

:- ensure_loaded(comsemOperators).

:- use_module(comsemPredicates,[memberList/2,
                                compose/3,
                                printRepresentations/1]).

:- use_module(exampleModels,[example/2]).

:- use_module(modelCheckerTestSuiteDRT,[test/4]).


/*========================================================================
   Evaluate a DRS in an example model
========================================================================*/

evaluate(DRS,Example):-
   evaluate(DRS,Example,[]-_).


/*========================================================================
   Evaluate a DRS in an example model wrt to assignments
========================================================================*/

evaluate(DRS,Example,AssignmentIn-AssignmentOut):-
   example(Example,Model),
   (	
       satisfyDrs(DRS,Model,AssignmentIn-AssignmentOut,pos), !,
       printStatus(pos)
   ;
       printStatus(neg)
   ).
   

/*========================================================================
   Testsuite
========================================================================*/

evaluate:-
   format('~n>>>>> DRT MODEL CHECKER 1 ON TESTSUITE <<<<<~n',[]),
   test(DRS,Example,Assignment,Status),
   format('~n~nInput DRS:',[]),
   printRepresentations([DRS]),
   format('Example Model: ~p~nStatus: ',[Example]),
   printStatus(Status),
   format('~nModel Checker says: ',[]),
   evaluate(DRS,Example,Assignment-_),
   fail.

evaluate.


/*========================================================================
   Print status of a testsuite example
========================================================================*/

printStatus(pos):- write('Satisfied in model. ').
printStatus(neg):- write('Not satisfied in model. ').
printStatus(undef):- write('Cannot be evaluated. ').


/*========================================================================
  Discourse Representation Structures
========================================================================*/

satisfyDrs(drs([],Conds),Model,G-G,Pol):-
   satisfyConditions(Conds,Model,G,Pol).

satisfyDrs(drs([X|L],Conds),model(D,F),G-H,pos):-
   memberList(V,D),
   satisfyDrs(drs(L,Conds),model(D,F),[g(X,V)|G]-H,pos).

satisfyDrs(drs([X|L],Conds),model(D,F),G-G,neg):-
   setof(V,memberList(V,D),All),
   setof(V,(memberList(V,D),
            satisfyDrs(drs(L,Conds),model(D,F),[g(X,V)|G]-_,neg)),All).


/*========================================================================
   Merge
========================================================================*/

satisfyDrs(merge(Drs1,Drs2),Model,G-I,pos):-
   satisfyDrs(Drs1,Model,G-H,pos),
   satisfyDrs(Drs2,Model,H-I,pos).

satisfyDrs(merge(Drs,_),Model,G-G,neg):-
   satisfyDrs(Drs,Model,G-_,neg).

satisfyDrs(merge(Drs1,Drs2),Model,G-G,neg):-
   satisfyDrs(Drs1,Model,G-H,pos),
   satisfyDrs(Drs2,Model,H-_,neg).


/*========================================================================
   DRS Conditions
========================================================================*/

satisfyConditions([],_,_,_).
satisfyConditions([C|L],Model,G,Pol):-
   satisfyCondition(C,Model,G,Pol),
   satisfyConditions(L,Model,G,Pol).


/*========================================================================
   Disjunction
========================================================================*/

satisfyCondition(Drs1 v Drs2,Model,G,pos):-
   satisfyDrs(Drs1,Model,G-_,pos);
   satisfyDrs(Drs2,Model,G-_,pos).

satisfyCondition(Drs1 v Drs2,Model,G,neg):-
   satisfyDrs(Drs1,Model,G-_,neg),
   satisfyDrs(Drs2,Model,G-_,neg).


/*========================================================================
   Implication
========================================================================*/

satisfyCondition(Drs1 > Drs2,Model,G,pos):-
   satisfyDrs(Drs1,Model,G-H,pos),
   satisfyDrs(Drs2,Model,H-_,pos).

satisfyCondition(Drs > _,Model,G,pos):-
   satisfyDrs(Drs,Model,G-_,neg).

satisfyCondition(Drs1 > Drs2,Model,G,neg):-
   satisfyDrs(Drs1,Model,G-H,pos),
   satisfyDrs(Drs2,Model,H-_,neg).



/*========================================================================
   Negation
========================================================================*/

satisfyCondition(~ Drs,Model,G,pos):-
   satisfyDrs(Drs,Model,G-_,neg).

satisfyCondition(~ Drs,Model,G,neg):-
   satisfyDrs(Drs,Model,G-_,pos).


/*========================================================================
   Equality
========================================================================*/

satisfyCondition(equal(X,Y),Model,G,pos):-
   i(X,Model,G,Value1),
   i(Y,Model,G,Value2),
   Value1=Value2.

satisfyCondition(equal(X,Y),Model,G,neg):-
   i(X,Model,G,Value1),
   i(Y,Model,G,Value2),
   \+ Value1=Value2.


/*========================================================================
   One-place predicates
========================================================================*/

satisfyCondition(Cond,model(D,F),G,pos):-
   compose(Cond,Symbol,[Argument]),
   i(Argument,model(D,F),G,Value),
   memberList(f(1,Symbol,Values),F),
   memberList(Value,Values).

satisfyCondition(Cond,model(D,F),G,neg):-
   compose(Cond,Symbol,[Argument]),
   i(Argument,model(D,F),G,Value),
   memberList(f(1,Symbol,Values),F),
   \+ memberList(Value,Values).


/*========================================================================
   Two-place predicates
========================================================================*/

satisfyCondition(Cond,model(D,F),G,pos):-
   compose(Cond,Symbol,[Arg1,Arg2]),
   i(Arg1,model(D,F),G,Value1),
   i(Arg2,model(D,F),G,Value2),
   memberList(f(2,Symbol,Values),F),
   memberList((Value1,Value2),Values).

satisfyCondition(Cond,model(D,F),G,neg):-
   compose(Cond,Symbol,[Arg1,Arg2]),
   i(Arg1,model(D,F),G,Value1),
   i(Arg2,model(D,F),G,Value2),
   memberList(f(2,Symbol,Values),F),
   \+ memberList((Value1,Value2),Values).


/*========================================================================
   Interpretation of Constants and Variables
========================================================================*/

i(X,model(_,F),G,Value):-
   (
       var(X),
       memberList(g(Y,Value),G),
       Y==X, ! % IMPORTANT CUT!
   ;
       atom(X),
       memberList(f(0,X,Value),F)
   ).