package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa
doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Framework/Sig/Reduction/Eval/index.html
Module Reduction.Eval
Signature of reduction rules for product evaluations
In a reduced product, evaluations of member domains are combined by conjunction. Since each domain Di can return disjunctive evaluations (e_i1, f_i1) ∨ ... , the overall evaluation of D1 ∧ ... ∧ Dn is translated into a disjunctive normal form (e_11 ∧ ... ∧ e_n1, f_11 ∩ ... ∩ f_n1) ∨ ...
Each resulting conjunction, called a product evaluation, represents the evaluations of the domains on the same state partition. Since expressions can not be combined, a transfer function F performed over a product evaluation (e_1 ∧ ... ∧ e_n, f) is equivalent to (F e_1 f) ∩ ... ∩ (F e_n f), which is inefficient.
The goal of a reduction rule is to reduce a product evaluation (e_1 ∧ ... ∧ e_n, f) into a more efficient evaluation (e', f') by keeping the most precise evaluation and eventually keep information about the other ones in the abstract state (such as equality with e').
type 'a eval_reduction_man = {get_man : 't. 't Core.All.id -> ('a, 't) Core.All.man;(*Get the manger of a domain
*)
}Manager used by reduction rules
module type EVAL_REDUCTION = sig ... endSignature of an evaluation reduction rule
Registration
val register_eval_reduction : (module EVAL_REDUCTION) -> unitRegister a new eval reduction
val find_eval_reduction : string -> (module EVAL_REDUCTION)Find an eval reduction by its name