MutCC

gapt.provers.congruence.MutCC
See theMutCC companion object
final class MutCC

Congruence closure implementation closely following [1]

[1] R. Nieuwenhuis and A. Oliveras, Fast congruence closure and extensions, Information and Computation 205.4 (2007), 557-580.

Attributes

Companion
object
Source
congruence.scala
Graph
Supertypes
class Object
trait Matchable
class Any

Members list

Type members

Classlikes

class Explainer

Attributes

Source
congruence.scala
Supertypes
class Object
trait Matchable
class Any

Value members

Constructors

def this(n: Int)

Attributes

Source
congruence.scala

Concrete methods

def addEqn(l: Int, r: Int, lr: Int): Unit

Attributes

Source
congruence.scala
def addEqn(eqn: Eqn): Unit

Attributes

Source
congruence.scala
override def clone(): MutCC

Create a copy of the receiver object.

Create a copy of the receiver object.

The default implementation of the clone method is platform dependent.

Attributes

Returns

a copy of the receiver object.

Note

not specified by SLS as a member of AnyRef

Definition Classes
Object
Source
congruence.scala

Attributes

Source
congruence.scala
def isEq(a: Int, b: Int): Boolean

Attributes

Source
congruence.scala
def merge(p: Pending): Unit

Attributes

Source
congruence.scala
def merge(a: Int, b: Int, ref: Int): Unit

Attributes

Source
congruence.scala
def propagate(): Unit

Attributes

Source
congruence.scala
def resize(newN: Int): MutCC

Attributes

Source
congruence.scala

Concrete fields

Attributes

Source
congruence.scala
val lookup: Map[(Int, Int), Eqn]

Attributes

Source
congruence.scala
val n: Int

Attributes

Source
congruence.scala
val parent: Array[Int]

Attributes

Source
congruence.scala

Attributes

Source
congruence.scala

Attributes

Source
congruence.scala
val repr: Array[Int]

Attributes

Source
congruence.scala
val use: Array[Vector[Eqn]]

Attributes

Source
congruence.scala