1:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).    2:- module(mpred_pttp_compile,[]).    3:- endif.    4
    5:- abolish(pttp_prove,6).    6:- abolish(search_cost,3).    7:- abolish(search,6).    8:- abolish(make_wrapper,3).    9:- abolish(add_features,2).   10:- abolish(add_args,13).   11
   12
   13%%% ****h* PTTP/PTTP-dalit
   14%%% COPYRIGHT
   15%%%   Copyright (c) 1988-2003 Mark E. Stickel, SRI International, Menlo Park, CA 94025  USA
   16%%% 
   17%%%   Permission is hereby granted, free of charge, to any person obtaining a
   18%%%   copy of this software and associated documentation files (the "Software"),
   19%%%   to deal in the Software without restriction, including without limitation
   20%%%   the rights to use, copy, modify, merge, publish, distribute, sublicense,
   21%%%   and/or sell copies of the Software, and to permit persons to whom the
   22%%%   Software is furnished to do so, subject to the following conditions:
   23%%% 
   24%%%   The above copyright notice and this permission notice shall be included
   25%%%   in all copies or substantial portions of the Software.
   26%%% 
   27%%%   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
   28%%%   EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
   29%%%   MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
   30%%%   IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
   31%%%   CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
   32%%%   TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
   33%%%   SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
   34%%% DESCRIPTION
   35%%%  
   36%%%      A Prolog Technology Theorem Prover
   37%%%  
   38%%%               Mark E. Stickel
   39%%%  
   40%%%   This file contains changes to PTTP to use
   41%%%   depth-first iterative deepening dalit_search with bound on
   42%%%   D_Alit (maximum number of A-literals on a branch)
   43%%%   instead of
   44%%%   D_Inf (total number of subgoals).
   45%%%
   46%%%   To use, load pttp and then load this file
   47%%%   to replace changed definitions.
   48%%% SOURCE
   49
   50:- abolish(pttp_prove,6).   51pttp_prove(Goal,Max,Min,Inc,ProofIn,ProofOut):-dalit_prove(Goal,Max,Min,Inc,ProofIn,ProofOut).
   52
   53dalit_prove(Goal,Max,Min,Inc,ProofIn,ProofOut) :-
   54	expand_input_proof(ProofIn,PrfEnd),
   55	PrevInc is Min + 1,
   56	dalit_add_args(INFO,Goal,_,_,[],_,_,[],[],DepthIn,[PrfEnd|PrfEnd],ProofOut1,Goal1,_),
   57	!,
   58	timed_call(dalit_search(Goal1,Max,Min,Inc,PrevInc,DepthIn),'Proof'),
   59	contract_output_proof(ProofOut1,ProofOut),
   60	write_proof(ProofOut1),
   61	nl.
   62
   63dalit_prove(Goal,Max,Min,Inc,ProofIn) :-
   64	dalit_prove(Goal,Max,Min,Inc,ProofIn,_).
   65
   66dalit_prove(Goal,Max,Min,Inc) :-
   67	dalit_prove(Goal,Max,Min,Inc,[],_).
   68
   69dalit_prove(Goal,Max,Min) :-
   70	dalit_prove(Goal,Max,Min,1,[],_).
   71
   72dalit_prove(Goal,Max) :-
   73	dalit_prove(Goal,Max,0,1,[],_).
   74
   75dalit_prove(Goal) :-
   76	dalit_prove(Goal,10000,0,1,[],_).
   77
   78:- abolish(search_cost,3).   79search_cost(Body,HeadArgs,N):-dalit_search_cost(Body,HeadArgs,N).
   80dalit_search_cost(Body,HeadArgs,N) :-
   81	Body = dalit_search_cost(M) ->
   82		N = M;
   83	Body = (A , B) ->
   84		(A = dalit_search_cost(M) ->	% if first conjunct is dalit_search_cost(M),
   85			N = M;		% dalit_search cost of conjunction is M
   86		%true ->
   87			dalit_search_cost(A,HeadArgs,N1),
   88			dalit_search_cost(B,HeadArgs,N2),
   89			max(N1,N2,N));
   90	Body = (A ; B) ->
   91		dalit_search_cost(A,HeadArgs,N1),
   92		dalit_search_cost(B,HeadArgs,N2),
   93		min(N1,N2,N);
   94	pttp_builtin(Body) ->
   95		N = 0;
   96	%true ->
   97		N = 1.
   98
   99:- abolish(search,6).  100search(Goal,Max,Min,Inc,PrevInc,DepthIn):-dalit_search(Goal,Max,Min,Inc,PrevInc,DepthIn).
  101
  102dalit_search(_Goal,Max,Min,_Inc,_PrevInc,_DepthIn) :-
  103	Min > Max,
  104	!,
  105	fail.
  106dalit_search(Goal,_Max,Min,_Inc,PrevInc,DepthIn) :-
  107        write_search_progress(Min),
  108	DepthIn = Min,
  109	call(Goal),
  110	true.			% should fail if solution found previously
  111dalit_search(Goal,Max,Min,Inc,_PrevInc,DepthIn) :-
  112	Min1 is Min + Inc,
  113	dalit_search(Goal,Max,Min1,Inc,Inc,DepthIn).
  114
  115:- abolish(make_wrapper,3).  116make_wrapper(Body,HeadArgs,N):-dalit_make_wrapper(Body,HeadArgs,N).
  117
  118dalit_make_wrapper(_DefinedPreds,[query,0],true) :-
  119	!.
  120dalit_make_wrapper(DefinedPreds,[P,N],Result) :-
  121	functor(Goal,P,N),
  122	Goal =.. [P|Args],
  123	ExtraArgs = [PosAncestors,NegAncestors,DepthIn,ProofIn,ProofOut],
  124	list_append(Args,ExtraArgs,Args1),
  125	Head =.. [P|Args1],
  126	internal_functor(P,IntP),
  127	list_length_pttp(ExtraArgs,NExtraArgs),
  128	NN is N + NExtraArgs + 1,
  129	(identical_member_special([IntP,NN],DefinedPreds) ->
  130	        list_append(ExtraArgs,[GoalAtom],ExtraArgs2),
  131		list_append(Args,ExtraArgs2,Args2),
  132		IntHead =.. [IntP|Args2];
  133	%true ->
  134		IntHead = fail),
  135	(is_negative_functor(P) ->
  136		negated_literal(Goal,PosGoal),
  137		Red = redn,  % atom in proof is negation of actual literal
  138		C1Ancestors = NegAncestors,
  139		C2Ancestors = PosAncestors;
  140	%true ->
  141		PosGoal = Goal,
  142		Red = red,
  143		C1Ancestors = PosAncestors,
  144		C2Ancestors = NegAncestors),
  145	(N = 0 ->	% special case for propositional calculus
  146		V1 = (identical_member_special(GoalAtom,C2Ancestors) , !);
  147	%true ->
  148		V1 = ((identical_member_special(GoalAtom,C2Ancestors) , !);
  149		       unifiable_member(GoalAtom,C2Ancestors))),
  150	V2 = (
  151		 ProofIn = [Prf,[Red,GoalAtom,PosAncestors,NegAncestors]|PrfEnd],
  152		 ProofOut = [Prf|PrfEnd]),
  153	conjoin_pttp(V1,V2,Reduce),
  154	Result = (Head :- GoalAtom = PosGoal,
  155		  	  (identical_member_special_loop_check(GoalAtom,C1Ancestors) ->
  156			   	fail;
  157			  %true ->
  158			   	(Reduce;
  159				 IntHead))).
  160
  161query(PosAncestors,NegAncestors,DepthIn,ProofIn,ProofOut) :-
  162	int_query(PosAncestors,NegAncestors,DepthIn,ProofIn,ProofOut,query).
  163
  164:- abolish(add_features,2).  165add_features(A,B):-dalit_add_features(A,B).
  166
  167dalit_add_features((Head :- Body),(Head1 :- Body1)) :-
  168	(functor(Head,query,_) ->
  169		Head2 = Head,
  170		dalit_add_args(INFO,Body,yes,query,[],
  171		         PosAncestors,NegAncestors,
  172			 PosAncestors,NegAncestors,
  173		         DepthIn,
  174			 ProofIn,ProofOut,
  175			 Body1,_);
  176	%true ->
  177		linearize(Head,Head2,[],_,true,Matches),
  178		(is_negative_literal(Head) ->
  179			PosGoal = no;
  180		%true ->
  181			PosGoal = yes),
  182		Head =.. [_|HeadArgs],
  183		dalit_add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
  184                         PosAncestors,NegAncestors,
  185			 NewPosAncestors,NewNegAncestors,
  186		         Depth1,
  187			 ProofIn,ProofOut,
  188			 Body2,New),
  189		(is_ftVar(New) ->
  190			PushAnc = true;
  191		PosGoal = yes ->
  192			NewNegAncestors = NegAncestors,
  193			PushAnc = (NewPosAncestors = [GoalAtom|PosAncestors]);
  194		%true ->
  195			NewPosAncestors = PosAncestors,
  196			PushAnc = (NewNegAncestors = [GoalAtom|NegAncestors])),
  197		dalit_search_cost(Body,HeadArgs,Cost),
  198		test_and_decrement_search_cost_expr(DepthIn,Cost,Depth1,TestExp),
  199		conjoin_pttp(PushAnc,Body2,Body4),
  200		conjoin_pttp(Matches,Body4,Body5),
  201		conjoin_pttp(TestExp,Body5,Body1)),
  202    	Head2 =.. [P|L],
  203	internal_functor(P,IntP),
  204	list_append(L,[PosAncestors,NegAncestors,
  205		       DepthIn,
  206		       ProofIn,ProofOut,
  207		       GoalAtom],
  208		    L1),
  209	Head1 =.. [IntP|L1].
  210
  211:- abolish(add_args,13).  212
  213add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
  214         PosAncestors,NegAncestors,
  215	 NewPosAncestors,NewNegAncestors,
  216	 DepthIn,
  217	 ProofIn,ProofOut,
  218	 Body1,New):- 
  219  dalit_add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
  220         PosAncestors,NegAncestors,
  221	 NewPosAncestors,NewNegAncestors,
  222	 DepthIn,
  223	 ProofIn,ProofOut,
  224	 Body1,New).
  225
  226dalit_add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
  227         PosAncestors,NegAncestors,
  228	 NewPosAncestors,NewNegAncestors,
  229	 DepthIn,
  230	 ProofIn,ProofOut,
  231	 Body1,New) :-
  232	Body = (A , B) ->
  233		dalit_add_args(INFO,A,PosGoal,GoalAtom,HeadArgs,
  234                         PosAncestors,NegAncestors,
  235			 NewPosAncestors,NewNegAncestors,
  236		         DepthIn,
  237			 ProofIn,Proof1,
  238		         A1,New),
  239		dalit_add_args(INFO,B,PosGoal,GoalAtom,HeadArgs,
  240		         PosAncestors,NegAncestors,
  241			 NewPosAncestors,NewNegAncestors,
  242			 DepthIn,
  243			 Proof1,ProofOut,
  244                         B1,New),
  245		conjoin_pttp(A1,B1,Body1);
  246	Body = (A ; B) ->
  247		throw(unimplemented);
  248	functor(Body,dalit_search_cost,_) ->
  249		ProofOut = ProofIn,
  250		Body1 = true;
  251	Body = infer_by(N) ->
  252		(PosGoal = yes -> 
  253			N1 = N;
  254		%true ->  % atom in proof is negation of actual literal
  255			isNegOf(N1,N)),
  256		Body1 = (ProofIn = [Prf,[N1,GoalAtom,PosAncestors,NegAncestors]|PrfEnd],
  257			 ProofOut = [Prf|PrfEnd]);
  258	Body = dalit_search_cost(N) ->
  259		ProofOut = ProofIn,
  260		Body1 = true;
  261	pttp_builtin(Body) ->
  262		ProofOut = ProofIn,
  263		Body1 = Body;
  264	%true ->
  265		Body =.. L,
  266		list_append(L,
  267                       [NewPosAncestors,NewNegAncestors,
  268			DepthIn,
  269			ProofIn,ProofOut],
  270		       L1),
  271		Body1 =.. L1,
  272		New = yes.
  273%%% ***
  274
  275:- fixup_exports.