package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module LinearTwoVarEquality.ActionSource

Parameters

Signature

Sourcetype bitvector = B.bitvector
Sourcetype integer = B.integer
Sourcetype boolean = B.boolean
Sourcetype enum = B.enum
Sourcetype ('a, 'b) relation = ('a, 'b) t

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

Sourcetype 'term wrapper =
  1. | Wrap : ('value * ('value, 'term) mapping) -> 'term wrapper

Existential wrapper for mappings

Sourceval 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)

Sourceval 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.

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)