Commit 80be053c authored by BARGAIN Orianne's avatar BARGAIN Orianne
Browse files

change maxsat solver and all reductions for bottom minimisation (with still an error at the end)

parent 0183380f
......@@ -107,7 +107,7 @@ solve_sat(G1, G2, Reductions, Bottom) :-
),
run_sat(Filename, Bottom),
open('/tmp/out.sat', read, Stream, []),
read_string(Stream, '', "\n\r", _, String),
read_string(Stream, '', "\n\r", End, String),
(
(
String = "UNSAT",
......@@ -119,9 +119,11 @@ solve_sat(G1, G2, Reductions, Bottom) :-
write('sepi\n'),
write_morph(Tabint, G1, G2),
debug(sepi, "sepi found", []),
(Reductions=yes ->
(Bottom=no, Reductions=yes ->
(add_solution(G1, G2, String),
solve_sat(G1, G2, Reductions, Bottom)); true)
solve_sat(G1, G2, Reductions, Bottom)); true),
(Bottom=yes, Reductions=yes ->
debug(bottom, "End: ~w", [End]))
)
);
write('no sepi found\n');
......@@ -131,18 +133,16 @@ run_sat(Filename, Bottom) :-
debug(sepi, "running satsolver", []),
debug(bottom, "Filename: ~w", [Filename]),
(Bottom=yes ->
debug(bottom, "running minimaxsat", []),
process_create(path('minimaxsat1.0'),
['-F=2',Filename],
debug(bottom, "running rc2", []),
process_create(path('rc2.py'),
['-vv','-e','all',Filename],
[process(Id), stderr(null), stdout(pipe(Out))]),
read_lines(Out, Line),
read_lines(Out, Sepis),
close(Out),
re_matchsub("v (?<sol>.*)", Line, Sub, []),
Sol=Sub.sol,
open('/tmp/out.sat', write, Stream),
format(Stream, "~w~n", [Sol]),
print_lines(Sepis, Stream),
close(Stream),
debug(bottom, "minimaxsat output: ~w", [Sol])
debug(bottom, "rc2 output solution: ~w", [Sepis])
;
debug(bottom, "running glucose", []),
process_create(path(glucose),
......@@ -152,19 +152,45 @@ run_sat(Filename, Bottom) :-
get_option(timeout,Timeout),
catch(call_with_time_limit(Timeout,wait(Id,_)), _, (process_kill(Id), write('\ntimed out '), write(Timeout), write('sec\n'))).
read_lines(Out, Solution) :-
read_lines(Out, Solutions) :-
read_line_to_codes(Out, Line1),
read_lines(Line1, Out, Solution).
read_lines(end_of_file, _, "") :- !.
read_lines(Codes, _, Solution) :-
atom_codes(Solution, Codes),
re_match("v .*", Solution).
read_lines(_, Out, Solution) :- % debug read_lines(Codes, Out, Solution)
% atom_codes(Line, Codes), % debug
% debug(bottom, "Line is: ~w", [Line]),
Cost = "-1",
read_lines(Line1, Out, Solutions, Cost).
read_lines(end_of_file, _, [], _) :- !.
read_lines(Codes, Out, [], Cost) :-
atom_codes(Line, Codes),
re_match("c cost: .*", Line),
Cost = "1",
debug(bottom, "~w", [Line]),
read_line_to_codes(Out, _),
!.
read_lines(Codes, Out, Solutions, Cost) :-
atom_codes(Line, Codes),
(re_match("c cost: .*", Line);
re_match("o 0", Line)),
NewCost = "1",
Cost = "-1",
read_line_to_codes(Out, Line2),
read_lines(Line2, Out, Solutions, NewCost).
read_lines(Codes, Out, [Sepi|Solutions], Cost) :-
atom_codes(Line, Codes),
re_matchsub("v (?<sepi>.*)", Line, Sub, []),
Sepi=Sub.sepi,
debug(bottom, "~w", [Line]),
read_line_to_codes(Out, Line2),
read_lines(Line2, Out, Solution).
read_lines(Line2, Out, Solutions, Cost).
read_lines(_, Out, Solutions, Cost) :- % debug read_lines(Codes, Out, Solutions)
%atom_codes(Line, Codes), % debug
%debug(bottom, "Line is: ~w", [Line]),
read_line_to_codes(Out, Line2),
read_lines(Line2, Out, Solutions, Cost).
print_lines([],_) :- !.
print_lines([Head|Tail], Stream):-
format(Stream, "~w~n", [Head]),
%debug(bottom, "~w", [Head]),
print_lines(Tail, Stream).
write_morph(Tabint, G1, G2) :-
write_morph(Tabint, G1, G2, 0).
......
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