gapt
2.20.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.resolution/Clausifier

Clausifier

gapt.proofs.resolution.Clausifier
class Clausifier(propositional: Boolean, structural: Boolean, bidirectionalDefs: Boolean, cse: Boolean, ctx: MutableContext, nameGen: NameGenerator)

Attributes

Source
structuralCNF.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes

Members list

Value members

Concrete methods

def analyze(f: Formula): Int

Attributes

Source
structuralCNF.scala
def analyze(p: ResolutionProof): Unit

Attributes

Source
structuralCNF.scala
def expand(p: ResolutionProof): Unit

Attributes

Source
structuralCNF.scala
def expandDef(const: HOLAtomConst, fvs: List[Var], pol: Polarity): Unit

Attributes

Source
structuralCNF.scala
def getSkolemInfo(f: Formula, x: Var): (Expr, Expr)

Attributes

Source
structuralCNF.scala
def isDefn(p: ResolutionProof): Boolean

Attributes

Source
structuralCNF.scala
def mkAbbrevSym(): String

Attributes

Source
structuralCNF.scala
def mkSkolemSym(): String

Attributes

Source
structuralCNF.scala
def split(p: ResolutionProof): Unit

Attributes

Source
structuralCNF.scala
def splitAt(p: ResolutionProof, i: SequentIndex): Unit

Attributes

Source
structuralCNF.scala

Concrete fields

val alreadyDefined: Set[(Const, Polarity)]

Attributes

Source
structuralCNF.scala
val cnf: Set[ResolutionProof]

Attributes

Source
structuralCNF.scala
val commonSubExprs: Set[Expr]

Attributes

Source
structuralCNF.scala
val defs: Map[Expr, HOLAtomConst]

Attributes

Source
structuralCNF.scala
val skConsts: Map[Expr, Const]

Attributes

Source
structuralCNF.scala
val subExprs: Map[Expr, Int]

Attributes

Source
structuralCNF.scala
Generated with