Module `Equality.Action`

Parameters

module B : sig ... end

Signature

type bitvector = B.bitvector

type integer = B.integer

type boolean = B.boolean

type enum = B.enum

type ('a, 'b) relation = ('a, 'b) t

type (_, _) mapping =

| BitvectorMapping : (bitvector, Operator.Function_symbol.bitvector) mapping
| IntegerMapping : (integer, Operator.Function_symbol.integer) mapping
| BooleanMapping : (boolean, Operator.Function_symbol.boolean) mapping
| EnumMapping : (enum, Operator.Function_symbol.enum) mapping

One-to-one correspodance between value types and term types

type 'term wrapper =

| Wrap : ('value * ('value, 'term) mapping) -> 'term wrapper

Existential wrapper for mappings

val apply_relation : 
  'value_parent ->
  ('term_child, 'term_parent) relation ->
  ('value_parent, 'term_parent) mapping ->
  'term_child wrapper

apply_relation vp rel proof is the value vc obtained by applying relation rel to value vp. This is a simple forward transfer function.

The proof terms are there to ensure correspondance between the types of values (B.bitvector, B.boolean, B.integer, B.enum) and of terms (TC.bitvector, TC.boolean, TC.integer, TC.enum)

val refine_relation : 
  'value_parent ->
  'value_child ->
  ('term_child, 'term_parent) relation ->
  ('value_parent, 'term_parent) mapping ->
  ('value_child, 'term_child) mapping ->
  'value_parent option

refine_relation ~size vp vc rel proof_p proof_c refines the value vp into, using knowledge that applying rel to vp must be in vc. This is a simple backward transfer function. None is returned when no new information can be deduced.

Note: this returns the newly learned value. It should be intersected with vp for best precision.

Module Equality.Action

Parameters

Signature

Module `Equality.Action`