trait PropositionalLogic extends AnyRef
- Alphabetic
- By Inheritance
- PropositionalLogic
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- All
Type Members
- trait AbsVar extends AnyRef
- final case class And(ops: Set[Prop]) extends Prop with Product with Serializable
- final case class AtMostOne(ops: List[Sym]) extends Prop with Product with Serializable
- abstract type Const
- final case class Eq(p: Var, q: Const) extends Prop with Product with Serializable
- type Model = Map[Sym, Boolean]
- final case class Not(a: Prop) extends Prop with Product with Serializable
- final case class Or(ops: Set[Prop]) extends Prop with Product with Serializable
- class Prop extends AnyRef
- trait PropMap extends AnyRef
- trait PropTraverser extends AnyRef
- final case class Solution(model: Model, unassigned: List[Sym]) extends Product with Serializable
- abstract type Solvable
- final class Sym extends Prop
- abstract type Tree
- abstract type Type
- abstract type TypeConst <: Const
- trait TypeConstExtractor extends AnyRef
- abstract type ValueConst <: Const
- trait ValueConstExtractor extends AnyRef
- abstract type Var <: AbsVar
- trait VarExtractor extends AnyRef
Abstract Value Members
- abstract val EmptyModel: Model
- abstract val NoModel: Model
- abstract val NullConst: Const
- abstract def TypeConst: TypeConstExtractor
- abstract def ValueConst: ValueConstExtractor
- abstract val Var: VarExtractor
- abstract def eqFreePropToSolvable(f: Prop): Solvable
- abstract def findAllModelsFor(solvable: Solvable, pos: Position = NoPosition): List[Solution]
- abstract def findModelFor(solvable: Solvable): Model
- abstract def prepareNewAnalysis(): Unit
- abstract def reportWarning(message: String): Unit
- abstract def uncheckedWarning(pos: Position, msg: String): Unit
Concrete Value Members
-
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 PropositionalLogic to any2stringadd[PropositionalLogic] performed by method any2stringadd in scala.Predef.
- Definition Classes
- any2stringadd
-
def
->[B](y: B): (PropositionalLogic, B)
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to ArrowAssoc[PropositionalLogic] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @inline()
- def /\(props: Iterable[Prop]): Product with Serializable with Prop
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def \/(props: Iterable[Prop]): Product with Serializable with Prop
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
- val budgetProp: sys.Prop[String]
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
def
ensuring(cond: (PropositionalLogic) ⇒ Boolean, msg: ⇒ Any): PropositionalLogic
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to Ensuring[PropositionalLogic] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
-
def
ensuring(cond: (PropositionalLogic) ⇒ Boolean): PropositionalLogic
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to Ensuring[PropositionalLogic] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
-
def
ensuring(cond: Boolean, msg: ⇒ Any): PropositionalLogic
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to Ensuring[PropositionalLogic] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
-
def
ensuring(cond: Boolean): PropositionalLogic
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to Ensuring[PropositionalLogic] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to StringFormat[PropositionalLogic] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @inline()
- def gatherSymbols(p: Prop): Set[Sym]
- def gatherVariables(p: Prop): Set[Var]
-
final
def
getClass(): Class[_]
- 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 propToSolvable(p: Prop): Solvable
- def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop])
-
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 http://www.decision-procedures.org/slides/propositional_logic-2x3.pdf
-
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( ... ) @native()
-
def
→[B](y: B): (PropositionalLogic, B)
- Implicit
- This member is added by an implicit conversion from PropositionalLogic to ArrowAssoc[PropositionalLogic] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- object AnalysisBudget
- object And extends Serializable
- object False extends Prop with Product with Serializable
- object Or extends Serializable
- object Sym
- object True extends Prop with Product with Serializable
The Scala compiler and reflection APIs.