Module Cc_literal

module Cc_literal: sig .. end

Literal representation for Congruence Closure.

module Variable: Id.Generator

Variables are represented by unique identifiers.

type literal =

`\|`	`Equality of Variable.t * Variable.t`
`\|`	`Disequality of Variable.t * Variable.t`

The type of (dis)equality literals.

val invalid_literal : literal

An invalid literal.

val is_valid_literal : literal -> bool

Is a literal valid.

val equal : literal -> literal -> bool

equal l m literals l and m equal (understands that equality and disequality are commutative)?

val negation : literal -> literal

negation l is the nation of l.

type lemma =

`\|`	`RoK of Variable.t * Variable.t * Variable.t`	`(*`	`RoK(a,i,x)` is the lemma `ai = x`, generated when `a = Kx`	`*)`
`\|`	`Row1 of Variable.t * Variable.t * Variable.t`	`(*`	`Row1(b,i,x)` is the lemma `bi = x`, generated when `b = Uaix` for some `a`	`*)`
`\|`	`Row2 of Variable.t * Variable.t * Variable.t * Variable.t`	`(*`	`Row2(a,b,i,j)` is the lemma `i!=j => aj = bj`, generated when `b=Uaix` for some `x`	`*)`
`\|`	`Ext of Variable.t * Variable.t`	`(*`	`Ext(a,b)` is the lemma `a!=b => \exists k.ak != bk`.	`*)`

The type of lemmas.

module Variable_map: Index.Map  with type key = Variable.t

module Variable_hash: Hashtbl.S  with type key = Variable.t

module Variable_map2: Index.Map2 
  with type key0 = Variable.t and type key1 = Variable.t

module Variable_set: Index.Set  with type elt = Variable.t

Hosted by the

^* web site.
^*Other names and brands may be claimed as the property of others.