gapt
2.18.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

Value members

Concrete methods

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

Concrete fields

val cc: CC
val evIds: Map[Var, Int]
val solver: ISolver

Implicits

Implicits

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