Trees

Type Members

final case class ConnectiveApplication(symbol: ConnectiveSymbol, formulas: List[Formula]) extends Formula with Product with Serializable
final case class ConnectiveSymbol(name: String, arity: Int) extends Product with Serializable
sealed abstract class Formula extends AnyRef
final case class FunctionApplication(fSymbol: FunctionSymbol, terms: List[Term]) extends Term with Product with Serializable
final case class FunctionSymbol(name: String, argSorts: List[Sort], returnSort: Sort) extends Product with Serializable
final case class ITE(condition: Formula, thenTerm: Term, elseTerm: Term) extends Term with Product with Serializable
final case class PredicateApplication(symbol: PredicateSymbol, terms: List[Term]) extends Formula with Product with Serializable
final case class PredicateSymbol(name: String, argSorts: List[Sort]) extends Product with Serializable
final case class QuantifierApplication(symbol: QuantifierSymbol, variable: Variable, formula: Formula) extends Formula with Product with Serializable
final case class QuantifierSymbol(name: String) extends Product with Serializable
final case class Sort(name: String, subSorts: List[Sort]) extends Product with Serializable
sealed abstract class Term extends AnyRef
final case class TermQuantifierApplication(symbol: TermQuantifierSymbol, variable: Variable, terms: List[Term]) extends Term with Product with Serializable
final case class TermQuantifierSymbol(name: String, argSorts: List[Sort], returnSort: Sort) extends Product with Serializable
final case class Variable(name: String, sort: Sort) extends Term with Product with Serializable

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
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
def freshFunctionSymbol(prefix: FunctionSymbol): FunctionSymbol
def freshFunctionSymbol(prefix: String, argSorts: List[Sort], returnSort: Sort): FunctionSymbol
def freshPredicateSymbol(prefix: PredicateSymbol): PredicateSymbol
def freshPredicateSymbol(prefix: String, argSorts: List[Sort]): PredicateSymbol
def freshVariable(prefix: Variable): Variable
def freshVariable(prefix: String, sort: Sort): Variable
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
def hashCode(): Int

Definition Classes
AnyRef → Any
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
final def notifyAll(): Unit

Definition Classes
AnyRef
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( ... )
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

Related Doc: package core

object Trees

Type Members

final case class ConnectiveApplication(symbol: ConnectiveSymbol, formulas: List[Formula]) extends Formula with Product with Serializable

final case class ConnectiveSymbol(name: String, arity: Int) extends Product with Serializable

sealed abstract class Formula extends AnyRef

final case class FunctionApplication(fSymbol: FunctionSymbol, terms: List[Term]) extends Term with Product with Serializable

final case class FunctionSymbol(name: String, argSorts: List[Sort], returnSort: Sort) extends Product with Serializable

final case class ITE(condition: Formula, thenTerm: Term, elseTerm: Term) extends Term with Product with Serializable

final case class PredicateApplication(symbol: PredicateSymbol, terms: List[Term]) extends Formula with Product with Serializable

final case class PredicateSymbol(name: String, argSorts: List[Sort]) extends Product with Serializable

final case class QuantifierApplication(symbol: QuantifierSymbol, variable: Variable, formula: Formula) extends Formula with Product with Serializable

final case class QuantifierSymbol(name: String) extends Product with Serializable

final case class Sort(name: String, subSorts: List[Sort]) extends Product with Serializable

sealed abstract class Term extends AnyRef

final case class TermQuantifierApplication(symbol: TermQuantifierSymbol, variable: Variable, terms: List[Term]) extends Term with Product with Serializable

final case class TermQuantifierSymbol(name: String, argSorts: List[Sort], returnSort: Sort) extends Product with Serializable

final case class Variable(name: String, sort: Sort) extends Term with Product with Serializable

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def finalize(): Unit

def freshFunctionSymbol(prefix: FunctionSymbol): FunctionSymbol

def freshFunctionSymbol(prefix: String, argSorts: List[Sort], returnSort: Sort): FunctionSymbol

def freshPredicateSymbol(prefix: PredicateSymbol): PredicateSymbol

def freshPredicateSymbol(prefix: String, argSorts: List[Sort]): PredicateSymbol

def freshVariable(prefix: Variable): Variable

def freshVariable(prefix: String, sort: Sort): Variable

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

final def wait(): Unit

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

Inherited from AnyRef

Inherited from Any

Ungrouped