gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.cutintro

gapt.cutintro

package gapt.cutintro

Members list

Type members

Classlikes

class ClauseWithIndexLists(val literals: List[LiteralWithIndexLists])

Combined data of many unified literals in a clause and whether the clause is a potential part of a formula in disjunctive normal form that makes all leaves of the reduced representation true

Combined data of many unified literals in a clause and whether the clause is a potential part of a formula in disjunctive normal form that makes all leaves of the reduced representation true

Attributes

Source
introducePiCut.scala
Supertypes
class Object
trait Matchable
class Any
class ClausesWithIndexLists(val clauses: List[ClauseWithIndexLists])

Combined data of many clauses in a set of clauses and whether the clauses translate to a formula in disjunctive normal form that makes all leaves of the reduced representation true

Combined data of many clauses in a set of clauses and whether the clauses translate to a formula in disjunctive normal form that makes all leaves of the reduced representation true

Attributes

Source
introducePiCut.scala
Supertypes
class Object
trait Matchable
class Any
object CutIntroduction

Attributes

Source
CutIntroduction.scala
Supertypes
class Object
trait Matchable
class Any
Self type
trait GrammarFindingMethod

Attributes

Source
CutIntroduction.scala
Supertypes
class Object
trait Matchable
class Any
Known subtypes
class MaxSATMethod
object ReforestMethod.type
class LeafIndex(val oneToMList: Set[Int], val oneToPList: Set[Int])

Contains two sets to store integers

Contains two sets to store integers

Value parameters

oneToMList

Supposed to be a subset of {1,...,m}

oneToPList

Supposed to be a subset of {1,...,p}

Attributes

Source
introducePiCut.scala
Supertypes
class Object
trait Matchable
class Any
class LiteralWithIndexLists(val literal: Formula, val leafIndexList: List[LeafIndex], val numberOfDNTAs: Int, val foundNonEmptyPList: Boolean, val foundEmptyMList: Boolean)

Supposed to contain the data of a unified literal and whether it makes a non-tautological leaf of the reduced representation true

Supposed to contain the data of a unified literal and whether it makes a non-tautological leaf of the reduced representation true

Value parameters

foundEmptyMList

Supposed to be true if there is a at least one leaf of the reduced representation and one substitution of the form (xCut->r_j,yCut->beta_j) such that the leaf becomes true

foundNonEmptyPList

Supposed to be true if there is a at least one leaf of the reduced representation and one substitution of the form (xCut->alpha,yCut->t_i(alpha)) such that the leaf becomes true

leafIndexList

Supposed to contain the data which leaf of the reduced representation becomes true for which substitution of the literal

Attributes

Source
introducePiCut.scala
Supertypes
class Object
trait Matchable
class Any
case class MaxSATMethod(solver: MaxSATSolver, nonTerminalLengths: Int*) extends GrammarFindingMethod

Attributes

Companion
object
Source
CutIntroduction.scala
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
object MaxSATMethod

Attributes

Companion
class
Source
CutIntroduction.scala
Supertypes
trait Product
trait Mirror
class Object
trait Matchable
class Any
Self type
object Pi2CutIntroduction

Attributes

Source
pi2cutintro.scala
Supertypes
class Object
trait Matchable
class Any
Self type
case class Pi2SeHs(reducedRepresentation: Sequent[Formula], universalEigenvariable: Var, existentialEigenvariables: List[Var], substitutionsForAlpha: List[Expr], substitutionsForBetaWithAlpha: List[Expr])

Schematic extended Herbrand sequent for schematic Pi-2 grammars

Schematic extended Herbrand sequent for schematic Pi-2 grammars

Value parameters

existentialEigenvariables

The variables that are introduced for the existentially quantified variable of the cut formula (beta_1,...,beta_m)

reducedRepresentation

The schematic extended Herbrand sequent without placeholder for the cut ( F[x\U_1] |- G[y\U_2] )

substitutionsForAlpha

The terms (except from the eigenvariable) that are introduced for the universally quantified variable of the cut formula (r_1,...,r_m)

substitutionsForBetaWithAlpha

The terms (except from the eigenvariables) that are introduced for the existentially quantified variable of the cut formula independent from the existential eigenvariables (t_1(alpha),...,t_p(alpha))

universalEigenvariable

The variable that is introduced for the universally quantified variable of the cut formula (alpha)

Attributes

Source
introducePiCut.scala
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
case object ReforestMethod extends GrammarFindingMethod

Attributes

Source
CutIntroduction.scala
Supertypes
trait Singleton
trait Product
trait Mirror
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
Self type
case class SchematicExtendedHerbrandSequent(us: Sequent[(FOLFormula, Seq[Seq[FOLTerm]])], ss: Seq[(Seq[FOLVar], Seq[Seq[FOLTerm]])])

Represents a schematic extended Herbrand sequent.

Represents a schematic extended Herbrand sequent.

Value parameters

ss

Instances of the cut-implications.

us

Formulas of the original end-sequent, together with their instances.

Attributes

Source
CutIntroduction.scala
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
case class SolutionStructure(sehs: SchematicExtendedHerbrandSequent, formulas: Seq[FOLFormula])

Attributes

Source
SolutionStructure.scala
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all
object beautifySolution

Attributes

Source
beautifySolution.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object gStarUnify

Computes the unified literals, i.e. the set of literals that are used to contruct the cut formula

Computes the unified literals, i.e. the set of literals that are used to contruct the cut formula

Attributes

Source
gStarUnify.scala
Supertypes
class Object
trait Matchable
class Any
Self type
gStarUnify.type
object improveSolutionLK

Attributes

Source
improveSolutionLK.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object introducePi2Cut

Computes the cut formula for a given schematic extended Herbrand sequent

Computes the cut formula for a given schematic extended Herbrand sequent

Attributes

Source
introducePiCut.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object pi2GrammarToSEHS

Attributes

Source
pi2cutintro.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object proveWithPi2Cut

Constructs a proof for a given schematic Pi2-grammar if a cut formula exists

Constructs a proof for a given schematic Pi2-grammar if a cut formula exists

Attributes

Source
proveWithPi2Cut.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object sehsToVTRATG

Attributes

Source
CutIntroduction.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object solutionViaInterpolation

Solution finding algorithm for Π₁-cut-introduction based on the Duality algorithm for constrained Horn clause verification[1].

Solution finding algorithm for Π₁-cut-introduction based on the Duality algorithm for constrained Horn clause verification[1].

[1] K. L. McMillan, A. Rybalchenko, Solving Constrained Horn Clauses using Interpolation, technical report MSR-TR-2013-6, available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/MSR-TR-2013-6.pdf

Attributes

Source
solutionViaInterpolation.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object vtratgToSEHS

Attributes

Source
CutIntroduction.scala
Supertypes
class Object
trait Matchable
class Any
Self type
Generated with