1		:- module(difference_logic_solver, [init_idl_solver/1,
2		register_constraint/2,
3		register_constraints/2,
4		solve_idl_conj/2,
5		is_idl_constraint/1,
6		get_solver_result/2,
7		get_all_solutions_on_bt/2,
8		try_candidate_bounds/3,
9		get_registered_vars/2,
10		get_unsat_core/1,
11		infer_constraints_for_idl_solver/2,
12		negate_dl_constraint/2,
13		remove_unsat_core/0]).
14
15		:- use_module(library(lists), [select/3]).
16		:- use_module(library(plunit)).
17
18		:- use_module(probsrc(preferences), [set_preference/2]).
19		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, conjunction_to_list/2]).
20		:- use_module(cdclt_solver('difference_logic/ast_to_difference_logic')).
21
22		:- dynamic predecessor/2, negative_weight/0, contains_zero/0, constraint_store/3, unsat_core/1.
23		:- volatile predecessor/2, negative_weight/0, contains_zero/0, constraint_store/3, unsat_core/1.
24
25		% A graph based solver for difference logic, i.e., constraints of the form Minuend - Subtrahend <= Constant.
26		% Each node represents a variable. For a constraint x-y<=c a weighted edge (y,c,x) is added, while not(x-y<=c) yields
27		% the edge (x,-c-1,y).
28		% A difference logic constraint system is satisfiable if its corresponding graph does not contain a negative cycle.
29		% If satisfiable, the shortest path to a variable yields its solution.
30		% Otherwise, the conjunction of constraints corresponding to the edges of the negative cycle are an unsat core.
31		% Note: Integer inequality has to be rewritten beforehand since it yields a disjunction in difference logic.
32
33		%% solve_idl_conj(+Pred, -Result).
34		solve_idl_conj(Pred, Result) :-
35		init_idl_solver(GraphMut),
36		conjunction_to_list(Pred, ConjList),
37		( register_constraints(GraphMut, ConjList),
38		!,
39		get_solver_result(GraphMut, Result)
40		; get_solver_result(GraphMut, TResult),
41		TResult == contradiction_found,
42		!,
43		get_unsat_core(Core),
44		Result = contradiction_found(Core)
45		; Result = no_solution_found(no_idl_constraint)
46		).
47
48		%% init_idl_solver.
49		init_idl_solver(GraphMut) :-
50		create_mutable(graph(nodes([]),edges([]),shortest_paths([])), GraphMut),
51		set_preference(normalize_ast, true),
52		retractall(predecessor(_,_)),
53		retractall(unsat_core(_)),
54		retractall(constraint_store(_,_,_)),
55		retractall(negative_weight),
56		retractall(contains_zero).
57
58		negate_dl_constraint(b(equal(A,B),pred,Info), NegDL) :-
59		!,
60		NegDL = b(not_equal(A,B),pred,Info).
61		negate_dl_constraint(b(not_equal(A,B),pred,Info), NegDL) :-
62		!,
63		NegDL = b(equal(A,B),pred,Info).
64		negate_dl_constraint(b(negation(Constraint),pred,[]), Constraint).
65		negate_dl_constraint(Constraint, b(negation(Constraint),pred,[])).
66
67		%% get_registered_vars(+GraphMut, -Vars).
68		get_registered_vars(GraphMut, Vars) :-
69		get_mutable(graph(nodes(Vars),_,_), GraphMut).
70
71		%% register_constraints(+GraphMut, +ListOfConstraints).
72		register_constraints(_, []).
73		register_constraints(GraphMut, [Constraint|T]) :-
74		register_constraint(GraphMut, Constraint),
75		register_constraints(GraphMut, T).
76
77		%% register_constraint(+GraphMut, +Constraint).
78		% Accepted top level operators are <,<=,= and its negations.
79		% Fails if constraint can not be transformed to difference logic
80		% or produces a contradiction with existing constraints.
81		register_constraint(GraphMut, Constraint) :-
82		%write('Register Constraint..'),nl,
83		%translate:print_bexpr(Constraint),nl,
84		( is_idl_constraint(Constraint)
85		-> register_idl_constraint(GraphMut, Constraint),
86		solve_incremental_constraint(GraphMut, Constraint)
87		; rewrite_to_idl(Constraint, DLConstraints),
88		register_constraints_from_conj_list(GraphMut, DLConstraints),
89		solve_incremental_list(GraphMut, DLConstraints)
90		).
91
92		%% relax_edge_cond(+GraphMut, +In, +Out, +Weight, -ND).
93		relax_edge_cond(GraphMut, In, Out, Weight, ND) :-
94		get_mutable(graph(_,_,shortest_paths(SPs)), GraphMut),
95		member((In,DIn), SPs),
96		member((Out,DOut), SPs),
97		ND is DIn + Weight,
98		ND < DOut.
99
100		%% relax_node_distance(+GraphMut, +In, +Out, +ND, -DiffToOld).
101		relax_node_distance(GraphMut, In, Out, ND, DiffToOld) :-
102		assert_distance(GraphMut, Out, ND, DiffToOld),
103		assert_predecessor(Out, In).
104
105		solve_incremental_constraint(GraphMut, DLConstraint) :-
106		get_edge_from_dl_constraint(DLConstraint, In, Out, Weight),
107		solve_incremental(GraphMut, In, Out, Weight).
108
109		solve_incremental_list(_, []).
110		solve_incremental_list(GraphMut, [DLConstraint|T]) :-
111		solve_incremental_constraint(GraphMut, DLConstraint),
112		solve_incremental_list(GraphMut, T).
113
114		%% solve_incremental(+In, +Out, +Weight).
115		% Update shortest paths while searching for a negative cycle.
116		solve_incremental(_, _, _, _) :-
117		% no negative cycle without a negative weight
118		\+ negative_weight.
119		solve_incremental(GraphMut, In, Out, Weight) :-
120		negative_weight,
121		detect_negative_cycle_inc(GraphMut, [], In, Out, Weight, NegativeCycle),
122		( NegativeCycle == none
123		-> % shortest paths stored in dis/2 are a solution
124		true
125		; get_unsat_core_from_negative_cycle(GraphMut, NegativeCycle, UnsatCore),
126		%nl, write('Unsat Core: '), nl,translate:print_bexpr(UnsatCore),nl,
127		%writeq(UnsatCore),nl,
128		asserta(unsat_core(UnsatCore)),
129		fail
130		).
131
132		%% get_edge_from_dl_constraint(+Node, -In, -Out, -Weight).
133		get_edge_from_dl_constraint(b(less_equal(Sub,Constant),pred,_), In, Out, Weight) :-
134		% edge (y,c,x) for x-y<=c
135		get_id_names_from_idl_minus(Sub, Out, In),
136		get_int_value(Constant, Weight).
137		get_edge_from_dl_constraint(b(negation(Constraint),pred,_), In, Out, Weight) :-
138		% edge (x,-c-1,y) for not(x-y<=c)
139		Constraint = b(less_equal(Sub,Constant),pred,_),
140		get_id_names_from_idl_minus(Sub, In, Out),
141		get_int_value(Constant, TWeight),
142		Weight is TWeight * -1 - 1.
143
144		get_id_names_from_idl_minus(b(minus(Id1,Id2),integer,_), In, Out) :-
145		Id1 = b(identifier(In),integer,_),
146		Id2 = b(identifier(Out),integer,_).
147
148		%% get_all_solutions_on_bt(+GraphMut, -SolverResult).
149		get_all_solutions_on_bt(GraphMut, SolverResult) :-
150		% TO DO: randomized enumeration order, log upper and lower bounded vars?
151		get_solver_result(GraphMut, TSolverResult),
152		TSolverResult = solution(Bindings),
153		( SolverResult = TSolverResult
154		; exclude_solution_bt(GraphMut, Bindings),
155		get_all_solutions_on_bt(GraphMut, SolverResult)
156		).
157
158		exclude_solution_bt(GraphMut, [binding(VarName,int(Val),_)|T]) :-
159		% register inequality constraint VarName /= Val with choicepoint since rewriting yields a disjunction
160		% i.e., x/=c -> x-_zero<=c-1 or _zero-x<=-c-1
161		( exclude_solution_from_binding(GraphMut, VarName, Val)
162		; remove_unsat_core,
163		Val1 is Val * -1,
164		% equality
165		LEQ1 = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val),integer,[])),pred,[]),
166		LEQ2 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]),
167		register_constraints(GraphMut, [LEQ1,LEQ2]),
168		exclude_solution_bt(GraphMut, T)
169		).
170
171		exclude_solution_from_binding(GraphMut, VarName, Val) :-
172		DisjVal1 is Val - 1,
173		DisjVal2 is Val * -1 - 1,
174		VarId = b(identifier(VarName),integer,[]),
175		ZeroId = b(identifier('_zero'),integer,[]),
176		Disj1 = b(less_equal(b(minus(VarId,ZeroId),integer,[]),b(integer(DisjVal1),integer,[])),pred,[]),
177		Disj2 = b(less_equal(b(minus(ZeroId,VarId),integer,[]),b(integer(DisjVal2),integer,[])),pred,[]),
178		( remove_unsat_core,
179		register_constraint(GraphMut, Disj1)
180		; remove_unsat_core,
181		register_constraint(GraphMut, Disj2)
182		).
183
184		%% try_candidate_bounds(+GraphMut, +CandidateTuples, -SolverResult).
185		% Try candidate bounds obtained by syntactic analysis of non idl constraints when backtracking from ProB to IDL solver.
186		% CandidateTuples is a list of tuples of variable and possible bounding values.
187		try_candidate_bounds(GraphMut, CandidateTuples, SolverResult) :-
188		try_candidate_bounds(GraphMut, none, CandidateTuples, Diff-Diff, SolverResult).
189
190		% Successively try one value for each variable with choicepoints to find all combinations on backtracking.
191		try_candidate_bounds(GraphMut, Solution, [], L-Diff, SolverResult) :-
192		Diff = [],
193		L \== [],
194		try_candidate_bounds(GraphMut, Solution, L, NDiff-NDiff, SolverResult).
195		try_candidate_bounds(GraphMut, Solution, [(_,[])|T], L-Diff, SolverResult) :-
196		try_candidate_bounds(GraphMut, Solution, T, L-Diff, SolverResult).
197		try_candidate_bounds(GraphMut, none, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :-
198		% x=val
199		LEQ1 = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val),integer,[])),pred,[]),
200		NVal is Val * -1,
201		LEQ2 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(NVal),integer,[])),pred,[]),
202		remove_unsat_core,
203		register_constraints(GraphMut, [LEQ1,LEQ2]),
204		get_solver_result(GraphMut, TSolverResult),
205		TSolverResult = solution(_),
206		( SolverResult = TSolverResult
207		; Diff = [(VarName,TVals)|NDiff],
208		try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult)
209		).
210		try_candidate_bounds(GraphMut, Solution, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :-
211		( Solution == none
212		; ground(Solution),
213		Solution = solution(Bindings),
214		member(binding(VarName,int(OldVal),_), Bindings),
215		Val < OldVal
216		),
217		Val1 is Val - 1,
218		% x<val
219		LEQ = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]),
220		remove_unsat_core,
221		register_constraint(GraphMut, LEQ),
222		get_solver_result(GraphMut, TSolverResult),
223		TSolverResult = solution(_),
224		( SolverResult = TSolverResult
225		; Diff = [(VarName,TVals)|NDiff],
226		try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult)
227		).
228		try_candidate_bounds(GraphMut, Solution, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :-
229		( Solution == none
230		; ground(Solution),
231		Solution = solution(Bindings),
232		member(binding(VarName,int(OldVal),_), Bindings),
233		Val > OldVal
234		),
235		Val1 is Val * -1 - 1,
236		% x>val
237		LEQ = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]),
238		remove_unsat_core,
239		register_constraint(GraphMut, LEQ),
240		get_solver_result(GraphMut, TSolverResult),
241		TSolverResult = solution(_),
242		( SolverResult = TSolverResult
243		; Diff = [(VarName,TVals)|NDiff],
244		try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult)
245		).
246		try_candidate_bounds(GraphMut, Solution, [(VarName,[_|TVals])|T], L-Diff, SolverResult) :-
247		Diff = [(VarName,TVals)|NDiff],
248		try_candidate_bounds(GraphMut, Solution, T, L-NDiff, SolverResult).
249
250		remove_unsat_core :-
251		retract(unsat_core(_)),
252		!.
253		remove_unsat_core.
254
255		%% get_solver_result(+GraphMut, -SolverResult).
256		get_solver_result(_, SolverResult) :-
257		unsat_core(_),
258		!,
259		SolverResult = contradiction_found.
260		get_solver_result(GraphMut, SolverResult) :-
261		get_mutable(graph(_,_,shortest_paths(SPs)), GraphMut),
262		shortest_paths_to_bindings(SPs, [], TempBindings), % TO DO: shift at the same time?
263		ground(TempBindings),
264		possibly_shift_solution_for_zero(TempBindings, Bindings),!,
265		SolverResult = solution(Bindings).
266
267		shortest_paths_to_bindings([], Acc, Acc).
268		shortest_paths_to_bindings([(VarName,Val)|T], Acc, Bindings) :-
269		number_to_atom(Val, ValAtom),
270		shortest_paths_to_bindings(T, [binding(VarName,int(Val),ValAtom)|Acc], Bindings).
271
272		%% detect_negative_cycle_inc(+GraphMut, +Queue, +In, +Out, +Weight, -NegativeCycle).
273		% Incremental negative cycle detection and shortest path computation as suggested by Chao Wang et al.
274		% Queue is sorted by maximal node value changes.
275		detect_negative_cycle_inc(GraphMut, Queue, In, Out, Weight, NegativeCycle) :-
276		( relax_edge_cond(GraphMut, In, Out, Weight, NDOut)
277		-> relax_node_distance(GraphMut, In, Out, NDOut, DiffToOld),
278		insertion_sort(Queue, Out, DiffToOld, NQueue)
279		; NQueue = Queue
280		),
281		detect_negative_cycle_inc(GraphMut, In, Out, NQueue, NegativeCycle).
282
283		detect_negative_cycle_inc(_, _, _, [], none).
284		detect_negative_cycle_inc(GraphMut, StartIn, StartOut, [(CurNode,_)|T], NegativeCycle) :-
285		get_adjacent_edges(GraphMut, CurNode, Adjacent),
286		detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, Adjacent, T, NQueue, TNegativeCycle),
287		(TNegativeCycle \== none
288		-> NegativeCycle = TNegativeCycle
289		; detect_negative_cycle_inc(GraphMut, StartIn, StartOut, NQueue, NegativeCycle)
290		).
291
292		detect_negative_cycle_inc_process_edges(_, _, _, [], Queue, Queue, none).
293		detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, [(In,Weight,Out,_)|T], Queue, NQueue, NegativeCycle) :-
294		( relax_edge_cond(GraphMut, In, Out, Weight, NDOut)
295		-> ( (In == StartIn, Out == StartOut)
296		-> get_negative_cycle_from_predecessors(Out, NegativeCycle)
297		; relax_node_distance(GraphMut, In, Out, NDOut, DiffToOld),
298		insertion_sort(Queue, Out, DiffToOld, TQueue),
299		detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, T, TQueue, NQueue, NegativeCycle)
300		)
301		; detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, T, Queue, NQueue, NegativeCycle)
302		).
303
304		get_adjacent_edges(GraphMut, Node, Adjacent) :-
305		get_mutable(graph(_,edges(Edges),_), GraphMut),
306		memberchk(Node:TAdjacent, Edges),
307		!,
308		Adjacent = TAdjacent.
309		get_adjacent_edges(_, _, []).
310
311		%% get_negative_cycle_from_predecessors(+Out, -NegativeCycle).
312		get_negative_cycle_from_predecessors(Out, NegativeCycle) :-
313		get_negative_cycle_from_predecessors(Out, Out, [], NegativeCycle).
314
315		get_negative_cycle_from_predecessors(Start, Start, Acc, Acc) :-
316		Acc \== [].
317		get_negative_cycle_from_predecessors(Start, CurNode, Acc, NegativeCycle) :-
318		retract(predecessor(CurNode, PreNode)),
319		get_negative_cycle_from_predecessors(Start, PreNode, [PreNode|Acc], NegativeCycle).
320
321		%% get_unsat_core_from_negative_cycle(+GraphMut, +NegativeCycle, -UnsatCore).
322		% Conjunct the constraints corresponding to the negative cycle in the constraint graph.
323		get_unsat_core_from_negative_cycle(GraphMut, [SrcNode|T], UnsatCore) :-
324		get_mutable(graph(_,edges(Edges),_), GraphMut),
325		get_unsat_core_from_negative_cycle(Edges, [SrcNode|T], SrcNode, [], UnsatCoreList),
326		conjunct_predicates(UnsatCoreList, UnsatCore), !.
327
328		%% get_unsat_core_from_negative_cycle(+Edges, +NegativeCycleNodes, +SrcNode, +Acc, -UnsatCoreList).
329		get_unsat_core_from_negative_cycle(Edges, [CurNode], SrcNode, Acc, NewAcc) :-
330		!,
331		member(CurNode:Adjacent, Edges),
332		member((CurNode,_,SrcNode,DLConstraint), Adjacent),
333		get_original_constraint(DLConstraint, Constraint),
334		%nl,write('Constraint: '), nl, translate:print_bexpr(DLConstraint),nl,
335		%write('Original Constraint: '), nl, translate:print_bexpr(Constraint),nl,
336		NewAcc = [Constraint|Acc].
337		get_unsat_core_from_negative_cycle(Edges, [CurNode,NextNode|T], SrcNode, Acc, UnsatCoreList) :-
338		member(CurNode:Adjacent, Edges),
339		member((CurNode,_,NextNode,DLConstraint), Adjacent),
340		get_original_constraint(DLConstraint, Constraint),
341		%nl,write('Constraint: '), nl, translate:print_bexpr(DLConstraint),nl,
342		%write('Original Constraint: '), nl, translate:print_bexpr(Constraint),nl,
343		get_unsat_core_from_negative_cycle(Edges, [NextNode|T], SrcNode, [Constraint|Acc], UnsatCoreList).
344
345		get_original_constraint(b(_,_,Info), Constraint) :-
346		member(idl_origin(TConstraint), Info),
347		!,
348		Constraint = TConstraint.
349		get_original_constraint(b(negation(b(_,_,Info)),_,_), Constraint) :-
350		member(idl_origin(TConstraint), Info),
351		!,
352		Constraint = b(negation(TConstraint),pred,[]).
353		get_original_constraint(DLConstraint, DLConstraint) :-
354		is_idl_constraint(DLConstraint).
355
356		%% get_unsat_core(-UnsatCore).
357		% Return asserted unsat core or fail.
358		get_unsat_core(UnsatCore) :-
359		unsat_core(UnsatCore).
360
361		%% possibly_shift_solution_for_zero(+TempBindings, -Bindings).
362		% Constraints of the form x<=c are transformed to x-_zero<=c where _zero is an artificial variable
363		% which is not part of the solution. If _zero is used, the resulting solution has to be shifted by -_zero for each variable
364		% so that _zero=0 holds.
365		possibly_shift_solution_for_zero(TempBindings, Bindings) :-
366		\+ contains_zero,
367		!,
368		Bindings = TempBindings.
369		possibly_shift_solution_for_zero(TempBindings, Bindings) :-
370		select(binding('_zero',int(ZeroVal),_), TempBindings, Rest),
371		( ZeroVal == 0
372		-> Bindings = Rest
373		; shift_solution(ZeroVal, Rest, [], Bindings)
374		).
375
376		%% shift_solution(+ZeroVal, +TempBindings, +Acc, -Shifted).
377		shift_solution(_, [], Acc, Acc).
378		shift_solution(ZeroVal, [binding(VarName,int(Value),_)|T], Acc, Shifted) :-
379		NValue is Value - ZeroVal,
380		number_to_atom(NValue, NValueAtom),
381		shift_solution(ZeroVal, T, [binding(VarName,int(NValue),NValueAtom)|Acc], Shifted).
382
383		number_to_atom(Number, Atom) :-
384		number_codes(Number, Codes),
385		atom_codes(Atom, Codes).
386
387		register_constraints_from_conj_list(_, []).
388		register_constraints_from_conj_list(GraphMut, [DLConstraint|T]) :-
389		register_idl_constraint(GraphMut, DLConstraint),
390		register_constraints_from_conj_list(GraphMut, T).
391
392		register_idl_constraint(GraphMut, DLConstraint) :-
393		( DLConstraint = b(less_equal(b(minus(Minuend,Subtrahend),integer,_),Constant),pred,_),
394		Pol = pos
395		; DLConstraint = b(negation(b(less_equal(b(minus(Minuend,Subtrahend),integer,_),Constant),pred,_)),pred,_),
396		Pol = neg
397		),
398		get_int_value(Constant, Value),
399		get_int_var_name(Minuend, MinuendVar),
400		get_int_var_name(Subtrahend, SubtrahendVar),
401		register_node_for_var(GraphMut, MinuendVar),
402		register_node_for_var(GraphMut, SubtrahendVar),
403		add_edge_for_polarity(GraphMut, Pol, DLConstraint, MinuendVar, SubtrahendVar, Value).
404
405		add_edge_for_polarity(GraphMut, pos, DLConstraint, MinuendVar, SubtrahendVar, Value) :-
406		% edge (y,c,x) for x-y<=c
407		add_edge(GraphMut, DLConstraint, SubtrahendVar, MinuendVar, Value),
408		bt_asserta(constraint_store(SubtrahendVar,MinuendVar,DLConstraint)).
409		add_edge_for_polarity(GraphMut, neg, DLConstraint, MinuendVar, SubtrahendVar, Value) :-
410		% edge (x,-c-1,y) for not(x-y<=c)
411		NValue is Value * -1 - 1,
412		add_edge(GraphMut, DLConstraint, MinuendVar, SubtrahendVar, NValue),
413		bt_asserta(constraint_store(MinuendVar,SubtrahendVar,DLConstraint)).
414
415		/*print_graph(GraphMut) :-
416		get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut),
417		format("Graph:~nNodes: ~w~nEdges: ~w~nShortest Paths: ~w~n~n", [Nodes,Edges,SPs]).*/
418
419		%% add_edge(+GraphMut, +DLConstraint, +In, +Out, +Value).
420		% Possibly replace edge since there can be only one edge between two nodes in integer difference logic.
421		% For instance, x-y<=2 => x-y<=3.
422		add_edge(GraphMut, DLConstraint, In, Out, Value) :-
423		get_mutable(graph(Nodes,edges(Edges),SPs), GraphMut),
424		add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges),
425		update_mutable(graph(Nodes,edges(NewEdges),SPs), GraphMut).
426
427		add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges) :-
428		select(In:Adjacent, Edges, REdges),
429		!,
430		( select((In,OldValue,Out,_), Adjacent, RAdjacent)
431		-> ( Value < OldValue
432		-> NewEdges = [In:[(In,Value,Out,DLConstraint)|RAdjacent]|REdges],
433		register_negative_weight(Value)
434		; NewEdges = Edges
435		)
436		; NewEdges = [In:[(In,Value,Out,DLConstraint)|Adjacent]|REdges],
437		register_negative_weight(Value)
438		).
439		add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges) :-
440		NewEdges = [In:[(In,Value,Out,DLConstraint)]|Edges],
441		register_negative_weight(Value).
442
443		%% assert_contains_zero.
444		assert_contains_zero :-
445		\+ contains_zero,
446		!,
447		bt_asserta(contains_zero).
448		assert_contains_zero.
449
450		%% register_negative_weight(+Value).
451		register_negative_weight(Value) :-
452		\+ negative_weight,
453		Value < 0,
454		!,
455		bt_asserta(negative_weight).
456		register_negative_weight(_).
457
458		%% register_node_for_var(+GraphMut, +VarName).
459		register_node_for_var(GraphMut, VarName) :-
460		get_mutable(graph(nodes(Nodes),_,_), GraphMut),
461		member(VarName, Nodes),
462		!.
463		register_node_for_var(GraphMut, VarName) :-
464		( VarName == '_zero'
465		-> assert_contains_zero
466		; true
467		),
468		get_mutable(graph(nodes(Nodes),Edges,shortest_paths(SPs)), GraphMut),
469		update_mutable(graph(nodes([VarName|Nodes]),Edges,shortest_paths([(VarName,0)|SPs])), GraphMut).
470
471		is_idl_constraint(Constraint) :-
472		( Constraint = b(less_equal(Sub,Constant),pred,_)
473		; Constraint = b(negation(b(less_equal(Sub,Constant),pred,_)),pred,_)
474		),
475		Sub = b(minus(Id1,Id2),integer,_),
476		get_int_value(Constant, _),
477		Id1 = b(identifier(_),integer,_),
478		Id2 = b(identifier(_),integer,_).
479
480		%% get_int_var_name(+IdentifierAst, -VarName).
481		get_int_var_name(b(identifier(VarName),integer,_), VarName).
482
483		%% insertion_sort(+List, +Node, +DiffToOld, -Sorted) :-
484		% Sort by largest change in distance.
485		insertion_sort([], Node, Dist, [(Node,Dist)]).
486		insertion_sort([(Node1,Dist1)|T], Node, Dist, Sorted) :-
487		Dist1 < Dist,
488		!,
489		Sorted = [(Node,Dist),(Node1,Dist1)|T].
490		insertion_sort([(Node1,Dist1)|T], Node, Dist, [(Node1,Dist1)|NT]) :-
491		insertion_sort(T, Node, Dist, NT).
492
493		assert_distance(GraphMut, Node, NDNode, DiffToOld) :-
494		get_mutable(graph(Nodes,Edges,shortest_paths(SPs)), GraphMut),
495		select((Node,Old), SPs, Rest),
496		NewSPs = [(Node,NDNode)|Rest],
497		update_mutable(graph(Nodes,Edges,shortest_paths(NewSPs)), GraphMut),
498		DiffToOld is Old - NDNode.
499
500		assert_predecessor(Node, PreNode) :-
501		bt_retract(predecessor(Node,_)),
502		bt_asserta(predecessor(Node,PreNode)).
503		assert_predecessor(Node, PreNode) :-
504		\+ predecessor(Node,_),
505		bt_asserta(predecessor(Node,PreNode)).
506
507		bt_asserta(Term) :-
508		asserta(Term); (retract(Term), fail).
509
510		bt_retract(Assertion) :-
511		( retract(Assertion)
512		-> ( true
513		; asserta(Assertion),
514		fail
515		)
516		; fail
517		).
518
519		% TO DO: are there more constraints? x:{1,3,7}?
520		infer_constraints_for_idl_solver(MemberNat, [Constraint]) :-
521		% x:NAT -> _zero-x <= 0
522		% x:NAT1 -> _zero-x <= -1
523		MemberNat = b(member(Id,Natural),pred,_),
524		Id = b(identifier(_),integer,_),
525		( Natural = b(integer_set('NATURAL'),set(integer),_),
526		Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),Id),integer,[]),b(integer(0),integer,[])),pred,[idl_origin(MemberNat)])
527		; Natural = b(integer_set('NATURAL1'),set(integer),_),
528		Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),Id),integer,[]),b(integer(-1),integer,[])),pred,[idl_origin(MemberNat)])
529		).
530		infer_constraints_for_idl_solver(MemberInterval, [LEQ1,LEQ2]) :-
531		% x:min..max -> _zero-x<=-min & x<=max
532		MemberInterval = b(member(Id,Interval),pred,_),
533		Id = b(identifier(_),integer,_),
534		Interval = b(interval(Min,Max),set(integer),_),
535		Min = b(integer(MinVal),integer,MinInfo),
536		Max = b(integer(_),integer,_),
537		MinVal1 is MinVal * -1,
538		LEQ1 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]), Id),integer,[]),b(integer(MinVal1),integer,MinInfo)),pred,[idl_origin(MemberInterval)]),
539		LEQ2 = b(less_equal(b(minus(Id,b(identifier('_zero'),integer,[])),integer,[]),Max),pred,[idl_origin(MemberInterval)]).
540		infer_constraints_for_idl_solver(EqualCard, [Constraint]) :-
541		% x=card(s) -> _zero-x<=0
542		% x=size(s) -> _zero-x<=0
543		( EqualCard = b(equal(Id,CardOrSize),pred,_)
544		; EqualCard = b(equal(CardOrSize,Id),pred,_)
545		),
546		Id = b(identifier(_),integer,_),
547		( CardOrSize = b(card(_),integer,_)
548		; CardOrSize = b(size(_),integer,_)
549		),
550		Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]), Id),integer,[]),b(integer(0),integer,[])),pred,[idl_origin(EqualCard)]).
551
552
553		:- begin_tests(difference_logic_solver).
554
555		test(simple_sat1, [nondet]) :-
556		init_idl_solver(GraphMut),
557		% a-c<=1 & c-b<=-3
558		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
559		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])),
560		!,
561		get_solver_result(GraphMut, Res),
562		ground(Res),
563		Res = solution(Bindings),
564		member(binding(a,int(-2),'-2'), Bindings),
565		member(binding(b,int(0),'0'), Bindings),
566		member(binding(c,int(-3),'-3'), Bindings),
567		\+ get_unsat_core(_).
568
569		test(simple_sat2, [nondet]) :-
570		init_idl_solver(GraphMut),
571		% a-c<=-1 & c-b<=3
572		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
573		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(3),integer,[])),pred,[])),
574		!,
575		get_solver_result(GraphMut, Res),
576		ground(Res),
577		Res = solution(Bindings),
578		member(binding(a,int(-1),'-1'), Bindings),
579		member(binding(b,int(0),'0'), Bindings),
580		member(binding(c,int(0),'0'), Bindings),
581		\+ get_unsat_core(_).
582
583		test(simple_sat3, [nondet]) :-
584		init_idl_solver(GraphMut),
585		% a-c<=1 & c-b<=3
586		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
587		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(3),integer,[])),pred,[])),
588		!,
589		get_solver_result(GraphMut, Res),
590		ground(Res),
591		Res = solution(Bindings),
592		member(binding(a,int(0),'0'), Bindings),
593		member(binding(b,int(0),'0'), Bindings),
594		member(binding(c,int(0),'0'), Bindings),
595		\+ get_unsat_core(_).
596
597		test(simple_sat4, [nondet]) :-
598		init_idl_solver(GraphMut),
599		% a-1<=1 & 3<=b & 2<=b-1
600		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(integer(1),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
601		register_constraint(GraphMut, b(less_equal(b(integer(3),integer,[]),b(identifier(b),integer,[])),pred,[])),
602		register_constraint(GraphMut, b(less_equal(b(integer(2),integer,[]),b(minus(b(identifier(b),integer,[]),b(integer(1),integer,[])),integer,[])),pred,[])),
603		!,
604		get_solver_result(GraphMut, Res),
605		ground(Res),
606		Res = solution(Bindings),
607		member(binding(a,int(2),'2'), Bindings),
608		member(binding(b,int(3),'3'), Bindings),
609		\+ get_unsat_core(_).
610
611		test(simple_sat_introduce_zero, [nondet]) :-
612		init_idl_solver(GraphMut),
613		% a-b<=-1 & a<=-1
614		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
615		register_constraint(GraphMut, b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),
616		!,
617		get_solver_result(GraphMut, Res),
618		ground(Res),
619		Res = solution(Bindings),
620		member(binding(a,int(-1),'-1'), Bindings),
621		member(binding(b,int(0),'0'), Bindings),
622		\+ get_unsat_core(_).
623
624		test(simple_sat_rewrite_equality, [nondet]) :-
625		init_idl_solver(GraphMut),
626		% a-b<=-1 & a=1
627		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
628		register_constraint(GraphMut, b(equal(b(identifier(a),integer,[]),b(integer(1),integer,[])),pred,[])),
629		!,
630		get_solver_result(GraphMut, Res),
631		Res = solution(Bindings),
632		member(binding(a,int(1),'1'), Bindings),
633		member(binding(b,int(2),'2'), Bindings),
634		\+ get_unsat_core(_).
635
636		test(simple_sat_all_solutions_single_var, [nondet]) :-
637		init_idl_solver(GraphMut),
638		% all solutions for x>0 & x<5
639		register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])),
640		register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(10),integer,[])),pred,[])),
641		!,
642		findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults),
643		SolverResults == [solution([binding(x,int(1),'1')]),solution([binding(x,int(2),'2')]),solution([binding(x,int(3),'3')]),solution([binding(x,int(4),'4')]),solution([binding(x,int(5),'5')]),solution([binding(x,int(6),'6')]),solution([binding(x,int(7),'7')]),solution([binding(x,int(8),'8')]),solution([binding(x,int(9),'9')])].
644
645		test(simple_sat_all_solutions_two_vars, [nondet]) :-
646		init_idl_solver(GraphMut),
647		% all solutions for x>0 & x<4 & y>0 & y<4
648		register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])),
649		register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(4),integer,[])),pred,[])),
650		register_constraint(GraphMut, b(greater(b(identifier(y),integer,[]),b(integer(0),integer,[])),pred,[])),
651		register_constraint(GraphMut, b(less(b(identifier(y),integer,[]),b(integer(4),integer,[])),pred,[])),
652		!,
653		findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults),
654		length(SolverResults, Length),
655		Length == 9,
656		SolverResults == [solution([binding(y,int(1),'1'),binding(x,int(1),'1')]),solution([binding(y,int(2),'2'),binding(x,int(2),'2')]),solution([binding(y,int(3),'3'),binding(x,int(3),'3')]),solution([binding(x,int(2),'2'),binding(y,int(3),'3')]),solution([binding(x,int(1),'1'),binding(y,int(3),'3')]),solution([binding(x,int(1),'1'),binding(y,int(2),'2')]),solution([binding(y,int(2),'2'),binding(x,int(3),'3')]),solution([binding(y,int(1),'1'),binding(x,int(2),'2')]),solution([binding(y,int(1),'1'),binding(x,int(3),'3')])].
657
658		test(simple_sat_all_solutions_two_vars_subtraction, [nondet]) :-
659		init_idl_solver(GraphMut),
660		% all solutions for x>0 & x<10 & y>0 & y<10 & x-y>5
661		register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])),
662		register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(10),integer,[])),pred,[])),
663		register_constraint(GraphMut, b(greater(b(identifier(y),integer,[]),b(integer(0),integer,[])),pred,[])),
664		register_constraint(GraphMut, b(less(b(identifier(y),integer,[]),b(integer(10),integer,[])),pred,[])),
665		register_constraint(GraphMut, b(greater(b(minus(b(identifier(x),integer,[]),b(identifier(y),integer,[])),integer,[]),b(integer(5),integer,[])),pred,[])),
666		!,
667		findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults),
668		length(SolverResults, Length),
669		Length == 6,
670		SolverResults == [solution([binding(y,int(1),'1'),binding(x,int(7),'7')]),solution([binding(y,int(2),'2'),binding(x,int(8),'8')]),solution([binding(y,int(3),'3'),binding(x,int(9),'9')]),solution([binding(y,int(2),'2'),binding(x,int(9),'9')]),solution([binding(y,int(1),'1'),binding(x,int(8),'8')]),solution([binding(y,int(1),'1'),binding(x,int(9),'9')])].
671
672		test(simple_unsat1, [nondet]) :-
673		init_idl_solver(GraphMut),
674		% a-c<=1 & c-b<=-3 & b-a<=1
675		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
676		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])),
677		\+ register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(b),integer,[]),b(identifier(a),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
678		!,
679		get_solver_result(GraphMut, Res),
680		Res == contradiction_found,
681		get_unsat_core(UnsatCore),
682		UnsatCore = b(conjunct(b(conjunct(b(less_equal(b(minus(b(identifier(b),integer,_),b(identifier(a),integer,_)),integer,_),b(integer(1),integer,_)),pred,_),b(less_equal(b(minus(b(identifier(a),integer,_),b(identifier(c),integer,_)),integer,_),b(integer(1),integer,_)),pred,_)),pred,_),b(less_equal(b(minus(b(identifier(c),integer,_),b(identifier(b),integer,_)),integer,_),b(integer(-3),integer,_)),pred,_)),pred,_).
683
684		test(simple_unsat2, [nondet]) :-
685		init_idl_solver(GraphMut),
686		% c-c<=1 & a-c<=1 & c-b<=-3 & b-a<=1
687		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
688		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
689		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])),
690		\+ register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(b),integer,[]),b(identifier(a),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
691		!,
692		get_solver_result(GraphMut, Res),
693		Res == contradiction_found,
694		get_unsat_core(UnsatCore),
695		% c-c<=1 is not part of the unsat core
696		UnsatCore = b(conjunct(b(conjunct(b(less_equal(b(minus(b(identifier(b),integer,_),b(identifier(a),integer,_)),integer,_),b(integer(1),integer,_)),pred,_),b(less_equal(b(minus(b(identifier(a),integer,_),b(identifier(c),integer,_)),integer,_),b(integer(1),integer,_)),pred,_)),pred,_),b(less_equal(b(minus(b(identifier(c),integer,_),b(identifier(b),integer,_)),integer,_),b(integer(-3),integer,_)),pred,_)),pred,_).
697
698		test(simple_unsat_negation, [nondet]) :-
699		init_idl_solver(GraphMut),
700		% a-b<=-1 & a<=-1 & b<=10 & not(a<=-1)
701		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
702		register_constraint(GraphMut, b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),
703		register_constraint(GraphMut, b(less_equal(b(identifier(b),integer,[]),b(integer(10),integer,[])),pred,[])),
704		\+ register_constraint(GraphMut, b(negation(b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),pred,[])),
705		!,
706		get_solver_result(GraphMut, Res),
707		Res = contradiction_found,
708		get_unsat_core(UnsatCore),
709		% not(a<=-1) & a<=-1
710		UnsatCore = b(conjunct(b(negation(b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_),b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_).
711
712		test(simple_unsat_negation_rewrite_beforehand, [nondet]) :-
713		init_idl_solver(GraphMut),
714		% we receive the same unsat core containing the original constraints when rewriting constraints before registering them
715		% a-b<=-1 & a<=-1 & b<=10 & not(a<=-1)
716		C2 = b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[]),
717		C3 = b(less_equal(b(identifier(b),integer,[]),b(integer(10),integer,[])),pred,[]),
718		C4 = b(negation(b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),pred,[]),
719		rewrite_to_idl(C2, C2IdlConjList),
720		rewrite_to_idl(C3, C3IdlConjList),
721		rewrite_to_idl(C4, C4IdlConjList),
722		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
723		register_constraints(GraphMut, C2IdlConjList),
724		register_constraints(GraphMut, C3IdlConjList),
725		\+ register_constraints(GraphMut, C4IdlConjList),
726		!,
727		get_solver_result(GraphMut, Res),
728		Res = contradiction_found,
729		get_unsat_core(UnsatCore),
730		% not(a<=-1) & a<=-1
731		UnsatCore = b(conjunct(b(negation(b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_),b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_).
732
733		:- end_tests(difference_logic_solver).
734
735		:- begin_tests(dynamic_state).
736
737		empty_graph_state(GraphMut) :-
738		\+ negative_weight,
739		\+ contains_zero,
740		get_mutable(graph(nodes([]),edges([]),shortest_paths([])), GraphMut),
741		\+ constraint_store(_,_,_).
742
743		test(register_constraint_undone_on_bt1, []) :-
744		init_idl_solver(GraphMut),
745		empty_graph_state(GraphMut),
746		Constraint = b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[]),
747		( register_constraint(GraphMut, Constraint),
748		get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut),
749		memberchk(a, Nodes),
750		memberchk(b, Nodes),
751		memberchk(b:[(b,1,a,_)], Edges),
752		memberchk((a,0), SPs),
753		memberchk((b,0), SPs),
754		constraint_store(b,a,Constraint),
755		\+ negative_weight,
756		\+ contains_zero,
757		fail
758		; empty_graph_state(GraphMut)
759		).
760
761		test(register_constraint_undone_on_bt2, []) :-
762		init_idl_solver(GraphMut),
763		empty_graph_state(GraphMut),
764		Constraint = b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[]),
765		( register_constraint(GraphMut, Constraint),
766		get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut),
767		memberchk(a, Nodes),
768		memberchk('_zero', Nodes),
769		memberchk('_zero':[('_zero',-1,a,_)], Edges),
770		memberchk((a,-1), SPs),
771		memberchk(('_zero',0), SPs),
772		constraint_store('_zero',a,b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
773		negative_weight,
774		contains_zero,
775		fail
776		; empty_graph_state(GraphMut)
777		).
778
779		test(register_constraint_overwrite_old, [nondet]) :-
780		init_idl_solver(GraphMut),
781		empty_graph_state(GraphMut),
782		% a-b<=2 is replaced by a-b<=1
783		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(2),integer,[])),pred,[])),
784		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
785		get_mutable(graph(nodes(_),edges(Edges),shortest_paths(SPs)), GraphMut),
786		memberchk('b':[('b',1,a,_)], Edges),
787		memberchk((a,0), SPs),
788		memberchk((b,0), SPs).
789
790		test(register_constraint_overwrite_old_undone_on_bt, [nondet]) :-
791		init_idl_solver(GraphMut),
792		empty_graph_state(GraphMut),
793		% a-b<=2 is replaced by a-b<=1 but effect is undone on backtracking
794		register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(2),integer,[])),pred,[])),
795		( register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
796		fail
797		; get_mutable(graph(nodes(_),edges(Edges),shortest_paths(SPs)), GraphMut),
798		memberchk('b':[('b',2,a,_)], Edges),
799		memberchk((a,0), SPs),
800		memberchk((b,0), SPs)
801		).
802
803		:- end_tests(dynamic_state).