gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.provers/gapt.provers.sat/DrupSolver

DrupSolver

gapt.provers.sat.DrupSolver
trait DrupSolver extends SATSolver, ResolutionProver

Attributes

Source
SATSolver.scala
Graph
Supertypes
trait SATSolver
trait Prover
class Object
trait Matchable
class Any
Show all
Known subtypes
class Glucose
object Glucose.type
class PicoSAT
object PicoSAT.type
class Sat4j
object Sat4j.type
Show all

Members list

Value members

Abstract methods

def getDrupProof(cnf: CNF): Option[RupProof]

Attributes

Source
SATSolver.scala

Concrete methods

def getDrupProof(formula: Formula): Option[RupProof]

Attributes

Source
SATSolver.scala
def getDrupProof(sequent: HOLSequent): Option[RupProof]

Attributes

Source
SATSolver.scala
override def getLKProof(sequent: HOLSequent)(implicit ctx: Maybe[MutableContext]): Option[LKProof]

Value parameters

seq

The sequent that should be proved.

Attributes

Returns

An LK-Proof of the sequent, or None if not successful.

Definition Classes
Source
SATSolver.scala
override def getResolutionProof(cnf: Iterable[HOLClause])(implicit ctx: Maybe[MutableContext]): Option[ResolutionProof]

Attributes

Definition Classes
Source
SATSolver.scala
override def isValid(seq: HOLSequent)(implicit ctx: Maybe[Context]): Boolean

Value parameters

seq

The sequent whose validity should be checked.

Attributes

Returns

True if the formula is valid.

Definition Classes
Source
SATSolver.scala

Inherited methods

def getEpsilonProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[EpsilonProof]

Attributes

Inherited from:
Prover
Source
provers.scala
def getEpsilonProof(seq: HOLSequent)(implicit ctx0: Maybe[MutableContext]): Option[EpsilonProof]

Attributes

Inherited from:
Prover
Source
provers.scala
override def getExpansionProof(seq: HOLSequent)(implicit ctx0: Maybe[MutableContext]): Option[ExpansionProof]

Attributes

Definition Classes
Inherited from:
ResolutionProver
Source
ResolutionProver.scala
def getExpansionProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[ExpansionProof]

Attributes

Inherited from:
Prover
Source
provers.scala
def getInterpolant(tree: Tree[Formula])(implicit ctx: Maybe[Context]): Option[Tree[Formula]]

Attributes

Inherited from:
Prover
Source
provers.scala
def getLKProof(seq0: HOLSequent, addWeakenings: Boolean)(implicit ctx0: Maybe[MutableContext]): Option[LKProof]

Attributes

Inherited from:
ResolutionProver
Source
ResolutionProver.scala
def getLKProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[LKProof]

Value parameters

formula

The formula that should be proved.

Attributes

Returns

An LK-Proof of :- formula, or None if not successful.

Inherited from:
Prover
Source
provers.scala
def getResolutionProof(seq: HOLSequent)(implicit ctx0: Maybe[MutableContext]): Option[ResolutionProof]

Attributes

Inherited from:
ResolutionProver
Source
ResolutionProver.scala
def getResolutionProof(formula: Formula)(implicit ctx: Maybe[MutableContext]): Option[ResolutionProof]

Attributes

Inherited from:
ResolutionProver
Source
ResolutionProver.scala
def getResolutionProof(sequentSet: Iterable[HOLSequent])(implicit ctx0: Maybe[MutableContext], dummyImplicit1: DummyImplicit, dummyImplicit2: DummyImplicit): Option[ResolutionProof]

Attributes

Inherited from:
ResolutionProver
Source
ResolutionProver.scala
def getResolutionProof(cnf: Iterable[ResolutionProof])(implicit ctx: Maybe[MutableContext], dummyImplicit: DummyImplicit): Option[ResolutionProof]

Attributes

Inherited from:
ResolutionProver
Source
ResolutionProver.scala
override def isUnsat(cnf: Iterable[HOLClause])(implicit ctx: Maybe[Context]): Boolean

Checks whether a set of clauses is propositionally unsatisfiable.

Checks whether a set of clauses is propositionally unsatisfiable.

Attributes

Definition Classes
Inherited from:
SATSolver
Source
SATSolver.scala
def isUnsat(formula: Formula)(implicit ctx: Maybe[Context]): Boolean

Checks whether a formula is unsatisfiable.

Checks whether a formula is unsatisfiable.

Attributes

Inherited from:
Prover
Source
provers.scala
def isValid(formula: Formula)(implicit ctx: Maybe[Context]): Boolean

Value parameters

formula

The formula whose validity should be checked.

Attributes

Returns

True if the formula is valid.

Inherited from:
Prover
Source
provers.scala
override def runSession[A](program: Session[A]): A

Method for running a session.

Method for running a session.

Type parameters

A

The return type of the session.

Value parameters

program

A proof session.

Attributes

Returns

The result of running the session.

Definition Classes
Inherited from:
OneShotProver
Source
provers.scala
def solve(formula: Formula): Option[PropositionalModel]

Attributes

Inherited from:
SATSolver
Source
SATSolver.scala
def solve(cnf: Iterable[HOLClause]): Option[PropositionalModel]

Attributes

Inherited from:
SATSolver
Source
SATSolver.scala
def solve(cnf: CNF): Option[Model]

Attributes

Inherited from:
SATSolver
Source
SATSolver.scala
Generated with