scala.tools.nsc.transform.patmat.ScalaLogic

TreesAndTypesDomain

trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis

Source: Logic.scala

Linear Supertypes

ScalaLogic.CheckableTreeAndTypeAnalysis, ScalaLogic.PropositionalLogic, AnyRef, Any

Known Subclasses

MatchAnalyzer, MatchApproximator, CommonSubconditionElimination, MatchOptimizer, OptimizingMatchTranslator

Type Hierarchy

Ordering

Alphabetic
By Inheritance

Inherited

TreesAndTypesDomain
CheckableTreeAndTypeAnalysis
PropositionalLogic
AnyRef
Any

Implicitly

by any2stringadd
by StringFormat
by Ensuring
by ArrowAssoc

Hide All
Show All

Visibility

Public
Protected

Type Members

trait AbsVar extends AnyRef
Definition Classes
PropositionalLogic
final case class And(ops: Set[Prop]) extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
final case class AtMostOne(ops: List[Sym]) extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
final case class Eq(p: Var, q: Const) extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
final case class Not(a: Prop) extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
final case class Or(ops: Set[Prop]) extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
sealed abstract class Prop extends AnyRef
Definition Classes
PropositionalLogic
trait PropMap extends AnyRef
Definition Classes
PropositionalLogic
trait PropTraverser extends AnyRef
Definition Classes
PropositionalLogic
final case class Solution(model: Model, unassigned: List[Sym]) extends Product with Serializable
Definition Classes
PropositionalLogic
final class Sym extends Prop
Definition Classes
PropositionalLogic
trait TypeConstExtractor extends AnyRef
Definition Classes
PropositionalLogic
trait ValueConstExtractor extends AnyRef
Definition Classes
PropositionalLogic
trait VarExtractor extends AnyRef
Definition Classes
PropositionalLogic
sealed abstract class Const extends AnyRef
type Model = Map[Sym, Boolean]
Definition Classes
PropositionalLogic
abstract type Solvable
Definition Classes
PropositionalLogic
type Tree = Global.Tree
Definition Classes
TreesAndTypesDomain → PropositionalLogic
type Type = Global.Type
Definition Classes
TreesAndTypesDomain → PropositionalLogic
sealed class TypeConst extends Const
sealed class ValueConst extends Const
class Var extends AbsVar

Abstract Value Members

abstract val EmptyModel: Model
Definition Classes
PropositionalLogic
abstract val NoModel: Model
Definition Classes
PropositionalLogic
abstract def eqFreePropToSolvable(f: Prop): Solvable
Definition Classes
PropositionalLogic
abstract def findAllModelsFor(solvable: Solvable, sym: Global.Symbol = NoSymbol): List[Solution]
Definition Classes
PropositionalLogic
abstract def hasModel(solvable: Solvable): Boolean
Definition Classes
PropositionalLogic
abstract def reportWarning(message: String): Unit
Definition Classes
PropositionalLogic
abstract val typer: (analyzer)#Typer
Definition Classes
CheckableTreeAndTypeAnalysis
abstract def uncheckedWarning(pos: Global.Position, msg: String, site: Global.Symbol): Unit
Definition Classes
PropositionalLogic

Concrete Value Members

