Commit bc2e0e1c authored by Mathieu Hemery's avatar Mathieu Hemery
Browse files

Correct the parser from glucose in solve_sat

parent c6a8ccb9
......@@ -329,6 +329,9 @@ write_morph(Tabint, G1, G2) :-
write_morph(Tabint, G1, G2, 0).
write_morph(_, [N1|_], [N2|_], N) :-
N is N1 * (N2 + 1) + 1.
write_morph([X|Tail], G1, G2, I) :-
X = "SAT",
write_morph(Tail, G1, G2, I).
write_morph([X|Tail], G1, G2, I) :-
atom_number(X, Xnum),
(m_to_morph(Xnum, G1, G2); true),
......@@ -490,14 +493,28 @@ add_solution(G1, G2, String) :-
write_neg_sol(Stream, Tabint, N1, N2),
close(Stream).
% solve_sat(+Graph1,+Graph2)
%
% search and write a SEpi between the 2 input graphs
% /!\ this function use indirectly /tmp/in.sat
solve_sat(G1, G2) :-
run_glucose('/tmp/in.sat'),
open('/tmp/out.sat', read, Stream, []),
read_string(Stream, '\n', "\r", _, String),
((String = "UNSAT", write('no sepi found\n'));
(split_string(String, " ", "", Tabint)),
write_morph(Tabint, G1, G2)); write('no sepi found\n'); true.
read_string(Stream, '', "\n\r", _, String),
(
(
String = "UNSAT",
write('no sepi found\n')
)
;
(
split_string(String, " \n", " \n", Tabint)
),
write_morph(Tabint, G1, G2)
);
write('no sepi found\n');
true.
search_sepi(G1, G2, Stream) :-
open('/tmp/in.sat', write, Stream),
......
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