Commit 99906c3c authored by FAGES Francois's avatar FAGES Francois
Browse files

mergning

Merge branch 'develop' of gitlab.inria.fr:lifeware/biocham into develop
parents f646f48a 9a4a0bf1
# make jupyter will make biocham without checking unitary tests (avoiding potential problems of access to BioModels in sbml.plt)
ADDITIONAL_MODULES= \
modules/sbml/sbml_utils.pl \
modules/partialfrac/partialfraction.pl
......
......@@ -198,8 +198,10 @@ def handle_bokeh_plot(fig, gui_fig, against, cds=None, gui_cds=None, old_handle=
gui_layout = gui_fig
if against != 'Time':
button = Button(label="Animate", callback=animation_callback(cds))
gui_button = Button(label="Animate", callback=animation_callback(gui_cds))
button = Button(label="Animate")
button.js_on_click(animation_callback(cds))
gui_button = Button(label="Animate")
gui_button.js_on_click(animation_callback(gui_cds))
layout = column(fig, button)
gui_layout = column(gui_fig, gui_button, sizing_mode="scale_width")
......
......@@ -289,7 +289,9 @@ reduction_methods(no).
reduction_methods(native).
reduction_methods(sat).
reduction_methods(sat_species).
reduction_methods(sat_reactions).
%! compile_from_pivp(+PIVP_string, +Output)
......@@ -1300,7 +1302,7 @@ breadth_search(PODE, ListVariable, Redvar) :-
displace_exponent([1],0,Lm,First_Var),
get_option(binomial_reduction, Reduction),
(
Reduction == sat
atom_concat('sat', _, Reduction)
->
maxsat_binomial_reduction(ListVariable, ListDerivative, First_Var, Redvar)
;
......@@ -1813,10 +1815,29 @@ maxsat_binomial_reduction(AllVariables, AllDerivatives, OutVar, Solution) :-
% hence their number is a good Top value for the hard clauses
length(AllVariables, N),
nth1(OutIndex, AllVariables, OutVar),
derivatives_to_variables(AllDerivatives, AllVariables, Coverings),
derivatives_to_variables(AllDerivatives, AllVariables, Coverings, AllMonomials),
get_option(binomial_reduction, Reduction),
(
Reduction == sat_species
->
% we have N-1 soft clauses for each variable
Top = N,
NVar = N,
NMono = 0,
M = 0
;
append(AllMonomials, MonoClauses),
length(MonoClauses, NMono),
sort(MonoClauses, SMonoClauses),
length(SMonoClauses, M),
% we have M soft clauses for each unique monomial
Top is M + 1,
NVar is N + M
),
debug(pivp, "all mono: ~w", [AllMonomials]),
% we overestimate the number of clauses, but rc2.py is ok with that
maplist(length, Coverings, NCov),
sum_list(NCov, NClauses),
sum_list([NMono, Top | NCov], NClauses),
tmp_file_stream(text, FileRoot, StreamFileInInit),
close(StreamFileInInit),
string_concat(FileRoot, ".wcnf", FileIn),
......@@ -1825,9 +1846,16 @@ maxsat_binomial_reduction(AllVariables, AllDerivatives, OutVar, Solution) :-
open(FileIn, write, Stream),
(
% header
format(Stream, "p wcnf ~d ~d ~d~n", [N, NClauses, N]),
write_variable_clauses(Stream, N, OutIndex),
write_derivative_covering_clauses(Stream, N, Coverings)
format(Stream, "p wcnf ~d ~d ~d~n", [NVar, NClauses, Top]),
write_variable_clauses(Stream, N, M, OutIndex, Top, Reduction),
write_derivative_covering_clauses(Stream, N, Top, Coverings),
(
Reduction == sat_reactions
->
write_monomial_clauses(Stream, N, Top, SMonoClauses, AllMonomials)
;
true
)
),
close(Stream)
),
......@@ -1837,22 +1865,41 @@ maxsat_binomial_reduction(AllVariables, AllDerivatives, OutVar, Solution) :-
run_sat(FileIn, yes, [ResVariables, _Weight]),
variable_string_to_solution(ResVariables, AllVariables, Solution)
),
delete_file(FileIn)
(
have_to_delete_temporary_files
->
delete_file(FileIn)
;
true
)
).
%! write_variable_clauses(+Stream, +N, +OutIndex) is det.
%! write_variable_clauses(+Stream, +N, +M, +OutIndex, +Top, +Reduction) is det.
%
% Write to stream one clause per possible variable to include.
% it is a hard clause (weight is N) if it is the output variable
% it is a hard clause (weight is Top) if it is the output variable
% otherwise the negation is a soft clause
write_variable_clauses(Stream, N, OutIndex) :-
write_variable_clauses(Stream, N, M, OutIndex, Top, Reduction) :-
forall(
between(1, N, I),
(
Reduction == sat_species
->
between(1, N, I)
;
(
% if we minimize monomials, no soft clauses for variables
I = OutIndex
;
Start is N + 1,
End is N + M,
between(Start, End, I)
)
),
(
(
I == OutIndex
->
Weight = N,
Weight = Top,
Value = I
;
Weight = 1,
......@@ -1863,11 +1910,11 @@ write_variable_clauses(Stream, N, OutIndex) :-
).
%! write_derivative_covering_clauses(Stream, N, Coverings)
%! write_derivative_covering_clauses(Stream, N, Top, Coverings)
%
% Write clause that impose that if a variable is present, its derivative is covered by
% present variables
write_derivative_covering_clauses(Stream, N, Coverings) :-
write_derivative_covering_clauses(Stream, N, Top, Coverings) :-
forall(
between(1, N, I),
(
......@@ -1883,13 +1930,35 @@ write_derivative_covering_clauses(Stream, N, Coverings) :-
% II is not at the right position in clause, but rc2.py is ok
% with that too
atomic_list_concat([II | Co], ' ', Clause),
format(Stream, "~d ~w 0~n", [N, Clause])
format(Stream, "~d ~w 0~n", [Top, Clause])
)
)
)
).
%! write_monomial_clauses(Stream, N, SMonoClauses, AllMonomials) is det.
%
% Write clauses imposing that if a variable is present, all monomials of its derivative are present too
write_monomial_clauses(Stream, N, Top, SMonoClauses, AllMonomials) :-
forall(
between(1, N, I),
(
nth1(I, AllMonomials, Monomials),
maplist(get_mono(SMonoClauses, N), Monomials, Numbers),
forall(
member(Number, Numbers),
format(Stream, "~d -~w ~w 0~n", [Top, I, Number])
)
)
).
get_mono(List, Offset, Element, Position) :-
nth1(Index, List, Element),
Position is Index + Offset.
%! variable_string_to_solution(+String: string, AllVariables: list, -Solution: list) is det.
%
% Convert the output of the MaxSAT solver (-1 2 3 -4 ...) to a list of the
......@@ -1909,22 +1978,30 @@ variable_string_to_solution(String, AllVariables, Solution) :-
).
%! derivatives_to_variables(+AllDerivatives, +AllVariables, -Coverings) is det.
%! derivatives_to_variables(+AllDerivatives, +AllVariables, -Coverings, -AllMonomials) is det.
%
% Return a list corresponding to the clauses for covering each derivative
derivatives_to_variables(AllDerivatives, AllVariables, Coverings) :-
maplist(derivative_to_variables(AllVariables), AllDerivatives, Coverings).
% and a list of all monomials (without coefficients) appearing in each derivative
derivatives_to_variables(AllDerivatives, AllVariables, Coverings, AllMonomials) :-
maplist(derivative_to_variables(AllVariables), AllDerivatives, Coverings, AllMonomials).
%! derivative_to_variables(+AllVariables, +Derivative, -Covering) is det.
%! derivative_to_variables(+AllVariables, +Derivative, -Covering, -Monomials) is det.
%
% Covering is a list of clauses covering all monomials of Derivative
derivative_to_variables(AllVariables, Derivative, Covering) :-
% Monomials is the list of monomials (without coefficients) appearing in Derivative
derivative_to_variables(AllVariables, Derivative, Covering, Monomials) :-
maplist(monomial_to_variables(AllVariables), Derivative, Coverings),
% we flatten our conjunction of conjunctions
append(Coverings, Covering).
append(Coverings, Covering),
maplist(monomial_remove_coeff, Derivative, Monomials).
%! monomial_remove_coeff([+Coeff, +Monomial], -Monomial) is det.
%
% Remove the coefficient of a monomial
monomial_remove_coeff([_, M], M).
%! monomial_to_variables(+AllVariables, +Monomial, -Covering) is det.
%
% make a list of clauses for the possible coverings of Monomial (ignoring its constant
......
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