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
- def /\(props: Iterable[Prop]): Product with Serializable with Prop
- def \/(props: Iterable[Prop]): Product with Serializable with Prop
- val budgetProp: sys.Prop[String]
- def gatherSymbols(p: Prop): Set[Sym]
- def gatherVariables(p: Prop): Set[Var]
- 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
- 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.