1:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).    2:- module(mpred_pttp_compile,[]).    3:- endif.    4
    5:- '$set_source_module'(baseKB).    6
    7:- abolish(pttp_prove,6).    8:- abolish(search_cost,3).    9:- abolish(search,6).   10:- abolish(make_wrapper,3).   11:- abolish(add_features,2).   12:- abolish(add_args,13).   13
   14pttp_prove(Goal,Max,Min,Inc,ProofIn,ProofOut,ShowProof) :-
   15	expand_input_proof(ProofIn,PrfEnd),
   16	PrevInc is Min + 1,
   17	add_args(Goal,Goal,_,_,[],_,_,[],[],DepthIn,DepthOut,[PrfEnd|PrfEnd],ProofOut1,Goal1,_),!,
   18        search(Goal1,Max,Min,Inc,PrevInc,DepthIn,DepthOut),
   19        (ShowProof == no ; ( contract_output_proof(ProofOut1,ProofOut),write_proof(ProofOut1),nl)).
   20
   21%%% ***
   22%%% ****f* PTTP/pttp_prove
   23%%% DESCRIPTION
   24%%%   pttp_prove(Goal) can be used to pttp_prove Goal using code compiled by PTTP.
   25%%%   It uses depth-first iterative-deepening search and prints the proof.
   26%%%
   27%%%   Depth-first iterative-deepening search can be controlled
   28%%%   by extra paramaters of the pttp_prove predicate:
   29%%%      pttp_prove(Goal,Max,Min,Inc,ProofIn)
   30%%%   Max is the maximum depth to search (defaults to a big number),
   31%%%   Min is the minimum depth to search (defaults to 0),
   32%%%   Inc is the amount to increment the bound each time (defaults to 1).
   33%%%   ProofIn specifies initial steps of proof to retrace (defaults to []).
   34%%%
   35%%%   A query can be compiled along with the axioms by including the
   36%%%   clause 'query :- ...'.  The query can then be proved by 'pttp_prove(query)'.
   37%%% SOURCE
   38
   39pttp_prove(Goal,Max,Min,Inc,ProofIn,ProofOut) :- prove_inc(Goal,Max,Min,Inc,ProofIn,ProofOut).
   40
   41prove_inc(Goal,Max,Min,Inc,ProofIn,ProofOut) :-
   42	expand_input_proof(ProofIn,PrfEnd),
   43	PrevInc is Min + 1,
   44	add_args(_INFO,Goal,_,_,[],_,_,[],[],DepthIn,DepthOut,[PrfEnd|PrfEnd],ProofOut1,Goal1,_),
   45	!,
   46	timed_call(search(Goal1,Max,Min,Inc,PrevInc,DepthIn,DepthOut),'Proof'),
   47	contract_output_proof(ProofOut1,ProofOut),
   48	must(write_proof(ProofOut1)),
   49	nl.
   50
   51pttp_prove(Goal,Max,Min,Inc,ProofIn) :-
   52	pttp_prove(Goal,Max,Min,Inc,ProofIn,_).
   53
   54pttp_prove(Goal,Max,Min,Inc) :-
   55	pttp_prove(Goal,Max,Min,Inc,[],_).
   56
   57pttp_prove(Goal,Max,Min) :-
   58	pttp_prove(Goal,Max,Min,1,[],_).
   59
   60pttp_prove(Goal,Max) :-
   61	pttp_prove(Goal,Max,2,3).
   62
   63%pttp_prove(Goal) :- pttp_prove(Goal,15).
   64pttp_prove(Goal) :-  pttp_prove(Goal,1000000,0,1,[],_).
   65
   66
   67%%% ****if* PTTP/test_and_decrement_search_cost_expr
   68%%% SOURCE
   69
   70test_and_decrement_search_cost_expr(DepthIn,Cost,Depth1,Expr) :-
   71	Cost == 0 ->
   72		Depth1 = DepthIn,
   73		Expr = true;
   74	%true ->
   75		Expr = test_and_decrement_search_cost(DepthIn,Cost,Depth1).
   76
   77test_and_decrement_search_cost(DepthIn,Cost,Depth1):- DepthIn >= Cost , Depth1 is DepthIn - Cost.
   78
   79%%% ****if* PTTP/add_features
   80%%% SOURCE
   81
   82add_features(In,Out):- is_ftVar(In),!,dtrace,Out=In.
   83add_features(true,true):- !.
   84add_features((Head :- Body),NewHeadBody):- 
   85   must_det_l((
   86    add_features0((Head :- Body),OUT),
   87    OUT = (Head1 :- Body1),
   88    new_head_body(Head, Body,Head1 ,Body1,NewHeadBody))).
   89
   90%new_head_body(Head, Body,Head1 ,Body1,(Head1 :- Body1)):-!.
   91% new_head_body(Head, Body,Head1 ,Body1,(Head1 :- head_body_was(Head, Body), Body1)):- arg_checks()
   92new_head_body(Head, infer_by(_ProofID),Head1 ,Body1,(Head1 :- Body1)):- ground(Head),!.
   93new_head_body(Head, _Body,Head1 ,Body1,(Head1 :- Body1)):- is_query_lit(Head),!.
   94new_head_body(_Head, _Body,Head1 ,Body1,(Head1 :- Body1)):- 
   95   true. 
   96   %   dmsg(pp((head_features(Head1) :-head_body_was(Head, Body), Body1))).
   97
   98:- meta_predicate(call_proof(0,*)).   99call_proof(Call,_):-catch(call(Call),E,(wdmsg(error(E:Call)),fail)).
  100
  101add_features0((Head :- Body),OUT):-pttp_builtin(Head),!, add_features_hb(Head , Body , _Head1 , Body1),!,OUT=(Head :- Body1).
  102add_features0(B,A):- add_features1(B,A).
  103
  104add_features1((Head :- Body),(Head1 :- Body1)) :- (ground(Head);is_query_lit(Head)),!, add_features_hb_normal(Head , Body , Head1 , Body1).
  105
  106add_features1((Head :- Body),(Head1 :- Body1)) :- add_features_hb(Head , Body , Head1 , Body1).
  107
  108add_features_hb(Head , Body ,Head1 , Body1) :-     
  109       linearize(Head,Head2,[],_,true,Matches),
  110       (is_negative_literal(Head) ->
  111               PosGoal = no;
  112       %true ->
  113               PosGoal = yes),
  114       Head =.. [HF|HeadArgs],
  115      
  116       add_args(Head,Body,
  117          PosGoal,GoalAtom,HeadArgs,
  118          PosAncestors,NegAncestors,
  119          NewPosAncestors,NewNegAncestors,
  120          Depth1,DepthOut,
  121          ProofIn,ProofOut,
  122                Body2,New),
  123
  124       (is_ftVar(New) ->
  125               PushAnc = true;
  126
  127       PosGoal = yes ->
  128               NewNegAncestors = NegAncestors,
  129               PushAnc = (NewPosAncestors = [GoalAtom|PosAncestors]);
  130       %true -> ( PosGoal == false)
  131               NewPosAncestors = PosAncestors,
  132               PushAnc = (NewNegAncestors = [GoalAtom|NegAncestors])),
  133
  134   search_cost(Body,HeadArgs,Cost),       
  135   test_and_decrement_search_cost_expr(DepthIn,Cost,Depth1,TestExp0),
  136
  137   argument_type_checking(HF,HeadArgs,TypeCheck),
  138   conjoin_pttp(TestExp0,TypeCheck,TestExp),
  139       conjoin_pttp(PushAnc,Body2,Body4),
  140       conjoin_pttp(Matches,Body4,Body5),
  141       conjoin_pttp(pretest_call(TestExp),Body5,Body1),
  142     
  143     add_head_args(Head2,
  144          PosGoal,GoalAtom,HeadArgs,
  145          PosAncestors,NegAncestors,
  146          NewPosAncestors,NewNegAncestors,
  147          DepthIn,DepthOut,
  148          ProofIn,ProofOut,Head1,New).
  149
  150add_features_hb_normal(Head , Body ,Head1 , Body1) :-
  151       ( is_query_lit(Head) ->
  152		Head2 = Head,
  153		add_args(Head2,Body,yes,query,[],
  154		         PosAncestors,NegAncestors,
  155			 PosAncestors,NegAncestors,
  156		         DepthIn,DepthOut,
  157			 ProofIn,ProofOut,
  158			 Body1,_);
  159	%true ->
  160		linearize(Head,Head2,[],_,true,Matches),
  161		(is_negative_literal(Head) ->
  162			PosGoal = no;
  163		%true ->
  164			PosGoal = yes),
  165		Head =.. [HF|HeadArgs],
  166            
  167		add_args(Head,Body,PosGoal,GoalAtom,HeadArgs,
  168                         PosAncestors,NegAncestors,
  169			 NewPosAncestors,NewNegAncestors,
  170		         Depth1,DepthOut,
  171			 ProofIn,ProofOut,
  172			 Body2,New),    
  173
  174		(is_ftVar(New) ->
  175			PushAnc = true;
  176
  177		PosGoal = yes ->
  178			NewNegAncestors = NegAncestors,
  179			PushAnc = (NewPosAncestors = [GoalAtom|PosAncestors]);
  180		%true -> ( PosGoal == false)
  181			NewPosAncestors = PosAncestors,
  182			PushAnc = (NewNegAncestors = [GoalAtom|NegAncestors])),
  183
  184
  185              search_cost(Body,HeadArgs,Cost),       
  186              test_and_decrement_search_cost_expr(DepthIn,Cost,Depth1,TestExp0),
  187              argument_type_checking(HF,HeadArgs,TypeCheck),
  188              conjoin_pttp(TestExp0,TypeCheck,TestExp),
  189		conjoin_pttp(PushAnc,Body2,Body4),
  190		conjoin_pttp(Matches,Body4,Body5),
  191		conjoin_pttp(pretest_call(TestExp),Body5,Body1)                
  192                ),
  193     
  194    	Head2 =.. [P|L],
  195	internal_functor(P,IntP),
  196	list_append(L,
  197                    [PosAncestors,NegAncestors,
  198		       DepthIn,DepthOut,
  199		       ProofIn,ProofOut,
  200		       GoalAtom],
  201		    L1),
  202	Head1 =.. [IntP|L1].
  203
  204
  205
  206add_head_args(HeadIn,
  207          _PosGoal,GoalAtom,_HeadArgs,
  208          PosAncestors,NegAncestors,
  209          _NewPosAncestors,_NewNegAncestors,
  210          DepthIn,DepthOut,
  211          ProofIn,ProofOut,
  212          Head1,_New):-
  213     correct_pttp_head(true_t,HeadIn,Head),
  214        Head =.. [P|L],
  215	internal_functor(P,IntP),
  216	list_append(L, [PosAncestors,NegAncestors, DepthIn,DepthOut, ProofIn,ProofOut, GoalAtom], L1),
  217	Head1 =.. [IntP|L1].
  218
  219%%% ***
  220%%% ****if* PTTP/add_args
  221%%% SOURCE
  222
  223:- was_export(add_args/15).  224
  225add_args(INFO,(A , B),PosGoal,GoalAtom,HeadArgs,
  226         PosAncestors,NegAncestors,
  227	 NewPosAncestors,NewNegAncestors,
  228	 DepthIn,DepthOut,
  229	 ProofIn,ProofOut,
  230	 Body1,New) :-
  231		add_args(INFO,A,PosGoal,GoalAtom,HeadArgs,
  232                         PosAncestors,NegAncestors,
  233			 NewPosAncestors,NewNegAncestors,
  234		         DepthIn,Depth1,
  235			 ProofIn,Proof1,
  236		         A1,New),
  237		add_args(INFO,B,PosGoal,GoalAtom,HeadArgs,
  238		         PosAncestors,NegAncestors,
  239			 NewPosAncestors,NewNegAncestors,
  240		         Depth1,DepthOut,
  241			 Proof1,ProofOut,
  242                         B1,New),
  243		conjoin_pttp(A1,B1,Body1),!.
  244
  245add_args(INFO,(A ; B),PosGoal,GoalAtom,HeadArgs,
  246         PosAncestors,NegAncestors,
  247	 NewPosAncestors,NewNegAncestors,
  248	 DepthIn,DepthOut,
  249	 ProofIn,ProofOut,
  250	 Body1,New) :-
  251               add_args(INFO,A,PosGoal,GoalAtom,HeadArgs,
  252		         PosAncestors,NegAncestors,
  253			 NewPosAncestors,NewNegAncestors,
  254		         DepthA,DepthOut,
  255			 ProofIn,ProofOut,
  256			 A2,New),
  257		add_args(INFO,B,PosGoal,GoalAtom,HeadArgs,
  258		         PosAncestors,NegAncestors,
  259			 NewPosAncestors,NewNegAncestors,
  260		         DepthB,DepthOut,
  261			 ProofIn,ProofOut,
  262			 B2,New),
  263   % dtrace,
  264                search_cost(A,HeadArgs,CostA),
  265		search_cost(B,HeadArgs,CostB),
  266		(CostA < CostB ->
  267			DepthA = DepthIn,
  268			Cost is CostB - CostA,
  269			test_and_decrement_search_cost_expr(DepthIn,Cost,DepthB,TestExp),
  270			A1 = A2,
  271			conjoin_pttp(pretest_call(TestExp),B2,B1);
  272		CostA > CostB ->
  273			DepthB = DepthIn,
  274			Cost is CostA - CostB,
  275			test_and_decrement_search_cost_expr(DepthIn,Cost,DepthA,TestExp),
  276			B1 = B2,
  277			conjoin_pttp(pretest_call(TestExp),A2,A1);
  278		%true ->
  279		        DepthA = DepthIn,
  280			DepthB = DepthIn,
  281			A1 = A2,
  282			B1 = B2),
  283		disjoin(A1,B1,Body1).
  284
  285add_args(_INFO,Search_cost,_PosGoal,_GoalAtom,_HeadArgs,_PosAncestors,_NegAncestors,_NewPosAncestors,_NewNegAncestors,Depth,Depth,Proof,Proof,true,_New):- 
  286  functor(Search_cost,search_cost,_),!.
  287
  288add_args(INFO,infer_by(_N),PosGoal,GoalAtom,_HeadArgs,
  289         PosAncestors,NegAncestors,
  290	 _NewPosAncestors,_NewNegAncestors,
  291	 Depth,Depth,
  292	 ProofIn,ProofOut,
  293	 Body1,_New) :-
  294    (PosGoal = yes -> 
  295			N1 = INFO;
  296		%true ->  % atom in proof is negation of actual literal
  297			isNegOf(N1,INFO)),
  298    Body1 = (ProofIn = [Prf,[N1,GoalAtom,PosAncestors,NegAncestors]|PrfEnd],
  299			 ProofOut = [Prf|PrfEnd]).
  300
  301add_args(_INFO,Body,_PosGoal,_GoalAtom,_HeadArgs,_PosAncestors,_NegAncestors,_NewPosAncestors,_NewNegAncestors,Depth,Depth,Proof,Proof,Body,_New):-
  302   pttp_builtin(Body),!.
  303
  304% normal lit
  305add_args(_INFO,BodyIn,
  306         _PosGoal,_GoalAtom,_HeadArgs,
  307         _PosAncestors,_NegAncestors,
  308	 NewPosAncestors,NewNegAncestors,
  309	 DepthIn,DepthOut,
  310	 ProofIn,ProofOut,
  311	 Body1,New) :-
  312   correct_pttp_head(asserted_t,BodyIn,Body), 
  313    Body =.. L,
  314    list_append(L, [NewPosAncestors,NewNegAncestors,DepthIn,DepthOut,ProofIn,ProofOut], L1),
  315    Body11 =.. L1,
  316    Body1 = call_proof(Body11,Body),
  317    New = yes.
  318
  319
  320
  321
  322
  323%%% ***
  324%%% ****if* PTTP/search_cost
  325%%% DESCRIPTION
  326%%%   Search cost is ordinarily computed by counting literals in the body.
  327%%%   It can be given explicitly instead by including a number, as in
  328%%%     p :- search_cost(3).     (ordinarily, cost would be 0)
  329%%%     p :- search_cost(1),q,r. (ordinarily, cost would be 2)
  330%%%     p :- search_cost(0),s.   (ordinarily, cost would be 1)
  331%%% SOURCE
  332
  333search_cost(Body,HeadArgs,N) :-
  334	Body = search_cost(M) ->
  335		N = M;
  336	Body = (A , B) ->
  337		(A = search_cost(M) ->	% if first conjunct is search_cost(M),
  338			N = M;		% search cost of conjunction is M
  339		%true ->
  340			search_cost(A,HeadArgs,N1),
  341			search_cost(B,HeadArgs,N2),
  342			N is N1 + N2);
  343	Body = (A ; B) ->
  344		search_cost(A,HeadArgs,N1),
  345		search_cost(B,HeadArgs,N2),
  346		min(N1,N2,N);
  347	pttp_builtin(Body) ->
  348		N = 0;
  349	%true ->
  350		N = 1.
  351%%% ***
  352%%% ****if* PTTP/search
  353%%% DESCRIPTION
  354%%%   Search driver predicate.
  355%%%   Note that depth-bounded execution of Goal is enabled by
  356%%%   the fact that the DepthIn and DepthOut arguments of
  357%%%   search are also the DepthIn and DepthOut arguments of Goal.
  358%%% SOURCE
  359:- meta_predicate search(0,?,?,?,?,?,?).  360search(Goal,Max,Min,Inc,PrevInc,DepthIn,DepthOut):-search0(Goal,Max,Min,Inc,PrevInc,DepthIn,DepthOut).
  361
  362:- meta_predicate search0(0,?,?,?,?,?,?).  363search0(Goal,Max,Min,Inc,PrevInc,DepthIn,DepthOut):- % dtrace,
  364        search1(Goal,Max,Min,Inc,PrevInc,DepthIn,DepthOut).
  365
  366search1(_Goal,Max,Min,_Inc,_PrevInc,_DepthIn,_DepthOut) :-
  367	Min > Max,
  368	!,
  369	fail.
  370
  371:- meta_predicate search1(0,*,*,*,*,*,*).  372search1(Goal,_Max,Min,_Inc,PrevInc,DepthIn,DepthOut) :-
  373        write_search_progress(Min),
  374	DepthIn = Min,
  375	catchv(call(Goal),E,(wdmsg(E=Goal),dtrace)),
  376	DepthOut < PrevInc.	% fail if solution found previously
  377search1(Goal,Max,Min,Inc,_PrevInc,DepthIn,DepthOut) :-
  378	Min1 is Min + Inc,
  379	search(Goal,Max,Min1,Inc,Inc,DepthIn,DepthOut).
  380%%% ***
  381
  382%%% ****if* PTTP/make_wrapper
  383%%% SOURCE
  384
  385make_wrapper(_DefinedPreds,[query,0],true) :-
  386	!.
  387make_wrapper(DefinedPreds,[P,N],Result):- must_det(make_wrapper0(DefinedPreds,[P,N],Result)).
  388
  389make_wrapper0(DefinedPreds,[P,N],Result) :-
  390	functor(Goal,P,N),
  391	Goal =.. [P|Args],
  392	ExtraArgs = [PosAncestors,NegAncestors,DepthIn,DepthOut,ProofIn,ProofOut],
  393	list_append(Args,ExtraArgs,Args1),
  394	Head =.. [P|Args1],
  395	internal_functor(P,IntP),
  396	list_length_pttp(ExtraArgs,NExtraArgs),
  397	NN is N + NExtraArgs + 1,
  398	(identical_member_special([IntP,NN],DefinedPreds) ->
  399	        list_append(ExtraArgs,[GoalAtom],ExtraArgs2),
  400		list_append(Args,ExtraArgs2,Args2),
  401		IntHead =.. [IntP|Args2];
  402	%true ->
  403		IntHead = fail),
  404	(is_negative_functor(P) ->
  405		negated_literal(Goal,PosGoal),
  406		Red = redn,  % atom in proof is negation of actual literal
  407		C1Ancestors = NegAncestors,
  408		C2Ancestors = PosAncestors;
  409	%true ->
  410		PosGoal = Goal,
  411		Red = red,
  412		C1Ancestors = PosAncestors,
  413		C2Ancestors = NegAncestors),
  414	(N = 0 ->	% special case for propositional calculus
  415		V1 = (identical_member_cheaper(GoalAtom,C2Ancestors) , !);
  416	%true ->
  417		V1 = ((identical_member_cheaper(GoalAtom,C2Ancestors) , !);
  418		       unifiable_member_cheaper(GoalAtom,C2Ancestors))),
  419	V2 = (DepthOut = DepthIn,
  420		 ProofIn = [Prf,[Red,GoalAtom,PosAncestors,NegAncestors]|PrfEnd],
  421		 ProofOut = [Prf|PrfEnd]),
  422	conjoin_pttp(V1,V2,Reduce),
  423	Result = (Head :- GoalAtom = PosGoal,
  424		  	  (identical_member_special_loop_check(GoalAtom,C1Ancestors) ->
  425			   	fail;
  426			  %true ->
  427			   	(Reduce;
  428				 IntHead))).
  429%%% ***
  430%%% ****if* PTTP/query
  431%%% DESCRIPTION
  432%%%   query uses the following definition instead of the more complex one
  433%%%   that would be created by make_wrapper
  434%%% SOURCE
  435
  436% 3 = suc(suc(1))
  437% 3/67 = div(suc(suc(1)),67)
  438
  439
  440query(PosAncestors,NegAncestors,DepthIn,DepthOut,ProofIn,ProofOut) :- 
  441  get_int_query(Int_query),
  442	call(Int_query,PosAncestors,NegAncestors,DepthIn,DepthOut,ProofIn,ProofOut,query).
  443
  444:- fixup_exports.