object AnalysisBudget
Definition Classes
PropositionalLogic
object And extends java.io.Serializable
Definition Classes
PropositionalLogic
case object False extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
object Or extends java.io.Serializable
Definition Classes
PropositionalLogic
object Sym
Definition Classes
PropositionalLogic
case object True extends Prop with Product with Serializable
Definition Classes
PropositionalLogic
final def !=(arg0: Any): Boolean
Definition Classes
AnyRef → Any
final def ##: Int
Definition Classes
AnyRef → Any
def +(other: String): String
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toany2stringadd[TreesAndTypesDomain] performed by method any2stringadd in scala.Predef.
Definition Classes
any2stringadd
def ->[B](y: B): (TreesAndTypesDomain, B)
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toArrowAssoc[TreesAndTypesDomain] performed by method ArrowAssoc in scala.Predef.
Definition Classes
ArrowAssoc
Annotations
@inline()
def /\(props: Iterable[Prop]): Prop
Definition Classes
PropositionalLogic
final def ==(arg0: Any): Boolean
Definition Classes
AnyRef → Any
def \/(props: Iterable[Prop]): Prop
Definition Classes
PropositionalLogic
final def asInstanceOf[T0]: T0
Definition Classes
Any
def checkableType(tp: Global.Type): Global.Type
Definition Classes
CheckableTreeAndTypeAnalysis
def clone(): AnyRef
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.CloneNotSupportedException]) @native()
def ensuring(cond: (TreesAndTypesDomain) => Boolean, msg: => Any): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: (TreesAndTypesDomain) => Boolean): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean, msg: => Any): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def enumerateSubtypes(tp: Global.Type, grouped: Boolean): List[List[Global.Type]]
Definition Classes
CheckableTreeAndTypeAnalysis
final def eq(arg0: AnyRef): Boolean
Definition Classes
AnyRef
def equals(arg0: AnyRef): Boolean
Definition Classes
AnyRef → Any
def finalize(): Unit
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.Throwable])
def gatherSymbols(p: Prop): Set[Sym]
Definition Classes
PropositionalLogic
def gatherVariables(p: Prop): Set[Var]
Definition Classes
PropositionalLogic
final def getClass(): Class[_ <: AnyRef]
Definition Classes
AnyRef → Any
Annotations
@native()
def hashCode(): Int
Definition Classes
AnyRef → Any
Annotations
@native()
final def isInstanceOf[T0]: Boolean
Definition Classes
Any
final def ne(arg0: AnyRef): Boolean
Definition Classes
AnyRef
final def notify(): Unit
Definition Classes
AnyRef
Annotations
@native()
final def notifyAll(): Unit
Definition Classes
AnyRef
Annotations
@native()
def prepareNewAnalysis(): Unit
Definition Classes
TreesAndTypesDomain → PropositionalLogic
def propToSolvable(p: Prop): Solvable
Definition Classes
PropositionalLogic
def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop])
Definition Classes
PropositionalLogic
def simplify(f: Prop): Prop
Simplifies propositional formula according to the following rules: - eliminate double negation (avoids unnecessary Tseitin variables) - flatten trees of same connectives (avoids unnecessary Tseitin variables) - removes constants and connectives that are in fact constant because of their operands - eliminates duplicate operands - convert formula into NNF: all sub-expressions have a positive polarity which makes them amenable for the subsequent Plaisted transformation and increases chances to figure out that the formula is already in CNF
Simplifies propositional formula according to the following rules: - eliminate double negation (avoids unnecessary Tseitin variables) - flatten trees of same connectives (avoids unnecessary Tseitin variables) - removes constants and connectives that are in fact constant because of their operands - eliminates duplicate operands - convert formula into NNF: all sub-expressions have a positive polarity which makes them amenable for the subsequent Plaisted transformation and increases chances to figure out that the formula is already in CNF
Complexity: DFS over formula tree
See https://www.decision-procedures.org/slides/propositional_logic-2x3.pdf
Definition Classes
PropositionalLogic
final def synchronized[T0](arg0: => T0): T0
Definition Classes
AnyRef
def toString(): String
Definition Classes
AnyRef → Any
def uncheckableType(tp: Global.Type): Boolean
Definition Classes
CheckableTreeAndTypeAnalysis
final def wait(): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException])
final def wait(arg0: Long, arg1: Int): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException])
final def wait(arg0: Long): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException]) @native()
object Const
case object NullConst extends Const with Product with Serializable
Definition Classes
TreesAndTypesDomain → PropositionalLogic
object TypeConst extends TypeConstExtractor
Definition Classes
TreesAndTypesDomain → PropositionalLogic
object ValueConst extends ValueConstExtractor
Definition Classes
TreesAndTypesDomain → PropositionalLogic
object Var extends VarExtractor
Definition Classes
TreesAndTypesDomain → PropositionalLogic

Deprecated Value Members

def formatted(fmtstr: String): String
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toStringFormat[TreesAndTypesDomain] performed by method StringFormat in scala.Predef.
Definition Classes
StringFormat
Annotations
@deprecated @inline()
Deprecated
(Since version 2.12.16) Use formatString.format(value) instead of value.formatted(formatString), or use the f"" string interpolator. In Java 15 and later, formatted resolves to the new method in String which has reversed parameters.
def →[B](y: B): (TreesAndTypesDomain, B)
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toArrowAssoc[TreesAndTypesDomain] performed by method ArrowAssoc in scala.Predef.
Definition Classes
ArrowAssoc
Annotations
@deprecated
Deprecated
(Since version 2.13.0) Use -> instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.

