diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml index f306a61dbef455eeadd91a33c96a0c4ca823a261..36e832a57b6311d1ab1e3e011a73c2ffdf005e15 100644 --- a/src/plugins/value/engine/evaluation.ml +++ b/src/plugins/value/engine/evaluation.ml @@ -746,6 +746,9 @@ module Make type context = { (* The abstract domain state in which the evaluation takes place. *) state: Domain.t; + (* Maximum number of subdivisions. See {!Subdivided_evaluation} for + more details. *) + subdivision: int; (* The remaining fuel: maximum number of nested oracle uses, decremented at each call to the oracle. *) remaining_fuel: int; @@ -1093,7 +1096,8 @@ module Make fun expr -> let valuation = !cache in let context = { context with remaining_fuel } in - Subdivided_Evaluation.evaluate context valuation expr + let subdivnb = context.subdivision in + Subdivided_Evaluation.evaluate context valuation ~subdivnb expr >>=: fun (valuation, value) -> cache := valuation; value @@ -1104,15 +1108,20 @@ module Make with maximal precision. *) let root_context state = let remaining_fuel = root_fuel () in - { state; remaining_fuel; oracle } + let subdivision = Value_parameters.LinearLevel.get () in + { state; subdivision; remaining_fuel; oracle } - (* Context for a fast forward evaluation with minimal precision. *) + (* Context for a fast forward evaluation with minimal precision: + no subdivisions and no call to the oracle. *) let low_context state = let remaining_fuel = no_fuel in - { state; remaining_fuel; oracle } + let subdivision = 0 in + { state; subdivision; remaining_fuel; oracle } let subdivided_forward_eval valuation state expr = - Subdivided_Evaluation.evaluate (root_context state) valuation expr + let context = root_context state in + let subdivnb = context.subdivision in + Subdivided_Evaluation.evaluate context valuation ~subdivnb expr (* ------------------------------------------------------------------------ Backward Evaluation diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml index ab59086cbb73a0f8713fb71ffbccbad78be7b135..b832e789d36607e4baca8e462c25750d3d8e6abe 100644 --- a/src/plugins/value/engine/subdivided_evaluation.ml +++ b/src/plugins/value/engine/subdivided_evaluation.ml @@ -772,8 +772,7 @@ module Make in subdivide_subexpr vars valuation result alarms - let evaluate context valuation expr = - let subdivnb = Value_parameters.LinearLevel.get () in + let evaluate context valuation ~subdivnb expr = if subdivnb = 0 || not activated then Eva.evaluate context valuation expr else subdivide_evaluation context valuation subdivnb expr diff --git a/src/plugins/value/engine/subdivided_evaluation.mli b/src/plugins/value/engine/subdivided_evaluation.mli index 34f7836676cc5ec269d2a33cb881eedd9a29df48..25ed9703977c7d4aceb7effc7b63fc5df026d93b 100644 --- a/src/plugins/value/engine/subdivided_evaluation.mli +++ b/src/plugins/value/engine/subdivided_evaluation.mli @@ -44,7 +44,8 @@ module Make : sig val evaluate: - Eva.context -> Valuation.t -> exp -> (Valuation.t * Value.t) evaluated + Eva.context -> Valuation.t -> subdivnb:int -> + exp -> (Valuation.t * Value.t) evaluated val reduce_by_enumeration: Eva.context -> Valuation.t -> exp -> bool -> Valuation.t or_bottom