From b64a5ec51a1ed806a881a8d803071f927d730963 Mon Sep 17 00:00:00 2001 From: Gerard Basler Date: Sun, 15 Jun 2014 16:48:51 +0200 Subject: And, Or take sets of Props Remove redundant UniqueSym class. --- .../scala/tools/nsc/transform/patmat/Logic.scala | 49 ++++++++++++++-------- .../nsc/transform/patmat/MatchOptimization.scala | 8 ++-- .../scala/tools/nsc/transform/patmat/Solving.scala | 39 +++++++++-------- 3 files changed, 57 insertions(+), 39 deletions(-) (limited to 'src/compiler') diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala index e6ddf8b758..175aea77da 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala @@ -11,6 +11,7 @@ import scala.language.postfixOps import scala.collection.mutable import scala.reflect.internal.util.Statistics import scala.reflect.internal.util.HashSet +import scala.annotation.tailrec trait Logic extends Debugging { import PatternMatchingStats._ @@ -46,7 +47,7 @@ trait Logic extends Debugging { type Tree class Prop - case class Eq(p: Var, q: Const) extends Prop + final case class Eq(p: Var, q: Const) extends Prop type Const @@ -103,39 +104,53 @@ trait Logic extends Debugging { def implications: List[(Sym, List[Sym], List[Sym])] } + private def propToLinkedHashSet(ops: Seq[Prop]) = { + val set = new mutable.LinkedHashSet[Prop]() + ops.foreach(set += _) + set + } + // would be nice to statically check whether a prop is equational or pure, // but that requires typing relations like And(x: Tx, y: Ty) : (if(Tx == PureProp && Ty == PureProp) PureProp else Prop) - case class And(a: Prop, b: Prop) extends Prop - case class Or(a: Prop, b: Prop) extends Prop - case class Not(a: Prop) extends Prop + final case class And(ops: mutable.LinkedHashSet[Prop]) extends Prop + object And { + def apply(ops: Prop*) = new And(propToLinkedHashSet(ops)) + } + final case class Or(ops: mutable.LinkedHashSet[Prop]) extends Prop + object Or { + def apply(ops: Prop*) = new Or(propToLinkedHashSet(ops)) + } + + final case class Not(a: Prop) extends Prop case object True extends Prop case object False extends Prop // symbols are propositions - abstract case class Sym(variable: Var, const: Const) extends Prop { + final class Sym private[PropositionalLogic] (val variable: Var, val const: Const) extends Prop { private val id: Int = Sym.nextSymId - override def toString = variable +"="+ const +"#"+ id + override def toString = variable + "=" + const + "#" + id } - class UniqueSym(variable: Var, const: Const) extends Sym(variable, const) + object Sym { private val uniques: HashSet[Sym] = new HashSet("uniques", 512) def apply(variable: Var, const: Const): Sym = { - val newSym = new UniqueSym(variable, const) + val newSym = new Sym(variable, const) (uniques findEntryOrUpdate newSym) } - private def nextSymId = {_symId += 1; _symId}; private var _symId = 0 + def nextSymId = {_symId += 1; _symId}; private var _symId = 0 implicit val SymOrdering: Ordering[Sym] = Ordering.by(_.id) } - def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _)) - def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _)) + def /\(props: Iterable[Prop]) = if (props.isEmpty) True else And(props.toSeq: _*) + def \/(props: Iterable[Prop]) = if (props.isEmpty) False else Or(props.toSeq: _*) + trait PropTraverser { def apply(x: Prop): Unit = x match { - case And(a, b) => apply(a); apply(b) - case Or(a, b) => apply(a); apply(b) + case And(ops) => ops foreach apply + case Or(ops) => ops foreach apply case Not(a) => apply(a) case Eq(a, b) => applyVar(a); applyConst(b) case _ => @@ -154,8 +169,8 @@ trait Logic extends Debugging { trait PropMap { def apply(x: Prop): Prop = x match { // TODO: mapConserve - case And(a, b) => And(apply(a), apply(b)) - case Or(a, b) => Or(apply(a), apply(b)) + case And(ops) => And(ops map apply) + case Or(ops) => Or(ops map apply) case Not(a) => Not(apply(a)) case p => p } @@ -255,8 +270,8 @@ trait Logic extends Debugging { } } - debug.patmat("eqAxioms:\n"+ cnfString(toFormula(eqAxioms))) - debug.patmat("pure:"+ pure.map(p => cnfString(p)).mkString("\n")) + debug.patmat(s"eqAxioms:\n$eqAxioms") + debug.patmat(s"pure:${pure.mkString("\n")}") if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start) diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala index e9c81f4728..b3aef8a20e 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala @@ -46,16 +46,16 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis { val cond = test.prop def simplify(c: Prop): Set[Prop] = c match { - case And(a, b) => simplify(a) ++ simplify(b) - case Or(_, _) => Set(False) // TODO: make more precise - case Not(Eq(Var(_), NullConst)) => Set(True) // not worth remembering + case And(ops) => ops.toSet flatMap simplify + case Or(ops) => Set(False) // TODO: make more precise + case Not(Eq(Var(_), NullConst)) => Set(True) // not worth remembering case _ => Set(c) } val conds = simplify(cond) if (conds(False)) false // stop when we encounter a definite "no" or a "not sure" else { - val nonTrivial = conds filterNot (_ == True) + val nonTrivial = conds - True if (nonTrivial nonEmpty) { tested ++= nonTrivial diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala index 4330781013..c5475b50c0 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala @@ -44,23 +44,23 @@ trait Solving extends Logic { def negationNormalFormNot(p: Prop, budget: Int): Prop = if (budget <= 0) throw AnalysisBudget.exceeded else p match { - case And(a, b) => Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) - case Or(a, b) => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) - case Not(p) => negationNormalForm(p, budget - 1) - case True => False - case False => True - case s: Sym => Not(s) + case And(ps) => Or (ps map (negationNormalFormNot(_, budget - 1))) + case Or(ps) => And(ps map (negationNormalFormNot(_, budget - 1))) + case Not(p) => negationNormalForm(p, budget - 1) + case True => False + case False => True + case s: Sym => Not(s) } def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop = if (budget <= 0) throw AnalysisBudget.exceeded else p match { - case And(a, b) => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) - case Or(a, b) => Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) - case Not(negated) => negationNormalFormNot(negated, budget - 1) + case Or(ps) => Or (ps map (negationNormalForm(_, budget - 1))) + case And(ps) => And(ps map (negationNormalForm(_, budget - 1))) + case Not(negated) => negationNormalFormNot(negated, budget - 1) case True | False - | (_ : Sym) => p + | (_ : Sym) => p } val TrueF = formula() @@ -92,14 +92,17 @@ trait Solving extends Logic { case False => FalseF case s: Sym => lit(s) case Not(s: Sym) => negLit(s) - case And(a, b) => - val cnfA = conjunctiveNormalForm(a, budget - 1) - val cnfB = conjunctiveNormalForm(b, budget - cnfA.size) - cnfA ++ cnfB - case Or(a, b) => - val cnfA = conjunctiveNormalForm(a) - val cnfB = conjunctiveNormalForm(b) - distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size)) + case And(ps) => + val formula = formulaBuilder + ps foreach { p => + val cnf = conjunctiveNormalForm(p, budget - 1) + addFormula(formula, cnf) + } + toFormula(formula) + case Or(ps) => + ps map (conjunctiveNormalForm(_)) reduceLeft { (a, b) => + distribute(a, b, budget - (a.size + b.size)) + } } } -- cgit v1.2.3