package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500
doc/reduction/Reduction/Eval/index.html
Module Reduction.EvalSource
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
Signature of an evaluation reduction rule
Registration
Register a new eval reduction
Find an eval reduction by its name
List all eval reductions