Commit 4b263379 by Mathieu Hemery

Try a new version of always_pos/neg relying on determine_sign/2

parent 0c540072
 ... ... @@ -6,6 +6,7 @@ additive_normal_form/2, always_negative/1, always_positive/1, determine_sign/2, normalize_number/2, is_null/1, modulo/3 ... ... @@ -665,105 +666,121 @@ arithmetic_operation(- _). arithmetic_operation(_ ^ _). always_negative(A) :- rewrite(rewrite_simplify, A, B), B \= A, !, always_negative(B). always_negative(A) :- number(A), !, A =< 0. always_negative(- A) :- always_positive(A). %! always_negative(+Expr) %! always_positive(+Expr) % % Check if Expr is assure to be always negative/positive, fail if it can change sign % or if it is impossible to decide always_negative(A + B) :- always_negative(A), always_negative(B). always_negative(Expr) :- determine_sign(Expr, neg). always_negative(A - B) :- always_negative(A), always_positive(B). always_positive(Expr) :- determine_sign(Expr, pos). always_negative(A * B) :- always_negative(A), always_positive(B). always_negative(0 * _) :- !. %! determine_sign(+Expr, -Sign) % % Try to infer the sign of Expr, Sign will be unified to: neg/pos/zero/dnk (do not know) always_negative(A * B) :- always_positive(A), always_negative(B). % TODO : Verify if it needs rewriting %always_negative(A) :- % rewrite(rewrite_simplify, A, B), % B \= A, % !, % always_negative(B). always_negative(A / B) :- always_negative(A), always_positive(B). determine_sign(A, zero) :- is_null(A), !. always_negative(A / B) :- always_positive(A), always_negative(B). determine_sign(A, Sign) :- number(A), !, ( A = 0 -> Sign = zero ; A < 0 -> Sign = neg ; Sign = pos ). determine_sign(- A, NSign) :- determine_sign(A, Sign), !, ( Sign = pos -> NSign = neg ; Sign = neg -> NSign = pos ; NSign = Sign ). always_positive(A) :- rewrite(rewrite_simplify, A, B), B \= A, determine_sign(A + B, Sign) :- !, always_positive(B). ( determine_sign(A, SignAB), determine_sign(B, SignAB) -> Sign = SignAB ; Sign = dnk ). always_positive(A) :- number(A), determine_sign(A - B, Sign) :- !, A >= 0. determine_sign(A + (- B), Sign). determine_sign(A * B, Sign) :- determine_sign(A, SignA), determine_sign(B, SignB), ( (SignA = zero ; SignB = zero) -> Sign = zero ; (SignA = dnk ; SignB = dnk) -> Sign = dnk ; SignA = SignB -> Sign = pos ; Sign = neg ). always_positive(A):- % assumed for concentrations, parameters atom(A), !. determine_sign(A / B, Sign) :- determine_sign(A * B, Sign). always_positive(- A) :- always_negative(A). determine_sign(A, pos) :- % concentrations and parameters are assumed positive atom(A), !. always_positive(_A ^ B) :- determine_sign(_A ^ B, pos) :- number(B), ( modulo(B, 2, 0) -> !, true ). always_positive(A ^ _B) :- always_positive(A). always_positive(A + B) :- always_positive(A), always_positive(B). always_positive(A - B) :- always_positive(A), always_negative(B). always_positive(0 * _) :- !. always_positive(A * B) :- always_negative(A), always_negative(B). always_positive(A * B) :- always_positive(A), always_positive(B). determine_sign(A ^ _B, Sign) :- determine_sign(A, Sign). always_positive(A / B) :- always_positive(A), always_positive(B). determine_sign(exp(_A), pos). always_positive(A / B) :- always_negative(A), always_negative(B). always_positive(exp(_A)). normalize_number(N, Norm) :- ( ... ...
 ... ... @@ -9,6 +9,13 @@ test('distribute2', []) :- distribute((a+b)^2, a*a+a*b+(b*a+b*b)), distribute((a+b)^ -2, (a+b)^ -2). test('determine_sign', []) :- determine_sign((a+1)^2, pos), determine_sign((a-1)^3, dnk), determine_sign(-exp(a), neg), determine_sign((2+a)*0, zero). test('is_null', []) :- is_null(a*0*1/2), \+(is_null(a*b/0)). ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!