Inherited from ScalaLogic.CheckableTreeAndTypeAnalysis

Value Members

abstract val typer: (analyzer)#Typer
Definition Classes
CheckableTreeAndTypeAnalysis
def checkableType(tp: Global.Type): Global.Type
Definition Classes
CheckableTreeAndTypeAnalysis
def enumerateSubtypes(tp: Global.Type, grouped: Boolean): List[List[Global.Type]]
Definition Classes
CheckableTreeAndTypeAnalysis
def uncheckableType(tp: Global.Type): Boolean
Definition Classes
CheckableTreeAndTypeAnalysis

Inherited from ScalaLogic.PropositionalLogic

Value Members

abstract val EmptyModel: Model
Definition Classes
PropositionalLogic
abstract val NoModel: Model
Definition Classes
PropositionalLogic
abstract def eqFreePropToSolvable(f: Prop): Solvable
Definition Classes
PropositionalLogic
abstract def findAllModelsFor(solvable: Solvable, sym: Global.Symbol = NoSymbol): List[Solution]
Definition Classes
PropositionalLogic
abstract def hasModel(solvable: Solvable): Boolean
Definition Classes
PropositionalLogic
abstract def reportWarning(message: String): Unit
Definition Classes
PropositionalLogic
abstract def uncheckedWarning(pos: Global.Position, msg: String, site: Global.Symbol): Unit
Definition Classes
PropositionalLogic
def /\(props: Iterable[Prop]): Prop
Definition Classes
PropositionalLogic
def \/(props: Iterable[Prop]): Prop
Definition Classes
PropositionalLogic
def gatherSymbols(p: Prop): Set[Sym]
Definition Classes
PropositionalLogic
def gatherVariables(p: Prop): Set[Var]
Definition Classes
PropositionalLogic
def propToSolvable(p: Prop): Solvable
Definition Classes
PropositionalLogic
def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop])
Definition Classes
PropositionalLogic
def simplify(f: Prop): Prop
Simplifies propositional formula according to the following rules: - eliminate double negation (avoids unnecessary Tseitin variables) - flatten trees of same connectives (avoids unnecessary Tseitin variables) - removes constants and connectives that are in fact constant because of their operands - eliminates duplicate operands - convert formula into NNF: all sub-expressions have a positive polarity which makes them amenable for the subsequent Plaisted transformation and increases chances to figure out that the formula is already in CNF
Simplifies propositional formula according to the following rules: - eliminate double negation (avoids unnecessary Tseitin variables) - flatten trees of same connectives (avoids unnecessary Tseitin variables) - removes constants and connectives that are in fact constant because of their operands - eliminates duplicate operands - convert formula into NNF: all sub-expressions have a positive polarity which makes them amenable for the subsequent Plaisted transformation and increases chances to figure out that the formula is already in CNF
Complexity: DFS over formula tree
See https://www.decision-procedures.org/slides/propositional_logic-2x3.pdf
Definition Classes
PropositionalLogic

Inherited from AnyRef

Value Members

final def !=(arg0: Any): Boolean
Definition Classes
AnyRef → Any
final def ##: Int
Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean
Definition Classes
AnyRef → Any
def clone(): AnyRef
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.CloneNotSupportedException]) @native()
final def eq(arg0: AnyRef): Boolean
Definition Classes
AnyRef
def equals(arg0: AnyRef): Boolean
Definition Classes
AnyRef → Any
def finalize(): Unit
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.Throwable])
final def getClass(): Class[_ <: AnyRef]
Definition Classes
AnyRef → Any
Annotations
@native()
def hashCode(): Int
Definition Classes
AnyRef → Any
Annotations
@native()
final def ne(arg0: AnyRef): Boolean
Definition Classes
AnyRef
final def notify(): Unit
Definition Classes
AnyRef
Annotations
@native()
final def notifyAll(): Unit
Definition Classes
AnyRef
Annotations
@native()
final def synchronized[T0](arg0: => T0): T0
Definition Classes
AnyRef
def toString(): String
Definition Classes
AnyRef → Any
final def wait(): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException])
final def wait(arg0: Long, arg1: Int): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException])
final def wait(arg0: Long): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException]) @native()

Inherited from Any

Value Members

final def asInstanceOf[T0]: T0
Definition Classes
Any
final def isInstanceOf[T0]: Boolean
Definition Classes
Any

Inherited by implicit conversion any2stringadd fromTreesAndTypesDomain to any2stringadd[TreesAndTypesDomain]

Value Members

def +(other: String): String
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toany2stringadd[TreesAndTypesDomain] performed by method any2stringadd in scala.Predef.
Definition Classes
any2stringadd

Inherited by implicit conversion StringFormat fromTreesAndTypesDomain to StringFormat[TreesAndTypesDomain]

Value Members

def formatted(fmtstr: String): String
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toStringFormat[TreesAndTypesDomain] performed by method StringFormat in scala.Predef.
Definition Classes
StringFormat
Annotations
@deprecated @inline()
Deprecated
(Since version 2.12.16) Use formatString.format(value) instead of value.formatted(formatString), or use the f"" string interpolator. In Java 15 and later, formatted resolves to the new method in String which has reversed parameters.

Inherited by implicit conversion Ensuring fromTreesAndTypesDomain to Ensuring[TreesAndTypesDomain]

Value Members

def ensuring(cond: (TreesAndTypesDomain) => Boolean, msg: => Any): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: (TreesAndTypesDomain) => Boolean): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean, msg: => Any): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring
def ensuring(cond: Boolean): TreesAndTypesDomain
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toEnsuring[TreesAndTypesDomain] performed by method Ensuring in scala.Predef.
Definition Classes
Ensuring

Inherited by implicit conversion ArrowAssoc fromTreesAndTypesDomain to ArrowAssoc[TreesAndTypesDomain]

Value Members

def ->[B](y: B): (TreesAndTypesDomain, B)
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toArrowAssoc[TreesAndTypesDomain] performed by method ArrowAssoc in scala.Predef.
Definition Classes
ArrowAssoc
Annotations
@inline()
def →[B](y: B): (TreesAndTypesDomain, B)
Implicit
This member is added by an implicit conversion from TreesAndTypesDomain toArrowAssoc[TreesAndTypesDomain] performed by method ArrowAssoc in scala.Predef.
Definition Classes
ArrowAssoc
Annotations
@deprecated
Deprecated
(Since version 2.13.0) Use -> instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.

Packages

TreesAndTypesDomain

trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis

Type Members

Abstract Value Members

Concrete Value Members

Deprecated Value Members

Inherited from ScalaLogic.CheckableTreeAndTypeAnalysis

Value Members

Inherited from ScalaLogic.PropositionalLogic

Value Members

Inherited from AnyRef

Value Members

Inherited from Any

Value Members

Inherited by implicit conversion any2stringadd fromTreesAndTypesDomain to any2stringadd[TreesAndTypesDomain]

Value Members

Inherited by implicit conversion StringFormat fromTreesAndTypesDomain to StringFormat[TreesAndTypesDomain]

Value Members

Inherited by implicit conversion Ensuring fromTreesAndTypesDomain to Ensuring[TreesAndTypesDomain]

Value Members

Inherited by implicit conversion ArrowAssoc fromTreesAndTypesDomain to ArrowAssoc[TreesAndTypesDomain]

Value Members

Ungrouped

Packages

TreesAndTypesDomain

trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis

Type Members

Abstract Value Members

Concrete Value Members

Deprecated Value Members

Inherited from ScalaLogic.CheckableTreeAndTypeAnalysis

Value Members

Inherited from ScalaLogic.PropositionalLogic

Value Members

Inherited from AnyRef

Value Members

Inherited from Any

Value Members

Inherited by implicit conversion any2stringadd fromTreesAndTypesDomain to any2stringadd[TreesAndTypesDomain]

Value Members

Inherited by implicit conversion StringFormat fromTreesAndTypesDomain to StringFormat[TreesAndTypesDomain]

Value Members

Inherited by implicit conversion Ensuring fromTreesAndTypesDomain to Ensuring[TreesAndTypesDomain]

Value Members

Inherited by implicit conversion ArrowAssoc fromTreesAndTypesDomain to ArrowAssoc[TreesAndTypesDomain]

Value Members

Ungrouped

TreesAndTypesDomain