40
41:- module(clpcd_nf,
42 [
43 add_constraint/2,
44 nf/3,
45 entailed/2,
46 repair/3,
47 nf_constant/2,
48 wait_linear/4,
49 nf2term/3
50 ]). 51
52:- use_module(library(clpcd/geler)). 53:- use_module(library(clpcd/ineq)). 54:- use_module(library(clpcd/domain_ops)). 55:- use_module(library(clpcd/store)). 56:- use_module(library(clpcd/solve)). 57:- use_module(library(clpcd/highlight), []). 58
60
68
69add_constraint(Rel, CLP) :-
70 var(Rel),
71 !,
72 throw(instantiation_error(CLP:{Rel},1)).
73add_constraint((R,Rs), CLP) :-
74 !,
75 add_constraint(R, CLP),
76 add_constraint(Rs, CLP).
77add_constraint((R;Rs), CLP) :-
78 !,
79 ( add_constraint(R, CLP)
80 ; add_constraint(Rs, CLP)
81 ). 82add_constraint(L < R, CLP) :-
83 !,
84 nf(L-R,CLP,Nf),
85 submit_lt(Nf, CLP).
86add_constraint(L > R, CLP) :-
87 !,
88 nf(R-L,CLP,Nf),
89 submit_lt(Nf, CLP).
90add_constraint(L =< R, CLP) :-
91 !,
92 nf(L-R,CLP,Nf),
93 submit_le(Nf, CLP).
94add_constraint(<=(L,R), CLP) :-
95 !,
96 nf(L-R,CLP,Nf),
97 submit_le(Nf, CLP).
98add_constraint(L >= R, CLP) :-
99 !,
100 nf(R-L,CLP,Nf),
101 submit_le(Nf, CLP).
102add_constraint(L =\= R, CLP) :-
103 !,
104 nf(L-R,CLP,Nf),
105 submit_ne(CLP, Nf).
106add_constraint(L =:= R, CLP) :-
107 !,
108 nf(L-R,CLP,Nf),
109 submit_eq(Nf, CLP).
110add_constraint(L = R, CLP) :-
111 !,
112 nf(L-R,CLP,Nf),
113 submit_eq(Nf, CLP).
114add_constraint(Rel, CLP) :- throw(type_error(CLP:{Rel},1,'a constraint',Rel)).
115
122
123entailed(CLP, C) :-
124 negate(C,CLP,Cn),
125 \+ add_constraint(Cn, CLP).
126
131
132negate(Rel,CLP,_) :-
133 var(Rel),
134 !,
135 throw(instantiation_error(entailed(CLP,Rel),1)).
136negate((A,B),C,(Na;Nb)) :-
137 !,
138 negate(A,C,Na),
139 negate(B,C,Nb).
140negate((A;B),C,(Na,Nb)) :-
141 !,
142 negate(A,C,Na),
143 negate(B,C,Nb).
144negate(A<B,_,A>=B) :- !.
145negate(A>B,_,A=<B) :- !.
146negate(A=<B,_,A>B) :- !.
147negate(A>=B,_,A<B) :- !.
148negate(A=:=B,_,A=\=B) :- !.
149negate(A=B,_,A=\=B) :- !.
150negate(A=\=B,_,A=:=B) :- !.
151negate(Rel,CLP,_) :- throw( type_error(entailed(CLP,Rel),1,'a constraint',Rel)).
152
171
172submit_eq([], _). 173submit_eq([T|Ts], CLP) :-
174 submit_eq(Ts,CLP,T).
175submit_eq([],CLP,A) :- submit_eq_b(A, CLP). 176submit_eq([B|Bs],CLP,A) :- submit_eq_c(A,CLP,B,Bs). 177
181
183submit_eq_b(v(_,[]), _) :-
184 !,
185 fail.
187submit_eq_b(v(_,[X^P]), CLP) :-
188 var(X),
189 compare_d(CLP, <, 0, P),
190 !,
191 eval_d(CLP, 0, X).
193submit_eq_b(v(_,[NL^1]), CLP) :-
194 nonvar(NL),
195 nl_invertible(CLP,NL),
196 !,
197 nl_invert(CLP,NL,X,0,Inv),
198 nf(-Inv,CLP,S),
199 nf_add(X, CLP, S, New),
200 submit_eq(New, CLP).
202submit_eq_b(Term, CLP) :-
203 term_variables(Term,Vs),
204 geler(CLP,Vs,resubmit_eq(CLP, [Term])).
205
209
211submit_eq_c(v(I,[]),CLP,B,Rest) :-
212 !,
213 submit_eq_c1(Rest,CLP,B,I).
214submit_eq_c(v(B,[X^P1]), CLP, v(A,[Y^P2]), []) :-
215 compare_d(CLP, =, P2, 2*P1),
216 X==Y,
217 !,
218 solve_2nd_eq(CLP, A, B, X, P1, 0 ).
220submit_eq_c(A,CLP,B,Rest) :- 221 A = v(_,[X^1]),
222 var(X),
223 B = v(_,[Y^1]),
224 var(Y),
225 linear(Rest),
226 !,
227 Hom = [A,B|Rest],
228 229 nf_length(Hom,0,Len),
230 log_deref(Len, CLP, Hom, [], HomD),
231 solve(CLP,HomD).
233submit_eq_c(A,CLP,B,Rest) :-
234 Norm = [A,B|Rest],
235 term_variables(Norm,Vs),
236 geler(CLP,Vs,resubmit_eq(CLP, Norm)).
237
238root_d(CLP, I, K, P, R) :-
239 div_d(CLP, I, K, Base),
240 div_d(CLP, 1, P, Exp),
241 eval_d(CLP, Base ** Exp, N),
242 cast_d(CLP, N, R).
243
244solve_2nd_eq(CLP, A, B, X, P1, C) :-
245 eval_d(CLP, B*B, B2),
246 eval_d(CLP, 4*A*C, P),
247 ( compare_d(CLP, >, B2, P)
248 -> 249 eval_d(CLP, B2 - P, Disc),
250 div_d(CLP, B + sign(B)*sqrt(Disc), -2, Temp),
251 div_d(CLP, Temp, A, R1),
252 div_d(CLP, C, Temp, R2),
253 ( compare_d(CLP, <, R1, R2)
254 ->( Z = R1
255 ; Z = R2
256 )
257 ; ( Z = R2
258 ; Z = R1
259 )
260 )
261 ; compare_d(CLP, =, B2, P),
262 div_d(CLP, -B, 2*A, Z)
263 ),
264 eval_d(CLP, -1, M1),
265 submit_eq_c1([], CLP, v(M1,[X^P1]), Z).
266
270
274submit_eq_c1([], CLP, v(K,[X^P]), I) :-
275 var(X),
276 compare_d(CLP, \=, 0, P),
277 compare_d(CLP, =, integer(P), P),
278 compare_d(CLP, >, 0, sign(-I)*sign(K)),
279 compare_d(CLP, =, 1, integer(P) mod 2),
280 !,
281 root_d(CLP, I, K, P, R),
282 eval_d(CLP, -R, Val),
283 X = Val.
287submit_eq_c1([], CLP, v(K,[X^P]), I) :-
288 var(X),
289 compare_d(CLP, \=, 0, P),
290 compare_d(CLP, =, integer(P), P),
291 compare_d(CLP, =<, 0, sign(-I)*sign(K)),
292 compare_d(CLP, =, 0, integer(P) mod 2),
293 !,
294 root_d(CLP, -I, K, P, Val),
295 ( X = Val
296 ; eval_d(CLP, -Val, ValNeg),
297 X = ValNeg
298 ).
301submit_eq_c1([], CLP, v(K,[X^P]), I) :-
302 var(X),
303 compare_d(CLP, \=, 0, P),
304 compare_d(CLP, =<, 0, sign(-I)*sign(K)),
305 !,
306 root_d(CLP, -I, K, P, Val),
307 X = Val.
310submit_eq_c1([v(A,[Y^P2])], CLP, v(B,[X^P1]), C) :-
311 compare_d(CLP, =, P2, 2*P1),
312 X==Y,
313 !,
314 solve_2nd_eq(CLP, A, B, X, P1, C).
316submit_eq_c1([], _, v(_K,[X^_P]), _I) :-
317 var(X),
318 !,
319 fail.
323submit_eq_c1([], CLP, v(K,[X^P]), I) :-
324 nonvar(X),
325 X = _^_, 326 compare_d(CLP, =, 1, abs(P)),
327 compare_d(CLP, >=, 0, I),
328 compare_d(CLP, >=, 0, K),
329 !,
330 fail.
333submit_eq_c1([],CLP,v(K,[NL^P]),I) :-
334 nonvar(NL),
335 ( compare_d(CLP, =, P, 1),
336 div_d(CLP, -I, K, Y)
337 ; compare_d(CLP, =, P, -1),
338 div_d(CLP, -K, I, Y)
339 ),
340 nl_invertible(CLP,NL),
341 !,
342 nl_invert(CLP,NL,X,Y,Inv),
343 nf(-Inv,CLP,S),
344 nf_add(X, CLP, S, New),
345 submit_eq(New, CLP).
347submit_eq_c1(Rest,CLP,B,I) :-
348 B = v(_,[Y^1]),
349 var(Y),
350 linear(Rest),
351 !,
352 353 Hom = [B|Rest],
354 nf_length(Hom,0,Len),
355 normalize_scalar(I,Nonvar),
356 log_deref(Len, CLP, Hom, [], HomD),
357 add_linear_11(CLP, Nonvar, HomD, LinD),
358 solve(CLP,LinD).
360submit_eq_c1(Rest,CLP,B,I) :-
361 Norm = [v(I,[]),B|Rest],
362 term_variables(Norm,Vs),
363 geler(CLP,Vs,resubmit_eq(CLP, Norm)).
364
366
370
372submit_lt([], _) :- fail.
374submit_lt([A|As], CLP) :- submit_lt(As, CLP, A).
375
379
381submit_lt([], CLP, v(K,P)) :- submit_lt_b(P,CLP,K).
383submit_lt([B|Bs], CLP, A) :- submit_lt_c(Bs,CLP,A,B).
384
388
390submit_lt_b([],CLP,I) :-
391 !,
392 compare_d(CLP, <, I, 0).
394submit_lt_b([X^1],CLP,K) :-
395 var(X),
396 !,
397 ( compare_d(CLP, >, K, 0)
398 -> ineq_one_s_p_0(CLP, X) 399 ; ineq_one_s_n_0(CLP, X) 400 ).
402submit_lt_b(P,CLP,K) :-
403 term_variables(P,Vs),
404 geler(CLP,Vs,resubmit_lt(CLP, [v(K,P)])).
405
409
411submit_lt_c([],CLP,A,B) :-
412 A = v(I,[]),
413 B = v(K,[Y^1]),
414 var(Y),
415 !,
416 ineq_one(strict, CLP, Y, K, I).
418submit_lt_c(Rest,CLP,A,B) :-
419 Norm = [A,B|Rest],
420 ( linear(Norm)
421 -> 'solve_<'(CLP, Norm)
422 ; term_variables(Norm,Vs),
423 geler(CLP,Vs,resubmit_lt(CLP, Norm))
424 ).
425
430
432submit_le([], _).
434submit_le([A|As], CLP) :- submit_le(As, CLP, A).
435
439
441submit_le([], CLP, v(K,P)) :- submit_le_b(P,CLP,K).
443submit_le([B|Bs], CLP, A) :- submit_le_c(Bs,CLP,A,B).
444
448
450submit_le_b([],CLP,I) :-
451 !,
452 compare_d(CLP, =<, I, 0).
454submit_le_b([X^1],CLP,K) :-
455 var(X),
456 !,
457 ( compare_d(CLP, >, K, 0)
458 -> ineq_one_n_p_0(CLP, X) 459 ; ineq_one_n_n_0(CLP, X) 460 ).
462submit_le_b(P,CLP,K) :-
463 term_variables(P,Vs),
464 geler(CLP,Vs,resubmit_le(CLP, [v(K,P)])).
465
469
471submit_le_c([],CLP,A,B) :-
472 A = v(I,[]),
473 B = v(K,[Y^1]),
474 var(Y),
475 !,
476 ineq_one(nonstrict, CLP, Y, K, I).
478submit_le_c(Rest,CLP,A,B) :-
479 Norm = [A,B|Rest],
480 ( linear(Norm)
481 -> 'solve_=<'(CLP, Norm)
482 ; term_variables(Norm,Vs),
483 geler(CLP,Vs,resubmit_le(CLP, Norm))
484 ).
485
490
491submit_ne(CLP,Norm1) :-
492 ( nf_constant(Norm1,K)
493 -> compare_d(CLP, \=, 0, K)
494 ; linear(Norm1)
495 -> 'solve_=\\='(CLP,Norm1)
496 ; term_variables(Norm1,Vs),
497 geler(CLP,Vs,resubmit_ne(CLP,Norm1))
498 ).
499
503
504linear([]).
505linear(v(_,Ps)) :- linear_ps(Ps).
506linear([A|As]) :-
507 linear(A),
508 linear(As).
509
514
515linear_ps([]).
516linear_ps([V^1]) :- var(V). 517
522:- meta_predicate wait_linear(?, ?, ?, 0 ). 523
524wait_linear(CLP,Term,Var,Goal) :-
525 nf(Term,CLP,Nf),
526 ( linear(Nf)
527 -> Var = Nf,
528 call(Goal)
529 ; term_variables(Nf,Vars),
530 geler(CLP,Vars,wait_linear_retry(CLP, Nf, Var, Goal))
531 ).
535resubmit_eq(CLP, N) :-
536 repair(CLP, N, Norm),
537 submit_eq(Norm, CLP).
538resubmit_lt(CLP, N) :-
539 repair(CLP, N, Norm),
540 submit_lt(Norm, CLP).
541resubmit_le(CLP, N) :-
542 repair(CLP, N, Norm),
543 submit_le(Norm, CLP).
544resubmit_ne(CLP,N) :-
545 repair(CLP, N, Norm),
546 submit_ne(CLP,Norm).
547
548wait_linear_retry(CLP,Nf0,Var,Goal) :-
549 repair(CLP, Nf0, Nf),
550 ( linear(Nf)
551 -> Var = Nf,
552 call(Goal)
553 ; term_variables(Nf,Vars),
554 geler(CLP,Vars,wait_linear_retry(CLP, Nf, Var, Goal))
555 ).
557
558
563
564:- multifile
565 nl_invertible/2,
566 nl_invert/5. 567
569
576
578nf(X,_,Norm) :-
579 var(X),
580 !,
581 Norm = [v(1,[X^1])].
582nf(X,CLP,Norm) :-
583 nf_number(CLP,X,Norm),
584 !.
589nf(-A,CLP,Norm) :-
590 !,
591 nf(A,CLP,An),
592 nf_mul_factor(v(-1,[]), CLP, An, Norm).
593nf(+A,CLP,Norm) :-
594 !,
595 nf(A,CLP,Norm).
597nf(A+B,CLP,Norm) :-
598 !,
599 nf(A,CLP,An),
600 nf(B,CLP,Bn),
601 nf_add(An, CLP, Bn, Norm).
602nf(A-B,CLP,Norm) :-
603 !,
604 nf(A,CLP,An),
605 nf(-B,CLP,Bn),
606 nf_add(An, CLP, Bn, Norm).
608nf(A*B,CLP,Norm) :-
609 !,
610 nf(A,CLP,An),
611 nf(B,CLP,Bn),
612 nf_mul(CLP, An, Bn, Norm).
613nf(A/B,CLP,Norm) :-
614 !,
615 nf(A,CLP,An),
616 nf(B,CLP,Bn),
617 nf_div(Bn,CLP,An,Norm).
620nf(Term,CLP,Norm) :-
621 nonlin(CLP, Term, AL, Skel, SaL),
622 !,
623 maplist(nf_(CLP), AL, AnL),
624 nf_nonlin(CLP, Skel, AnL, SaL, Norm).
626nf(Term,CLP,_) :-
627 throw(type_error(nf(Term,CLP,_),1,'a numeric expression',Term)).
628
629nf_(CLP, Term, Norm) :- nf(Term, CLP, Norm).
630
634
635nf_number(CLP, N, Res) :-
636 cast_d(CLP, N, Num),
637 ( compare_d(CLP, =, 0, Num)
638 -> Res = []
639 ; Res = [v(Num,[])]
640 ).
641
643
644:- multifile
645 nonlin/5. 646
647nf_nonlin(CLP, Skel, AnL, SL, Norm) :-
648 ( maplist(nf_constant, AnL,SL)
649 -> eval_d(CLP,Skel,Res),
650 nf_number(CLP,Res,Norm)
651 ; Skel=_^_,
652 AnL = [A1n, A2n],
653 nf_constant(A2n,Exp),
654 integerp(CLP, Exp, I)
655 -> nf_power(CLP, I, A1n, Norm)
656 ; SL = AnL,
657 Norm = [v(1,[Skel^1])]
658 ).
659
663
664nf_constant([],Z) :- Z = 0.
665nf_constant([v(K,[])],K).
666
672
673nf_add([], _, Bs, Bs).
674nf_add([A|As], CLP, Bs, Cs) :- nf_add(Bs, CLP, A, As, Cs).
675
676nf_add([], _, A, As, Cs) :- Cs = [A|As].
677nf_add([B|Bs], CLP, A, As, Cs) :-
678 A = v(Ka,Pa),
679 B = v(Kb,Pb),
680 compare(Rel,Pa,Pb),
681 nf_add_case(Rel,CLP,A,As,Cs,B,Bs,Ka,Kb,Pa).
682
689nf_add_case(<,CLP,A,As,Cs,B,Bs,_,_,_) :-
690 Cs = [A|Rest],
691 nf_add(As, CLP, B, Bs, Rest).
692nf_add_case(>,CLP,A,As,Cs,B,Bs,_,_,_) :-
693 Cs = [B|Rest],
694 nf_add(Bs, CLP, A, As, Rest).
695nf_add_case(=,CLP,_,As,Cs,_,Bs,Ka,Kb,Pa) :-
696 eval_d(CLP, Ka + Kb, Kc),
697 ( 698 compare_d(CLP, =, Ka, -Kb)
699 -> nf_add(As, CLP, Bs, Cs)
700 ; Cs = [v(Kc,Pa)|Rest],
701 nf_add(As, CLP, Bs, Rest)
702 ).
703
704nf_mul(CLP, A, B, Res) :-
705 nf_length(A,0,LenA),
706 nf_length(B,0,LenB),
707 nf_mul_log(LenA, CLP, A, [], LenB, B, Res).
708
709nf_mul_log(0, _, As, As, _, _, []) :- !.
710nf_mul_log(1, CLP, [A|As], As, Lb, B, R) :-
711 !,
712 nf_mul_factor_log(Lb, CLP, B, [], A, R).
713nf_mul_log(2, CLP, [A1,A2|As], As, Lb, B, R) :-
714 !,
715 nf_mul_factor_log(Lb, CLP, B, [], A1, A1b),
716 nf_mul_factor_log(Lb, CLP, B, [], A2, A2b),
717 nf_add(A1b, CLP, A2b, R).
718nf_mul_log(N, CLP, A0, A2, Lb, B, R) :-
719 P is N>>1,
720 Q is N-P,
721 nf_mul_log(P, CLP, A0, A1, Lb, B, Rp),
722 nf_mul_log(Q, CLP, A1, A2, Lb, B, Rq),
723 nf_add(Rp, CLP, Rq, R).
724
725
727nf_add_2(CLP, Af, Bf, Res) :- 728 Af = v(Ka,Pa),
729 Bf = v(Kb,Pb),
730 compare(Rel,Pa,Pb),
731 nf_add_2_case(Rel, CLP, Af, Bf, Res, Ka, Kb, Pa).
732
733nf_add_2_case(<, _, Af, Bf, [Af,Bf], _, _, _).
734nf_add_2_case(>, _, Af, Bf, [Bf,Af], _, _, _).
735nf_add_2_case(=, CLP, _, _, Res, Ka, Kb, Pa) :-
736 eval_d(CLP, Ka + Kb, Kc),
737 ( 738 compare_d(CLP, =, Ka, -Kb)
739 -> Res = []
740 ; Res = [v(Kc,Pa)]
741 ).
742
746nf_mul_k([],_,_,[]).
747nf_mul_k([v(I,P)|Vs],CLP,K,[v(Ki,P)|Vks]) :-
748 eval_d(CLP, K*I, Ki),
749 nf_mul_k(Vs,CLP,K,Vks).
750
755nf_mul_factor(v(K,[]), CLP, Sum, Res) :-
756 !,
757 nf_mul_k(Sum,CLP,K,Res).
758nf_mul_factor(F, CLP, Sum, Res) :-
759 nf_length(Sum,0,Len),
760 nf_mul_factor_log(Len, CLP, Sum, [], F, Res).
761
767
768nf_mul_factor_log(0, _, As, As, _, []) :- !.
769nf_mul_factor_log(1, CLP, [A|As], As, F, [R]) :-
770 !,
771 mult(CLP,A,F,R).
772nf_mul_factor_log(2, CLP, [A,B|As], As, F, Res) :-
773 !,
774 mult(CLP,A,F,Af),
775 mult(CLP,B,F,Bf),
776 nf_add_2(CLP, Af, Bf, Res).
777nf_mul_factor_log(N, CLP, A0, A2, F, R) :-
778 P is N>>1, 779 Q is N-P,
780 nf_mul_factor_log(P, CLP, A0, A1, F, Rp),
781 nf_mul_factor_log(Q, CLP, A1, A2, F, Rq),
782 nf_add(Rp, CLP, Rq, R).
783
787
788mult(CLP, v(Ka,La),v(Kb,Lb),v(Kc,Lc)) :-
789 eval_d(CLP, Ka*Kb, Kc),
790 pmerge(La, CLP, Lb, Lc).
791
795
796pmerge([],_,Bs,Bs).
797pmerge([A|As],CLP,Bs,Cs) :- pmerge(Bs,CLP,A,As,Cs).
798
799pmerge([],_,A,As,Res) :- Res = [A|As].
800pmerge([B|Bs],CLP,A,As,Res) :-
801 A = Xa^Ka,
802 B = Xb^Kb,
803 compare(R,Xa,Xb),
804 pmerge_case(R,CLP,A,As,Res,B,Bs,Ka,Kb,Xa).
805
812
813pmerge_case(<,CLP,A,As,Res,B,Bs,_,_,_) :-
814 Res = [A|Tail],
815 pmerge(As,CLP,B,Bs,Tail).
816pmerge_case(>,CLP,A,As,Res,B,Bs,_,_,_) :-
817 Res = [B|Tail],
818 pmerge(Bs,CLP,A,As,Tail).
819pmerge_case(=,CLP,_,As,Res,_,Bs,Ka,Kb,Xa) :-
820 eval_d(CLP, Ka + Kb, Kc),
821 ( compare_d(CLP, =, 0, Kc)
822 -> pmerge(As,CLP,Bs,Res)
823 ; Res = [Xa^Kc|Tail],
824 pmerge(As,CLP,Bs,Tail)
825 ).
826
830
832nf_div([],_,_,_) :-
833 !,
834 zero_division.
836nf_div([v(K,P)],CLP,Sum,Res) :-
837 !,
838 div_d(CLP, 1, K, Ki),
839 mult_exp(P,-1,Pi),
840 nf_mul_factor(v(Ki,Pi), CLP, Sum, Res).
841nf_div(D,_,A,[v(1,[(A/D)^1])]).
842
846zero_division :- fail. 847
852mult_exp([],_,[]).
853mult_exp([X^P|Xs],K,[X^I|Tail]) :-
854 I is K*P,
855 mult_exp(Xs,K,Tail).
862nf_power(CLP, N, Sum, Norm) :-
863 compare(Rel,N,0),
864 ( Rel = (<)
865 -> Pn is -N,
866 867 binom(Sum, CLP, Pn, Inorm),
868 nf_div(Inorm,CLP,[v(1,[])],Norm)
869 ; Rel = (>)
870 -> 871 binom(Sum, CLP, N, Norm)
872 ; Rel = (=)
873 -> 874 Norm = [v(1,[])]
875 ).
876
881binom(Sum, _, 1, Power) :-
882 !,
883 Power = Sum.
884binom([], _, _, []).
885binom([A|Bs], CLP, N, Power) :-
886 ( Bs = []
887 -> nf_power_factor(CLP, A,N,Ap),
888 Power = [Ap]
889 ; Bs = [_|_]
890 -> factor_powers(N,CLP,A,v(1,[]),Pas),
891 sum_powers(N, CLP, Bs, [v(1,[])], Pbs, []),
892 combine_powers(Pas,CLP,Pbs,0,N,1,[],Power)
893 ).
894
895combine_powers([],_,[],_,_,_,Pi,Pi).
896combine_powers([A|As],CLP,[B|Bs],L,R,C,Pi,Po) :-
897 nf_mul(CLP, A, B, Ab),
898 nf_mul_k(Ab, CLP, C, Abc),
899 nf_add(Abc, CLP, Pi, Pii),
900 L1 is L+1,
901 R1 is R-1,
902 C1 is C*R//L1,
903 combine_powers(As,CLP,Bs,L1,R1,C1,Pii,Po).
904
905nf_power_factor(CLP, v(K,P),N,v(Kn,Pn)) :-
906 eval_d(CLP, K**N, Kn),
907 mult_exp(P,N,Pn).
908
909factor_powers(0,_,_,Prev,[[Prev]]) :- !.
910factor_powers(N,CLP,F,Prev,[[Prev]|Ps]) :-
911 N1 is N-1,
912 mult(CLP,Prev,F,Next),
913 factor_powers(N1,CLP,F,Next,Ps).
914sum_powers(0, _, _, Prev, [Prev|Lt], Lt) :- !.
915sum_powers(N, CLP, S, Prev, L0, Lt) :-
916 N1 is N-1,
917 nf_mul(CLP, S, Prev, Next),
918 sum_powers(N1, CLP, S, Next, L0, [Prev|Lt]).
919
921repair(CLP, Sum, Norm) :-
922 nf_length(Sum,0,Len),
923 repair_log(Len, CLP, Sum, [], Norm).
924repair_log(0, _, As, As, []) :- !.
925repair_log(1, CLP, [v(Ka,Pa)|As], As, R) :-
926 !,
927 repair_term(CLP, Ka, Pa, R).
928repair_log(2, CLP, [v(Ka,Pa),v(Kb,Pb)|As], As, R) :-
929 !,
930 repair_term(CLP, Ka, Pa, Ar),
931 repair_term(CLP, Kb, Pb, Br),
932 nf_add(Ar, CLP, Br, R).
933repair_log(N, CLP, A0, A2, R) :-
934 P is N>>1,
935 Q is N-P,
936 repair_log(P, CLP, A0, A1, Rp),
937 repair_log(Q, CLP, A1, A2, Rq),
938 nf_add(Rp, CLP, Rq, R).
939
940repair_term(CLP, K, P, Norm) :-
941 length(P,Len),
942 repair_p_log(Len,CLP,P,[],Pr,[v(1,[])],Sum),
943 nf_mul_factor(v(K,Pr), CLP, Sum, Norm).
944
945repair_p_log(0,_,Ps,Ps,[],L0,L0) :- !.
946repair_p_log(1,CLP,[X^P|Ps],Ps,R,L0,L1) :-
947 !,
948 repair_p(X,CLP,P,R,L0,L1).
949repair_p_log(2,CLP,[X^Px,Y^Py|Ps],Ps,R,L0,L2) :-
950 !,
951 repair_p(X,CLP,Px,Rx,L0,L1),
952 repair_p(Y,CLP,Py,Ry,L1,L2),
953 pmerge(Rx,CLP,Ry,R).
954repair_p_log(N,CLP,P0,P2,R,L0,L2) :-
955 P is N>>1,
956 Q is N-P,
957 repair_p_log(P,CLP,P0,P1,Rp,L0,L1),
958 repair_p_log(Q,CLP,P1,P2,Rq,L1,L2),
959 pmerge(Rp,CLP,Rq,R).
960
961repair_p(Term,_,P,[Term^P],L0,L0) :- var(Term), !.
962repair_p(Term,CLP,P,[],L0,L1) :-
963 nonvar(Term),
964 repair_p_one(Term, CLP, TermN),
965 integerp(CLP, P, I),
966 nf_power(CLP, I, TermN, TermNP),
967 nf_mul(CLP, TermNP, L0, L1).
973repair_p_one(Term, CLP, TermN) :-
974 nf_number(CLP,Term,TermN), 975 !.
976repair_p_one(A1/A2, CLP, TermN) :-
977 repair(CLP, A1, A1n),
978 repair(CLP, A2, A2n),
979 !,
980 nf_div(A2n,CLP,A1n,TermN).
981repair_p_one(Term, CLP, TermN) :-
982 nonlin(CLP, Term, AL, Skel, SaL),
983 maplist(repair(CLP), AL, AnL),
984 !,
985 nf_nonlin(CLP, Skel, AnL, SaL, TermN).
986repair_p_one(Term, CLP, TermN) :-
987 nf(Term, CLP, TermN).
988
989nf_length([],Li,Li).
990nf_length([_|R],Li,Lo) :-
991 Lii is Li+1,
992 nf_length(R,Lii,Lo).
997
999nf2term([],_,0).
1001nf2term([F|Fs],CLP,T) :-
1002 f02t(F,CLP,T0), 1003 yfx(Fs,CLP,T0,T). 1004
1005yfx([],_,T0,T0).
1006yfx([F|Fs],CLP,T0,TN) :-
1007 fn2t(F,CLP,Ft,Op),
1008 T1 =.. [Op,T0,Ft],
1009 yfx(Fs,CLP,T1,TN).
1010
1015f02t(v(K,P),CLP,T) :-
1016 ( 1017 P = []
1018 -> T = K
1019 ; compare_d(CLP, =, K, 1) 1020 -> p2term(P,CLP,T)
1021 ; compare_d(CLP, =, K, -1) 1022 -> T = -Pt,
1023 p2term(P,CLP,Pt)
1024 ; T = K*Pt,
1025 p2term(P,CLP,Pt)
1026 ).
1027
1032fn2t(v(K,P),CLP,Term,Op) :-
1033 ( compare_d(CLP, =, K, 1) 1034 -> Term = Pt,
1035 Op = +
1036 ; compare_d(CLP, =, K, -1) 1037 -> Term = Pt,
1038 Op = -
1039 ; compare_d(CLP, <, K, 0 ) 1040 -> eval_d(CLP, -K, Kf),
1041 Term = Kf*Pt,
1042 Op = -
1043 ; 1044 Term = K*Pt,
1045 Op = +
1046 ),
1047 p2term(P,CLP,Pt).
1048
1050p2term([X^P|Xs],CLP,Term) :-
1051 ( Xs = []
1052 -> pe2term(CLP,X,Xt),
1053 exp2term(P,Xt,Term)
1054 ; Xs = [_|_]
1055 -> Term = Xst*Xtp,
1056 pe2term(CLP,X,Xt),
1057 exp2term(P,Xt,Xtp),
1058 p2term(Xs,CLP,Xst)
1059 ).
1060
1062exp2term(1,X,X) :- !.
1063exp2term(-1,X,1/X) :- !.
1064exp2term(P,X,Term) :-
1065 1066 Term = X^P.
1067
1068pe2term(_,X,Term) :-
1069 var(X),
1070 Term = X.
1071pe2term(CLP,X,Term) :-
1072 nonvar(X),
1073 X =.. [F|Args],
1074 pe2term_args(Args,CLP,Argst),
1075 Term =.. [F|Argst].
1076
1077pe2term_args([],_,[]).
1078pe2term_args([A|As],CLP,[T|Ts]) :-
1079 nf2term(A,CLP,T),
1080 pe2term_args(As,CLP,Ts).
1081
1088
1089:- public
1090 transg/3. 1091
1092transg(resubmit_eq(CLP, Nf)) -->
1093 {
1094 nf2term([],CLP,Z),
1095 nf2term(Nf,CLP,Term)
1096 },
1097 [CLP:{Term=Z}].
1098transg(resubmit_lt(CLP, Nf)) -->
1099 {
1100 nf2term([],CLP,Z),
1101 nf2term(Nf,CLP,Term)
1102 },
1103 [CLP:{Term<Z}].
1104transg(resubmit_le(CLP, Nf)) -->
1105 {
1106 nf2term([],CLP,Z),
1107 nf2term(Nf,CLP,Term)
1108 },
1109 [CLP:{Term=<Z}].
1110transg(resubmit_ne(CLP, Nf)) -->
1111 {
1112 nf2term([],CLP,Z),
1113 nf2term(Nf,CLP,Term)
1114 },
1115 [CLP:{Term=\=Z}].
1116transg(wait_linear_retry(CLP,Nf,Res,Goal)) -->
1117 {
1118 nf2term(Nf,CLP,Term)
1119 },
1120 [CLP:{Term=Res}, Goal]