/* File: solve Purpose: Inequality reasoning Author: Martin Reinders & Bert Bredeweg & Floris Linnebank Date: August 1989 Part-of: GARP (version 2.0) Modified: 30 July 2004 Copyright (c) 2004, University of Amsterdam. All rights reserved. */ % FL nov 07: inequality reasoning redo: % % - canonical form also for = relations, this means there is only one possible way to write % a relation internally -> faster checking possible % % - division of base in relevant contexts with derivable relations attached: % base: % [context([Relations...], [Derivable], ContextPointer), context(_, _), ..., ...] % this way solve can work on interdependent sets of relations not combining relations without % a chance of success % % derivable works like before, for old calls: % - [AllDerivable..., ...] % % - unified analyse simple and analyse zero relations % less code, less work. % % Idea: immediate removal of weaker relations in solvecore: (not done yet) % therefore always only single relation about 2 variables present. % would allow for faster retrieval (memberchk vs member) of relations about same variables % could be expensive though and it does not save the remove_weaker work done later because % solve_core does not return the new derivable set (but it could in theory) % % IDEA: caching of contexts: simply retrieve derivable, given a set of relations. % Does not work (yet), it would need a translation into a generic form to have enough matches. % This translation is probably too expensive especially since many models % have quite low core inequality reasoning costs (<10%) % %%%%%%%%%%%%% append_relation: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Add a relation to the mathematical model: % fail if contradictory, % succeed with empty assumptions if it is a derivable or known relation, % succeed with assumptions if there are new relations (unknown / underivable) % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % other calls do not yet use the extra 2 arguments with AddersInOut so this extra clause % is added to catch old style calls. % CAN BE REMOVED IF OLD CALLS ARE UPDATED... (ABOUT 10 CHANGES) append_relation(R, Cin, Cout, Ap, As):- append_relation(R, Cin, Cout, Ap, As, [],[]). % fail if relation is invalid (i.e. a > a, or a+b > a+b) % FL june 07: new position of this check: before simplification append_relation(Intern, Cin, _, _, _, _, _):- illegal_relation(Intern), ( etrace(solve_derived_invalid, _, inequality) -> % only do the rest of the work if tracer is on... cio_q(Cin, Q), etrace(solve_invalid_input, [Intern, Q], inequality) ; true ), !, fail. % this extra call allows append_relation_all to hook in at exactly the % right point append_relation(R, Cin, Cout, Ap, As, Addersin, Addersout):- append_relation1(R, Cin, Cout, Ap, As, Addersin, Addersout, [], []). % FL december 2004: Solve does simplification of results: % x + y = x + z -> y = z, % but not simplification of the input... This is done here, before % the actual appendrelation2 call. % Last two arguments are Adders passed on for bit change updates. % (see: analyse zero equality) append_relation1(R, Cin, Cout, Ap, As, Addersin, Addersout, MoreRel, NewMore):- simplify_relations([R], [R1]), determine_pointers(R1, RP), cio_r(Cin, Relations), relevant_contexts(RP, Relations, Contexts, OtherContexts), !, append_relation2(R1, RP, Contexts, OtherContexts, Cin, Cout, Ap, As, Addersin, Addersout, MoreRel, NewMore). % append_relation2(+Relation, +InvolvedPointers, +Cin, -Cout, -AppendedRels, +AnalyseSimpleTrueFail, +AddersIn, -AddersOut) % % 4 options: % - relation is new context but evident -> return true % - relation is new context -> return new context % - relation is already derivable -> return true % - relation fits in single context -> solve single context % - relation connects multiple contexts -> solve combined context % % fails if inconsistent (solve_core will do this) % empty relevant contexts...>> but relation is evident -> return true append_relation2(AppendOne, _RP, [], _, Cio, Cio, [], _, Adders, Adders, MR, MR):- check_context_derivable(AppendOne, []), !. % empty relevant contexts...>> relation is new context -> return new context (actually solve new empty context) append_relation2(AppendOne, RP, [], OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR):- !, append_relation_core(AppendOne, RP, context([], [], RP), OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR). % - relation is already derivable -> return true append_relation2(AppendOne, _RP, Relevant, _, Cio, Cio, [], _, Adders, Adders, MR, MR):- check_context_derivable(AppendOne, Relevant), !. % - relation fits or extends single context -> solve single context append_relation2(AppendOne, RP, [context(R, D, CP)], OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR):- !, map_union(RP, CP, NewCP), % by definition not unique append_relation_core(AppendOne, RP, context(R, D, NewCP), OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR). % - relation connects multiple contexts -> solve combined context append_relation2(AppendOne, RP, Contexts, OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR):- combine_contexts(Contexts, CombiContext), !, append_relation_core(AppendOne, RP, CombiContext, OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR). % solve single context append_relation_core(AppendOne, _RP, context(Relations, Derivable, CP), OtherContexts, Cin, Cout, [AppendOne], DoAS, Adders, NAdders, MR, NMR):- !, cio_r_nr_d_nd_q_nq_c_nc(Cin, Cnew, _, NewContexts, AllDerivable, NewAllDerivable, Q, NQ, C, NC), append([AppendOne], Derivable, Known), % all relations we don't want to derive again solve_core([[]/AppendOne], Relations, Relations, Known, FreshDerived, Q), % fails is inconsistent %reconstruct: relations and derivable, construct allnew: apply_cannonical_form(FreshDerived, NewDerived), append(Known, NewDerived, NewDerivable1), append([AppendOne], NewDerived, AllNew1), append([AppendOne], Relations, NewRelations1), % remove a>=b if a>b is found: remove_weaker2(AllNew1, AllNew1, AllNew2), remove_weaker(AllNew2, NewRelations1, NewRelations2), remove_weaker(AllNew2, NewDerivable1, NewDerivable2), %reconstruct allderivable by adding allnew: append(AllNew2, AllDerivable, NewAllDerivable1), remove_weaker(AllNew2, NewAllDerivable1, NewAllDerivable2), % replace a with b if a=b flag(analyse_simple_found_contradiction, _, false), analyse_binairy_equality(DoAS, CP, NCP, AllNew2, Q, NQ, AllNew2, AllNew3, NewRelations2, NewRelations3, NewDerivable2, NewDerivable3, NewAllDerivable2, NewAllDerivable3, MR, NMR, C, NC, Adders, Adders1), sort(AllNew3, AllNew4), sort(NewRelations3, NewRelations), sort(NewDerivable3, NewDerivable), sort(NewAllDerivable3, NewAllDerivable), ( NewRelations \= [] -> NewContexts = [context(NewRelations, NewDerivable, NCP)|OtherContexts] ; NewContexts = OtherContexts % analyse binairy has removed complete context... ), ( C \= NC % if Correspondences have changed, they should be checked with the 0 = 0 relation, to fire any correspondences with the 0 = 0 relation now as a condition after the pointer updates. -> list_map([0], Z), AllNew = [relation(Z, = , Z)|AllNew4] ; AllNew4 = AllNew ), !, inspect_correspondence(AllNew, Cnew, Cout, DoAS, Adders1, NAdders). %%%%%%%%%%%%%%% append_relation_all: %%%%%%%%%%%%%%%%%%%%%%%%%%% % % implements append_relation for a set of relations % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % other calls do not yet use these arguments so this extra clause % is added to catch old style calls. % CAN BE REMOVED IF OLD CALLS ARE UPDATED... (ABOUT 10 CHANGES) append_relation_all(Append, Cin, Cout, AppendNotDerivable, DoAnalyseSimple):- append_relation_all(Append, Cin, Cout, AppendNotDerivable, DoAnalyseSimple, [], []). % fail if invalid input % FL june 07 new position of this check: before simplification append_relation_all(InternL, Cin, _, _, _, _, _):- member(Intern, InternL), illegal_relation(Intern), ( etrace(solve_derived_invalid, _, inequality) -> % only do the rest of the work if tracer is on... cio_q(Cin, Q), etrace(solve_invalid_input, [Intern, Q], inequality) ; true ), !, fail. % use predicates of single append relation to do all % append_relation_all([], Cio, Cio, [], _DoAnalyseSimple, Add, Add). append_relation_all([H|T], Cin, Cout, AppendNotDerivable, DoAnalyseSimple, Adin, Adout):- append_relation1(H, Cin, Cio, AppendNotDerivable1, DoAnalyseSimple, Adin, Add, T, NT), %pass on Tail for pointer updates !, append_relation_all(NT, Cio, Cout, AppendNotDerivable2, DoAnalyseSimple, Add, Adout), append(AppendNotDerivable1, AppendNotDerivable2, AppendNotDerivable). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % helper preds append relation % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % determine bitvector for a relation % determine_pointers(relation(R, _, L), BitVector):- map_union(R, L, All), % combine NotZero is \1, % remove zero pointer map_intersection(All, bitvector(NotZero), BitVector). % check_context_derivable(Relation, SetOfContexts % succeeds when first context with relation or implied relation is found % NB fails on empty list!!! % evident relation check_context_derivable(Rel, _):- evident(Rel), !. % success check_context_derivable(Rel, [context(_R, D, _CP)|_]):- is_context_derivable(Rel, D), !. %try next context check_context_derivable(Rel, [_|T]):- check_context_derivable(Rel, T). %NB fails on empty list!!! % is_context_derivable(Relation, Derivable) % NB evidence checking allready done!!!! % inverse for equality relation not necessary anymore: canonical form used is_context_derivable(relation(Left, Relation, Right), Derivable):- memberchk(relation(Left, Relation1, Right), Derivable), % only one relation can be present for each Left/Right pair ( Relation = Relation1 ; implies_relation(Relation1, Relation) ), !. % extra clause for the case that: % = relation implies >= relation, and left and right are switched. is_context_derivable(relation(Left, >=, Right), Derivable):- sort([Left, Right], [NLeft, NRight]), % cannonical form for = relations Left = NRight, % they were indeed switched! If not then previous clause should have succeeded allready. Right = NLeft, % (saves unnecessary memberchecks) memberchk(relation(NLeft, =, NRight), Derivable), !. % is_derivable/2 % % 1 + Relation, intern representation (<, =< reversed to >, >=) % 2 + Relations, known to be derivable (idem) % % is 1 a member of 2? (or directly implied by 2?, e.g. a > b -> a >= b is_derivable(Relation, _):- evident(Relation), !. is_derivable(Relation, Derivable):- is_context_derivable(Relation, Derivable). % during solve_core the set of derivable may become weak: more then one % relation known per variable pair. % therefore an extensive is_derivable check is needed. is_derivable_weakset(Relation, _):- evident(Relation), !. is_derivable_weakset(relation(Left, Relation, Right), Derivable):- memberchk(relation(Left, Relation, Right), Derivable), % direct hit !. %special clauses for >= is_derivable_weakset(relation(Left, >=, Right), Derivable):- memberchk(relation(Left, >, Right), Derivable), !. is_derivable_weakset(relation(Left, >=, Right), Derivable):- sort([Left, Right], [NLeft, NRight]), % cannonical form for = relations memberchk(relation(NLeft, =, NRight), Derivable), !. % check_derivable: % is a list of relations (intern representation) completely derivable? check_derivable([], _). check_derivable([H|T], D):- is_derivable(H, D), !, check_derivable(T, D). % tautologies evident(relation(X, =, X)). evident(relation(X, >=, X)). % implies_relation(+op1, -op2) % a op1 b -> a op2 b implies_relation(>, >=). implies_relation(=, >=). % relevant_contexts(+RelPointers, +RelationContexts, -RelevantContexts) % returns all contexts with a pointer overlap relevant_contexts(_RP, [], [], []). % relevant_context relevant_contexts(RP, [context(R, D, CP)|RT], [context(R, D, CP)|CT], OT):- map_intersection(RP, CP, bitvector(Common)), Common \== 0, % FL nov 07 used to be =\= but arithmetic is not necessary here (and slower!) !, relevant_contexts(RP, RT, CT, OT). % other context relevant_contexts(RP, [H|RT], CT, [H|OT]):- relevant_contexts(RP, RT, CT, OT). % combine multiple contexts into one. % (should always be list of 2 or more) % combine_contexts([context(Relations, Derivable, CP)|Tail], New):- combine_contexts2(Tail, Relations, Derivable, CP, New). combine_contexts2([], Relations, Derivable, CP, context(Relations, Derivable, CP)). combine_contexts2([context(Relations1, Derivable1, CP1)|T], Relations2, Derivable2, CP2, New):- append(Relations1, Relations2, Relations3), append(Derivable1, Derivable2, Derivable3), (map_union_unique(CP1, CP2, CP3); etrace(error_combine_connected_context, nil, nil)), % unique is extra check... CP's should never have an intersection allready !, combine_contexts2(T, Relations3, Derivable3, CP3, New). % remove_weaker(+Newrelations, +KnownRelations, -KnownStronger) % Arg1 is a list of new (derived) relations % Arg2 is a list of known (derived) relations % remove from Arg2 each relation a >= b if Arg1 contains a > b/ a = b remove_weaker([], Rs, Rs). remove_weaker([relation(L, >, R)| Tail], Rs, NRs):- memberchk(relation(L, >=, R), Rs), % memberchk is logically superfluous, % but, while written in C, the test is faster common_select(Rs, relation(L, >=, R), TRs), !, %remove_weaker([relation(L, >, R)|Tail], TRs, NRs). %why check again for this relation!? only one weaker should be present remove_weaker(Tail, TRs, NRs). remove_weaker([relation(L, =, R)|Tail], Rs, NRs):- memberchk(relation(L, >=, R), Rs), common_select(Rs, relation(L, >=, R), TRs), !, %remove_weaker([relation(L, =, R)|Tail], TRs, NRs). %why check again for this relation!? only one weaker should be present remove_weaker(Tail, TRs, NRs). remove_weaker([ relation(R, =, L) | Tail], Rs, NRs):- memberchk(relation(L, >=, R), Rs), common_select(Rs, relation(L, >=, R), TRs), !, %remove_weaker([relation(L, =, R)|Tail], TRs, NRs). %why check again for this relation!? only one weaker should be present remove_weaker(Tail, TRs, NRs). remove_weaker([_|Tail], Rs, NRs):- remove_weaker(Tail, Rs, NRs). % a secondversion, aims to do this quicker for 2 identical lists... % the idea is: take weak relation, search for strong. % % remove from Arg2 each relation a >= b if Arg2 contains a > b/ a = b remove_weaker2(List, Strong, Strongest):- memberchk(relation(L, >=, R), List), % weak relation present. ( memberchk(relation(L, >, R), Strong) ; canonical_form(relation(L, =, R), Rel), memberchk(Rel, Strong) ), %and strong present !, member_and_tail(relation(L, >=, R), List, Rest), %select rest from the inputlist select(relation(L, >=, R), Strong, Stronger), % remove weak relation from stronglist %continue with rest, remove_weaker2(Rest, Stronger, Strongest). % done remove_weaker2(_, Strongest, Strongest). % simplification should not be necessary and makes trace less insightfull illegal_relation(relation(Left, Relation, Right)):- invalid_relation(relation(Left, Relation, Right)), !. invalid_relation(relation(M, >, M)). % simplify_relation(+Left, +Right, -NLeft, -NRight) % If two sides of an (in)equality relation in intern representation contain the same quantities, % then these can be taken out: % a + b = a + c -> b = c % Sometimes leaving zero on one side: % a + b = b -> a = 0 % simplify list of relations simplify_relations([], []). simplify_relations([relation(Left, Rel, Right)|Tail], [relation(NLeft, Rel, NRight)|NewTail]):- simplify_relation(Left, Right, Left1, Right1), canonical_form(Left1, Right1, Rel, NLeft, NRight), !, simplify_relations(Tail, NewTail). % simplify one relation simplify_relation(Left, Right, NLeft, NRight):- map_without_intersection(Left, Right, NLeft1, NRight1), %new FL may 07: intercept [] pointer for zero, replace with: [0] zero_pointer(relation(NLeft1, dummy, NRight1), relation(NLeft, dummy, NRight)), !. simplify_relation(Left, Right, Left, Right). %%%%%%%%%%%%%%%%%%%%%%Inequality Reasoning / Solve : Core %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % The core solve process works by combining new relations with: % 1) derivable relations with the same variables % 2) base relations % 3) new derived relations % This is still much less then simply combining with all derivable % relations. % % Since new relations are added to the derivable set there may be more % then one relation about each pair of variables. e.g.: % A>B is known/derivable, A=B is added. % --> both are in the derivable set, % later they will be combined (to form the contradiction in this case) % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% solve_core(NR, TO, K, D, New, Q):- @tracer->>trace_on(inequality), !, flag(max_depth, MaxDepth, MaxDepth), flag(solve_extra_combinations, SEC, SEC), solve_trace(NR, TO, K, D, New1, Q, MaxDepth, SEC), add_empty_parents(New1, New1P), % Some relations can only be derived by combining derivable relations... (3) append(New1, D, ND), solve_trace(New1P, New1, New1, ND, New2, Q, MaxDepth, SEC), % so these are found here. append(New1, New2, New). solve_core(NR, TO, K, D, New, _):- flag(max_depth, MaxDepth, MaxDepth), flag(solve_extra_combinations, SEC, SEC), solve_normal(NR, TO, K, D, New1, MaxDepth, SEC), add_empty_parents(New1, New1P),% Some relations can only be derived by combining derivable relations... append(New1, D, ND), solve_normal(New1P, New1, New1, ND, New2, MaxDepth, SEC), % so these are found here. append(New1, New2, New). % done, return result solve_normal([], _, _, _, [], _, _):- !. % combine relation with derivable relation on same variables (1) % % only done if switch is on, because it can take up to 50% extra time... % solve_normal([Parents/Relation1|TailNew], KnownRelations, Known, Derivable, New, MaxDepth, true):- limit_parents(Parents, MaxDepth), get_derivable_same_var(Relation1, Derivable, Relation2), \+ Relation2 = Relation1, add_relation(Relation1, Relation2, Relation3a), % transivity zero_pointer(Relation3a, Relation3), % FL NEW: is x = [] is derived; replace: [] with [0] \+ Relation3 = Relation1, % not same as input \+ is_derivable_weakset(Relation3, Derivable), % not derivable \+ evident(Relation3), % not evident !, \+ invalid_relation(Relation3), % fail if contradiction return_simple_only(Relation3, NNew, New), !, solve_normal([Parents/Relation1, [Relation1, Relation2|Parents]/ Relation3 | TailNew], KnownRelations, Known, [Relation3|Derivable], NNew, MaxDepth, true). % combine with base relation (2) % add relation, succeeds if result is consistent, % has no term twice and can be simplified % if inconsistent: fail solve % if no simplification, or already derivable, or evident: next clause solve_normal([Parents/Relation1|TailNew], KnownRelations, Known, Derivable, New, MaxDepth, SEC):- limit_parents(Parents, MaxDepth), member_and_tail(Relation2, KnownRelations, TailKnown), add_relation(Relation1, Relation2, Relation3a), % transivity zero_pointer(Relation3a, Relation3), % FL NEW: is x = [] is derived; replace: [] with [0] \+ memberchk(Relation2, Parents), % not circular \+ is_derivable_weakset(Relation3, Derivable), % not derivable \+ evident(Relation3), % not evident !, \+ invalid_relation(Relation3), % fail if contradiction return_simple_only(Relation3, NNew, New), !, solve_normal([Parents/Relation1, [Relation1, Relation2|Parents]/ Relation3 | TailNew], TailKnown, Known, [Relation3|Derivable], NNew, MaxDepth, SEC). % tried all for first relation, try tail solve_normal([_|TailNew], _, Known, Derivable, New, MaxDepth, SEC):- !, solve_normal(TailNew, Known, Known, Derivable, New, MaxDepth, SEC). % ------------------- same when tracing inequality reasoning ---------- % done, return result solve_trace([], _, _, _, [], _, _MaxDepth, _):- !. % combine relation with derivable relation on same variables % % only done if switch is on, because it can take up to 50% extra time... % solve_trace([Parents/Relation1|TailNew], KnownRelations, Known, Derivable, New, Q, MaxDepth, true):- flag(equal_intervals, Flag, Flag), % seems to eat resources combined with this option, fix needed in future Flag = fail, limit_parents(Parents, MaxDepth), get_derivable_same_var(Relation1, Derivable, Relation2), \+ Relation2 = Relation1, add_relation(Relation1, Relation2, Relation3a), % transivity zero_pointer(Relation3a, Relation3), % FL NEW: is x = [] is derived; replace: [] with [0] \+ memberchk(Relation2, Parents), % not circular \+ is_derivable_weakset(Relation3, Derivable), % not derivable \+ evident(Relation3), % not evident !, (invalid_relation(Relation3) -> % fail if contradiction etrace(solve_derived_invalid, _, inequality), @tracer->>tell(inequality), show_antecedents(Parents, Relation1, Relation2, Relation3, 'contradiction.', Q), @tracer->>told, fail ; true ), return_simple_only(Relation3, NNew, New), !, (simple_relation(Relation3) -> etrace(solve_found_valid, _, inequality), @tracer->>tell(inequality), show_antecedents(Parents, Relation1, Relation2, Relation3, 'derived.', Q), @tracer->>told ; true ), append(Parents, [Relation1, Relation2], NewParents), solve_trace([Parents/Relation1, NewParents/ Relation3 | TailNew], KnownRelations, Known, [Relation3|Derivable], NNew, Q, MaxDepth, true). % add relation, succeeds if result is consistent, % has no term twice and can be simplified % if inconsistent: fail solve % if no simplification, or already derivable, or evident: next clause solve_trace([Parents/Relation1|TailNew], KnownRelations, Known, Derivable, New, Q, MaxDepth, SEC):- limit_parents(Parents, MaxDepth), member_and_tail(Relation2, KnownRelations, TailKnown), add_relation(Relation1, Relation2, Relation3a), % transivity zero_pointer(Relation3a, Relation3), % FL NEW: if x = [] is derived; replace: [] with [0] \+ memberchk(Relation2, Parents), % not circular \+ is_derivable_weakset(Relation3, Derivable), % not derivable \+ evident(Relation3), % not evident !, (invalid_relation(Relation3) -> % fail if contradiction etrace(solve_derived_invalid, _, inequality), @tracer->>tell(inequality), show_antecedents(Parents, Relation1, Relation2, Relation3, 'contradiction.', Q), @tracer->>told, fail ; true ), return_simple_only(Relation3, NNew, New), !, (simple_relation(Relation3) -> etrace(solve_found_valid, _, inequality), @tracer->>tell(inequality), show_antecedents(Parents, Relation1, Relation2, Relation3, 'derived.', Q), @tracer->>told ; true ), append(Parents, [Relation1, Relation2], NewParents), solve_trace([Parents/Relation1, NewParents/ Relation3 | TailNew], TailKnown, Known, [Relation3|Derivable], NNew, Q, MaxDepth, SEC). % tried all for first relation, try tail solve_trace([_|TailNew], _, Known, Derivable, New, Q, MaxDepth, SEC):- !, solve_trace(TailNew, Known, Known, Derivable, New, Q, MaxDepth, SEC). % a lot of speed can be gained in some cases % if the number of parents is constrained. (FL June 07) % % if many calculus relations exist in the model, % then many new but uninformative calculus relations can be derived. % % after X steps the full partial ordering is probably allready traversed % so the rest of the derivations is only about uninformative new combinations % of quantities. % uninitialised maxdepth flag -> 0 limit_parents(_Parents, 0):- !. % fails if number of parents is over limit limit_parents(Parents, MaxDepth):- length(Parents, Depth), Depth < MaxDepth, !. % member_and_tail % return member and everything behind it member_and_tail(H, [H|T], T). member_and_tail(H, [_|T], NT):- member_and_tail(H, T, NT). % return only parameter > landmark, parameter > parameter, etc. return_simple_only(Relation, New, [Relation|New]) :- simple_relation(Relation), !. return_simple_only(_, New, New). simple_relation(relation(L, _, R)):- map_count(L, C1), C1 < 2, map_count(R, C2), C2 < 2. add_empty_parents([], []). add_empty_parents([H|T], [[]/H|NT]):- add_empty_parents(T, NT). get_derivable_same_var(relation(L, _Relin, R), Derivable, relation(L, Rel, R)):- memberchk(relation(L, _Rel, R), Derivable), % at least one %traced, tiny bit faster with this pre check member(relation(L, Rel, R), Derivable). get_derivable_same_var(relation(L, _Relin, R), Derivable, relation(R, Rel, L)):- memberchk(relation(R, _Rel, L), Derivable), % at least one member(relation(R, Rel, L), Derivable). /* * add_relation(+R1, +R2, -R3) * add relation between two sums, represented as bitmaps * * succeeds only if both left sides or right sides don't have a common term * and the result can be simplified * * This scheme implements transitivity and reasoning about sums * * some examples: * * a > b /\ b > c -> a > c * a + b > c /\ a = d -> d + b > c * (this result is not returned, but may lead to another result) * d = 0 /\ d + b > c -> b > c * * note a lot of relations can be derived in many ways * * to prevent some superfluous derivations, if a quantity is equal to * another quantity, it is replaced with that quantity (if possible) * see append_relations(_all) / analyse_simple_equality * */ % Patch 3-3-2004 by FL: this case wasn't captured, because it cannot be % derived using transitivity. This technique of combining weaker relations % to stronger ones is mentioned in simmons '89, add_relation(relation(X, >=, Y), relation(Y, >=, X), relation(X, =, Y)):- !. % transitivity: add_relation(relation(Le1, Rel1, Ri1), relation(Le2, Rel2, Ri2), relation(Le3, Rel3, Ri3)):- add_compatible(Rel1, Rel2, Rel3), map_union_unique(Le1, Le2, L), % union left sides (no term twice) map_union_unique(Ri1, Ri2, R), map_without_intersection(L, R, Le3, Ri3), % simplify !. % if first clause failed, and one relation is '=', then reverse one relation add_relation(relation(Le1, Rel1, Ri1), relation(Ri2, =, Le2), relation(Le3, Rel3, Ri3)):- !, % do not use clause 3 add_compatible(Rel1, =, Rel3), map_union_unique(Le1, Le2, L), map_union_unique(Ri1, Ri2, R), map_without_intersection(L, R, Le3, Ri3), !. add_relation(relation(Ri1, =, Le1), relation(Le2, Rel2, Ri2), relation(Le3, Rel3, Ri3)):- add_compatible(=, Rel2, Rel3), map_union_unique(Le1, Le2, L), map_union_unique(Ri1, Ri2, R), map_without_intersection(L, R, Le3, Ri3), !. % < =< were inversed add_compatible(=, =, =). add_compatible(=, >, >). add_compatible(=, >=, >=). add_compatible(>, =, >). add_compatible(>, >=, >). add_compatible(>, >, >). add_compatible(>=, =, >=). add_compatible(>=, >=, >=). add_compatible(>=, >, >). inverse(<, >). inverse(=<, >=). inverse(=, =). inverse(>=, =<). inverse(>, <). % substitue [] with zeropointer [0] (FL june 07) % and remove excess zeropointers from additions % if x = [] is derived; replace: [] with [0] if x = [ 0, y ] is % derived; replace: [0, y ] with y % zero_pointer(relation(bitvector(Left), Rel, bitvector(Right)), relation(bitvector(NewLeft), Rel, bitvector(NewRight))):- process_zero_pointer(Left, NewLeft), process_zero_pointer(Right, NewRight). % [] becomes [0] (NB zeropointer: [0] is the integer/bitvector: 1) process_zero_pointer(0, 1):-!. % addition with zero [0, 5, 6] becomes [5, 6] process_zero_pointer(Q, NQ):- Y is Q /\ 1, Y == 1, % there is a zero in the quantity (nb this check first: cheap) X is popcount(Q), X > 1, % there is an addition !, NQ is Q /\ \1, % subtract the zero (AND operation with NOT zero) (could also be simple: - 1) !. % else no change process_zero_pointer(Q, Q). % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % ANALYSE SOLVE RESULTS: ANALYSE BINAIRY EQUALITY % % % analyse results of solve % if simple equality (between two parameters or a parameter and a constant, % (not zero)) % replace quantity pointer of one of these with the other in all relations % % don't analyse when resolving influences/proportional relations % % Two extra arguments: adders in /out these also contain pointers and should also be updated. % This one list should be left structurally intact during the changes: % it actually is two lists. (not to need 4 extra arguments) % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% analyse_binairy_equality(false, CP, CP, _, Q, Q, N, N, R, R, D, D, AllD, AllD, MR, MR, C, C, A, A). analyse_binairy_equality(true, CP, CP, [], Q, Q, N, N, R, R, D, D, AllD, AllD, MR, MR, C, C, A, A). analyse_binairy_equality(true, CP, NCP, [relation(Right, =, Left)|Tail], Q, NQ, N, NN, R, NR, D, ND, AllD, NAllD, MR, NMR, C, NC, A, NA):- map_list(Left, [ ILeft ]), map_list(Right, [ IRight ]), list_map([ILeft, IRight], M), % if 0 = x is derived, it is always the zero pointer that is inserted (NB cannonical form!) % NB Right and Left swapped to keep lowest pointer (and 0) % and in additions the zero pointer is left out. eg. x = 0, x + y = z -> y = z instead of y + 0 = z % like in process zero pointer replace_index_relations(M, ILeft, IRight, N, N1), replace_index_relations(M, ILeft, IRight, R, R1), replace_index_relations(M, ILeft, IRight, D, D1), replace_index_relations(M, ILeft, IRight, AllD, AllD1), replace_index_relations(M, ILeft, IRight, Tail, Tail1), replace_index_relations(M, ILeft, IRight, MR, MR1), replace_index_relations_for_correspondence(M, ILeft, IRight, C, C1), % fails if that would produce a 'double quantity' % sets flag if contradiction found replace_index_in_adders(ILeft, IRight, A, A1), % Note the adder pointers are updated !, replace_index(ILeft, IRight, Q, Q1), replace_context_pointer(Left, Right, CP, CP1), analyse_binairy_equality(true, CP1, NCP, Tail1, Q1, NQ, N1, NN, R1, NR, D1, ND, AllD1, NAllD, MR1, NMR, C1, NC, A1, NA). analyse_binairy_equality(true, CP, NCP, [_|Tail], Q, NQ, N, NN, R, NR, D, ND, AllD, NAllD, MR, NMR, C, NC, A, NA) :- flag(analyse_simple_found_contradiction, false, false), analyse_binairy_equality(true, CP, NCP, Tail, Q, NQ, N, NN, R, NR, D, ND, AllD, NAllD, MR, NMR, C, NC, A, NA). replace_context_pointer(Remove, _, CP, NCP):- map_difference(CP, Remove, NCP). % replace index relations fails if F & S are in a sum together % or if an inconsistent relation is found: x > x replace_index_relations(_, _, _, [], []). % fail if F & S are already in a sum together replace_index_relations(M, _F, _S, [ relation(Left, _, Right) | _ ], _) :- %list_map([F, S], M), ( map_intersection(M, Left, M) ; map_intersection(M, Right, M) ), !, fail. replace_index_relations(M, F, S, [ relation(Left, Rel, Right) | Tail ], Result) :- m_replace_two(F, S, Left, Right, NLeft, NRight), !, % fails if F not in Left OR Right zero_pointer(relation(NLeft, Rel, NRight), Relation), use_if_not_evident(Relation, NewTail, Result), replace_index_relations(M, F, S, Tail, NewTail). replace_index_relations(M, F, S, [ Relation | Tail ], [ Relation | NewTail ]) :- replace_index_relations(M, F, S, Tail, NewTail). % Patch FL July 2004 Solve failed to find an obvious contradiction: % probably all parents used already in this particular case % form was: % 2 = 1, 1 > 2 % analyse simple constructs the contradictive relation: 1 > 1 % this fails here to make append relation fail thus providing an extra % chance to capture inconsistencies use_if_not_evident(relation(M, >, M), Result, Result):- !, flag(analyse_simple_found_contradiction, _, true), etrace(solve_simple_found_invalid, _, add_relation), !, fail. use_if_not_evident(Rel, Result, Result):- evident(Rel), !. use_if_not_evident(Rel, Result, [Rel|Result]). % suceed for fist, try second or succeed m_replace_two(First, Second, Org1, Org2, New1, New2) :- map_replace(First, Second, Org1, New1), (map_replace(First, Second, Org2, New2) ; Org2 = New2), !. % failed for first, try second or fail m_replace_two(First, Second, Org1, Org2, Org1, New2) :- map_replace(First, Second, Org2, New2). replace_index_relations_for_correspondence(_, _, _, [], []). replace_index_relations_for_correspondence(M, I1, I2, [correspondence(L1, L2)|T], NewList):- replace_index_relations_cor(M, I1, I2, L1, NL1, Change1), replace_index_relations_cor(M, I1, I2, L2, NL2, Change2), !, ( no_full_tautology_or_contradiction_correspondence(Change1, Change2, NL1, NL2, undirected) -> NewList = [correspondence(NL1, NL2)|NT] ; NewList = NT %correspondence has become useless ), !, replace_index_relations_for_correspondence(M, I1, I2, T, NT). replace_index_relations_for_correspondence(M, I1, I2, [if_correspondence(L1, L2)|T], NewList):- replace_index_relations_cor(M, I1, I2, L1, NL1, Change1), replace_index_relations_cor(M, I1, I2, L2, NL2, Change2), !, ( no_full_tautology_or_contradiction_correspondence(Change1, Change2, NL1, NL2, directed) -> NewList = [if_correspondence(NL1, NL2)|NT] ; NewList = NT %correspondence has become useless ), !, replace_index_relations_for_correspondence(M, I1, I2, T, NT). % FL July 2004 % correspondences can have contradictory relations which just indicates there not % active in this state, therefore no use_if_not_evident is used here. replace_index_relations_cor(_, _, _, [], [], false). % fail if F & S are already in a sum together replace_index_relations_cor(M, _F, _S, [ relation(Left, _, Right) | _ ], _, false) :- %list_map([F, S], M), ( map_intersection(M, Left, M) ; map_intersection(M, Right, M) ), !, fail. replace_index_relations_cor(M, F, S, [ relation(Left, Rel, Right) | Tail ], [relation(NLeft, Rel, NRight)|NewTail], true) :- m_replace_two(F, S, Left, Right, NLeft, NRight), !, % fails if F not in Left OR Right replace_index_relations_cor(M, F, S, Tail, NewTail, _). replace_index_relations_cor(M, F, S, [ Relation | Tail ], [ Relation | NewTail ], Change) :- replace_index_relations_cor(M, F, S, Tail, NewTail, Change). % no changes: still relevant correspondence. no_full_tautology_or_contradiction_correspondence(false, false, _, _, _):- !. % directed, contradictory conditions: irrelevant no_full_tautology_or_contradiction_correspondence(_, _, L1, _, directed):- contradiction_in_list(L1), !, fail. % directed, tautologous consequenses: irrelevant no_full_tautology_or_contradiction_correspondence(_, _, _, L2, directed):- full_tautology_list(L2), !, fail. % undirected, only tautologys: irrelevant no_full_tautology_or_contradiction_correspondence(_, _, L1, L2, undirected):- full_tautology_list(L1), full_tautology_list(L2), !, fail. % undirected, contradiction in both lists: irrelevant no_full_tautology_or_contradiction_correspondence(_, _, L1, L2, undirected):- contradiction_in_list(L1), contradiction_in_list(L2), !, fail. % still relevant correspondence. no_full_tautology_or_contradiction_correspondence(_, _, _, _, _). contradiction_in_list([]):-!, fail. contradiction_in_list([H|_]):- invalid_relation(H),!. contradiction_in_list([_|T]):- contradiction_in_list(T). full_tautology_list([]). full_tautology_list([H|T]):- evident(H), full_tautology_list(T). % FL december-2003: GARP 2.0 new: replace index for adder lists (influence resolution) % Note that the structure of the list (length, positioning of items is % left intact replace_index_in_adders(_, _, [], []). replace_index_in_adders(ILeft, IRight, [Adder|Tail], [NAdder|NTail]):- replace_index_single_adder(ILeft, IRight, Adder, NAdder), replace_index_in_adders(ILeft, IRight, Tail, NTail). replace_index_single_adder(ILeft, IRight, adder(Q, Addlist), adder(NQ, NAddlist)):- map_replace(ILeft, IRight, Q, NQ), !, replace_index_addlist(ILeft, IRight, Addlist, NAddlist). % map replace failed for Q replace_index_single_adder(ILeft, IRight, adder(Q, Addlist), adder(Q, NAddlist)):- replace_index_addlist(ILeft, IRight, Addlist, NAddlist). replace_index_addlist(_, _, [], []). replace_index_addlist(ILeft, IRight, [H|T], [NH|NT]):- H =.. [Type, Q], map_replace(ILeft, IRight, Q, NQ), !, NH =.. [Type, NQ], replace_index_addlist(ILeft, IRight, T, NT). % map replace failed for Q replace_index_addlist(ILeft, IRight, [H|T], [H|NT]):- replace_index_addlist(ILeft, IRight, T, NT). % replace_index/4 % update quantity list: % replace all occurences of I1 by I2 replace_index(_, _, [], []). replace_index(I1, I2, [ H/I1 | Tail ], [ H/I2 | NewTail ]) :- !, replace_index(I1, I2, Tail, NewTail). replace_index(I1, I2, [ H | Tail ], [ H | NewTail ]) :- replace_index(I1, I2, Tail, NewTail). %%%%%%%%%%%%%%%%%% Correspondence Inspection %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % inspect_correspondence: % checks all correspondences if they fire because of a given set of new relations % % inspect_a_correspondence: % checks if a new correpondence fires given the set of derivable relations % % inspect_some_correspondences: % implements inspect_a_correspondence for a set of new correspondences % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* To remove FL may 07, passing on adders now for pointer updates... inspect_correspondence(Relations, Cin, Cout, DoAnalyseSimple):- inspect_correspondence2(Relations, Cin, Cout, [], DoAnalyseSimple, [], []). */ inspect_correspondence(Relations, Cin, Cout, DoAnalyseSimple, AddersIn, AddersOut):- inspect_correspondence2(Relations, Cin, Cout, [], DoAnalyseSimple, AddersIn, AddersOut). inspect_correspondence2([], Cio, Cio, [], _DoAnalyseSimple, Adders, Adders):- !. inspect_correspondence2(Relations, Cin, Cout, Previous, DoAnalyseSimple, AddersIn, AddersOut):- cio_c_nc_d(Cin, Cnew, Correspondence, RCorrespondence, Derivable), ( select(correspondence(L1, L2), Correspondence, RCorrespondence) ; select(correspondence(L2, L1), Correspondence, RCorrespondence) ; select(if_correspondence(L1, L2), Correspondence, RCorrespondence) ), ( L1 = [] % An empty list means no conditions: fire correspondence. ; select(One, L1, RL1), is_derivable(One, Relations), check_derivable(RL1, Derivable) ), append(Previous, L2, ToAdd), !, inspect_correspondence2(Relations, Cnew, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut). inspect_correspondence2(_, Cio, Cio, [], _, Adders, Adders):- !. inspect_correspondence2(_, Cin, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut):- append_relation_all(ToAdd, Cin, Cout, _, DoAnalyseSimple, AddersIn, AddersOut). inspect_a_correspondence(correspondence(L1, L2), Cin, Cout):- cio_d(Cin, D), %strictly_relevant_contexts(BV, R, Contexts, _), %relevant_contexts(BV, R, Contexts, _), ( ( check_derivable(L1, D), !, append_relation_all(L2, Cin, Cout, _, true) ) ; ( check_derivable(L2, D), !, append_relation_all(L1, Cin, Cout, _, true) ) ). inspect_a_correspondence(if_correspondence(L1, L2), Cin, Cout):- cio_d(Cin, D), %strictly_relevant_contexts(BV, R, Contexts, _), %relevant_contexts(BV, R, Contexts, _), check_derivable(L1, D), !, append_relation_all(L2, Cin, Cout, _, true). inspect_a_correspondence(_, Cio, Cio). inspect_some_correspondences([], Cio, Cio). inspect_some_correspondences([H|T], Cin, Cout):- inspect_a_correspondence(H, Cin, Cnew), correct_changed_pointers(Cin, Cnew, T, NT), % pointers can change, leading to invalid correspondences in tail inspect_some_correspondences(NT, Cnew, Cout). %no pointer changes correct_changed_pointers(Cio, Cio, Corr, Corr):-!. %no pointer changes correct_changed_pointers(Cold, Cnew, Corr, Corr):- cio_q(Cold, Q), cio_q(Cnew, Q), !. %pointers changed! update correspondences correct_changed_pointers(Cold, Cnew, CorrIn, CorrOut):- cio_q(Cold, Q), cio_q(Cnew, NQ), determine_changed_pointers(Q, NQ, Changes), switch_changed_pointers(Changes, CorrIn, CorrOut). %done determine_changed_pointers([], [], []). % unchanged pointer determine_changed_pointers([Q/P|T], [Q/P|NT], Changes):- !, determine_changed_pointers(T, NT, Changes). % unchanged pointer, strange position determine_changed_pointers([Q/P|T], NQ, Changes):- member(Q/P, NQ), !, determine_changed_pointers(T, NQ, Changes). % changed pointer determine_changed_pointers([Q/P|T], [Q/NP|NT], [changed(P, NP)|Changes]):- !, determine_changed_pointers(T, NT, Changes). % changed pointer, strange position determine_changed_pointers([Q/P|T], NQ, [changed(P, NP)|Changes]):- member(Q/NP, NQ), !, determine_changed_pointers(T, NQ, Changes). % pointer dissapeared? should not happen determine_changed_pointers([_Q/_P|T], NQ, Changes):- etrace(pointer_error, determine_changed_pointers, general), !, determine_changed_pointers(T, NQ, Changes). % done switch_changed_pointers([], Corr, Corr). % change switch_changed_pointers([changed(Old, New)|T], CorrIn, CorrOut):- list_map([Old, New], M), replace_index_relations_for_correspondence(M, Old, New, CorrIn, CorrNew), switch_changed_pointers(T, CorrNew, CorrOut). %%%%%%%%%%%%%%%%%%%%%%%%%% resolve influences and proportional relations %%%%%%%%%%%%%%%%%%%% % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% resolve_influence_proportional(Cin, Cout, OldSod, Constraints, SecondOrderDerivatives, AmbiguousDerivatives):- cio_ip_nip(Cin, Cnew, IP, []), % collect i/p relations etrace(solve_ir_search, _, resolve), findall(adder(Quantity, AddList), % find all effects on each quantity adder(Quantity, _, AddList, [], IP, []), Adders1), % put adders in causal order: sort_adders(Adders1, Adders), adder_strings(Adders, Adderstrings), % calculates full causal paths !, % resolve these effects per quantity % backtracking allowed for ambiguous influences/prop. rel. % FL mar 08: return list of ambiguos derivatives for termination possibility resolve_adders(Adders, Adderstrings, Cnew, Cout1, OldSod, AmbiguousDerivatives), % FL mar 07: NEW: determine 2nd order derivative % Returns a list of preds: [sod_info(Q, Derivative, SecondOrderDerivative, Influences, FullCausalPath), ..., ...] % New june 07: 3rd element {single, multiple} to indicate if it is a single or multiple influence % SecondOrderDerivative can be [pos, neg, zero, pos_zero, neg_zero, unknown] % April 08: Constraints: assumed terminating ambiguous derivatives should not be found to be moving in % the opposite direction. resolve_2ndorder_adders(Adders, Adderstrings, Cout1, Cout, SecondOrderDerivatives, Constraints). % adder/6: % find all influences and proportional relation on a quantity % no more inf/prop for a certain quantity, return Addlist adder(Quantity, Quantity, AddListOut, AddListIn, [], _):- nonvar(Quantity), list_to_set(AddListIn, AddListOut). %FL: filter double adders (bad model) % backtrack: select next quantity and find inf/prop in restlist adder(Quantity, _, AddList, _, [], RestIP) :- RestIP \== [], adder(Quantity, _, AddList, [], RestIP, []). % if called for the first time Quantity is uninstantiated % and will be matched with the quantity in prop/inf Head % otherwise Head must be a next prop/inf on Quantity. adder(ResultQuantity, Quantity, AddList, Previous, [Head | Tail ], RestIP) :- adder_relation(Head, Quantity, First), !, adder(ResultQuantity, Quantity, AddList, [First|Previous], Tail, RestIP). % Head is not an inf/prop on Quantity, put it on RestList adder(ResultQuantity, Quantity, AddList, Previous, [Head | Tail ], RestIP) :- adder(ResultQuantity, Quantity, AddList, Previous, Tail, [Head|RestIP]). %% %%% % FL new july 2007, % % Add adder order heuristic: try to resolve influences first, % for better tracing. % further ordering algorithm is a bit naive: % insert after adders that influence it. % progress indicator and several iterations are needed. % now hacked by doing it three times. sort_adders(AddersIn, AddersOut):- split_adders_inf_prop(AddersIn, Inf, PropIn), insertion_sort_adders(PropIn, [], Prop1), insertion_sort_adders(Prop1, [], Prop2), % A hack, do it three times, fixes most mess ups insertion_sort_adders(Prop2, [], Prop), append(Inf, Prop, AddersOut). % influences in front... split_adders_inf_prop([], [], []). split_adders_inf_prop([H|T], [H|IT], PT):- inf_adder(H), !, split_adders_inf_prop(T, IT, PT). split_adders_inf_prop([H|T], IT, [H|PT]):- split_adders_inf_prop(T, IT, PT). %heuristic: assumes if first adder is influence then so is the rest, ignore rest inf_adder(adder(_, [First|_])):- First =.. [_, value(_)]. % insertion_sort_adders(In, Sofar, Out, NotInserted, Progress). insertion_sort_adders([], Out, Out). insertion_sort_adders([adder(X, AddList)|T], SoFar, AddersOut):- insert_adder(X, AddList, AddList, SoFar, NewSoFar), insertion_sort_adders(T, NewSoFar, AddersOut). %checked all addItems, put in front of rest, insert_adder(X, AddList, [], SoFarBack, [adder(X, AddList)|SoFarBack]). % check addItem, insert in part of the list after the influencing adder insert_adder(X, AddList, [AddItem|AddListTail], SoFar, NewSoFar):- AddItem =.. [_, Qty], memberchk(adder(Qty, _), SoFar), % influence Qty is influenced itself. !, split_adders_sofar(Qty, SoFar, SoFarFront, SoFarBack), insert_adder(X, AddList, AddListTail, SoFarBack, NewSoFarBack), append(SoFarFront, NewSoFarBack, NewSoFar). % check addItem, no influencing adder, ignore item insert_adder(X, AddList, [_|AddListTail], SoFar, NewSoFar):- insert_adder(X, AddList, AddListTail, SoFar, NewSoFar). % split_adders_sofar(Qty, Input, InputFront, InputBack) % find the adder in SoFar that influences Qty, % return Front and Back of List, % Front includes the adder that influences Qty % fails if no adder influences Qty, but with a memberchk in front of the call % that should never happen. % found, done split_adders_sofar(Qty, [adder(Qty, List)|Tail], [adder(Qty, List)], Tail):- !. split_adders_sofar(Qty, [adder(QtyB, ListB)|Tail], [adder(QtyB, ListB)|Front], Back):- split_adders_sofar(Qty, Tail, Front, Back). adder_strings(Adders, Adderstrings):- reverse(Adders, RAdders), adder_strings_2(RAdders, RStrings), reverse(RStrings, Adderstrings). adder_strings_2([], []). adder_strings_2([adder(Q, List)|AdderTail], [adder(Q, CompleteList)|CompleteTail]):- adder_string_complete(List, AdderTail, CompleteList), % by using the addertail, loops are impossible !, adder_strings_2(AdderTail, CompleteTail). % adderstingcomplete failed: probably a loop: next adder_strings_2([H|AdderTail], [H|CompleteTail]):- etrace(warningAdderStringLoop, [], _), adder_strings_2(AdderTail, CompleteTail). adder_string_complete([], _, []). %Influenced Q adder_string_complete([H|T], AdderTail, [NH|NT]):- H =.. [PosNeg, Q], memberchk(adder(Q, List), AdderTail), % substitute Q with its adder !, adder_string_complete(List, AdderTail, NList), % substitute Q's in this sub-adder NH =.. [PosNeg, adder(Q, NList)], adder_string_complete(T, AdderTail, NT). % substitute others %non Influenced Q adder_string_complete([H|T], AdderTail, [H|NT]):- adder_string_complete(T, AdderTail, NT). % resolve_adders(+Adders, +Cin, -Cout) % - change Adders from extern to intern representation % - apply closed world on all quantities (under switch control) % this means setting derivatives of unaffected quantities to zero. % - resolve the resulting adders within Cio context. resolve_adders(Adders, Adderstrings, Cin, Cout, Sod, AmbiguousDerivatives):- cio_q_nq(Cin, Cnew1, Q, NQ), adders_quantities(Adders, IntAdders1, Q, NQ), % convert adderlist to intern representation !, flag(cw_assumption, Flag, Flag), ( algorithm_assumption_flag(Flag, fail, cw_assumption) -> Cnew2 = Cnew1 ; % set unknown, uninfluenced, influencing quantities to zero etrace(solve_cw_start, _, resolve), apply_closed_world_to_adders(NQ, IntAdders1, Cnew1, Cnew2) % FL SHOULDNT ADDERS BE PASSED ON FOR POINTER UPDATES? ), test_2nd_order_continuity_constraints(Sod, Adders, Adderstrings, IntAdders1, IntAdders, Cnew2, Cnew3), resolve_adders_2(IntAdders, Adders, Cnew3, Cout, true, AmbiguousDerivatives). % FL may 2004: pass on normal adderlist for use in tracer % fails if contradiction % apply_closed_world_to_adders(+Quantities, +Adders, +Cin, -Cout) % december-2003 by FL: % set every value or derivative to zero if unknown, uninfluenced % and influencing something: % NB: In this version it is done for all. But correspondences and complex % equations may cause quantities to be known later on, causing contradiction. % Therefore, this feature can be switched off (see algorithm option switches), apply_closed_world_to_adders([], _, Cio, Cio). % zero pointer can be skipped.. (already zero of course) apply_closed_world_to_adders([_Value/0|QTail], Adders, Cin, Cout):- !, apply_closed_world_to_adders(QTail, Adders, Cin, Cout). apply_closed_world_to_adders([Value/DQ|QTail], Adders, Cin, Cout):- list_map([DQ], DM), \+ memberchk(adder(DM, _), Adders), % if not influenced itself member(adder(_, L), Adders), % and it influences something ( memberchk(pos(DM), L); memberchk(neg(DM), L) % only pos neg, no up and down yet ), cio_d(Cin, Derivable), \+ get_quantity_sign(DM, Derivable, _), % and it's sign is not known !, list_map([0], ZeroMap), % then it can be assumed zero % Analyse simple & zero equality should be false not to % create invalid pointers in Qlist or Adders etrace(solve_cw_zero, [Value], resolve), canonical_form(relation(DM, =, ZeroMap), Rel), append_relation(Rel, Cin, Cnew, _, false), % this may fail if the model supplies information in contradiction with the assumption !, apply_closed_world_to_adders(QTail, Adders, Cnew, Cout). % quantity not zero-assumable: ignore it apply_closed_world_to_adders([_|QTail], Adders, Cin, Cout):- apply_closed_world_to_adders(QTail, Adders, Cin, Cout). % switch is off test_2nd_order_continuity_constraints(_Sod, _Adders, _Adderstrings, IntAdders, IntAdders, Cnew, Cnew):- flag(second_order_continuity, F, F), algorithm_assumption_flag(F, fail, second_order_continuity), !. % switch is on test_2nd_order_continuity_constraints(Sod, Adders, Adderstrings, IntAddersIn, IntAddersOut, Cin, Cout):- flag(second_order_continuity, F, F), algorithm_assumption_flag(F, true, second_order_continuity), %etrace(solve_sod_continuity_start, [], resolve), test_2nd_order_continuity_constraints2(Sod, Adders, Adderstrings, IntAddersIn, IntAddersOut, Cin, Cout), %etrace(solve_sod_continuity_end, [], resolve), !. % done / no 2nd order derivatives known test_2nd_order_continuity_constraints2([], _Adders, _Adderstrings, IntAdders, IntAdders, Cnew, Cnew):- !. % 2nd order derivative with unchanged causal model for Qty. test_2nd_order_continuity_constraints2([sod_info(Par, Der, DDer, OldList, OldPath)|Tail], Adders, Adderstrings, IntAddersIn, IntAddersOut, Cin, Cout):- OldList = [_,_|_], % only multiple influenced should be checked... DDer \= unknown, %this would not impose constraints. memberchk(adder(derivative(Par), NewList), Adders), memberchk(adder(derivative(Par), NewPath), Adderstrings), translate_addlist_to_2ndorder(NewList, NList1), %translate to make same form as oldlist sort(NList1, NList), sort(OldList, OList), NList = OList, NewPath = OldPath, %this could be the only check, the single list of local influences is old code... !, % causal model unchanged for this qty. add constraint do_2ndorder_continuity(Par, Der, DDer, Constraint), ( Constraint \= nil -> intern_representation(Constraint, Relation, Cin, Cnew), try_append(append_relation(Relation, Cnew, Cnew1, _Added, true, IntAddersIn, IntAdders)) ; Cin = Cnew1, IntAdders = IntAddersIn ), test_2nd_order_continuity_constraints2(Tail, Adders, Adderstrings, IntAdders, IntAddersOut, Cnew1, Cout). % no compatible adder for this 2nd order derivative % (causal model changed) test_2nd_order_continuity_constraints2([_|Tail], Adders, Adderstrings, IntAddersIn, IntAddersOut, Cin, Cout):- test_2nd_order_continuity_constraints2(Tail, Adders, Adderstrings, IntAddersIn, IntAddersOut, Cin, Cout). % no progress, discard adders and derive unknown for these quantities. resolve_adders_2(_, _, Cio, Cio, false, []). % first time, or progress resolve_adders_2(Adders, TrAdders, Cin, Cout, true, AmbiguousDerivatives):- resolve(Adders, TrAdders, Cin, Cnew, [], Unresolved, [], UnTrAd, Progress, AmbDer1), resolve_adders_2(Unresolved, UnTrAd, Cnew, Cout, Progress, AmbDer2), append(AmbDer1, AmbDer2, AmbiguousDerivatives). % FL May 2004: added adders in normal representation for tracer use. % % FL July 2004: If semi-ambiguous result is obtained: % (>=) then only two ambiguous alternatives are generated. % resolve(+Adders, +TracerAdders, +Cin, -Cout, +[], % -Unresolved, +[], -UnresolvedTracerAdders, -Progress) % for each adder: % - if not all values of terms are known (incomplete): % put adder on Unresolved list, % progress for that addder = false, % but true in general if other adders produce progress % - elseif single adder: add result, progress = true % - else construct balance expression and evaluate: % - if ambiguous (not enough information): % add different values for Q upon backtracking, progress = true % - if positive, zero, or negative: add this result, progress = true % all done, return results: resolve([], [], Cin, Cin, Unresolved, Unresolved, UTracer, UTracer, false, []). % adder incomplete -> put on Unresolved list resolve([adder(Q, AddList)|Tail], [adder(TrQ, TrList)|TrTail], Cin, Cout, Unresolved, UnresolvedOut, UTracer, UTracerOut, Progress, AmbDer) :- cio_q_d(Cin, QList, Derivable), % check quantities in Addlist for known values, % transform pos, neg to up, down & noforce, % return incomplete or complete to indicate if all values are known complete_adder(AddList, Derivable, NewAddList, Incomplete, TrList, TracerAddList), Incomplete = incomplete, !, %is it ok to cut here? because below it says: note this may fail... choicepoint seems unnecessary... Fl Feb 07 tempflo etrace(solve_ir_set, [TrQ, TrList, QList, Derivable], resolve), etrace(solve_ir_unres, [TracerAddList], resolve), % note this may fail resolve(Tail, TrTail, Cin , Cout, [adder(Q, NewAddList)|Unresolved], UnresolvedOut, [adder(TrQ, TrList)|UTracer], UTracerOut, Progress, AmbDer). % adder complete, single influence -> evaluate & add results resolve([adder(Q, [Influence])|Tail], [adder(TrQ, [TrInf])|TrTail], Cin, Cout, UnresolvedIn, UnresolvedOut, UTracer, UTracerOut, Progress, AmbDer) :- cio_q_d(Cin, QList, Derivable), get_sign(Influence, Derivable, Sign), !, etrace(solve_ir_set, [TrQ, [TrInf], QList, Derivable], resolve), etrace(solve_ir_single_res, [TrInf, Sign], resolve), etrace(solve_ir_res, [TrQ, Sign], resolve), add_resolution_result(Q, TrQ, Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [Unresolved1, NewTail]), % ANA !, % note this may fail resolve(NewTail, TrTail, Cnew , Cout, Unresolved1, UnresolvedOut, UTracer, UTracerOut, TailProgress, AmbDer). % adder complete -> first try sign addition, % if that fails: next clause will construct balance resolve([adder(Q, AddList)|Tail], [adder(TrQ, TrList)|TrTail], Cin, Cout, UnresolvedIn, UnresolvedOut, UTracer, UTracerOut, Progress, AmbDer) :- cio_q_d(Cin, QList, Derivable), try_sign_addition(AddList, Derivable, zero, Sign, TrList, TrEffects),% NB fails if ambiguous !, etrace(solve_ir_set, [TrQ, TrList, QList, Derivable], resolve), etrace(solve_ir_add, [TrEffects], resolve), etrace(solve_ir_res, [TrQ, Sign], resolve), add_resolution_result(Q, TrQ,Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]), !, resolve(NewTail, TrTail, Cnew , Cout, NewUnresolved, UnresolvedOut, UTracer, UTracerOut, TailProgress, AmbDer). % adder complete -> construct balance, evaluate & add results resolve([adder(Q, AddList)|Tail], [adder(TrQ, TrList)|TrTail], Cin, Cout, UnresolvedIn, UnresolvedOut, UTracer, UTracerOut, Progress, AmbDer) :- cio_q_d(Cin, QList, Derivable), % check quantities in Addlist for known values, transform pos, neg to up, down & noforce complete_adder(AddList, Derivable, CompleteAddList, Incomplete, _, _), Incomplete = complete, etrace(solve_ir_set, [TrQ, TrList, QList, Derivable], resolve), etrace(solve_ir_bal, [TrList, Pos, Neg], resolve), % make_balance [BalanceValue, min1, min2, ...] = [pos1, pos2, ...] (intern representation) make_balance(Q, CompleteAddList, Cin, Ctest1, Balance, BV), % add and evaluate balance relation in testcio (balance not added to relations) % try_balance gives feedback if append_relation fails try_balance(append_relation(Balance, Ctest1, Ctest2, _, false)), % Analyse simple & zero equality should be false not to create an invalid Q pointers to testcio indexes % get value of balancequantity cio_d(Ctest2, Derivable2), %test quantity sign (also >= and =<) get_balance_result(BV, Derivable2, Sign),%because no analyse zero & simple equality, BV is still a valid pointer !, %no backtracking on this part ( memberchk(Sign, [zero, pos, neg]) % definitive result -> ( etrace(solve_ir_bal_res, [TrQ, Pos, Neg, Sign], resolve), add_resolution_result(Q, TrQ,Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]), AmbDer = TailAmbDer, !) ; % else: ambiguous result, Sign is a list of possibilities in this case ( etrace(solve_ir_bal_unres, [TrQ, Pos, Neg, Sign], resolve), %add_resolution_result(Q, ambiguous, Cin, Cnew, Progress, TailProgress, add_resolution_result(Q, TrQ, Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]), AmbDer = [TrQ|TailAmbDer] ) ), % note this may fail resolve(NewTail, TrTail, Cnew , Cout, NewUnresolved, UnresolvedOut, UTracer, UTracerOut, TailProgress, TailAmbDer). % Balance should always be appendible, because BalanceValue is a newly generated quantity try_balance(X):- call(X),!. try_balance(_):- etrace(solve_append_bal_error, _, general), fail. % appending a result is not always possible, sometimes a derivative is already % known through another information source (defined in model, inequality etc.) % In this case the tracer shows that resolution result was not added. try_append(X):- call(X), !. try_append(X):- etrace(solve_add_ir_res_fail, X, resolve), fail. % add_resolution_result(+Q, +TrQ, +Sign, +Cin, -Cout, -Progress, +TailProgress, % +[UnresolvedIn, AdderTailIn], -[UnresolvedOut, AdderTailOut]) % Q is the quantity in question (intern). TrQ is its normal name, for tracing % Sign is a single value, or a list of values (ambiguity) % unresolved and adderlist are passed on to update their pointers, % because analyse zero / simple equality can change these % valid new result: let progress be true if not already derivable, add_resolution_result(Q, _TrQ, Sign, Cin, Cout, Progress, TailProgress, [UnresolvedIn, AdderTailIn], [UnresolvedOut, AdderTailOut]):- % ANA memberchk(Sign, [zero, pos, neg]), zero_relation_sign(Rel, Sign), list_map([0], Empty), right_order(relation(Q, Rel, Empty), Relation1), canonical_form(Relation1, Relation), append_split(UnresolvedIn, AdderTailIn, I, OtherAddersIn), % makes one list, for easy passing on with append relatoin. pointers can be updated, but list stays intact. try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(UnresolvedOut, AdderTailOut, I, OtherAddersOut), % splits the list again at the same point. (Added = [], Progress=TailProgress; Progress=true), !. % ambiguous influence on Q: return all possibilities (upon backtracking) add_resolution_result(Q, TrQ, Sign, Cin, Cout, Progress, TailProgress, [UnresolvedIn, AdderTailIn], [UnresolvedOut, AdderTailOut]):- % ANA member(S, Sign), nth1(N, Sign, S), etrace(pathstart, resolve), %tempflo, cat? etrace(solve_ir_amb_nth, [TrQ, N, S], resolve), zero_relation_sign(Rel, S), list_map([0], Empty), right_order(relation(Q, Rel, Empty), Relation1), canonical_form(Relation1, Relation), once(( append_split(UnresolvedIn, AdderTailIn, I, OtherAddersIn), try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(UnresolvedOut, AdderTailOut, I, OtherAddersOut), (Added = [], Progress=TailProgress; Progress=true) )). % place a relation in the right order: internaly only =, > and >= are used (not < and =<) right_order(relation(L, <, R), relation(R, >, L)) :- !. right_order(relation(L, =<, R), relation(R, >=, L)) :- !. right_order(R, R):- !. % append_split(+L1, +L2, -I, -All) % append to lists, return the index where the (virtual) separation is append_split(L1, L2, I, All):- length(L1, I), append( L1, L2, All). % split_append(-L1, -L2, +I, +All) % ANA % divide a list into two lists splitting at index I split_append([], All, 0, All):-!. split_append([H|L1], L2, I, [H|T]):- J is I - 1, split_append(L1, L2, J, T). % FL Feb 2007 moved write_addone clauses to interface_garp3.pl % complete_adder: takes an addList and evaluates to zero % if sign is known then change notation to up/down/noforce % otherwise return incomplete and semi transformed list. % unknown quantities are passed on for tracer complete_adder([], _, [], complete, [], []):-!. %not yet incomplete -> complete complete_adder([], _, [], incomplete, [], []):-!. %already incomplete complete_adder([H|T], Derivable, [Result | NewAddList], Incomplete, [_|TT], TraceList):- get_balance_sign(H, Derivable, Result), %returns: up(Q), down(Q), noforce(Q) or fails !, complete_adder(T, Derivable, NewAddList, Incomplete, TT, TraceList). % could not get quantity sign -> set incomplete indicator & continue with rest of list. complete_adder([H|T], Derivable, [H | NewAddList], incomplete, [HT|TT], [HT|TraceTail]):- !, complete_adder(T, Derivable, NewAddList, incomplete, TT, TraceTail). % FL june 07: before constructing balance, first try sign addition... % this can save some valuable inequality reasoning time % try_sign_addition(List, Derivable, SignIn, SignOut, TrList, EfList):- remove_weaker2(Derivable, Derivable, StrongDerivable), %since we draw conclusions on the first relation we find... !, try_sign_addition2(List, StrongDerivable, SignIn, SignOut, TrList, EfList). % returns Sign and annotated tracerAddlist: Add/Sign/Effect try_sign_addition2([], _Derivable, Sign, Sign, [], []). try_sign_addition2([H|T], Derivable, SignIn, SignOut, [TrH|TrT], [TrQ/Sign/Effect|EffectsT]):- get_add_sign(H, Derivable, Sign, Effect), % nb fails if unknown sign !, add_signs(SignIn, Effect, NewSign), % nb fails if result is unknown / ambiguous !, TrH =.. [_,TrQ], try_sign_addition2(T, Derivable, NewSign, SignOut, TrT, EffectsT). % no effect, continue get_add_sign(noforce(_Quantity), _, zero, zero):- !. % get interpreted sign get_add_sign(Add, Relations, Sign, Result):- Add =.. [Dir, Quantity], list_map([0], Z), derive_quantity_sign(Quantity, Relations, Z, Sign), !, interpret_sign(Sign, Dir, Result), !. % nb differs from get_quantity_sign % because ambiguous signs are also accepted % NB no canonical form needed here (FL nov 07) derive_quantity_sign(Z, _Relations, Z, zero):-!. derive_quantity_sign(Quantity, Relations, Z, Sign):- member(relation(Quantity, Relation, Z), Relations), zero_sign(Relation, Sign). derive_quantity_sign(Quantity, Relations, Z, Sign):- member(relation(Z, Relation, Quantity), Relations), inverse(Relation, Inverse), zero_sign(Inverse, Sign). %relations to signs zero_sign(>, pos). zero_sign(>=, pos_zero). zero_sign(=, zero). zero_sign(<, neg). zero_sign(=<, neg_zero). % interpret_sign(+signIn, +Direction, -signout). interpret_sign(zero, _, zero). interpret_sign(pos, up, pos). interpret_sign(neg, up, neg). interpret_sign(pos, pos, pos). interpret_sign(neg, pos, neg). interpret_sign(pos, down, neg). interpret_sign(neg, down, pos). interpret_sign(pos, neg, neg). interpret_sign(neg, neg, pos). % add_signs(+Sign1, +Sign2, NewSign) % zero has no effect: keep sign add_signs(Sign, zero, Sign). add_signs(zero, Sign, Sign). % equal signs: keep sign add_signs(Sign, Sign, Sign). % strong and weak: keep strong add_signs(pos_zero, pos, pos). add_signs(neg_zero, neg, neg). % all others: ambiguous >>> fail! % make_balance(+Quantity, +AddList, +Cin, -Cout, -Balance, -BalanceValue_intern) % make balance expression in intern representation: [min, min, BV] = [pos, pos] make_balance(Quantity, AddList, Cin, Cout, Relation, BV):- % create a balance value quantity: make_abstract_balance_quantity(Quantity, Cin, Cnew, I, BV), % get pointer lists for the positive and negative influences/props. add_to_balance(AddList, LeftList, RightList), append([I], LeftList, ILeftList), % d_q see intern.pl double_quantities(ILeftList, NLeftList, [], Cnew, Cnew1), double_quantities(RightList, NRightList, [], Cnew1, Cout), % create bitmaps for both sides of the balance. list_map(NLeftList, Left), list_map(NRightList, Right), zero_pointer(relation(Left, =, Right), Relation1), canonical_form(Relation1, Relation). % make_abstract_balance_quantity(+Quantity, +Cin, -Cout, -I, -BV), % adds a balancequantity in the temporary Cio for influence resolution make_abstract_balance_quantity(Quantity, Cin, Cout, I, BV):- % construct a pointer for the quantiy: flag(q_cnt, P, P), I is P + 1, flag(q_cnt, _, I), cio_q_nq(Cin, Cout, Q, NQ), list_map([I], BV), map_list(Quantity, [X]), % construct a name for the quantity: memberchk(Name/X, Q), Name =.. [_, N], atom_concat(d_, N, QName), atom_concat(i_r_balance_, QName, BalanceName), % update the quantity list: NQ = [BalanceName/I|Q]. % add_to_balance2(+Addlist, -Leftlist, -Rightlist) add_to_balance([], [], []). add_to_balance([up(Q)|Tail], Left, [I|Right]):- map_list(Q, [I]), add_to_balance(Tail, Left, Right). add_to_balance([down(Q)|Tail], [I|Left], Right):- map_list(Q, [I]), add_to_balance(Tail, Left, Right). add_to_balance([noforce(_Q)|Tail], Left, Right):- add_to_balance(Tail, Left, Right). % get_balance_sign(+Influence, +Derivable, -NewInfluence) % returns: noforce if influencing quantity is zero, otherwise, leaves influence direction intact, % but changes from pos/neg to up/down to indicate, that influence has a known relation to zero. get_balance_sign(up(Quantity), _, up(Quantity)):- !. get_balance_sign(down(Quantity), _, down(Quantity)):- !. get_balance_sign(noforce(Quantity), _, noforce(Quantity)):- !. get_balance_sign(pos(Quantity), Relations, Result):- get_quantity_sign(Quantity, Relations, Sign), !, (Sign = zero -> Result = noforce(Quantity); Result = up(Quantity) ). get_balance_sign(neg(Quantity), Relations, Result):- get_quantity_sign(Quantity, Relations, Sign), !, (Sign = zero -> Result = noforce(Quantity); Result = down(Quantity) ). get_sign(pos(Quantity), Relations, Sign):- get_quantity_sign(Quantity, Relations, Sign). get_sign(neg(Quantity), Relations, Sign):- get_quantity_sign(Quantity, Relations, QSign), inverse_sign(QSign, Sign). inverse_sign(neg, pos). inverse_sign(pos, neg). inverse_sign(zero, zero). % FL may 07: with zero pointer 0, there is never a x = 0 relation: % so a special clause for the zero pointer is needed. get_quantity_sign(Quantity, _Relations, zero):- list_map([0], Quantity), % FL [] is old, now bitvector(1) [0] indicates zero !. get_quantity_sign(Quantity, Relations, Sign):- list_map([0], M), % FL [] is old, now bitvector(1) [0] indicates zero member(relation(Quantity, Relation, M), Relations), zero_relation_sign(Relation, Sign), !. get_quantity_sign(Quantity, Relations, Sign):- list_map([0], M), % FL [] is old, now bitvector(1) [0] indicates zero member(relation(M, Relation, Quantity), Relations), inverse(Relation, Inverse), zero_relation_sign(Inverse, Sign), !. % zero_relation_sign(R, Sign): % if a parameter has relation R to 0, return Sign zero_relation_sign(>, pos). % zero_relation_sign(>=, pos_zero). zero_relation_sign(=, zero). zero_relation_sign(<, neg). % zero_relation_sign(=<, neg_zero). % get_balance_result(+Quantity, +Relations, -Sign):- % New for garp 2.0 % Like get quantity sign, but always succeeds: % returns a sign, e.g. pos, or a list of possibilities in case of ambiguity % e.g. [pos,zero] or [pos, zero, neg] get_balance_result(Quantity, Relations, Sign):- list_map([0], M), member(relation(Quantity, Relation, M), Relations), zero_relation_signs(Relation, Sign), !. get_balance_result(Quantity, Relations, Sign):- list_map([0], M), member(relation(M, Relation, Quantity), Relations), inverse(Relation, Inverse), zero_relation_signs(Inverse, Sign), !. get_balance_result(_, _, [neg, zero, pos]). zero_relation_signs(>, pos). zero_relation_signs(>=, [zero, pos]). zero_relation_signs(=, zero). zero_relation_signs(<, neg). zero_relation_signs(=<, [neg, zero]). % replace quantities with their intern representation in a list of adders adders_quantities([], [], Qio, Qio). adders_quantities([ adder(Q, L) | T ], [ adder(IQ, IL) | NT ], Qin, Qout):- intern_quantities([ pos(Q) | L ], [ pos(IQ) | IL ], Qin, Qnew), adders_quantities(T, NT, Qnew, Qout). intern_quantities([], [], Qio, Qio). intern_quantities([pos(Quantity)|T], [pos(Intern)|NT], Qin, Qout):- memberchk(Quantity/Item, Qin), !, list_map([Item], Intern), intern_quantities(T, NT, Qin, Qout). intern_quantities([pos(Quantity)|T], [pos(Intern)|NT], Qin, Qout):- flag(q_cnt, P, 0), /* increase q_cnt */ I is P + 1, flag(q_cnt, _, I), list_map([I], Intern), intern_quantities(T, NT, [Quantity/I|Qin], Qout), !. intern_quantities([neg(Quantity)|T], [neg(Intern)|NT], Qin, Qout):- member(Quantity/Item, Qin), !, list_map([Item], Intern), intern_quantities(T, NT, Qin, Qout). intern_quantities([neg(Quantity)|T], [neg(Intern)|NT], Qin, Qout):- flag(q_cnt, P, 0), /* increase q_cnt */ I is P + 1, flag(q_cnt, _, I), list_map([I], Intern), intern_quantities(T, NT, [Quantity/I|Qin], Qout), !. % -------------------------------------------------- %% % % Second Order Derivative Influence Resolution % % -------------------------------------------------- %% % resolve_adders(+Adders, +Cin, -Cout) % - change Adders from extern to intern representation % - apply closed world on all quantities (under switch control) % this means setting derivatives of unaffected quantities to zero. % - resolve the resulting adders within Cio context. resolve_2ndorder_adders(_Adders, _AdderStrings, Cin, Cin, [], _):- flag(second_order_derivatives, F, F), algorithm_assumption_flag(F, fail, second_order_derivatives), !. resolve_2ndorder_adders(Adders, AdderStrings, Cin, Cout, Results, Constraints):- flag(second_order_derivatives, F, F), algorithm_assumption_flag(F, true, second_order_derivatives), etrace(solve_resolve_2ndorder_start, _, resolve), translate_adders_to_2ndorder(Adders, Adders2Tracer), cio_q_nq(Cin, Cnew1, Q, NQ), adders_quantities(Adders2Tracer, Adders2Intern, Q, NQ), % convert adderlist to intern representation Cin = Cout, !, flag(cw_assumption, Flag, Flag), ( algorithm_assumption_flag(Flag, fail, cw_assumption) -> Cnew2 = Cnew1 ; % set unknown, uninfluenced, influencing quantities to zero etrace(solve_cw_start, _, resolve), apply_closed_world_to_adders(NQ, Adders2Intern, Cnew1, Cnew2) ), resolve_2ndorder_adders(Adders2Intern, Adders2Tracer, AdderStrings, Cnew2, _CioResults, true, [], Results, Constraints), etrace(solve_resolve_2ndorder_done, _, resolve). % no progress, discard adders % BEFORE and derive unknown for these quantities. % but no added info in there. resolve_2ndorder_adders(_UnknownAdders, _UnknownTrAdders, _AdderStrings, Cio, Cio, false, Results, Results, _). % derive_unknown_2ndorder(UnknownAdders, UnknownTrAdders, ResultsIn, ResultsOut). % first time, or progress resolve_2ndorder_adders(Adders, TrAdders, AddStrings, Cin, Cout, true, ResultsIn, ResultsOut, Constraints):- resolve_2ndorder(Adders, TrAdders, AddStrings, Cin, Cnew, [], Unresolved, [], UnTrAd, [], UnAddStr, Progress, ResultsIn, Results1, Constraints), resolve_2ndorder_adders(Unresolved, UnTrAd, UnAddStr, Cnew, Cout, Progress, Results1, ResultsOut, Constraints). translate_adders_to_2ndorder([], []). translate_adders_to_2ndorder([adder(derivative(Q), AddList)|Tail], [adder(second_derivative(Q), AddList2)|TracerTail]):- translate_addlist_to_2ndorder(AddList, AddList2), translate_adders_to_2ndorder(Tail, TracerTail). translate_addlist_to_2ndorder([], []). translate_addlist_to_2ndorder([pos(derivative(Q))|Tail], [pos(second_derivative(Q))|NT]):- translate_addlist_to_2ndorder(Tail, NT). translate_addlist_to_2ndorder([neg(derivative(Q))|Tail], [neg(second_derivative(Q))|NT]):- translate_addlist_to_2ndorder(Tail, NT). translate_addlist_to_2ndorder([pos(value(Q))|Tail], [pos(derivative(Q))|NT]):- translate_addlist_to_2ndorder(Tail, NT). translate_addlist_to_2ndorder([neg(value(Q))|Tail], [neg(derivative(Q))|NT]):- translate_addlist_to_2ndorder(Tail, NT). % resolve_2ndorder(+Adders, +TracerAdders, +Cin, -Cout, +[], % -Unresolved, +[], -UnresolvedTracerAdders, -Progress) % Very much like resolve/9, see comments there... % but on ambiguous result: discard, continue with next. % all done, return results: resolve_2ndorder([], [], [], Cin, Cin, Unresolved, Unresolved, UTracer, UTracer, UStrings, UStrings, false, Results, Results, _). % adder incomplete -> put on Unresolved list resolve_2ndorder([adder(Q, AddList)|Tail], [adder(TrQ, TrList)|TrTail], [adder(StrQ, TrString)|StrTail], Cin, Cout, Unresolved, UnresolvedOut, UTracer, UTracerOut, UStr, UStrOut, Progress, ResultsIn, ResultsOut, Constraints) :- cio_q_d(Cin, QList, Derivable), % check quantities in Addlist for known values, % transform pos, neg to up, down & noforce, % return incomplete or complete to indicate if all values are known complete_2ndorder_adder(AddList, Derivable, NewAddList, Incomplete, TrList, TracerAddList), Incomplete = incomplete, !, %is it ok to cut here? because below it says: note this may fail... choicepoint seems unnecessary... Fl Feb 07 tempflo etrace(solve_2ndorder_ir_set, [TrQ, TrList, QList, Derivable], resolve), etrace(solve_2ndorder_ir_unres, [TracerAddList], resolve), % note this may fail resolve_2ndorder(Tail, TrTail, StrTail, Cin , Cout, [adder(Q, NewAddList)|Unresolved], UnresolvedOut, [adder(TrQ, TrList)|UTracer], UTracerOut, [adder(StrQ, TrString)|UStr], UStrOut, Progress, ResultsIn, ResultsOut, Constraints). % adder complete, single influence -> evaluate & add results resolve_2ndorder([adder(Q, [Influence])|Tail], [adder(TrQ, [TrInf])|TrTail], [adder(_StrQ, TrString)|StrTail], Cin, Cout, UnresolvedIn, UnresolvedOut, UTracer, UTracerOut, UStrIn, UStrOut, Progress, ResultsIn, ResultsOut, Constraints) :- cio_q_d(Cin, QList, Derivable), get_2ndorder_sign(Influence, Derivable, Sign), !, etrace(solve_2ndorder_ir_set, [TrQ, [TrInf], QList, Derivable], resolve), etrace(solve_2ndorder_ir_single_res, [TrInf, Sign], resolve), etrace(solve_2ndorder_ir_res, [TrQ, Sign], resolve), add_2ndorder_resolution_result(Q, TrQ, Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [Unresolved1, NewTail]), % ANA test_assumed_sod_constraints(Constraints, TrQ, Sign), !, % April 08: for tracing/visualize also single influence sod's are recorded % get the derivative sign for our SOD List get_derivative_sign(TrQ, QList, Derivable, Der), TrQ = second_derivative(X), resolve_2ndorder(NewTail, TrTail, StrTail, Cnew , Cout, Unresolved1, UnresolvedOut, UTracer, UTracerOut, UStrIn, UStrOut, TailProgress, [sod_info(X, Der, Sign, [TrInf], TrString)|ResultsIn], ResultsOut, Constraints). % adder complete -> first try sign addition. if that does not work: % next clause: construct balance, evaluate & add results resolve_2ndorder([adder(Q, AddList)|Tail], [adder(TrQ, TrList)|TrTail], [adder(_StrQ, TrString)|StrTail], Cin, Cout, UnresolvedIn, UnresolvedOut, UTracer, UTracerOut, UStrIn, UStrOut, Progress, ResultsIn, ResultsOut, Constraints) :- cio_q_d(Cin, QList, Derivable), try_sign_addition(AddList, Derivable, zero, Sign, TrList, TrEffects),% NB fails if ambiguous !, etrace(solve_2ndorder_ir_set, [TrQ, TrList, QList, Derivable], resolve), etrace(solve_2ndorder_ir_add, [TrEffects], resolve), etrace(solve_2ndorder_ir_res, [TrQ, Sign], resolve), TrQ = second_derivative(X), add_2ndorder_resolution_result(Q, TrQ, Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]), test_assumed_sod_constraints(Constraints, TrQ, Sign), !, % get the derivative sign for our SOD List get_derivative_sign(TrQ, QList, Derivable, Der), % note this may fail resolve_2ndorder(NewTail, TrTail, StrTail, Cnew , Cout, NewUnresolved, UnresolvedOut, UTracer, UTracerOut, UStrIn, UStrOut, TailProgress, [sod_info(X, Der, Sign, TrList, TrString)|ResultsIn], ResultsOut, Constraints). % adder complete -> construct balance, evaluate & add results resolve_2ndorder([adder(Q, AddList)|Tail], [adder(TrQ, TrList)|TrTail], [adder(_StrQ, TrString)|StrTail], Cin, Cout, UnresolvedIn, UnresolvedOut, UTracer, UTracerOut, UStrIn, UStrOut, Progress, ResultsIn, ResultsOut, Constraints) :- cio_q_d(Cin, QList, Derivable), % check quantities in Addlist for known values, transform pos, neg to up, down & noforce complete_2ndorder_adder(AddList, Derivable, CompleteAddList, Incomplete, _, _), Incomplete = complete, etrace(solve_2ndorder_ir_set, [TrQ, TrList, QList, Derivable], resolve), etrace(solve_2ndorder_ir_bal, [TrList, Pos, Neg], resolve), % make_balance [BalanceValue, min1, min2, ...] = [pos1, pos2, ...] (intern representation) make_balance(Q, CompleteAddList, Cin, Ctest1, Balance, BV), % add and evaluate balance relation in testcio (balance not added to relations) % try_balance gives feedback if append_relation fails try_balance(append_relation(Balance, Ctest1, Ctest2, _, false)), % Analyse simple & zero equality should be false not to create an invalid Q pointers to testcio indexes % get value of balancequantity cio_d(Ctest2, Derivable2), %test quantity sign (also >= and =<) get_balance_result(BV, Derivable2, Sign),%because no analyse zero & simple equality, BV is still a valid pointer !, %no backtracking on this part TrQ = second_derivative(X), ( memberchk(Sign, [zero, pos, neg]) % definitive result -> ( etrace(solve_2ndorder_ir_bal_res, [TrQ, Pos, Neg, Sign], resolve), add_2ndorder_resolution_result(Q, TrQ, Sign, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]), test_assumed_sod_constraints(Constraints, TrQ, Sign), Result = Sign, !) ; % else: ambiguous result, Sign is a list of possibilities in this case % discard any results, continue. ( %flag(assume_steady_derivatives, Flag, Flag), %NB FL may 07 hardcoded off now, switch needed %Flag = fail, ( %algorithm_assumption_flag(Flag, fail, assume_steady_derivatives) true -> ambiguous_sign(Sign, Result), etrace(solve_2ndorder_ir_bal_res, [TrQ, Pos, Neg, Result], resolve), add_2ndorder_resolution_result(Q, TrQ, Result, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]) %test_assumed_sod_constraints(Constraints, TrQ, Sign)% not needed here, ambiguous is always compatible with assumed termination... ; % in case agressive CW assumption is on, assume a zero effect in case of ambiguity Result = zero, etrace(solve_2ndorder_ir_bal_res_assume_zero, [TrQ, Pos, Neg, Result], resolve), add_2ndorder_resolution_result(Q, TrQ, Result, Cin, Cnew, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]) ) ) ), get_derivative_sign(TrQ, QList, Derivable, Der), %should always be known, because normal IR was already done on this par % note this may fail resolve_2ndorder(NewTail, TrTail, StrTail, Cnew , Cout, NewUnresolved, UnresolvedOut, UTracer, UTracerOut, UStrIn, UStrOut, TailProgress, [sod_info(X, Der, Result, TrList, TrString)|ResultsIn], ResultsOut, Constraints). % get derivative for in the sod-info (second order derivative) get_derivative_sign(second_derivative(Qty), QList, Derivable, Der):- memberchk(derivative(Qty)/I, QList), list_map([I], DerQty), get_quantity_sign(DerQty, Derivable, Der), !. %should always be known, because normal IR was already done on this par % On an assumed transition the 2nd order derivative cannot indicate % the reverse transition, in this case the assumption was wrong and % the transition should fail test_assumed_sod_constraints(Constraints, second_derivative(Q), Sign):- member(Sign/Q, Constraints), TrQ = second_derivative(Q), etrace(solve_2ndorder_wrong_assumed_derivative_termination, [TrQ, Sign], [general, resolve]), !, fail. test_assumed_sod_constraints(_Constraints, _TrQ, _Sign). % complete_adder: takes an addList and evaluates to zero % if sign is known then change notation to up/down/noforce % otherwise return incomplete and semi transformed list. % unknown quantities are passed on for tracer complete_2ndorder_adder([], _, [], complete, [], []):-!. %not yet incomplete -> complete complete_2ndorder_adder([], _, [], incomplete, [], []):-!. %already incomplete complete_2ndorder_adder([H|T], Derivable, [Result | NewAddList], Incomplete, [_|TT], TraceList):- get_2ndorder_balance_sign(H, Derivable, Result), %returns: up(Q), down(Q), noforce(Q) or fails !, complete_2ndorder_adder(T, Derivable, NewAddList, Incomplete, TT, TraceList). % could not get quantity sign -> set incomplete indicator & continue with rest of list. complete_2ndorder_adder([H|T], Derivable, [H | NewAddList], incomplete, [HT|TT], [HT|TraceTail]):- !, complete_2ndorder_adder(T, Derivable, NewAddList, incomplete, TT, TraceTail). get_2ndorder_balance_sign(up(Quantity), _, up(Quantity)):- !. get_2ndorder_balance_sign(down(Quantity), _, down(Quantity)):- !. get_2ndorder_balance_sign(noforce(Quantity), _, noforce(Quantity)):- !. get_2ndorder_balance_sign(pos(Quantity), Relations, Result):- get_2ndorder_quantity_sign(Quantity, Relations, Sign), !, (Sign = zero -> Result = noforce(Quantity); Result = up(Quantity) ). get_2ndorder_balance_sign(neg(Quantity), Relations, Result):- get_2ndorder_quantity_sign(Quantity, Relations, Sign), !, (Sign = zero -> Result = noforce(Quantity); Result = down(Quantity) ). get_2ndorder_quantity_sign(Quantity, _Relations, zero):- list_map([0], Quantity), !. get_2ndorder_quantity_sign(Quantity, Relations, Sign):- list_map([0], M), member(relation(Quantity, Relation, M), Relations), zero_relation_sign_2ndorder(Relation, Sign), !. get_2ndorder_quantity_sign(Quantity, Relations, Sign):- list_map([0], M), member(relation(M, Relation, Quantity), Relations), inverse(Relation, Inverse), zero_relation_sign_2ndorder(Inverse, Sign), !. zero_relation_sign_2ndorder(>, pos). zero_relation_sign_2ndorder(>=, pos_zero). zero_relation_sign_2ndorder(=, zero). zero_relation_sign_2ndorder(<, neg). zero_relation_sign_2ndorder(=<, neg_zero). zero_relation_sign_2ndorder(=?=, unknown). ambiguous_sign([neg, zero, pos], unknown). ambiguous_sign([zero, pos], pos_zero). ambiguous_sign([neg, zero], neg_zero). get_2ndorder_sign(pos(Quantity), Relations, Sign):- get_2ndorder_quantity_sign(Quantity, Relations, Sign). get_2ndorder_sign(neg(Quantity), Relations, Sign):- get_2ndorder_quantity_sign(Quantity, Relations, QSign), inverse_2ndorder_sign(QSign, Sign). inverse_2ndorder_sign(neg, pos). inverse_2ndorder_sign(pos, neg). inverse_2ndorder_sign(zero, zero). inverse_2ndorder_sign(pos_zero, neg_zero). inverse_2ndorder_sign(neg_zero, pos_zero). add_2ndorder_resolution_result(_Q, _TrQ, unknown, Cio, Cio, Progress, Progress, [Unresolved, Tail], [Unresolved, Tail]):- !. add_2ndorder_resolution_result(Q, _TrQ, pos_zero, Cin, Cout, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]):- !, list_map([0], Empty), right_order(relation(Q, >=, Empty), Relation), append_split(UnresolvedIn, Tail, I, OtherAddersIn), % makes one list, for easy passing on with append relatoin. pointers can be updated, but list stays intact. try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(NewUnresolved, NewTail, I, OtherAddersOut), % splits the list again at the same point. (Added = [], Progress=TailProgress; Progress=true), !. add_2ndorder_resolution_result(Q, _TrQ, neg_zero, Cin, Cout, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]):- !, list_map([0], Empty), right_order(relation(Q, =<, Empty), Relation), append_split(UnresolvedIn, Tail, I, OtherAddersIn), % makes one list, for easy passing on with append relatoin. pointers can be updated, but list stays intact. try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(NewUnresolved, NewTail, I, OtherAddersOut), % splits the list again at the same point. (Added = [], Progress=TailProgress; Progress=true), !. add_2ndorder_resolution_result(Q, _TrQ, pos, Cin, Cout, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]):- !, list_map([0], Empty), right_order(relation(Q, >, Empty), Relation), append_split(UnresolvedIn, Tail, I, OtherAddersIn), % makes one list, for easy passing on with append relatoin. pointers can be updated, but list stays intact. try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(NewUnresolved, NewTail, I, OtherAddersOut), % splits the list again at the same point. (Added = [], Progress=TailProgress; Progress=true), !. add_2ndorder_resolution_result(Q, _TrQ, neg, Cin, Cout, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]):- !, list_map([0], Empty), right_order(relation(Q, <, Empty), Relation), append_split(UnresolvedIn, Tail, I, OtherAddersIn), % makes one list, for easy passing on with append relatoin. pointers can be updated, but list stays intact. try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(NewUnresolved, NewTail, I, OtherAddersOut), % splits the list again at the same point. (Added = [], Progress=TailProgress; Progress=true), !. add_2ndorder_resolution_result(Q, _TrQ, zero, Cin, Cout, Progress, TailProgress, [UnresolvedIn, Tail], [NewUnresolved, NewTail]):- !, list_map([0], Empty), right_order(relation(Q, =, Empty), Relation), append_split(UnresolvedIn, Tail, I, OtherAddersIn), % makes one list, for easy passing on with append relatoin. pointers can be updated, but list stays intact. try_append(append_relation(Relation, Cin, Cout, Added, true, OtherAddersIn, OtherAddersOut)), split_append(NewUnresolved, NewTail, I, OtherAddersOut), % splits the list again at the same point. (Added = [], Progress=TailProgress; Progress=true), !. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BOUNDARY NEW > OLD %%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* get_derivable(L, R, Derivable, Rel):- memberchk(relation(L, Rel, R), Derivable), !. get_derivable(L, R, Derivable, Rel):- memberchk(relation(R, Rel1, L), Derivable), inverse(Rel1, Rel), !. incompatible_rels(>, <). incompatible_rels(>, =<). incompatible_rels(>, =). incompatible_rels(>=, <). incompatible_rels(=, <). incompatible_rels(=, >). incompatible_rels(<=, >). incompatible_rels(<, >). incompatible_rels(<, >=). incompatible_rels(<, =). */ /* * append_relation(+Relation, +Cin, -Cout, -Appended, +AnalyseSimple) * append_relation_all(+RelationList, .. idem ..). * append a relation/relationlist to the cio structure * Relation in intern representaion * Appended: relations appended (i.e. not already derivable) * AnalyseSimple: true -> replace a with b if a=b is derived * false -> don't replace * FL nov 07 INeq overhaul % FL december 2004: % In the influence resolution procedure in garp 2.0 the list of adders % (influences to add) is passed on when appending a relation. % This way, AnalyseSimpleEquality and Zero Analysis can % change pointers/bits, without invalidating the adders. % other calls do not yet use these arguments so this extra clause % is added to catch old style calls. append_relation(R, Cin, Cout, Ap, As):- append_relation(R, Cin, Cout, Ap, As, [],[]). % fail if relation is invalid (i.e. a > a, or a+b > a+b) % FL june 07: new position of this check: before simplification append_relation(Intern, Cin, _, _, _, _, _):- illegal_relation(Intern), ( etrace(solve_derived_invalid, _, inequality) -> % only do the rest of the work if tracer is on... cio_q(Cin, Q), etrace(solve_invalid_input, [Intern, Q], inequality) ; true ), !, fail. % FL december 2004: Solve does simplification of results: % x + y = x + z -> y = z, % but not simplification of the input... This is done here, before % the actual appendrelation2 call. % Last two arguments are Adders passed on for bit change updates. % (see: analyse zero equality) append_relation(R, Cin, Cout, Ap, As, Addersin, Addersout):- simplify_relations([R], [R1]), !, append_relation2(R1, Cin, Cout, Ap, As, Addersin, Addersout). FL june 07: old position of illegal_rel check % fail if relation is invalid (i.e. a > a, or a+b > a+b) % FL december 2004: new name & 2 extra arguments, see above. commmented out append_relation2(Intern, Cin, _, _, _, _, _):- illegal_relation(Intern), ( etrace(solve_derived_invalid, _, inequality) -> % only do the rest of the work if tracer is on... cio_q(Cin, Q), etrace(solve_invalid_input, [Intern, Q], inequality) ; true ), !, fail. FL nov 07 INeq overhaul % relation is already derivable % FL december 2004: new name & 2 extra arguments, see above. append_relation2(Intern, Cio, Cio, [], _, Ad, Ad):- cio_d(Cio, Derivable), is_derivable(Intern, Derivable), % etrace(solve_derivable_rel, _, add_relation), gives too many extra statements in e.g. Inf Res. !. % append relation (fail if inconsistent) % FL december 2004: new name (+2) & 2 extra arguments, see above. append_relation2(AppendOne, Cin, Cout, [AppendOne], DoAnalyseSimple, Adders, NAdders):- cio_r_nr_d_nd_q_nq_c_nc(Cin, Cnew, Relations, SortedFinalAllRelations, Derivable, SortedFinalAllNewDerivable, Q, NQ, C, NC), append([AppendOne], Derivable, KnownDerivable), % all relations we don't want to derive again solve([[]/AppendOne], Relations, Relations, KnownDerivable, NewDerived, Q), % fails is inconsistent append(KnownDerivable, NewDerived, AllNewDerivable), % all relations we have derived now append([AppendOne], NewDerived, AllNew), % all new relations append([AppendOne], Relations, AllRelations), % all relations used as a base %remove_weaker(AllNew, AllNew, StrongAllNew), remove_weaker2(AllNew, AllNew, StrongAllNew), % remove a>=b if a>b is found remove_weaker(StrongAllNew, AllRelations, StrongAllRelations), %remove_weaker2(AllRelations, AllRelations, StrongAllRelations), % also in base remove_weaker(StrongAllNew, AllNewDerivable, StrongAllNewDerivable), %remove_weaker2(AllNewDerivable, AllNewDerivable, StrongAllNewDerivable), % also in all derived flag(analyse_simple_found_contradiction, _, false), analyse_simple_equality(DoAnalyseSimple, StrongAllNew, Q, Q1, StrongAllNew, SimpleAllNew, StrongAllRelations, SimpleAllRelations, StrongAllNewDerivable, SimpleAllNewDerivable, C, C1, Adders, Adders1), % Note that adderlists are passed on % replace a with b if a=b analyse_zero_equality(DoAnalyseSimple, SimpleAllNew, FinalAllNew, SimpleAllNewDerivable, FinalAllNewDerivable, SimpleAllRelations, FinalAllRelations, Q1, NQ, C1, NC, Adders1, Adders2), % Note that adderlists are passed on % FL december 2004 new in garp 2.0: zero analysis = analyse simple equality using: % x = 0, y = 0 -> x=y pattern sort(FinalAllRelations, SortedFinalAllRelations), % remove duplicates sort(FinalAllNew, SortedFinalAllNew), sort(FinalAllNewDerivable, SortedFinalAllNewDerivable), !, inspect_correspondence(SortedFinalAllNew, Cnew, Cout, DoAnalyseSimple, Adders2, NAdders). % inspect if and iff statements (correspondence) % FL december 2004: 2 extra arguments, see above. append_relation_all(Append, Cin, Cout, AppendNotDerivable, DoAnalyseSimple):- append_relation_all(Append, Cin, Cout, AppendNotDerivable, DoAnalyseSimple, [], []). % fail if invalid input % FL june 07 new position of this check: before simplification append_relation_all(InternL, Cin, _, _, _, _, _):- member(Intern, InternL), illegal_relation(Intern), ( etrace(solve_derived_invalid, _, inequality) -> % only do the rest of the work if tracer is on... cio_q(Cin, Q), etrace(solve_invalid_input, [Intern, Q], inequality) ; true ), !, fail. % FL december 2004: Solve does simplification of results: % x + y = x + z -> y = z, % but not simplification of the input... This is done here, before % the actual appendrelation2 call. % Last two arguments are Adders passed on for bit change updates. % (see: analyse zero equality) append_relation_all(Append1, Cin, Cout, AppendNotDerivable, DoAnalyseSimple, Adin, Adout):- simplify_relations(Append1, Append), !, append_relation_all2(Append, Cin, Cout, AppendNotDerivable, DoAnalyseSimple, Adin, Adout). old position of this check... % fail if invalid input % FL december 2004: new name & 2 extra arguments, see above. append_relation_all2(InternL, Cin, _, _, _, _, _):- member(Intern, InternL), illegal_relation(Intern), ( etrace(solve_derived_invalid, _, inequality) -> % only do the rest of the work if tracer is on... cio_q(Cin, Q), etrace(solve_invalid_input, [Intern, Q], inequality) ; true ), !, fail. % append relations (fail if inconsistent) % Adderlist is passed on for bit change updates: see analyse zero equality % results in 2 extra arguments append_relation_all2(Append, Cin, Cout, AppendNotDerivable, DoAnalyseSimple, A, NA):- cio_r_nr_d_nd_q_nq_c_nc(Cin, Cnew, Relations, SortedFinalAllRelations, Derivable, SortedFinalAllNewDerivable, Q, NQ, C, NC), remove_weaker(Append, Append, StrongAppend), remove_derivable(StrongAppend, Derivable, AppendNotDerivable), !, ( AppendNotDerivable == [], Cin = Cout, A = NA ; append(AppendNotDerivable, Derivable, KnownDerivable), % all relations we don't want to derive again append(AppendNotDerivable, Relations, KnownRelations), add_empty_parents(AppendNotDerivable, AppendNotDerivable2), solve(AppendNotDerivable2, KnownRelations, KnownRelations, KnownDerivable, NewDerived, Q), % fails is inconsistent% add relation, succeeds if result is consistent, % has no term twice and can be simplified % if inconsistent: fail solve % if no simplification, or already derivable, or evident: append(KnownDerivable, NewDerived, AllNewDerivable), % all relations we have derived now append(AppendNotDerivable, NewDerived, AllNew), % all new relations append(AppendNotDerivable, Relations, AllRelations), % all relations used as a base %remove_weaker(AllNew, AllNew, StrongAllNew), remove_weaker2(AllNew, AllNew, StrongAllNew), % remove a>=b if a>b is found remove_weaker(StrongAllNew, AllRelations, StrongAllRelations), %remove_weaker2(AllRelations, AllRelations, StrongAllRelations), % also in base remove_weaker(StrongAllNew, AllNewDerivable, StrongAllNewDerivable), %remove_weaker2(AllNewDerivable, AllNewDerivable, StrongAllNewDerivable), % also in all derived analyse_simple_equality(DoAnalyseSimple, StrongAllNew, Q, NQ, StrongAllNew, FinalAllNew, StrongAllRelations, FinalAllRelations, StrongAllNewDerivable, FinalAllNewDerivable, C, NC, A, NA1), % Note that adderlists are passed on % replace a with b if a=b % analyse zero equality is not done here, because it is done in the % single version of append relation, % because it is exhaustive it is most efficient to do it once in a while. sort(FinalAllRelations, SortedFinalAllRelations), % remove duplicates sort(FinalAllNew, SortedFinalAllNew), sort(FinalAllNewDerivable, SortedFinalAllNewDerivable), !, inspect_correspondence(SortedFinalAllNew, Cnew, Cout, DoAnalyseSimple, NA1, NA) % inspect if and iff statements ), !. % remove_derivable(+ToInspect, +KnownRelations, -NotDerivable) % % remove all derivable relations (given Arg2) from Arg1 % */ /* remove_derivable([], _, []). remove_derivable([H|T], D, NT):- is_derivable(H, D), !, remove_derivable(T, D, NT). remove_derivable([H|T], D, [H|NT]):- remove_derivable(T, D, NT). */ /* -------------------------------------------------------------------- * solve(+NewRelations, +ToInspect, +AllKnown, +AllDerivable, -New) * * for each relation in NewRelations: * add first of NewRelations with all of ToInspect (= AllKnown on first call) * if a valid, not evident and not already known relation is found: * add it to NewRelations * Return only relations between two single quantities or constants * */ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % New approach to inequality reasoning: First the relations are divided % into contexts with shared, connected variables, thus minimizing % derivations between otherwise unconnected variables. % % A redo of add_relation would be good because now the contexts have to % be determined again and again. % % (caching is not possible: analyse zero etc. change pointers so they % should be adapted too, which is an equal amount of work.) % /* solve(NR, TO, K, D, New, Q):- split_contexts(NR, TO, K, D, Contexts), solve_contexts(Contexts, New, Q). %done solve_contexts([], [], _Q). % empty new relations >> skip (nb: does not save much, % only some flag calls solve_contexts([context([], _TO, _K, _D, _)|T], New, Q):- !, solve_contexts(T, New, Q). % solve context solve_contexts([context(NR, TO, K, D, _)|T], New, Q):- solve_core(NR, TO, K, D, N, Q), solve_contexts(T, NT, Q), append(N, NT, New). split_contexts(NR, TO, K, D, Contexts):- context_tag(D, TD), % construct first set of contexts using a tagged version of D which is a superset of NR, TO and K pointer_contexts(TD, NR, TO, K, PointerContexts1), % merge contexts with common elements merge_contexts(PointerContexts1, Contexts). context_tag([], []). context_tag([Rel|T], [Rel/CP|NT]):- determine_pointers(Rel, CP), context_tag(T, NT). %% %%%%%%% % take each element of D and put it in existing or new pointer context % pointer_contexts([], [], [], [], []). % make new context with H as single element of D and its pointers as % the new bitvector describing the context (contextpointers CP pointer_contexts([H/CP|T], NRin, TOin, Kin, [context(CNR, CTO, CK, [H], CP)|ContextT]):- insert_nr(H, NRin, NRout, CNR), insert_to_k(H, TOin, TOout, CTO), insert_to_k(H, Kin, Kout, CK), pointer_contexts(T, NRout, TOout, Kout, ContextT). %done insert_nr(_Rel, [], [], []). %fit insert_nr(Rel, [List/Rel|T], T, [List/Rel]):- !. %relation fits in context, done % insert_nr(Rel, T, NRout, NT). % no fit insert_nr(Rel, [H|T], [H|NRoutT], NR):- insert_nr(Rel, T, NRoutT, NR). %done insert_to_k(_Rel, [], [], []). %fit insert_to_k(Rel, [Rel|T], T, [Rel]):- !. % relation fits in context, done % insert_to_k(Rel, T, NRout, NT). % no fit insert_to_k(Rel, [H|T], [H|NRoutT], NR):- insert_to_k(Rel, T, NRoutT, NR). %%%%%%%%%%%%%%%% % merge_contexts([], []). % merge possible: extract all contexts from tail that have common % elements with current context merge_contexts([context(NR1, TO1, K1, D1, CP1)|T], RM):- select(context(NR2, TO2, K2, D2, CP2), T, Rest), map_intersection(CP1, CP2, bitvector(Common)), Common =\= 0, !, % common elements: merge contexts map_union(CP1, CP2, CP), append(NR1, NR2, NR), append(TO1, TO2, TO), append(K1, K2, K), append(D1, D2, D), % try to find more possible merges for this context merge_contexts([context(NR, TO, K, D, CP)|Rest], RM). % no merge possible merge_contexts([H|T], [H|TM]):- merge_contexts(T, TM). */ % % %%%%%%%%END NEWWWWW %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 /* cache_solve_result(_NR, _K, _D, _New):- flag(solve_caching, F, F), F\= 0, !. cache_solve_result(NR, K, D, New):- %hash_term(NR/K, Hash), % should be enough as an identifier %assertz(solve_cache(Hash, NR/K/D/New)). assertz(solve_cache(NR/K, D/New)). get_cached_solve_result(_NR, _K, _D, _New):- flag(solve_caching, F, F), F\= 0, !, fail. get_cached_solve_result(NR, K, D, New):- %hash_term(NR/K, Hash), %solve_cache(Hash, NR/K/D/New). solve_cache(NR/K, D/New). */ % ----------- resolve influences and proportional relations ------------ /*** FL december-2003: old resolve_adders from garp 1.7 *** * with partial closed world assumption * resolve_adders(Adders, Cin, Cout):- cio_q_nq(Cin, Cnew, Q, NQ), adders_quantities(Adders, NewAdders, Q, NQ), !, resolve_adders(NewAdders, Cnew, Cout, true). % fails if contradiction % no progress see if we can set some uninfluenced influence to zero % we must be conservative: % set a quantity to zero that is proportionalto / an influence on some % other quantity, if possible. Then try to find new results. % it is difficult to predict what will happen, because the quantity may % have all kinds of relations to other quantities, for instance: % % derivative(a) > derivative(b) % not very likely, but possible % prop_pos(c, a) % c is proportional to a % prop_pos(b, c) % b is proportional to c % assume a to be zero % derive: derivative(b) > zero % resolve: c = zero % resolve: b = zero -> contradiction % % so if the assumption fails, try another one, but don't fail the % complete predicate resolve_adders(Adders, Cin, Cout, false):- cio_q(Cin, Q), member(Value/DQ, Q), % a value or derivative list_map([DQ], DM), \+ memberchk(adder(DM, _), Adders), % not influenced itself member(adder(_, L), Adders), % it influences something ( memberchk(pos(DM), L); memberchk(neg(DM), L) ), cio_d(Cin, Der), % it's sign is not known \+ get_sign(pos(DM), Der, _), list_map([], ZeroMap), % it can be assumed append_relation(relation(DM, =, ZeroMap), Cin, Cnew, _, false), tracer(resolve, 'assuming %w is zero', [Value]), resolve_adders(Adders, Cnew, Cout, true), % now we are sure the assumption is safe ! !. resolve_adders(_, Cio, Cio, false). resolve_adders(Adders, Cin, Cout, true):- % first time, or progress resolve(Adders, Cin, Cnew, Unresolved, Progress), resolve_adders(Unresolved, Cnew, Cout, Progress). *** FL december-2003: end of old resolve_adders, new garp 2.0 starts here ***/ /* --- resolve_addders_2/4: old garp 1.7.2 ---- % no progress, discard adders and derive unknown for these quantities. resolve_adders(_, Cio, Cio, false). % first time, or progress resolve_adders(Adders, Cin, Cout, true):- resolve(Adders, Cin, Cnew, [], Unresolved, Progress), resolve_adders(Unresolved, Cnew, Cout, Progress). *** FL May 2004: garp 2.0 version (with tracer adders in normal representation) */ /*** FL december-2003: GARP 1.7 resolve clauses not weighing influences... *** % resolve: for each adder: determine signs of terms % if ambiguous (at least one positive and one negative term): discard adder % if positive, zero, or negative sum: add this result % if not all terms are known: put adder on Unresolved list resolve([], Cin, Cin, [], false). resolve([ adder(Q, AddList) | Tail ], Cin, Cout, NewUnresolved, Progress) :- (@tracer->>tell(resolve) -> %gp3 0.3 cio_q(Cin, QL), print_sum(Q, QL), write(' is influenced by / proportional to: '), forall(member(One, AddList), write_addone(One, QL)), nl, @tracer->>told, ! ; true ), cio_d(Cin, Derivable), sign_addlist(AddList, Derivable, first, NewAddList, Result), (@tracer->>tell(resolve) -> %gp3 0.3 print_sum(Q, QL), write(' evaluated to be influenced by / proportional to: '), forall(member(One, NewAddList), write_addone(One, QL)), nl, write('which is '), write_ln(Result), @tracer->>told, ! ; true ), !, add_adder_result(Q, Result, Cin, Cnew, Progress, RestProgress, NewUnresolved, Unresolved, adder(Q, NewAddList)), % note this may fail resolve(Tail, Cnew, Cout, Unresolved, RestProgress). write_addone(X, _):- var(X), !. write_addone(pos(One), QL):- write('positive '), print_sum(One, QL), tab(2), !. write_addone(neg(One), QL):- write('negative '), print_sum(One, QL), tab(2), !. write_addone(One, _):- write(One), tab(2), !. % incomplete information: add new adder to unresolved of tail, % Let progress be progress of tail add_adder_result(_, incomplete, Cin, Cin, Progress, Progress, [Adder|Unresolved], Unresolved, Adder):- !. % valid new result: let progress be true if not already derivable add_adder_result(Q, Sign, Cin, Cout, Progress, TailProgress, Unresolved, Unresolved, _):- zero_relation_sign(Relation, Sign), list_map([], Empty), right_order(relation(Q, Relation, Empty), Irel), append_relation(Irel, Cin, Cout, Added, false), (Added = [], Progress=TailProgress; Progress=true), !. % ambiguous influence on Q: return all possibilities (upon backtracking) add_adder_result(Q, ambiguous, Cin, Cout, Progress, TailProgress, Unresolved, Unresolved, _):- list_map([], Empty), member(Relation, [ <, =, > ]), right_order(relation(Q, Relation, Empty), Irel), once(( append_relation(Irel, Cin, Cout, Added, false), ( Added = [], Progress=TailProgress; Progress=true ) )). right_order(relation(L, <, R), relation(R, >, L)) :- !. right_order(relation(L, =<, R), relation(R, >=, L)) :- !. right_order(R, R):- !. % determine sum of influences/proportional relations sign_addlist([], _, Result, [], Result):- !. % if already ambiguous, don't mind the tail sign_addlist(_, _, ambiguous, [], ambiguous):- !. % get sign, determine sum, do tail (let head of newtail be sign of head) sign_addlist([H|T], Relations, PrevSign, [H|NewTail], Result):- memberchk(H, [ pos, zero, neg ]), !, sign_add(PrevSign, H, NewSign), sign_addlist(T, Relations, NewSign, NewTail, Result). sign_addlist([H|T], Relations, PrevSign, [Sign|NewTail], Result):- get_sign(H, Relations, Sign), !, sign_add(PrevSign, Sign, NewSign), sign_addlist(T, Relations, NewSign, NewTail, Result). % could not get sign: do tail (let Head of newtail be Head) % if previous + tail is ambiguous, sign is not important % otherwise return incomplete sign_addlist([H|T], Relations, PrevSign, [H|NewTail], Result):- sign_addlist(T, Relations, PrevSign, NewTail, NewResult), sign_incomplete(NewResult, Result). *** FL december-2003: New GARP 2.0 resolve clauses and subs below replace above ******/ /***** endnew FL june 07 *****/ /*** * FL december-2003: New GARP 2.0 code ends here, * sign_incomplete & sign_add unused by garp 2.0 *** sign_incomplete(ambiguous, ambiguous):- ! . % if already 'ambiguous' then unknown sign makes no difference sign_incomplete(_, incomplete):- ! . % we can't establish the correct sign sign_add(first, S, S). % first sign sign_add(zero, zero, zero). sign_add(pos, pos, pos). sign_add(neg, neg, neg). sign_add(pos, zero, pos). sign_add(zero, pos, pos). sign_add(neg, zero, neg). sign_add(zero, neg, neg). sign_add(pos, neg, ambiguous). sign_add(neg, pos, ambiguous). */ % sign_add(pos_zero, pos, pos). % sign_add(pos_zero, zero, pos_zero). % sign_add(pos_zero, neg, ambiguous). % ???????? % sign_add(neg_zero, neg, neg). % sign_add(neg_zero, zero, neg_zero). % sign_add(neg_zero, pos, ambiguous). % ???????? % sign_add(pos, pos_zero, pos). % sign_add(zero, pos_zero, pos_zero). % sign_add(neg, pos_zero, ambiguous). % ???????? % sign_add(neg, neg_zero, neg). % sign_add(zero, neg_zero, neg_zero). % sign_add(pos, neg_zero, ambiguous). % ???????? /*** * FL december-2003: get_sign still used in garp 2.0 (by other clauses then sign_add!) ***/ /* %done. derive_unknown_2ndorder([], [], Results, Results). derive_unknown_2ndorder([_|UnknownAddersTail], [adder(TrQ, _)|UnknownTrAddersTail], ResultsIn, ResultsOut):- TrQ = second_derivative(Q), derive_unknown_2ndorder(UnknownAddersTail, UnknownTrAddersTail, [Q/unknown|ResultsIn], ResultsOut). */ /* %% -------------------------------------------------------------------- %% ANALYSE SOLVE RESULTS: ANALYSE SIMPLE / ZERO EQUALITY ETC. %% -------------------------------------------------------------------- */ % analyse results of solve % if simple equality (between two parameters or a parameter and a constant, % (not zero)) % replace quantity pointer of one of these with the other in all relations % don't analyse when resolving influences/proportional relations % FL: in GARP 2.0 two extra arguments: adders in /out % these also contain pointers and should also be updated. % This one list should be left intact during the changes: it actually is two lists. % (programmers frivolity not to need 4 extra arguments) % New may 07: FIX to incorporate /* analyse_simple_equality(false, _, Q, Q, N, N, Relations, Relations, Derivable, Derivable, C, C, A, A). analyse_simple_equality(true, [], Q, Q, N, N, Relations, Relations, Derivable, Derivable, C, C, A, A). analyse_simple_equality(true, [ relation(Left, =, Right) | Tail ], Q, NQ, N, NN, Relations, NewRelations, Derivable, NewDerivable, C, NC, A, NA) :- map_list(Left, [ ILeft ]), map_list(Right, [ IRight ]), % NEW fl may 07: do not replace zero pointers... analyze zero takes care of that... ILeft \== 0, IRight \== 0, % should update later and remove analyze zero procedure: % if x = 0 or 0 = x is derived, it is always the zero pointer that is inserted % and in additions the zero pointer is left out. eg. x = 0, x + y = z -> y = z instead of y + 0 = z % like in process zero pointer replace_index_relations(ILeft, IRight, N, TN), replace_index_relations(ILeft, IRight, Relations, TRelations), replace_index_relations(ILeft, IRight, Derivable, TDerivable), replace_index_relations(ILeft, IRight, Tail, NTail), replace_index_relations_for_correspondence(ILeft, IRight, C, TC), % fails if that would produce a 'double quantity' % sets flag if contradiction found replace_index_in_adders(ILeft, IRight, A, TA), % Note the adder pointers are updated !, replace_index(ILeft, IRight, Q, TQ), analyse_simple_equality(true, NTail, TQ, NQ, TN, NN, TRelations, NewRelations, TDerivable, NewDerivable, TC, NC, TA, NA). analyse_simple_equality(true, [ _ | Tail ], Q, NQ, N, NN, Relations, NewRelations, Derivable, NewDerivable, C, NC, A, NA) :- flag(analyse_simple_found_contradiction, false, false), analyse_simple_equality(true, Tail, Q, NQ, N, NN, Relations, NewRelations, Derivable, NewDerivable, C, NC, A, NA). */ /* replace_index_relations_for_correspondence(_, _, [], [], _). replace_index_relations_for_correspondence(I1, I2, [ correspondence(L1, L2)/BV1/BV2 | T ], [correspondence(NL1, NL2)/NBV1/NBV2 | NT], Remove):- replace_index_relations_cor(I1, I2, L1, NL1), replace_index_relations_cor(I1, I2, L2, NL2), replace_context_pointer(Remove, _, BV1, NBV1), replace_context_pointer(Remove, _, BV2, NBV2), !, replace_index_relations_for_correspondence(I1, I2, T, NT, Remove). replace_index_relations_for_correspondence(I1, I2, [ if_correspondence(L1, L2)/BV1/BV2 | T ], [if_correspondence(NL1, NL2)/NBV1/NBV2 | NT], Remove):- replace_index_relations_cor(I1, I2, L1, NL1), replace_index_relations_cor(I1, I2, L2, NL2), replace_context_pointer(Remove, _, BV1, NBV1), replace_context_pointer(Remove, _, BV2, NBV2), !, replace_index_relations_for_correspondence(I1, I2, T, NT, Remove). */ /*** FL december-2003: END NEW ***/ /*----------------- analyse zero equality -------------------------*/ /* FL januari 2004 : analyse_zero_equality UPDATE FL mar 07: bitversion * * in Analyse-simple-equality, y is replaced by x if x=y, * to minimize the set of relations even further this is also done if: * q = zero & p = zero because p = q is now derivable in theory. * * To do this efficiently all pointers to quantities equal to zero are put in a * list. Then all these pointers are replaced by the pointer 0, * Note that pointers start counting at 1 so 0 is always free. * A lot of empty relations will come up like: 0 = 0, etc. these are removed * Some sums will contain a zero: x + 0 > y, these extra zeros are removed: x > y * Then zero = 0 is added to the relationsset. * * quantities are equal to zero if: q = zero, or if q >= zero & zero >= q, * * FL march 2004: The latter being unnecessary now that solve can deduct q=zero * in this case. * * Note that zero is mapped to the empty list: []. * * When applying the zeroset (changing pointers) relations are checked * on contradictions also. eg. 0>0, In that case the operation fails. (message displayed) * * This operation is done exhaustively on all known relations, not only on new relations, * arguments: * - the list with pointers equal to zero is easily obtained * - some call's do not analyse zero equality, but the smaller the relationset, * the faster solve works. * - double quantity equalities will not be affected. * * the operation is only performed when new relations contain a zero equality * this lowers the number of times this operation is carried out & saves time. * FL mar 07: NB it is done now always unless no relation in any set has a zero equality * * In Adders and Correspondences indexes are replaced also, * empty relations are not removed here. In correspondences they can do no harm. * * * * List notation is used, c-predicates for map operations being inadequate: * Todo: analyse-zero-equality using map operations and new c predicates. * Not neccesary however for time complexity is not a problem in practice * */ /* % analyse simple equality set to false: return input analyse_zero_equality(false, New, New, Derivable, Derivable, Base, Base, QList, QList, Corr, Corr, Adders, Adders). */ /* Switch removed, do it always, FL % analyse zero equality set to false in switch: return input analyse_zero_equality(_, New, New, Derivable, Derivable, Base, Base, QList, QList, Corr, Corr, Adders, Adders):- flag(no_analyse_zero, Flag, Flag), algorithm_assumption_flag(Flag, true, no_analyse_zero), !. */ /* % relations do not contain a zero equality: return input bitvector version analyse_zero_equality(true, New, New, Derivable, Derivable, Base, Base, QList, QList, Corr, Corr, Adders, Adders):- % smallest % map_list_for_relation_set(New, New1), %(select(relation(bitvector(1), =, bitvector(0)), New, NewR) ; New = NewR), \+ contains_equality_to_zero(New), % next % map_list_for_relation_set(Base, Base1), %(select(relation(bitvector(1), =, bitvector(0)), Base, BaseR) ; Base = BaseR), \+ contains_equality_to_zero(Base), % biggest set last % map_list_for_relation_set(Derivable, Derivable1), %(select(relation(bitvector(1), =, bitvector(0)), Derivable, DerivableR) ; Derivable = DerivableR), \+ contains_equality_to_zero(Derivable), !. % analyse zero equality bitvector version analyse_zero_equality(true, NewIn, NewOut, DerivableIn, DerivableOut, BaseIn, BaseOut, QListIn, QListOut, CorrIn, CorrOut, AddersIn, AddersOut):- % find all zero indexes % flstop, % map_list_for_relation_set(NewIn, New), % map_list_for_relation_set(DerivableIn, Derivable), % map_list_for_relation_set(BaseIn, Base), % map_list_for_correspondences(CorrIn, Corr), % map_list_for_adders(AddersIn, Adders), % get_zero_set(Derivable, ZerosL), % delete(ZerosL, 0, ZerosetL), % after the first zero-analysis, 0 is always part of the list get_bitwise_zero_set(DerivableIn, Zeros, BitZeros), % (Zeros = ZerosL ; flstop), delete(Zeros, 0, Zeroset), % after the first zero-analysis, 0 is always part of the list % delete bitwise 0 (NB bitmap 1 corresponds to [0]) NotZero is \1, BitZeroset is BitZeros /\ NotZero, InvBitZeroset is \BitZeros, % (Zeroset = ZerosetL ; flstop), % apply_zero_set(Derivable, Zeroset, Derivable1), % apply_zero_set(New, Zeroset, New1), % apply_zero_set(Base, Zeroset, Base1), % apply_zero_set_correspondences(Corr, Zeroset, Corr1), % apply_zero_set_adders(Adders, Zeroset, Adders1), % convert back to map representation % list_map_for_relation_set(New1, NewOutL), % list_map_for_relation_set(Derivable1, DerivableOutL), % list_map_for_relation_set(Base1, BaseOutL), % list_map_for_correspondences(Corr1, CorrOutL), % list_map_for_adders(Adders1, AddersOutL), % change all zero indexes to 0, % remove extra 0's & evident relations, % add [] = [0], % find contradiction? x>x then fail apply_bitwise_zero_set(DerivableIn, InvBitZeroset, DerivableOut), apply_bitwise_zero_set(NewIn, InvBitZeroset, NewOut), apply_bitwise_zero_set(BaseIn, InvBitZeroset, BaseOut), apply_bitwise_zero_set_correspondences(CorrIn, InvBitZeroset, CorrOut), apply_bitwise_zero_set_adders(AddersIn, BitZeroset, InvBitZeroset, AddersOut), % (NewOutL == NewOut ; flstop), % ( DerivableOut == DerivableOutL ; flstop), % ( BaseOut == BaseOutL ; flstop), % ( CorrOut == CorrOutL ; flstop), % ( AddersOut == AddersOutL ; flstop), % update Qlist replace_indexes_with_zeros(Zeroset, QListIn, QListOut). */ %*-------------- Analyse zero equality tools: ----------------------* /* % set of relations has at least one relation to zero. memberchk version with bitvectors...:) contains_equality_to_zero(List):- memberchk(relation(bitvector(1), =, bitvector(_)), List),!. contains_equality_to_zero(List):- memberchk(relation(bitvector(_), =, bitvector(1)), List),!. % get_bitwise_zero_set(+Relations, -Zeroset, -Bitwisezeros) % FL mar 07: bitwise version % find all quantities / pointers equal to zero in a relationset: % intern-list representation, use q = [] or q>=[] /\ []>=q % NOW: q = bitvector(0) etc. NB [] = bitvector(0), [0] is bitvector(1), % done get_bitwise_zero_set([], [], 0). % X equal to zero, add to zeroset get_bitwise_zero_set([relation(bitvector(X), =, bitvector(1))|Tail], [Xindex|ZTail], BitZeros):- % X is single item: e.g. list: [3], not addition like [3, 5] 1 is popcount(X), !, map_list(bitvector(X), [Xindex]), get_bitwise_zero_set(Tail, ZTail, BZTail), % take the union of tail and X BitZeros is BZTail \/ X. % X equal to zero, add to zeroset get_bitwise_zero_set([relation(bitvector(1), =, bitvector(X))|Tail], [Xindex|ZTail], BitZeros):- % X is single item: e.g. list: [3], not addition like [3, 5] 1 is popcount(X), !, map_list(bitvector(X), [Xindex]), get_bitwise_zero_set(Tail, ZTail, BZTail), % take the union of tail and X BitZeros is BZTail \/ X. % X equal or greater to zero if also inverse then add to zeroset get_bitwise_zero_set([relation(bitvector(X), >=, bitvector(1))|Tail], [Xindex|ZTail], BitZeros):- % X is single item: e.g. list: [3], not addition like [3, 5] 1 is popcount(X), bitwise_combine_to_zero(right, X, Tail), !, map_list(bitvector(X), [Xindex]), get_bitwise_zero_set(Tail, ZTail, BZTail), % take the union of tail and X BitZeros is BZTail \/ X. % X equal or greater to zero if also inverse then add to zeroset get_bitwise_zero_set([relation(bitvector(1), >=, bitvector(X))|Tail], [Xindex|ZTail], BitZeros):- % X is single item: e.g. list: [3], not addition like [3, 5] 1 is popcount(X), bitwise_combine_to_zero(left, X, Tail), !, map_list(bitvector(X), [Xindex]), get_bitwise_zero_set(Tail, ZTail, BZTail), % take the union of tail and X BitZeros is BZTail \/ X. % no zero equality, next relation get_bitwise_zero_set([_|Tail], ZTail, BitZeros):- get_bitwise_zero_set(Tail, ZTail, BitZeros). bitwise_combine_to_zero(right, X, Relations):- memberchk(relation(bitvector(1), >=, bitvector(X)), Relations). bitwise_combine_to_zero(left, X, Relations):- memberchk(relation(bitvector(X), >=, bitvector(1)), Relations). % apply zeros for Qlist, use analyse simple equality predicate. NB still List operated! replace_indexes_with_zeros([], In, In). replace_indexes_with_zeros([H|T], In, Out):- replace_index(H, 0, In, New), replace_indexes_with_zeros(T, New, Out). % apply_zero_set(+RelationsIn, +Zeroset, -RelationsOut) % apply zeros to set of relations in intern-list representation % append the relation 0 = zero, which is removed because evident. apply_bitwise_zero_set(RelationsIn, IZeroset, RelationsOut):- apply_bitwise_zeros(RelationsIn, IZeroset, RelationsOut). % Relations1), % fails in case of contradiction %append([relation(bitvector(1), =, bitvector(0))], Relations1, RelationsOut). % apply_zeros(+RelationsIn, +Zeroset, -RelationsOut) % apply zeros to set of relations in intern-bit representation, % fails with error report in case of a contradiction apply_bitwise_zeros([], _, []). % valid new relation after zero application, return, continue with rest apply_bitwise_zeros([relation(X, Rel, Y)|Tail], IZeros, Out):- % change indexes in zeroset to zero, leave one zero if no other indexes. change_bitwise_indexes_to_one_zero(X, IZeros, X1), change_bitwise_indexes_to_one_zero(Y, IZeros, Y1), bitwise_check_relation(X1, Rel, Y1, Result), % (0=0 (empty)) or x>x (contradiction) or x=x evident or x?y(normal) !, determine_b_c_r_result(Result, relation(X1, Rel, Y1), NewTail, Out), apply_bitwise_zeros(Tail, IZeros, NewTail). % keep relation determine_b_c_r_result(normal, relation(X, Rel, Y), NewTail, [relation(X, Rel, Y)|NewTail]). % discard relation determine_b_c_r_result(evident, _, Out, Out). % fail on contradiction determine_b_c_r_result(contradiction, _, _, _):- etrace(solve_zero_found_invalid, _, add_relation), !, fail. % change_indexes_to_one_zero(+BitmapIn, +Zerosmap, -BitmapOut) % remove all elements in zeros from list, leave one zero if no other % element/pointer is present % eg. [4, 5], zeros=5 -> [4] % eg. [5], zeros=5 -> [0] % eg. [], zeros=5 -> [] change_bitwise_indexes_to_one_zero(bitvector(0), _InvZeromap, bitvector(0)):- !. change_bitwise_indexes_to_one_zero(bitvector(In), InvZeromap, bitvector(Out)):- Out1 is In /\ InvZeromap, % subtract the zeroset ( Out1 == 0 % [] -> Out = 1 %-> [0] ; Out1 = Out % -> [X, Y, Z] ). % check relation for information value bitwise_check_relation(X, Rel, X, Result):- !, (Rel == > -> Result = contradiction % x > x is impossible ; Result = evident). % x = x or x >= x is evident. bitwise_check_relation(X, Rel, Y, Result):- %list is empty or contains only 0's only_bitwise_zeros_in_list(X), only_bitwise_zeros_in_list(Y), !, (Rel == > -> Result = contradiction % zero > zero is impossible ; Result = evident). % zero = zero is evident empty/no information value % case else: normal bitwise_check_relation(_X, _Rel, _Y, normal). % succeed if list is empty or contains only 0's % bitwise check is very easy... :) only_bitwise_zeros_in_list(bitvector(0)). only_bitwise_zeros_in_list(bitvector(1)). % apply for correspondences & adders % apply_zero_set_correspondences(+CorrespondencesIn, +Zeroset, -CorrespondencesOut) % Pointers in correspondences (intern-list representation) need to be updated. % all relations are returned: % an if_correspondence([relation( 0 > 0), ...) will not fire % an if_correspondence([relation( 0 = 0), ...) will fire % so information is preserved, however, correspondences containing no % information are formed. They can do no harm though. apply_bitwise_zero_set_correspondences([], _IZeroset, []). apply_bitwise_zero_set_correspondences([H|T], IZeroset, [NH|NT]):- H =.. [C, Relations1, Relations2], put_all_bitwise_zero_indexes(Relations1, IZeroset, NR1), put_all_bitwise_zero_indexes(Relations2, IZeroset, NR2), NH =.. [C, NR1, NR2], apply_bitwise_zero_set_correspondences(T, IZeroset, NT). % apply_zero_set_adders(+AddersIn, +Zeroset, +AddersOut) % Pointers in adders (intern-list representation) need to be updated also. apply_bitwise_zero_set_adders([], _Zeroset, _InvZeroset, []). apply_bitwise_zero_set_adders([H|T], Zeroset, InvZeroset, [NH|NT]):- H =.. [adder, Q, List], replace_bitwise_zero_indexes(Q, InvZeroset, NQ), put_all_bitwise_zero_indexes_addlist(List, Zeroset, NList), NH =.. [adder, NQ, NList], apply_bitwise_zero_set_adders(T, Zeroset, InvZeroset, NT). %replace all zero indexes with 0 in a relation. put_all_bitwise_zero_indexes([], _, []). put_all_bitwise_zero_indexes([relation(X, Rel, Y)|Tail], IZList,[relation(X1, Rel, Y1)|NTail]):- replace_bitwise_zero_indexes(X, IZList, X1), replace_bitwise_zero_indexes(Y, IZList, Y1), !, put_all_bitwise_zero_indexes(Tail, IZList, NTail). % do not replace empty: [] with zero [0] replace_bitwise_zero_indexes(bitvector(0), _Zeromap, bitvector(0)):- !. replace_bitwise_zero_indexes(bitvector(In), InvZeromap, bitvector(Out)):- %InverseZeros is \Zeromap, Out1 is In /\ InvZeromap, %subtract the zeroset. ( Out1 == 0 % [] -> Out = 1 %-> [0] ; Out1 = Out % -> [X, Y, Z] ). % replace all zero indexes with 0 in an addlist. % eg. [pos(X), neg(Y)] put_all_bitwise_zero_indexes_addlist([], _, []). put_all_bitwise_zero_indexes_addlist([H|T], ZMap,[NH|NT]):- H =.. [X, bitvector(Q)], Res is Q /\ ZMap, ( Res == 0 % Q is not in Zmap -> NQ = Q ; NQ = 1 % bitvector 1 is the zero pointer: [0] ), !, NH =.. [X, bitvector(NQ)], % X could be: noforce, saves evaluation later on... put_all_bitwise_zero_indexes_addlist(T, ZMap, NT). */ /*** FL januari 2004: NEW GARP 2.0 SPECIFIC ENDS HERE ***/ /* correspondence relations inspected when a correspondence relation is found, or when a new relation is derived */ /* FL 7-3-2004: Old version: has a... * Bug: when analyse simple encounters an x=y relation, it replaces all y's with * x and removes the x=y (now x=x) relation. If this x=y relation is the condition part of * a correspondence, this results in an empty list. The empty list should mean: * no conditions -> fire correspondence. But the empty list fails the is_derivable * check. (common_select fails on the empty list). * an empty list as consequence is of no concern; append_relation_all is a list * operation and has no problem with empty lists. inspect_correspondence(Relations, Cin, Cout):- inspect_correspondence(Relations, Cin, Cout, []). inspect_correspondence(Relations, Cin, Cout, Previous):- cio_c_nc_d(Cin, Cnew, Correspondence, RCorrespondence, Derivable), ( common_select(Correspondence, correspondence(L1, L2), RCorrespondence) ; common_select(Correspondence, correspondence(L2, L1), RCorrespondence) ; common_select( Correspondence, if_correspondence(L1, L2), RCorrespondence) ), common_select(L1, One, RL1), is_derivable(One, Relations), check_derivable(RL1, Derivable), append(Previous, L2, ToAdd), !, inspect_correspondence(Relations, Cnew, Cout, ToAdd). inspect_correspondence(_, Cio, Cio, []):- !. inspect_correspondence(_, Cin, Cout, ToAdd):- append_relation_all(ToAdd, Cin, Cout, _, true). *** New version below: ***/ /* % fails on empty list determine_pointers_list([H], [H/BV], BV):- !, determine_pointers(H, BV). determine_pointers_list([H|T], [H/BV|NT], NBV):- determine_pointers(H, BV), determine_pointers_list(T, NT, TBV), map_union(BV, TBV, NBV). */ /* check_context_derivable_set([], _). check_context_derivable_set([Rel|T], Contexts):- check_context_derivable(Rel, Contexts), check_context_derivable_set(T, Contexts). */ /* % FL may 07, passing on adders now for pointer updates... inspect_correspondence(Relations, Cin, Cout, DoAnalyseSimple):- inspect_correspondence(Relations, Cin, Cout, [], DoAnalyseSimple, [], []). inspect_correspondence(Relations, Cin, Cout, DoAnalyseSimple, AddersIn, AddersOut):- inspect_correspondence(Relations, Cin, Cout, [], DoAnalyseSimple, AddersIn, AddersOut). inspect_correspondence(Relations, Cin, Cout, Previous, DoAnalyseSimple, AddersIn, AddersOut):- cio_c_nc_d(Cin, Cnew, Correspondence, RCorrespondence, Derivable), determine_pointers_list(Relations, _, RBV), % if nothing in common, it cannot fire ( common_select(Correspondence, correspondence(L1, L2)/BV/_, RCorrespondence) ; common_select(Correspondence, correspondence(L2, L1)/BV/_, RCorrespondence) ; common_select( Correspondence, if_correspondence(L1, L2)/BV/_, RCorrespondence) ), ( L1 = [] % An empty list means no conditions: fire correspondence. ; map_intersection(BV, RBV, bitvector(Common)), % could this be more strict? Common =\= 0, common_select(L1, One, RL1), is_derivable(One, Relations), check_derivable(RL1, Derivable) ), append(Previous, L2, ToAdd), !, inspect_correspondence(Relations, Cnew, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut). inspect_correspondence(_, Cio, Cio, [], _, Adders, Adders):- !. inspect_correspondence(_, Cin, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut):- append_relation_all(ToAdd, Cin, Cout, _, DoAnalyseSimple, AddersIn, AddersOut). control_corr([]). control_corr([H/_/_|T]):- H=..[_, L1, L2], all_canonical(L1), all_canonical(L2), control_corr(T). all_canonical(_):-!. all_canonical([]). all_canonical([H|T]):- ( canonical(H) ; flstop ), !, all_canonical(T). canonical(relation(L, =, R)):- !, sort([L, R], [L, R]). canonical(_). */ /* % FL nov 07, new context version: Only check relevant correspondences. % Only use relevant derivable. % FL may 07, passing on adders now for pointer updates... inspect_correspondence(Relations, Cin, Cout, DoAnalyseSimple):- inspect_correspondence(Relations, Cin, Cout, DoAnalyseSimple, [], []). inspect_correspondence([], Cio, Cio, _DoAnalyseSimple, Adders, Adders). inspect_correspondence([Relation|T], Cin, Cout, DoAnalyseSimple, AddersIn, AddersOut):- cio_c(Cin, Corr), determine_pointers(Relation, BV), relevant_correspondences(BV, Corr, Relevant), Relevant \= [], !, cio_r(Cin, Contexts), (relevant_contexts(BV, Contexts, [context(_, Derivable, _, _)], _); flstop), !, inspect_correspondence2(Relation, Relevant, Derivable, Cin, Cnew, [], DoAnalyseSimple, AddersIn, AddersNew), inspect_correspondence(T, Cnew, Cout, DoAnalyseSimple, AddersNew, AddersOut). %no relevant correspondences, skip inspect_correspondence([_Relation|T], Cin, Cout, DoAnalyseSimple, AddersIn, AddersOut):- inspect_correspondence(T, Cin, Cout, DoAnalyseSimple, AddersIn, AddersOut). % inspected all: but nothing to append inspect_correspondence2(_Relation, [], _D, Cio, Cio, [], _DoAnalyseSimple, Adders, Adders):- !. % inspected all: append consequential relations inspect_correspondence2(_Relation, [], _D, Cin, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut):- append_relation_all(ToAdd, Cin, Cout, _, DoAnalyseSimple, AddersIn, AddersOut). % check a relevant correspondence. > fires inspect_correspondence2(Relation, [R/_/_|T], Derivable, Cin, Cout, Previous, DoAnalyseSimple, AddersIn, AddersOut):- ( R = correspondence(L1, L2) ; R = correspondence(L2, L1) ; R = if_correspondence(L1, L2) ), ( common_select(L1, One, RL1), is_derivable(One, [Relation]), check_derivable(RL1, Derivable) ; % new: L1 = [] % An empty list means no conditions: fire correspondence. ), !, append(Previous, L2, ToAdd), cio_c_nc(Cin, Cnew, C, NC), delete(C, R, NC), inspect_correspondence2(Relation, T, Derivable, Cnew, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut). % check a relevant correspondence. > does not fire inspect_correspondence2(Relation, [_R|T], Derivable, Cin, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut):- inspect_correspondence2(Relation, T, Derivable, Cin, Cout, ToAdd, DoAnalyseSimple, AddersIn, AddersOut). relevant_correspondences(_BV, [], []). relevant_correspondences(BV, [C/CBV/CCV|CorrT], [C/CBV/CCV|Relevant]):- map_intersection(BV, CBV, bitvector(Common)), % could this be more strict? Common =\= 0, !, relevant_correspondences(BV, CorrT, Relevant). relevant_correspondences(BV, [_|CorrT], Relevant):- relevant_correspondences(BV, CorrT, Relevant). */ /* % strictly_relevant_contexts(+RelPointers, +RelationContexts, -RelevantContexts):- % returns contexts that are supersets of the pointerset. strictly_relevant_contexts(_RP, [], [], []). % relevant_context strictly_relevant_contexts(RP, [context(R, D, CP)|RT], [context(R, D, CP)|CT], OT):- map_union(RP, CP, CP), %RP is subset of CP !, strictly_relevant_contexts(RP, RT, CT, OT). % other context strictly_relevant_contexts(RP, [H|RT], CT, [H|OT]):- strictly_relevant_contexts(RP, RT, CT, OT). */ /* inspect_a_correspondence(correspondence(L1, L2)/BV/_, Cin, Cout):- cio_r(Cin, R), %strictly_relevant_contexts(BV, R, Contexts, _), relevant_contexts(BV, R, Contexts, _), ( ( check_context_derivable_set(L1, Contexts), !, append_relation_all(L2, Cin, Cout, _, true) ) ; ( check_context_derivable_set(L2, Contexts), !, append_relation_all(L1, Cin, Cout, _, true) ) ). inspect_a_correspondence(if_correspondence(L1, L2)/BV/_, Cin, Cout):- cio_r(Cin, R), %strictly_relevant_contexts(BV, R, Contexts, _), relevant_contexts(BV, R, Contexts, _), check_context_derivable_set(L1, Contexts), !, append_relation_all(L2, Cin, Cout, _, true). inspect_a_correspondence(_, Cio, Cio). inspect_some_correspondences([], Cio, Cio). inspect_some_correspondences([H|T], Cin, Cout):- inspect_a_correspondence(H, Cin, Cnew), inspect_some_correspondences(T, Cnew, Cout). */ /* inspect_a_correspondence(correspondence(L1, L2)/BV/_, Cin, Cout):- cio_d(Cin, Derivable), check_derivable(L1, Derivable), !, append_relation_all(L2, Cin, Cout, _, true). inspect_a_correspondence(correspondence(L1, L2)/BV/_, Cin, Cout):- cio_d(Cin, Derivable), check_derivable(L2, Derivable), !, append_relation_all(L1, Cin, Cout, _, true). inspect_a_correspondence(if_correspondence(L1, L2)/BV/_, Cin, Cout):- cio_d(Cin, Derivable), check_derivable(L1, Derivable), !, append_relation_all(L2, Cin, Cout, _, true). inspect_a_correspondence(_, Cio, Cio). */ /*************** old listversion analyse zero preds.. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % % % % % % get_zero_set(+Relations, -Zeroset) % find all quantities / pointers equal to zero in a relationset: % intern-list representation, use q = [] or q>=[] /\ []>=q % done get_zero_set([], []). % X equal to zero, add to zeroset get_zero_set([relation([X], =, [])|Tail], [X|ZTail]):- !, get_zero_set(Tail, ZTail). % X equal to zero, add to zeroset get_zero_set([relation([], =, [X])|Tail], [X|ZTail]):- !, get_zero_set(Tail, ZTail). % X equal or greater to zero if also inverse then add to zeroset get_zero_set([relation([X], >=, [])|Tail], [X|ZTail]):- combine_to_zero(right, X, Tail), !, get_zero_set(Tail, ZTail). % X equal or greater to zero if also inverse then add to zeroset get_zero_set([relation([], >=, [X])|Tail], [X|ZTail]):- combine_to_zero(left, X, Tail), !, get_zero_set(Tail, ZTail). % no zero equality, next relation get_zero_set([_|Tail], ZTail):- get_zero_set(Tail, ZTail). combine_to_zero(right, X, Relations):- memberchk(relation([], >=, [X]), Relations). combine_to_zero(left, X, Relations):- memberchk(relation([X], >=, []), Relations). % apply_zero_set(+RelationsIn, +Zeroset, -RelationsOut) % apply zeros to set of relations in intern-list representation % append the relation 0 = zero, which is removed because evident. apply_zero_set(RelationsIn, Zeroset, RelationsOut):- apply_zeros(RelationsIn, Zeroset, Relations1), % fails in case of contradiction append([relation([0], =, [])], Relations1, RelationsOut). % apply_zeros(+RelationsIn, +Zeroset, -RelationsOut) % apply zeros to set of relations in intern-list representation, % fails with error report in case of a contradiction apply_zeros([], _, []). % valid new relation after zero application, return, continue with rest apply_zeros([relation(X, Rel, Y)|Tail], Zeros, [relation(X1, Rel, Y1)|NewTail]):- % change indexes in zeroset to zero, leave one zero if no other indexes. change_indexes_to_one_zero(X, Zeros, X1, false), change_indexes_to_one_zero(Y, Zeros, Y1, false), \+ empty_relation(X1, Rel, Y1, _Result), !, %\+ invalid_relation(relation(X1, Rel, Y1)), % X > X (contradiction) fail (FL July 2004: superfluous empty relation checks for contradiction) %!, apply_zeros(Tail, Zeros, NewTail). % empty relation after zero application, discard, continue with rest apply_zeros([relation(X, Rel, Y)|Tail], Zeros, NewTail):- % change indexes in zeroset to zero, leave one zero if no other indexes. change_indexes_to_one_zero(X, Zeros, X1, false), change_indexes_to_one_zero(Y, Zeros, Y1, false), empty_relation(X1, Rel, Y1, Result),% 0 = 0 (empty) or x>x (contradiction) or x=x evident memberchk(Result, [empty, evident]), !, apply_zeros(Tail, Zeros, NewTail). % change_indexes_to_one_zero(+ListIn, +Zeros, -ListOut, +false) % remove all elements in zeros from list, leave one zero if no other % element/pointer is present (indicater set to true). % eg. [4, 5], zeros=5 -> [4] % eg. [5], zeros=5 -> [0] % done change_indexes_to_one_zero([], _, [], _). % no other pointers unequal to zero return [0] change_indexes_to_one_zero([X], Zeros, [0], false):- memberchk(X, Zeros),!. % other pointers found before, return empty change_indexes_to_one_zero([X], Zeros, [], true):- memberchk(X, Zeros),!. % nonzero pointer, return it. change_indexes_to_one_zero([X], _, [X], _). % zero pointer in front, remove from list. change_indexes_to_one_zero([X, Y|Tail], Zeros, NewTail, NonZeroInList):- memberchk(X, Zeros),!, change_indexes_to_one_zero([Y|Tail], Zeros, NewTail, NonZeroInList). % nonzero pointer, return it, set indicator, to true change_indexes_to_one_zero([X, Y|Tail], Zeros, [X|NewTail], _NonZeroInList):- change_indexes_to_one_zero([Y|Tail], Zeros, NewTail, true). % check relation for information value empty_relation(X, Rel, X, Result):- !, (Rel == > -> Result = contradiction, % x > x is impossible etrace(solve_zero_found_invalid, _, add_relation) ; Result = evident). % x = x or x >= x is evident. empty_relation(X, Rel, Y, Result):- %list is empty or contains only 0's only_zeros_in_list(X), only_zeros_in_list(Y), !, (Rel == > -> Result = contradiction, % zero > zero is impossible etrace(solve_zero_found_invalid, _, add_relation) ; Result = empty). % zero = zero is evident empty/no information value % succeed if list is empty or contains only 0's only_zeros_in_list([]). only_zeros_in_list([0|T]):- only_zeros_in_list(T). % * apply for correspondences & adders * % apply_zero_set_correspondences(+CorrespondencesIn, +Zeroset, -CorrespondencesOut) % Pointers in correspondences (intern-list representation) need to be updated. % all relations are returned: % an if_correspondence([relation( 0 > 0), ...) will not fire % an if_correspondence([relation( 0 = 0), ...) will fire % so information is preserved, however, correspondences containing no % information are formed. They can do no harm though. apply_zero_set_correspondences([], _Zeroset, []). apply_zero_set_correspondences([H|T], Zeroset, [NH|NT]):- H =.. [C, Relations1, Relations2], put_all_zero_indexes(Relations1, Zeroset, NR1), put_all_zero_indexes(Relations2, Zeroset, NR2), NH =.. [C, NR1, NR2], apply_zero_set_correspondences(T, Zeroset, NT). % apply_zero_set_adders(+AddersIn, +Zeroset, +AddersOut) % Pointers in adders (intern-list representation) need to be updated also. apply_zero_set_adders([], _Zeroset, []). apply_zero_set_adders([H|T], Zeroset, [NH|NT]):- H =.. [adder, Q, List], replace_zero_indexes(Q, Zeroset, NQ), put_all_zero_indexes_addlist(List, Zeroset, NList), NH =.. [adder, NQ, NList], apply_zero_set_adders(T, Zeroset, NT). %replace all zero indexes with 0 in a relation. put_all_zero_indexes([], _, []). put_all_zero_indexes([relation(X, Rel, Y)|Tail], ZList,[relation(X1, Rel, Y1)|NTail]):- replace_zero_indexes(X, ZList, X1), replace_zero_indexes(Y, ZList, Y1), !, put_all_zero_indexes(Tail, ZList, NTail). replace_zero_indexes([], _, []). replace_zero_indexes([I|T], ZList, [0|NT]):- memberchk(I, ZList), !, replace_zero_indexes(T, ZList, NT). replace_zero_indexes([H|T], ZList, [H|NT]):- replace_zero_indexes(T, ZList, NT). % replace all zero indexes with 0 in an addlist. % eg. [pos(X), neg(Y)] put_all_zero_indexes_addlist([], _, []). put_all_zero_indexes_addlist([H|T], ZList,[NH|NT]):- H =.. [X, [Q]], memberchk(Q, ZList), !, NH =.. [X, [0]], % X could be: noforce, saves evaluation later on... put_all_zero_indexes_addlist(T, ZList, NT). put_all_zero_indexes_addlist([H|T], ZList,[H|NT]):- put_all_zero_indexes_addlist(T, ZList, NT). %*--------------special list to map and back tools for sets--------*% % list_map_for_relation_set(+InternRelationsIn, -InternListRelationsOut) % From LIST to Map % convert bitmap representation to list (map_list), for a whole % set of relations (intern representation), % making them intern-list representation list_map_for_relation_set([], []). list_map_for_relation_set([relation(X, Rel, Y)|Tail], [relation(X1, Rel, Y1)|NewTail]):- list_map(X, X1), list_map(Y, Y1), list_map_for_relation_set(Tail, NewTail). % map_list_for_relation_set(+InternListRelationsOut, -InternRelationsIn) % From MAP to LIST % convert list representation to bitmap (list_map), for a whole % set of relations (intern-list representation), % making them intern representation map_list_for_relation_set([], []). map_list_for_relation_set([relation(X, Rel, Y)|Tail], [relation(X1, Rel, Y1)|NewTail]):- map_list(X, X1), map_list(Y, Y1), map_list_for_relation_set(Tail, NewTail). % From LIST to Map for correspondences list_map_for_correspondences([], []). list_map_for_correspondences([H|T], [NH|NT]):- H =.. [C, Relations1, Relations2], list_map_for_relation_set(Relations1, NR1), list_map_for_relation_set(Relations2, NR2), NH =.. [C, NR1, NR2], list_map_for_correspondences(T, NT). % From LIST to Map for adders list_map_for_adders([], []). list_map_for_adders([H|T], [NH|NT]):- H =.. [adder, Q, List], list_map(Q, NQ), list_map_addlist(List, NList), NH =.. [adder, NQ, NList], list_map_for_adders(T, NT). list_map_addlist([], []). list_map_addlist([H|T], [NH|NT]):- H =.. [X, Q], list_map(Q, NQ), NH =.. [X, NQ], list_map_addlist(T, NT). % From MAP to LIST for correspondences map_list_for_correspondences([], []). map_list_for_correspondences([H|T], [NH|NT]):- H =.. [C, Relations1, Relations2], map_list_for_relation_set(Relations1, NR1), map_list_for_relation_set(Relations2, NR2), NH =.. [C, NR1, NR2], map_list_for_correspondences(T, NT). % From MAP to LIST for adders map_list_for_adders([], []). map_list_for_adders([H|T], [NH|NT]):- H =.. [adder, Q, List], map_list(Q, NQ), map_list_addlist(List, NList), NH =.. [adder, NQ, NList], map_list_for_adders(T, NT). map_list_addlist([], []). map_list_addlist([H|T], [NH|NT]):- H =.. [X, Q], map_list(Q, NQ), NH =.. [X, NQ], map_list_addlist(T, NT). %*-------- End listmap maplist tools ---------*% % End listversion analyse zero preds...................*/