/*
Prolog inleveropdracht
Niels Out	0435899		nout@science.uva.nl

in samenwerking met Aksel en Andreas

logica & symbolische Robotica



Wij denken dat bij het kijken of model legaal is, de lijst afgaan lineair is.
het checken of de modelwaarden al in de lijst voorkomen, wordt met een dynamische aanroep van value(A,B)
gedaan, wat op zich lineair is.. maar intern in prolog waarschijnlijk kwadratisch wordt.

Vervolgens geld voor de consistency: perfect, de controles zijn "exhaustive"/


*/



%equivalentie
:- op(900,xfx,<->).

%implicatie
:- op(800,xfx,->).


%disjunctie	
:- op(700,xfy,v).

%conjunctie
:- op(600,xfy,^).

%negatie
:- op(500,fy,~).
%conjunctie
:- op(600,xfy,^).

%negatie
:- op(500,fy,~).

:- dynamic(value/2).

pl-true(S,M) :-
	retractall(value(_,_)),
	addvalues(M),
	check(S,X),
	write('the sentence is with this model: '),!,writeln(X),
	((X == 0,!,fail);
	true).


addvalue(T/V) :-
	value(T,X),
	X \= V,
	write(X),write(' is not the same as '),writeln(V),
	write(' twice '),write(T),writeln(' with other values wrong model!! BREAK'),!,fail.
	
addvalue(T/V) :-
	retractall(value(T,_)),
	assert(value(T,V)).

addvalues([H|T]) :-	%add the model to the database
	addvalue(H),
	addvalues(T).

addvalues([]) :-
	writeln('the model is allowed!').


check(P,V) :-
	value(P,V),!.	%if the value from a sentence is known, give that value

check(L <-> R,1) :-
	!,
	check(L,X),
	check(R,X).
check(_ <-> _,0) :- !.
	
check(A -> B,1) :-
	!,
	check(A,0);
	check(B,1).

check(_ -> _,0) :- !.

check(A v B,1) :-
	!,
	check(A,1);
	check(B,1).

check(_ v _,0) :- !.


check(A ^ B,1) :-
	!,
	check(A,1),
	check(B,1).

check(_ ^ _,0) :- !.

check(~A,X) :-
	!,
	check(A,V),
	turn(V,X).

check(A,0) :-	%if something is unknown, then it's false on default
	write(A),writeln(' isnt known in the system.. sorry!'),!.
	

turn(1,0).
turn(0,1).

	
print_list([]).
print_list([H|T]) :-		
	tab(2),writeln(H),
	print_list(T).