Commit 6b01b8c8 authored by BARGAIN Orianne's avatar BARGAIN Orianne

renaming options

parent 4a14e374
......@@ -74,7 +74,7 @@ add_solution(File, Solution) :-
% @arg File Name of the cnf file in DIMACS format
% @arg Solution List of positive/negative integers for literals, or []
run_sat(File, Solution) :-
run_sat(File, normal, [Line]),
run_sat(File, no, [Line]),
(
Line = 'UNSAT'
->
......@@ -93,7 +93,7 @@ run_sat(File, Solution) :-
run_sat(FileIn, Bottom, Sepis) :-
statistics(walltime, [_ | [_]]),
(
Bottom = normal
Bottom = no
->
call_sat(FileIn, Sepis)
;
......
......@@ -15,24 +15,24 @@
%% Main part of SEPI search
%! search_sepi(+G1, +G2, +Stream, +Merge, +Bottom)
%! search_sepi(+G1, +G2, +Stream, +Merge, +Extremal_sepi)
%
% call all function that write clauses to the CNF file
% according to the options
%
% @arg G1 graph 1 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg G2 graph 2 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg Stream Stream for the CNF file
% @arg Merge no/neigh/old cf. sepi:merge_restriction/1
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
search_sepi(G1, G2, Stream, Merge, Bottom) :-
once(write_header(G1, G2, Stream, Bottom, Merge, 0)),
% @arg G1 graph 1 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg G2 graph 2 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg Stream Stream for the CNF file
% @arg Merge no/neighbours/old cf. sepi:merge_restriction/1
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
search_sepi(G1, G2, Stream, Merge, Extremal_sepi) :-
once(write_header(G1, G2, Stream, Extremal_sepi, Merge, 0)),
G1 = [N1| _],
G2 = [N2| _],
get_option(stats,Stats),
statistics(walltime, [_ | [_]]),
partial_surj(N1, N2, Stream, Bottom),
subgraph_epi(G1, G2, Stream, Bottom),
partial_surj(N1, N2, Stream, Extremal_sepi),
subgraph_epi(G1, G2, Stream, Extremal_sepi),
statistics(walltime, [_ | [Execution_time_core]]),
(
Stats = yes
......@@ -44,7 +44,7 @@ search_sepi(G1, G2, Stream, Merge, Bottom) :-
true
),
(
Merge = neigh
Merge = neighbours
->
statistics(walltime, [_ | [_]]),
once(merge_neigh(G1, G2, Stream)),
......@@ -77,13 +77,13 @@ search_sepi(G1, G2, Stream, Merge, Bottom) :-
true
),
(
Bottom \= normal
Extremal_sepi \= no
->
W is 1,
format(Stream, 'c bottom constraints \n', []),
statistics(walltime, [_ | [_]]),
(
Bottom = min_bottom
Extremal_sepi = minimal_deletion
->
bottom_min_constraint(N1, N2, W, Stream)
;
......@@ -130,14 +130,14 @@ write_header(G1, G2, Stream, Bottom, Merge, Solutions):-
Added_clauses_bottom is N1,
is_dummy(Na1, N1, N2, Na1, Na2, Nb_core_variables),
(
Bottom \= normal
Bottom \= no
->
Clauses_bottom is 1
;
Clauses_bottom is 0
),
(
Merge = neigh
Merge = neighbours
->
Clauses_neigh is 1
;
......@@ -146,7 +146,7 @@ write_header(G1, G2, Stream, Bottom, Merge, Solutions):-
Total_clauses is (Nb_core_clauses + Added_clauses_mapping + Clauses_neigh * Added_clauses_neigh + Clauses_bottom * Added_clauses_bottom),
Total_variables is Nb_core_variables,
(
Bottom \= normal
Bottom \= no
->
Top is (Added_clauses_bottom + 1),
format(Stream, "p wcnf ~d ~d ~d~n", [Total_variables, Total_clauses, Top]),
......@@ -180,7 +180,7 @@ partial_surj(N1, N2, Stream, Bottom) :-
left_totality(N1, N2, Stream, Bottom) :-
N1_1 is N1 - 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "~d ", [Top])
......@@ -197,7 +197,7 @@ left_totality(N1, N2, I, N, Stream, Bottom) :-
N is N2 + 1,
I1 is I + 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 2,
format(Stream, "0\n~d ", [Top])
......@@ -216,7 +216,7 @@ left_totality(N1, N2, I, J, Stream, Bottom) :-
right_totality(N1, N2, Stream, Bottom) :-
N2_1 is N2 - 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "~d ", [Top])
......@@ -231,7 +231,7 @@ right_totality(N1, N2, N1, N2, Stream, _) :-
right_totality(N1, N2, N1, J, Stream, Bottom) :-
J1 is J + 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "0\n~d ", [Top])
......@@ -298,7 +298,7 @@ subgraph_epi(G1, G2, Stream, Bottom) :-
left_totality_arcs(N1, N2, Na1, Na2, Stream, Bottom) :-
Na1_1 is Na1 - 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "~d ", [Top])
......@@ -315,7 +315,7 @@ left_totality_arcs(N1, N2, Na1, Na2, I, Na2, Stream, Bottom) :-
I1 is I + 1,
is_dummy(I, N1, N2, Na1, Na2, X),
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "~d 0\n~d ", [X, Top])
......@@ -334,7 +334,7 @@ left_totality_arcs(N1, N2, Na1, Na2, I, J, Stream, Bottom) :-
right_totality_arcs(N1, N2, Na1, Na2, Stream, Bottom) :-
Na2_1 is Na2 - 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "~d ", [Top])
......@@ -349,7 +349,7 @@ right_totality_arcs(_, _, Na1, Na2, Na1, Na2, Stream, _) :-
right_totality_arcs(N1, N2, Na1, Na2, Na1, J, Stream, Bottom) :-
J1 is J + 1,
(
Bottom \= normal
Bottom \= no
->
Top is N1 + 1,
format(Stream, "0\n~d ", [Top])
......@@ -496,7 +496,7 @@ write_redundant_morph(N1, N2, Arcs1, Arcs2, I, J, K, Stream, Bottom) :-
write_redundant_morph(N1, N2, Arcs1, Arcs2, I, J, K1, Stream, Bottom).
%! bigraph_constraint(+N1, +N2, +Id1, +Id2, +Stream, +Bottom)
%! bigraph_constraint(+N1, +N2, +Id1, +Id2, +Stream, +Extremal_sepi)
%
% mu is a morphism from an initial graph G1 to an image graph G2
% A can't have the image B through mu if they don't have the same type
......@@ -505,9 +505,9 @@ write_redundant_morph(N1, N2, Arcs1, Arcs2, I, J, K, Stream, Bottom) :-
% @arg N2 Number of vertices in graph 2
% @arg Id1 id of graph 1
% @arg Id2 id of graph 2
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
% @arg Stream Stream for the CNF file
bigraph_constraint(N1, N2, Id1, Id2, Stream, Bottom):-
bigraph_constraint(N1, N2, Id1, Id2, Stream, Extremal_sepi):-
N1_1 is N1 - 1,
N2_1 is N2 - 1,
numlist(0,N1_1,Vertex_G1),
......@@ -524,14 +524,14 @@ bigraph_constraint(N1, N2, Id1, Id2, Stream, Bottom):-
not(TypeA is TypeB)
)
->
write_bigraph_constraint(A, B, N1, N2, Stream, Bottom)
write_bigraph_constraint(A, B, N1, N2, Stream, Extremal_sepi)
;
true
)
).
%! write_bigraph_constraint(+A, +B, +N1, +N2, +Stream, +Bottom)
%! write_bigraph_constraint(+A, +B, +N1, +N2, +Stream, +Extremal_sepi)
%
% mu is a morphism from an initial graph G1 to an image graph G2
% A and B don't have the same type, thus A can't have the image B
......@@ -540,13 +540,13 @@ bigraph_constraint(N1, N2, Id1, Id2, Stream, Bottom):-
% @arg B Vertex B in graph 2
% @arg N1 Number of vertices in graph 1
% @arg N2 Number of vertices in graph 2
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
% @arg Stream Stream for the CNF file
write_bigraph_constraint(A, B, N1, N2, Stream, Bottom):-
write_bigraph_constraint(A, B, N1, N2, Stream, Extremal_sepi):-
m_ij(A, B, N2, X),
X1 is -X,
(
Bottom \= normal
Extremal_sepi \= no
->
Top is N1 + 1,
format(Stream, "~d ~d 0~n", [Top, X1])
......
......@@ -3,7 +3,7 @@
[
% Public API
search_reduction/2,
reduction/1,
extremal_sepi/1,
merge_restriction/1
]
).
......@@ -30,15 +30,15 @@
solve this NP-complete problem.').
:- grammar(reduction).
:- grammar(extremal_sepi).
reduction(normal).
extremal_sepi(no).
:- grammar_doc('\\emphright{Search standard reduction.}').
reduction(min_bottom).
extremal_sepi(minimal_deletion).
:- grammar_doc('\\emphright{Search reduction that minimises bottom (i.e., the number of deletions).}').
reduction(max_bottom).
extremal_sepi(maximal_deletion).
:- grammar_doc('\\emphright{Search reduction that maximises bottom (i.e., the number of deletions).}').
:- grammar(merge_restriction).
......@@ -46,7 +46,7 @@ reduction(max_bottom).
merge_restriction(no).
:- grammar_doc('\\emphright{Search standard reduction.}').
merge_restriction(neigh).
merge_restriction(neighbours).
:- grammar_doc('\\emphright{Search reduction with local two-neighbour restriction.}').
merge_restriction(old).
......@@ -57,8 +57,8 @@ merge_restriction(old).
:- initial(option(merge_restriction: no)).
:- initial(option(timeout: 180)).
:- initial(option(all_reductions: no)).
:- initial(option(max_reductions: 200)).
:- initial(option(reduction: normal)).
:- initial(option(max_nb_reductions: 200)).
:- initial(option(extremal_sepi: no)).
:- initial(option(stats: no)).
......@@ -88,9 +88,9 @@ search_reduction(FileName1, FileName2) :-
option(timeout, number, Timeout, 'timeout for the (Max)SAT solver'),
option(all_reductions, yesno, Reductions,
'specifies if solver is looking for all SEPI reductions or not'),
option(max_reductions, number, MaxReduc,
option(max_nb_reductions, number, MaxReduc,
'limits the number of SEPI reductions the solver is looking for'),
option(reduction, reduction, Bottom, 'defines the type of reduction searched'),
option(extremal_sepi, extremal_sepi, Bottom, 'defines the type of reduction searched'),
option(stats, yesno, _Stats, 'display computation time'),
debug(sepi, "Debugging sepi", []),
(
......@@ -106,14 +106,13 @@ search_reduction(FileName1, FileName2) :-
merge_restriction: Merge,
timeout: Timeout,
all_reductions: Reductions,
max_reductions: MaxReduc,
reduction: Bottom
max_nb_reductions: MaxReduc,
extremal_sepi: Bottom
],
main_search_reduction(G1, G2, FileIn)
),
(
delete_file(FileRoot),
delete_file(FileIn)
delete_file(FileRoot)
;
true
)
......@@ -144,8 +143,8 @@ main_search_reduction(G1, G2, FileIn):-
get_option(merge_restriction, Merge),
get_option(timeout, Timeout),
get_option(all_reductions, Reductions),
get_option(max_reductions, MaxReduc),
get_option(reduction, Bottom),
get_option(max_nb_reductions, MaxReduc),
get_option(extremal_sepi, Bottom),
debug(sepi, "Options: Mapping: ~w, Merge: ~w, Timeout, ~w, All Reductions: ~w, Max Reductions: ~w, Reduction: ~w", [Mapping, Merge, Timeout, Reductions, MaxReduc, Bottom]),
open(FileIn, write, Stream),
once(search_sepi(G1, G2, Stream, Merge, Bottom)),
......
......@@ -58,7 +58,7 @@ test('all_reductions_sucess') :-
test('bottom_min_success') :-
with_output_to(
atom(Result),
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM2.bc", reduction: min_bottom).')
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM2.bc", extremal_sepi: minimal_deletion).')
),
atomic_list_concat(Split, '\n', Result),
count_end('-> deleted', Split, 1).
......@@ -67,7 +67,7 @@ test('bottom_min_success') :-
test('bottom_min_fail') :-
with_output_to(
atom(Result),
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM3.bc", reduction: min_bottom).')
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM3.bc", extremal_sepi: minimal_deletion).')
),
atomic_list_concat(Split, '\n', Result),
count_start('no sepi found', Split, 1).
......@@ -76,7 +76,7 @@ test('bottom_min_fail') :-
test('all_bottom_min_success') :-
with_output_to(
atom(Result),
command('search_reduction("library:examples/sepi/MM4.bc", "library:examples/sepi/MM2.bc", all_reductions: yes, reduction: min_bottom).')
command('search_reduction("library:examples/sepi/MM4.bc", "library:examples/sepi/MM2.bc", all_reductions: yes, extremal_sepi: minimal_deletion).')
),
atomic_list_concat(Split, '\n', Result),
count_start('sepi', Split, 3).
......@@ -85,7 +85,7 @@ test('all_bottom_min_success') :-
test('bottom_max_success') :-
with_output_to(
atom(Result),
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM2.bc", reduction: max_bottom).')
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM2.bc", extremal_sepi: maximal_deletion).')
),
atomic_list_concat(Split, '\n', Result),
count_end('-> deleted', Split, 2).
......@@ -94,7 +94,7 @@ test('bottom_max_success') :-
test('all_bottom_max_success') :-
with_output_to(
atom(Result),
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM2.bc", reduction: max_bottom, all_reductions: yes).')
command('search_reduction("library:examples/sepi/MM1.bc", "library:examples/sepi/MM2.bc", extremal_sepi: maximal_deletion, all_reductions: yes).')
),
atomic_list_concat(Split, '\n', Result),
count_start('sepi', Split, 2).
......
......@@ -31,9 +31,9 @@ constraints(G1, G2, [(Label1 -> deleted)|T], Stream) :-
G2 = [N2, _, _, _],
species(Label1, X, Id1),
m_ij(X, N2, N2, Dummy),
get_option(reduction, Reduction),
get_option(extremal_sepi, Extremal_sepi),
(
not(Reduction=normal)
Extremal_sepi \= no
->
Top is N1 + 1,
format(Stream, "~d ~d 0~n", [Top, Dummy])
......@@ -48,9 +48,9 @@ constraints(G1, G2, [(Label1 -> Label2)|T], Stream) :-
species(Label1, X1, Id1),
species(Label2, X2, Id2),
m_ij(X1, X2, N2, X),
get_option(reduction, Reduction),
get_option(extremal_sepi, Extremal_sepi),
(
not(Reduction=normal)
Extremal_sepi \= no
->
Top is N1 + 1,
format(Stream, "~d ~d 0~n", [Top, X])
......
......@@ -133,9 +133,9 @@ neigh_clauses_not_neigh_assert(A, B, N1, G2, Stream):-
(
m_ij(A, Y, N2, May),
m_ij(B, Y, N2, Mby),
get_option(reduction, Reduction),
get_option(extremal_sepi, Extremal_sepi),
(
not(Reduction=normal)
Extremal_sepi \= no
->
Top is N1 + 1,
format(Stream, "~d -~d -~d 0~n", [Top, May, Mby])
......
......@@ -15,7 +15,7 @@ count_start(Atom, List, Count) :-
test('sepi_merge_neigh_fail') :-
with_output_to(
atom(Output),
command('search_reduction("library:examples/sepi/N1.bc", "library:examples/sepi/N3.bc", merge_restriction: neigh).')
command('search_reduction("library:examples/sepi/N1.bc", "library:examples/sepi/N3.bc", merge_restriction: neighbours).')
),
Output = 'no sepi found\nNumber of reductions: 0\n'.
......@@ -23,7 +23,7 @@ test('sepi_merge_neigh_fail') :-
test('sepi_merge_neigh_success') :-
with_output_to(
atom(Result),
command('search_reduction("library:examples/sepi/N1.bc", "library:examples/sepi/N7.bc", merge_restriction: neigh).')
command('search_reduction("library:examples/sepi/N1.bc", "library:examples/sepi/N7.bc", merge_restriction: neighbours).')
),
atomic_list_concat(Split, '\n', Result),
count_start('sepi', Split, 1).
......
......@@ -18,13 +18,10 @@
% Can't use MAX-SAT solver with old merge restriction
/* search_sepi_merge */
/* search_sepi_merge(+G1, +G2, +Stream, +Merge, +Bottom)
/* search_sepi_merge(+G1, +G2, +Stream)
+G1: graph 1 [NbVertexe, NbSpecie, EdgesList, Id]
+G2: graph 2 [NbVertexe, NbSpecie, EdgesList, Id]
+Stream: where to write clauses
+Merge: yes if merge restriction
+Bottom: yes if bottom minimisation*/
+Stream: where to write clauses */
search_sepi_merge(G1, G2, Stream) :-
merge_cond(G1, G2, Stream),
restrict_merge(G1, G2, Stream), !.
......
......@@ -16,31 +16,31 @@
%% SAT Solver part
%% Call the sat solver and write the solution once all clauses are written in the Stream
%! solve_sat(+G1, +G2, +FileIn, +Reductions, +Bottom, +Merge, +MaxReduc, +NbDelete, -NbReductions)
%! solve_sat(+G1, +G2, +FileIn, +Reductions, +Extremal_sepi, +Merge, +MaxReduc, +NbDelete, -NbReductions)
%
% @arg G1 graph 1 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg G2 graph 2 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg FileIn input file for sat solver
% @arg Reductions yesno yes if looking for all reductions between G1 and G2
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
% @arg Merge yes if merge reduction
% @arg MaxReduc limit the numer of reductions
% @arg NbDelete number of deletion in the solution
% @arg NbReductions number of reductions
solve_sat(_G1, _G2, _FileIn, _Reductions, _Bottom, _Merge, 0, _NbDeleteInit, 0) :-
solve_sat(_G1, _G2, _FileIn, _Reductions, _Extremal_sepi, _Merge, 0, _NbDeleteInit, 0) :-
write('no sepi found\n'),
!.
solve_sat(G1, G2, FileIn, Reductions, Bottom, Merge, MaxReduc, NbDeleteInit, NbReductions) :-
run_sat(FileIn, Bottom, Output),
solve_sat(G1, G2, FileIn, Reductions, Extremal_sepi, Merge, MaxReduc, NbDeleteInit, NbReductions) :-
run_sat(FileIn, Extremal_sepi, Output),
(
(
Output = []
;
Output = ['UNSAT']
;
Bottom \= normal,
% we have already started min/maxing bottom
Extremal_sepi \= no,
% we have already started min/maxing Extremal_sepi
NbDeleteInit \= "-1",
% we find a worse solution
Output \= [_, NbDeleteInit | _]
......@@ -51,7 +51,7 @@ solve_sat(G1, G2, FileIn, Reductions, Bottom, Merge, MaxReduc, NbDeleteInit, NbR
;
Output = [Sepi | OutputRest],
(
Bottom \= normal
Extremal_sepi \= no
->
OutputRest = [NbDelete | _]
;
......@@ -62,15 +62,15 @@ solve_sat(G1, G2, FileIn, Reductions, Bottom, Merge, MaxReduc, NbDeleteInit, NbR
split_string(Sepi, " \n", " \n", Tabint),
write_morph(Tabint, G1, G2),
(
Bottom = normal
Extremal_sepi = no
->
true
;
Bottom = min_bottom
Extremal_sepi = minimal_deletion
->
format("Number of deletions: ~w~n", [NbDelete])
;
% max_bottom
% maximal_deletion
G1 = [N1,_, _, _],
number_string(Number, NbDelete),
NbDeleteMax is (N1 - Number),
......@@ -80,12 +80,12 @@ solve_sat(G1, G2, FileIn, Reductions, Bottom, Merge, MaxReduc, NbDeleteInit, NbR
Reductions = yes
->
debug(sepi, "Looking for other solutions", []),
get_option(max_reductions, MaxSol),
get_option(max_nb_reductions, MaxSol),
NbSol is (MaxSol - MaxReduc + 1),
debug(sepi, "MaxSol: ~w - MaxReduc: ~w - NbSol: ~w", [MaxSol, MaxReduc, NbSol]),
add_solution(G1, G2, FileIn, Tabint, Bottom, Merge, NbSol),
add_solution(G1, G2, FileIn, Tabint, Extremal_sepi, Merge, NbSol),
MaxSubReduc is MaxReduc - 1,
solve_sat(G1, G2, FileIn, Reductions, Bottom,
solve_sat(G1, G2, FileIn, Reductions, Extremal_sepi,
Merge, MaxSubReduc, NbDelete, NbSubReductions),
NbReductions is NbSubReductions + 1
;
......@@ -137,26 +137,26 @@ m_to_morph(I, G1, G2) :-
%% Compute all reductions
%! add_solution(+G1, +G2, +FileIn, +Tabint, +Bottom, +Merge, +NbSol)
%! add_solution(+G1, +G2, +FileIn, +Tabint, +Extremal_sepi, +Merge, +NbSol)
%
% @arg G1 graph 1 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg G2 graph 2 [NbVertexe, NbSpecie, EdgesList, Id]
% @arg FileIn Input file for sat solver
% @arg Tabint previous sepi found
% @arg Bottom yes if bottom minimisation
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
% @arg Merge yes if merge restriction
% @arg NbSol nb of solutions already found
add_solution(G1, G2, FileIn, Tabint, Bottom, Merge, NbSol) :-
add_solution(G1, G2, FileIn, Tabint, Extremal_sepi, Merge, NbSol) :-
debug(sepi, "adding solution to input file", []),
G1 = [N1 | _],
G2 = [N2 | _],
open(FileIn, update, Stream1),
write_header(G1, G2, Stream1, Bottom, Merge, NbSol),
write_header(G1, G2, Stream1, Extremal_sepi, Merge, NbSol),
format(Stream1, "c ", []),
close(Stream1),
open(FileIn, append, Stream2),
(
Bottom = normal
Extremal_sepi = no
->
true
;
......
......@@ -93,19 +93,19 @@ is_dummy(I, N1, N2, Narcs1, Narcs2, X) :-
X is X1 + I.
%! implies(+A, +B, +Stream, +Bottom, +Top)
%! implies(+A, +B, +Stream, +Extremal_sepi, +Top)
%
% translate 'A=>B' to '-A or B'
%
% @arg A First SAT variable
% @arg B Second SAT variable
% @arg Stream Stream for the CNF file
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
% @arg Top Clause's weight in the CNF file
implies(A, B, Stream, Bottom, Top) :-
% @arg A First SAT variable
% @arg B Second SAT variable
% @arg Stream Stream for the CNF file
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
% @arg Top Clause's weight in the CNF file
implies(A, B, Stream, Extremal_sepi, Top) :-
A1 is -A,
(
Bottom \= normal
Extremal_sepi \= no
->
format(Stream, '~d ~d ~d 0~n', [Top, A1, B])
;
......@@ -113,21 +113,21 @@ implies(A, B, Stream, Bottom, Top) :-
).
%! a_and_b_implies(+A, +B, +C, +Stream, +Bottom, +Top)
%! a_and_b_implies(+A, +B, +C, +Stream, +Extremal_sepi, +Top)
%
% translate 'A and B => C' to '-A or -B or C'
%
% @arg A First SAT variable
% @arg B Second SAT variable
% @arg C Third SAT variable
% @arg Stream Stream for the CNF file
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
% @arg Top Clause's weight in the CNF file
a_and_b_implies(A, B, C, Stream, Bottom, Top) :-
% @arg A First SAT variable
% @arg B Second SAT variable
% @arg C Third SAT variable
% @arg Stream Stream for the CNF file
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
% @arg Top Clause's weight in the CNF file
a_and_b_implies(A, B, C, Stream, Extremal_sepi, Top) :-
A1 is -A,
B1 is -B,
(
Bottom \= normal
Extremal_sepi \= no
->
format(Stream, '~d ~d ~d ~d 0~n', [Top, A1, B1, C])
;
......@@ -135,61 +135,61 @@ a_and_b_implies(A, B, C, Stream, Bottom, Top) :-
).
%! inf_imp_not_equ(+I, +J, +N1, +N2, +Stream, +Bottom)
%! inf_imp_not_equ(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
%
% mu is a morphism from an initial graph G1 to an image graph G2
% 'mu(i) < j' implies 'mu(i) != j'
%
% @arg I Interger representing the vertex i in the initial graph
% @arg J Interger representing the vertex j in the image graph
% @arg N1 Number of vertices in the initial graph
% @arg N2 Number of vertices in the image graph
% @arg Stream Stream for the CNF file
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
inf_imp_not_equ(I, J, N1, N2, Stream, Bottom) :-
% @arg I Interger representing the vertex i in the initial graph
% @arg J Interger representing the vertex j in the image graph
% @arg N1 Number of vertices in the initial graph
% @arg N2 Number of vertices in the image graph
% @arg Stream Stream for the CNF file
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
inf_imp_not_equ(I, J, N1, N2, Stream, Extremal_sepi) :-
m_inf_ij(I, J, N1, N2, X1),
m_ij(I, J, N2, X2),
X3 is -X2,
Top is N1 + 1,
implies(X1, X3, Stream, Bottom, Top).
implies(X1, X3, Stream, Extremal_sepi, Top).
%! equ_impl_inf(+I, +J, +N1, +N2, +Stream, +Bottom)
%! equ_impl_inf(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
%
% mu is a morphism from an initial graph G1 to an image graph G2
% 'mu(i) = j' implies 'mu(i) < j + 1'
%
% @arg I Interger representing the vertex i in the initial graph
% @arg J Interger representing the vertex j in the image graph
% @arg N1 Number of vertices in the initial graph
% @arg N2 Number of vertices in the image graph
% @arg Stream Stream for the CNF file
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
equ_impl_inf(I, J, N1, N2, Stream, Bottom) :-
% @arg I Interger representing the vertex i in the initial graph
% @arg J Interger representing the vertex j in the image graph
% @arg N1 Number of vertices in the initial graph
% @arg N2 Number of vertices in the image graph
% @arg Stream Stream for the CNF file
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
equ_impl_inf(I, J, N1, N2, Stream, Extremal_sepi) :-
J1 is J + 1,
m_ij(I, J, N2, X1),
m_inf_ij(I, J1, N1, N2, X2),
Top is N1 + 1,
implies(X1, X2, Stream, Bottom, Top).
implies(X1, X2, Stream, Extremal_sepi, Top).
%! inf_impl_inf(+I, +J, +N1, +N2, +Stream, +Bottom)
%! inf_impl_inf(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
%
% mu is a morphism from an initial graph G1 to an image graph G2
% 'mu(i) < j' implies 'mu(i) < j + 1'
%
% @arg I Interger representing the vertex i in the initial graph
% @arg J Interger representing the vertex j in the image graph
% @arg N1 Number of vertices in the initial graph
% @arg N2 Number of vertices in the image graph
% @arg Stream Stream for the CNF file
% @arg Bottom min_bottom/max_bottom/normal cf. sepi:reduction/1
inf_impl_inf(I, J, N1, N2, Stream, Bottom) :-
% @arg I Interger representing the vertex i in the initial graph
% @arg J Interger representing the vertex j in the image graph
% @arg N1 Number of vertices in the initial graph
% @arg N2 Number of vertices in the image graph
% @arg Stream Stream for the CNF file
% @arg Extremal_sepi no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
inf_impl_inf(I, J, N1, N2, Stream, Extremal_sepi) :-
J1 is J + 1,
m_inf_ij(I, J, N1, N2, X1),
m_inf_ij(I, J1, N1, N2, X2),
Top is N1 + 1,
implies(X1, X2, Stream, Bottom, Top).
implies(X1, X2, Stream, Extremal_sepi, Top).
%! nieme(+I, +List, -Value)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment