gapt
2.20.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.expansion/ExpansionProofToMG3iViaSAT

ExpansionProofToMG3iViaSAT

gapt.proofs.expansion.ExpansionProofToMG3iViaSAT
See theExpansionProofToMG3iViaSAT companion object
class ExpansionProofToMG3iViaSAT(val expansionProof: ExpansionProof)

Attributes

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

Members list

Type members

Types

type Counterexample = Set[Int]
type Result = Either[Counterexample, Unit]

Value members

Concrete methods

def addClause(p: LKProof): Unit
def addClause(p: LKProof, seq: HOLSequent): Unit
def addClause(lower: HOLSequent, upper: HOLSequent)(p: LKProof => LKProof): Unit
def atom(f: Formula): Int
def atom(e: ExpansionTree): Int
def clause(seq: HOLSequent): Seq[Int]
def expSeq(lits: Iterable[Int]): ExpansionSequent
def implication(lits: Iterable[Int]): HOLSequent
final def isESatisfiable(assumptions: IVecInt): Boolean
def mkCEx(eigenVariables: Set[Var], model: Iterable[Int]): List[Int]
def modelSequent(lits: Iterable[Int]): HOLSequent
def newVar(): Int
def refute(eigenVariables: Set[Var], model: Vector[Int]): Result
def solve(eigenVariables: Set[Var], assumptions: Set[Int]): Result
def solve(): Either[HOLSequent, LKProof]

Concrete fields

val atomToET: Map[Int, Set[ExpansionTree]]
val atomToEigenvars: Map[Int, Set[Var]]
val atomToSh: Map[Int, Formula]
val atomsWithFreeEigenvar: Map[Var, Set[Int]]
val cc: CC
val classical: Int
val drup: Buffer[Line]
val evIds: Map[Var, Int]
val hasEquality: Boolean
val proofs: Map[Set[Int], Either[LKProof, (Set[Int], LKProof => LKProof)]]
val shAtoms: Map[Formula, Int]
val solver: ISolver

Implicits

Implicits

implicit def clause2sat4j(clause: Iterable[Int]): IVecInt
implicit def sat4j2clause_(clause: IVecInt): Set[Int]
Generated with