Commit c1ad6ede authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

Try to extract free variables in FOLTL, fixes #53

parent 82decd3f
......@@ -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);
......@@ -1234,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