diff options
author | Gerard Basler <gerard.basler@gmail.com> | 2015-03-02 04:26:25 +0100 |
---|---|---|
committer | Gerard Basler <gerard.basler@leonteq.com> | 2015-03-02 11:14:49 +0100 |
commit | fe2572c0df8fd209fc5d2e1e32d913b889acbbdd (patch) | |
tree | 9118449d2a65258bda329e85e79243cdecf01390 | |
parent | 081c1f1d3ae01b1a237ab0f7cacdf04eecf71793 (diff) | |
download | scala-fe2572c0df8fd209fc5d2e1e32d913b889acbbdd.tar.gz scala-fe2572c0df8fd209fc5d2e1e32d913b889acbbdd.tar.bz2 scala-fe2572c0df8fd209fc5d2e1e32d913b889acbbdd.zip |
Bring back improvements from `SI-6942` that were lost during the switch to
Tseitin's transformation, e.g., use
`CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`
in order to simplify the resultung formula.
-rw-r--r-- | src/compiler/scala/tools/nsc/transform/patmat/Solving.scala | 38 |
1 files changed, 30 insertions, 8 deletions
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala index f071dc1077..c43f1b6209 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala @@ -65,7 +65,12 @@ trait Solving extends Logic { def size = symbols.size } - case class Solvable(cnf: Cnf, symbolMapping: SymbolMapping) + final case class Solvable(cnf: Cnf, symbolMapping: SymbolMapping) { + def ++(other: Solvable) = { + require(this.symbolMapping eq other.symbolMapping) + Solvable(cnf ++ other.cnf, symbolMapping) + } + } trait CnfBuilder { private[this] val buff = ArrayBuffer[Clause]() @@ -96,7 +101,11 @@ trait Solving extends Logic { } } - def buildCnf: Array[Clause] = buff.toArray + def buildCnf: Array[Clause] = { + val cnf = buff.toArray + buff.clear() + cnf + } } @@ -273,13 +282,26 @@ trait Solving extends Logic { // they could have been removed from the formula val symbolMapping = new SymbolMapping(gatherSymbols(p)) val cnfExtractor = new AlreadyInCNF(symbolMapping) + val cnfTransformer = new TransformToCnf(symbolMapping) + + def cnfFor(prop: Prop): Solvable = { + prop match { + case cnfExtractor.ToCnf(solvable) => + // this is needed because t6942 would generate too many clauses with Tseitin + // already in CNF, just add clauses + solvable + case p => + cnfTransformer.apply(p) + } + } + simplified match { - case cnfExtractor.ToCnf(solvable) => - // this is needed because t6942 would generate too many clauses with Tseitin - // already in CNF, just add clauses - solvable - case p => - new TransformToCnf(symbolMapping).apply(p) + case And(props) => + // SI-6942: + // CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN) + props.map(cnfFor).reduce(_ ++ _) + case p => + cnfFor(p) } } } |