1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%%                                                                           %%
    3%%      Version:  1.00   Date: 28/06/96   File: model.pl
    4%% Last Version:                          File:                              %%
    5%% Changes:                                                                  %%
    6%% 26/06/95 Created                                                          %%
    7%% 25/06/96 moved compatible from defaults.pl
    8%% 28/06/96 updated cnf,make_matrix, make_clause
    9%%                                                                           %%
   10%% Purpose:                                                                  %%
   11%%                                                                           %%
   12%% Author:  Torsten Schaub                                                   %%
   13%%                                                                           %%
   14%% Usage:   prolog model.pl                                                  %%
   15%%                                                                           %%
   16%%                                                                           %%
   17%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   18
   19:- ensure_loaded(base).   20
   21%%% ----------------------------------------------------------------------
   22%%% model_initialization/2
   23%%%     generates an initial model
   24
   25model_initialization(Matrix,cmm(Model,NewMatrix)) :-
   26	model_generation(matrix([],Matrix),NewMatrix,Model),
   27%	display_cmm('INITIALIZATION',cmm(Model,NewMatrix)),
   28	!.
   29
   30%%% Runtime predicate for consistency checking
   31%%%
   32
   33compatible(MatrixJ,cmm(Model,ModelMatrix),cmm(NewModel,NewModelMatrix)) :-
   34	satisfy_matrix(MatrixJ,Model,NewModel) ->
   35	        append_matrix(MatrixJ,ModelMatrix,NewModelMatrix),
   36%		display_cmm('CHECKING - satisfy':MatrixJ,cmm(NewModel,NewModelMatrix)),
   37		verbose('+ satisfiability check');
   38	adjoin_matrix(MatrixJ,ModelMatrix,ModelMatrix1) ->
   39%	        display_cmm('CHECKING - generation I':MatrixJ,cmm(Model,ModelMatrix)),
   40		model_generation(ModelMatrix1,NewModelMatrix,NewModel);
   41%		display_cmm('CHECKING - generation II':MatrixJ,cmm(NewModel,NewModelMatrix));
   42	%true ->
   43%		display_cmm('CHECKING - failure':MatrixJ,cmm(Model,ModelMatrix)),
   44		verbose('- compatible *failure*'),
   45		fail.
   46
   47%%% ----------------------------------------------------------------------
   48%%% satisfy_matrix/3
   49%%%     checks whether a given model, ModelI, satisfies
   50%%%     a formula in matrix form, Matrix, or whether the model
   51%%%     can be extended to a model, ModelO
   52%%%
   53
   54satisfy_matrix([],Model,Model).
   55satisfy_matrix([Clause],ModelI,ModelO) :-
   56	!,
   57	satisfy_clause(Clause,ModelI,ModelO).
   58satisfy_matrix([C1,C2],ModelI,ModelO) :-
   59	!,
   60	satisfy_clause(C1,ModelI,Model1),
   61	satisfy_clause(C2,Model1,ModelO).
   62satisfy_matrix([C1,C2,C3|M],ModelI,ModelO) :-
   63	satisfy_clause(C1,ModelI,Model1),
   64	satisfy_clause(C2,Model1,Model2),
   65	satisfy_clause(C3,Model2,Model3),
   66	satisfy_matrix(M,Model3,ModelO).
   67
   68satisfy_clause([],_,_) :- 
   69	!,
   70	fail.
   71satisfy_clause([L],ModelI,ModelO) :-
   72	!,
   73	satisfy_literal(L,ModelI,ModelO).
   74satisfy_clause([L1,L2],ModelI,ModelO) :-
   75	satisfy_literal(L1,ModelI,ModelO);
   76	satisfy_literal(L2,ModelI,ModelO).
   77satisfy_clause([L1,L2,L3|C],ModelI,ModelO) :-
   78	satisfy_literal(L1,ModelI,ModelO);
   79	satisfy_literal(L2,ModelI,ModelO);
   80	satisfy_literal(L3,ModelI,ModelO);
   81	satisfy_clause(C,ModelI,ModelO).
   82
   83satisfy_literal(L,ModelI,ModelO) :-
   84        identical_member(L,ModelI) ->
   85	       ModelO = ModelI;
   86	%true  ->
   87	       negated_literal(L,NegL),
   88	       \+ identical_member(NegL,ModelI),
   89	       ModelO = [L|ModelI].
   90
   91
   92%%% ----------------------------------------------------------------------
   93%%% model_generation/2
   94
   95model_generation(matrix(Units,Matrix),matrix(Units2,M1),Model) :-
   96	unit_extraction(Matrix,M1,Units1),
   97%	writeln(unit_extraction),display_matrix(Matrix),display_matrix(M1),display_units(Units1),
   98	dp(M1,Model1),
   99	append(Units,Units1,Units2),
  100/*	union(Units,Units1,Units2), append allows for multiple occurrences */
  101	append(Units2,Model1,Model),
  102	verbose('* model generation').
  103
  104dp([],[]) :- !.
  105dp(M,_) :-
  106	mymember([],M),
  107	!,
  108	fail.
  109dp(M,NewMod) :-
  110	M=[[L|_]|_],
  111	split(M,L,M1,M2),
  112	unit_extraction(M1,M3,U3),
  113	unit_extraction(M2,M4,U4),
  114	(dp(M3,Mod),
  115         KK = [L|U3];
  116	 dp(M4,Mod),
  117         negated_literal(L,K),
  118	 KK = [K|U4]),
  119        append(KK,Mod,NewMod).
  120
  121
  122split([],_,[],[]).
  123split([C|M],L,M3,M4) :-
  124	split(M,L,M1,M2),
  125	negated_literal(L,NegL),
  126	(myselect(L,C,RestC) ->
  127	      M3=M1,
  128	      M4=[RestC|M2];
  129	myselect(NegL,C,RestC) ->
  130	      M3=[RestC|M1],
  131	      M4=M2;
  132        %true ->
  133	      M3=[C|M1],
  134	      M4=[C|M2]).
  135
  136%%% ----------------------------------------------------------------------
  137%%% cnf/2
  138
  139cnf(NNF,CNF) :-
  140	NNF = (F1,F2) ->
  141	    cnf(F1,CNF1),
  142	    cnf(F2,CNF2),
  143	    conjoin(CNF1,CNF2,CNF);
  144        NNF = (F1;(F2,F3)) ->
  145	    cnf((F1;F2),CNF1),
  146	    cnf((F1;F3),CNF2),
  147	    conjoin(CNF1,CNF2,CNF);
  148        NNF = ((F1,F2);F3) ->
  149	    cnf((F1;F3),CNF1),
  150	    cnf((F2;F3),CNF2),
  151	    conjoin(CNF1,CNF2,CNF);
  152	NNF = (F1;F2) ->
  153	    cnf(F1,CNF1),
  154	    cnf(F2,CNF2),
  155            (cnf_p(CNF1,CNF2,F1,F2) ->
  156	           disjoin(CNF1,CNF2,CNF);
  157	    %true ->
  158		   disjoin(CNF1,CNF2,CNF12),
  159	           cnf(CNF12,CNF));
  160	%true ->
  161	    NNF=CNF.
  162
  163cnf_p(CNF1,CNF2,F1,F2) :-
  164	(F1=(_,_);F2=(_,_)) ->
  165	         fail;
  166		 F1=CNF1,F2=CNF2.
  167
  168make_matrix(Wff,Matrix) :-
  169	Wff = (A,B) ->
  170	      make_matrix(A,MA),
  171	      make_matrix(B,MB),
  172	      append(MA,MB,Matrix);
  173	Wff = true ->
  174	      Matrix = [];
  175	Wff = false ->
  176	      Matrix = [[]];
  177	%true ->
  178	      make_clause(Wff,Clause),
  179	      Matrix=[Clause].
  180
  181make_clause(Wff,Clause) :-
  182	Wff = (A;B) ->
  183	      make_clause(A,CA),
  184	      make_clause(B,CB),
  185	      append(CA,CB,Clause);
  186	%true ->
  187	      Clause=[Wff].
  188
  189%%% ----------------------------------------------------------------------
  190%%% combine_clauses\3
  191%%%       merges two CNFs into one while simplifying the resulting CNF
  192%%%       CARE: C1 is supposed to be smaller than C2
  193
  194combine_clauses(C,[],C) :-
  195	!,
  196	verbose('  trivial combination').
  197combine_clauses([[L]],C1,[[L]|C2]) :-
  198	!,
  199	verbose('  1 unit combination'),
  200	simplify(L,C1,C2).	
  201combine_clauses([[L1],[L2]],C1,[[L1],[L2]|C3]) :-
  202	!,
  203	verbose('  2 unit combinations'),
  204	simplify(L1,C1,C2),
  205	simplify(L2,C2,C3).
  206combine_clauses(C1,C2,C) :-	
  207	verbose('  general combination'),
  208	append(C1,C2,C3),
  209	unit_reduction(C3,C4),
  210	subs_reduction(C4,C).
  211
  212%%% ----------------------------------------------------------------------
  213%%% adjoin/3
  214%%%
  215/* adjoin guarantees         that the new information
  216          is satisfied by the current unit clauses
  217   adjoin does not guarantee that the new information 
  218                                  together with the current matrix
  219          is satisfied by the current unit clauses
  220   So you better watch for new unit clauses stemming from reducing the
  221   new matrix
  222
  223   Nonetheless: whenever a unit is added to the unit list, this literal
  224   has been removed (by simplify) from the matrix.
  225*/
  226      
  227adjoin_matrix([[L]],matrix(Units,_),_) :-
  228	verbose('  1 unit adjunction *failure*'),
  229	negated_literal(L,NegL),
  230	identical_member(NegL,Units),
  231	!,fail.
  232adjoin_matrix([[L]],matrix(Units,Matrix1),matrix([L|Units],Matrix2)) :-
  233	!,
  234	verbose('  1 unit adjunction'),
  235	simplify(L,Matrix1,Matrix2).
  236adjoin_matrix([[L1],[L2]],matrix(Units,_),_) :-
  237						% supposition not(negated_literal(L1,L2))
  238	verbose('  2 unit adjunction *failure*'),
  239	(negated_literal(L1,NegL) ; negated_literal(L2,NegL)),
  240	identical_member(NegL,Units),
  241	!,fail.
  242adjoin_matrix([[L1],[L2]],matrix(Units,Matrix1),matrix([L1,L2|Units],Matrix3)) :-
  243						% supposition not(negated_literal(L1,L2))
  244	!,
  245	verbose('  2 unit adjunctions'),
  246	simplify(L1,Matrix1,Matrix2),
  247	simplify(L2,Matrix2,Matrix3).
  248adjoin_matrix(Matrix1,matrix(Units,Matrix2),matrix(Units,Matrix3)) :-
  249	satisfy_matrix(Matrix1,Units,_) ->
  250	       	verbose('  full adjunction'),
  251		append(Matrix1,Matrix2,Matrix3);
  252	% true ->
  253		verbose('  weak satisfaction *failure*'),
  254		fail.
  255
  256
  257append_matrix([[L]],matrix(Units,Matrix),matrix(Units,[[L]|Matrix])) :-
  258						% allows for multiple occurrences
  259	verbose('  1 unit appendage'),
  260	!.
  261append_matrix([[L1],[L2]],matrix(Units,Matrix),matrix(Units,[[L1],[L2]|Matrix])) :-
  262						% allows for multiple occurrences
  263	verbose('  2 unit appendage'),
  264	!.
  265append_matrix(Matrix1,matrix(Units,Matrix2),matrix(Units,Matrix3)) :-
  266	verbose('  full appendage'),
  267	append(Matrix1,Matrix2,Matrix3).
  268
  269%%% ----------------------------------------------------------------------
  270%%% matrix_reduction/2
  271%%%      bunch of matrix reductions
  272%%%
  273
  274matrix_reduction(C1,C) :-
  275	taut_reduction(C1,C2),
  276	mult_reduction(C2,C3),
  277	unit_reduction(C3,C4),
  278	subs_reduction(C4,C).
  279
  280%%% ----------------------------------------------------------------------
  281%%% unit_reduction/2
  282%%%      unit reduction
  283%%%
  284
  285unit_reduction(M,[[L]|M1]) :-
  286	mymember([L],M),
  287	!,
  288	simplify(L,M,M2),
  289	unit_reduction(M2,M1).
  290unit_reduction(M,M).
  291
  292%%% unit_extraction/3 
  293%%%        is a special purpose reduction for model-finding
  294%%%          2nd arg gives matrix without unit clauses
  295%%%          3rd arg gives literals in unit clauses
  296
  297unit_extraction(M,M1,[L|R]) :-
  298	mymember([L],M),
  299	!,
  300	simplify(L,M,M2),
  301	unit_extraction(M2,M1,R).
  302unit_extraction(M,M,[]).
  303
  304
  305simplify(_L, [], [] ) .
  306simplify( L, [C|Cs] , NewCs ) :-
  307	mymember(L,C),
  308	!,
  309	simplify(L,Cs,NewCs).
  310simplify( L, [C|Cs], [NewC|NewCs] ) :-
  311	negated_literal(L,NegL),
  312	myselect(NegL,C,NewC),
  313	!,
  314	simplify(L,Cs,NewCs).
  315simplify( L, [C|Cs], [C|NewCs]    ) :-
  316	simplify(L,Cs,NewCs).
  317
  318%%% ----------------------------------------------------------------------
  319%%% subs_reduction/2
  320%%%      subs reduction
  321%%%
  322
  323subs_reduction([],[]).
  324subs_reduction([C1|M1],M) :-
  325	subs_reduction(M1,M2),
  326	(subsumes(C1,M2,M3) ->
  327	    M = [C1|M3];
  328	%true ->
  329	    M = M2).
  330
  331subsumes(_,[],[]).
  332subsumes(C1,[C2|_],_) :-
  333	mysubset(C2,C1),
  334	!,
  335	fail.
  336subsumes(C,[C1|M1],M) :-
  337	subsumes(C,M1,M2),
  338	!,
  339	(mysubset(C,C1) ->
  340	        M=M2;
  341	%true ->
  342		M=[C1|M2]).
  343
  344%%% ----------------------------------------------------------------------
  345%%% taut_reduction/2
  346%%%      taut reduction
  347%%%
  348
  349taut_reduction([],[]) :- !.
  350taut_reduction([C|M1],M2) :-
  351	taut_reduction(M1,M3),
  352	(taut_clause(C) ->
  353	    M2 = M3;
  354	%true ->
  355	    M2 = [C|M3]
  356	).
  357
  358taut_clause(C) :-
  359	mymember(L,C),
  360	negated_literal(L,K),
  361	mymember(K,C).
  362	
  363%%% ----------------------------------------------------------------------
  364%%% mult_reduction/2
  365%%%     mult reduction
  366%%%
  367
  368mult_reduction([],[]).
  369mult_reduction([C|M1],[NewC|M3]) :-
  370	mult_reduction(M1,M3),
  371	remove_dups(C,NewC).
  372
  373remove_dups([],[]).
  374remove_dups([L|RestC],NewC) :-
  375	remove_dups(RestC,NewRestC),
  376	(mymember(L,NewRestC) ->
  377	    NewC = NewRestC;
  378	%true ->
  379	    NewC = [L|NewRestC]
  380	)