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').

Sourcetype 'a eval_reduction_man = {
  1. get_man : 't. 't Core.All.id -> ('a, 't) Core.All.man;
    (*

    Get the manger of a domain

    *)
}

Manager used by reduction rules

Sourcemodule type EVAL_REDUCTION = sig ... end

Signature of an evaluation reduction rule

Registration

Sourceval register_eval_reduction : (module EVAL_REDUCTION) -> unit

Register a new eval reduction

Sourceval find_eval_reduction : string -> (module EVAL_REDUCTION)

Find an eval reduction by its name

Sourceval eval_reductions : unit -> string list

List all eval reductions