package mopsa
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4
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