Commit 51fe2340 authored by Mathieu Hemery's avatar Mathieu Hemery

Merge branch 'develop' of gitlab.inria.fr:lifeware/biocham into develop

parents c34ffced c1ad6ede
......@@ -653,6 +653,11 @@ rewrite_additive_normal_form(A * (B * C), D * C) :-
rewrite_additive_normal_form(A * (B * C), B * (A * C)) :-
number(B).
rewrite_additive_normal_form((A * B) / C, D * B) :-
number(A),
number(C),
D is A/C.
rewrite_additive_normal_form((A * B) / C, A * (B / C)) :-
number(A).
......
......@@ -693,6 +693,7 @@ compute_domain~w(const Table &table) {
declare_formula(ExpandedFormula, RootIndex),
write(
' \c
// using PPL::IO_Operators::operator<<;
for (Table::const_reverse_iterator i = table.rbegin(); i != table.rend();
++i) {
'),
......@@ -723,14 +724,6 @@ generate_sub_formula(Predicate, Index) :-
Precision is 10 ** FOLTLPrecision,
binary_predicate(Predicate, A, Op, B),
!,
with_output_to(
atom(Left),
generate_expression(A)
),
with_output_to(
atom(Right),
generate_expression(B)
),
peek_count(free_variables, FreeVariableCount),
(
(
......@@ -739,20 +732,41 @@ generate_sub_formula(Predicate, Index) :-
has_variable(B)
)
->
additive_normal_form(A*Precision, AA),
extract_variables(AA, AAA),
with_output_to(
atom(Left),
generate_expression(AAA)
),
additive_normal_form(B*Precision, BB),
extract_variables(BB, BBB),
with_output_to(
atom(Right),
generate_expression(BBB)
),
format(
' \c
Domain next_domain~d(~d, PPL::EMPTY);
{
PPL::Constraint_System cs;
cs.set_space_dimension(~d);
cs.insert((~a) * ~d ~a (~a) * ~d);
PPL::Constraint newconstraint = (~a) ~a (~a) ;
cs.insert(newconstraint);
// std::cerr << "Constraint: " << newconstraint << std::endl;
next_domain~d.add_disjunct(PPL::NNC_Polyhedron(cs));
}
',
[Index, FreeVariableCount, FreeVariableCount, Left, Precision,
Op, Right, Precision, Index]
[Index, FreeVariableCount, FreeVariableCount, Left, Op, Right, Index]
)
;
with_output_to(
atom(Left),
generate_expression(A)
),
with_output_to(
atom(Right),
generate_expression(B)
),
format(
' \c
Domain next_domain~d(~d, ~a ~a ~a ? PPL::UNIVERSE : PPL::EMPTY);
......@@ -953,7 +967,8 @@ check_linearity_expression(Expression) :-
->
throw(error(not_linear(Expression)))
;
true
check_linearity_expression(A),
check_linearity_expression(B)
).
check_linearity_expression(Expression) :-
......@@ -1233,3 +1248,39 @@ letter_index(Letter, Index) :-
user:portray(ltl_pattern(Thing)) :-
format("ltl_pattern ~p",[Thing]).
%! extract_variables(+Expr1, -Expr2)
%
% reorder a linear expression in additive normal form such that free variables are separated from their coefficients
% i.e. 3*x*a^2 (with x free) becomes (3*a^2)*x
extract_variables(A, A) :-
\+ has_variable(A),
!.
extract_variables(A, 1 * A) :-
is_free_variable(A),
!.
extract_variables(A + B, AA + BB) :-
extract_variables(A, AA),
extract_variables(B, BB).
extract_variables(A * B, E * X) :-
(
has_variable(A)
->
extract_variables(A, D * X),
simplify(B * D, E)
;
has_variable(B)
->
extract_variables(B, D * X),
simplify(A * D, E)
;
E = A,
X = B
).
extract_variables(A / B, (C / B) * X) :-
extract_variables(A, C * X).
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