diff options
Diffstat (limited to 'test/junit')
4 files changed, 679 insertions, 0 deletions
diff --git a/test/junit/scala/collection/mutable/ArrayBufferTest.scala b/test/junit/scala/collection/mutable/ArrayBufferTest.scala new file mode 100644 index 0000000000..8c83164027 --- /dev/null +++ b/test/junit/scala/collection/mutable/ArrayBufferTest.scala @@ -0,0 +1,36 @@ +package scala.collection.mutable + +import org.junit.runner.RunWith +import org.junit.runners.JUnit4 +import org.junit.{Assert, Test} + +import scala.tools.testing.AssertUtil + +/* Test for SI-9043 */ +@RunWith(classOf[JUnit4]) +class ArrayBufferTest { + @Test + def testInsertAll: Unit = { + val traver = ArrayBuffer(2, 4, 5, 7) + val testSeq = List(1, 3, 6, 9) + + def insertAt(x: Int) = { + val clone = traver.clone() + clone.insertAll(x, testSeq) + clone + } + + // Just insert some at position 0 + Assert.assertEquals(ArrayBuffer(1, 3, 6, 9, 2, 4, 5, 7), insertAt(0)) + + // Insert in the middle + Assert.assertEquals(ArrayBuffer(2, 4, 1, 3, 6, 9, 5, 7), insertAt(2)) + + // No strange last position weirdness + Assert.assertEquals(ArrayBuffer(2, 4, 5, 7, 1, 3, 6, 9), insertAt(traver.size)) + + // Overflow is caught + AssertUtil.assertThrows[IndexOutOfBoundsException] { insertAt(-1) } + AssertUtil.assertThrows[IndexOutOfBoundsException] { insertAt(traver.size + 10) } + } +} diff --git a/test/junit/scala/io/SourceTest.scala b/test/junit/scala/io/SourceTest.scala new file mode 100644 index 0000000000..3138a4589c --- /dev/null +++ b/test/junit/scala/io/SourceTest.scala @@ -0,0 +1,86 @@ + +package scala.io + +import org.junit.Test +import org.junit.Assert._ +import org.junit.runner.RunWith +import org.junit.runners.JUnit4 + +import scala.tools.testing.AssertUtil._ + +import java.io.{ Console => _, _ } + +@RunWith(classOf[JUnit4]) +class SourceTest { + + private implicit val `our codec` = Codec.UTF8 + private val charSet = Codec.UTF8.charSet.name + + private def sampler = """ + |Big-endian and little-endian approaches aren't + |readily interchangeable in general, because the + |laws of arithmetic send signals leftward from + |the bits that are "least significant." + |""".stripMargin.trim + + private def in = new ByteArrayInputStream(sampler.getBytes) + + @Test def canIterateLines() = { + assertEquals(sampler.lines.size, (Source fromString sampler).getLines.size) + } + @Test def canCustomizeReporting() = { + class CapitalReporting(is: InputStream) extends BufferedSource(is) { + override def report(pos: Int, msg: String, out: PrintStream): Unit = { + out print f"$pos%04x: ${msg.toUpperCase}" + } + class OffsetPositioner extends Positioner(null) { + override def next(): Char = { + ch = iter.next() + pos = pos + 1 + ch + } + } + withPositioning(new OffsetPositioner) + } + val s = new CapitalReporting(in) + // skip to next line and report an error + do { + val c = s.next() + } while (s.ch != '\n') + s.next() + val out = new ByteArrayOutputStream + val ps = new PrintStream(out, true, charSet) + s.reportError(s.pos, "That doesn't sound right.", ps) + assertEquals("0030: THAT DOESN'T SOUND RIGHT.", out.toString(charSet)) + } + @Test def canAltCustomizeReporting() = { + class CapitalReporting(is: InputStream)(implicit codec: Codec) extends Source { + override val iter = { + val r = new InputStreamReader(is, codec.decoder) + Iterator continually (codec wrap r.read()) takeWhile (_ != -1) map (_.toChar) + } + override def report(pos: Int, msg: String, out: PrintStream): Unit = { + out print f"$pos%04x: ${msg.toUpperCase}" + } + private[this] var _pos: Int = _ + override def pos = _pos + private[this] var _ch: Char = _ + override def ch = _ch + override def next = { + _ch = iter.next() + _pos += 1 + _ch + } + } + val s = new CapitalReporting(in) + // skip to next line and report an error + do { + val c = s.next() + } while (s.ch != '\n') + s.next() + val out = new ByteArrayOutputStream + val ps = new PrintStream(out, true, charSet) + s.reportError(s.pos, "That doesn't sound right.", ps) + assertEquals("0030: THAT DOESN'T SOUND RIGHT.", out.toString(charSet)) + } +} diff --git a/test/junit/scala/reflect/internal/PrintersTest.scala b/test/junit/scala/reflect/internal/PrintersTest.scala index 7043c26d5e..9bfe6eecb8 100644 --- a/test/junit/scala/reflect/internal/PrintersTest.scala +++ b/test/junit/scala/reflect/internal/PrintersTest.scala @@ -125,6 +125,8 @@ trait BasePrintTests { @Test def testName19 = assertPrintedCode("""class `class`""") @Test def testName20 = assertPrintedCode("""class `test name`""") + + @Test def testName21 = assertPrintedCode("""class `test.name`""") @Test def testIfExpr1 = assertResultCode(code = sm""" |val a = 1 diff --git a/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala b/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala new file mode 100644 index 0000000000..1fff9c9a32 --- /dev/null +++ b/test/junit/scala/tools/nsc/transform/patmat/SolvingTest.scala @@ -0,0 +1,555 @@ +package scala.tools.nsc.transform.patmat + +import org.junit.Assert._ +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.JUnit4 + +import scala.collection.mutable +import scala.tools.nsc.{Global, Settings} + +object TestSolver extends Logic with Solving { + + val global: Global = new Global(new Settings()) + + // disable max recursion depth in order to get all solutions + global.settings.YpatmatExhaustdepth.tryToSet("off" :: Nil) + + object TestSolver extends Solver { + + class Const { + override def toString: String = "Const" + } + + val NullConst = new Const + type Type = Int + + case class TypeConst(i: Int) extends Const + + object TypeConst extends TypeConstExtractor + + case class ValueConst(i: Int) extends Const + + object ValueConst extends ValueConstExtractor { + def apply(t: Tree): Const = ??? + } + + case class Tree(name: String) + + class Var(val x: Tree) extends AbsVar { + + override def equals(other: scala.Any): Boolean = other match { + case that: Var => this.x == that.x + case _ => false + } + + override def hashCode(): Int = x.hashCode() + + override def toString: String = { + s"Var($x)" + } + + def domainSyms = None + + def implications = Nil + + def mayBeNull = false + + def propForEqualsTo(c: Const): Prop = ??? + + def registerEquality(c: Const) = () + + def registerNull() = () + + def symForStaticTp = None + } + + object Var extends VarExtractor { + def apply(x: Tree): Var = new Var(x) + + def unapply(v: Var): Some[Tree] = Some(v.x) + } + + def prepareNewAnalysis() = {} + + def reportWarning(msg: String) = sys.error(msg) + + /** + * The DPLL procedure only returns a minimal mapping from literal to value + * such that the CNF formula is satisfied. + * E.g. for: + * `(a \/ b)` + * The DPLL procedure will find either {a = true} or {b = true} + * as solution. + * + * The expansion step will amend both solutions with the unassigned variable + * i.e., {a = true} will be expanded to {a = true, b = true} and + * {a = true, b = false}. + */ + def expandUnassigned(solution: Solution): List[Model] = { + import solution._ + + // the number of solutions is doubled for every unassigned variable + val expandedModels = 1 << unassigned.size + var current = mutable.ArrayBuffer[Model]() + var next = mutable.ArrayBuffer[Model]() + current.sizeHint(expandedModels) + next.sizeHint(expandedModels) + + current += model + + // we use double buffering: + // read from `current` and create a two models for each model in `next` + for { + s <- unassigned + } { + for { + model <- current + } { + def force(s: Sym, pol: Boolean) = model + (s -> pol) + + next += force(s, pol = true) + next += force(s, pol = false) + } + + val tmp = current + current = next + next = tmp + + next.clear() + } + + current.toList + } + + /** + * Old CNF conversion code, used for reference: + * - convert formula into NNF + * (i.e., no negated terms, only negated variables) + * - use distributive laws to convert into CNF + */ + def eqFreePropToSolvableViaDistribution(p: Prop) = { + val symbolMapping = new SymbolMapping(gatherSymbols(p)) + + type Formula = Array[TestSolver.Clause] + + def formula(c: Clause*): Formula = c.toArray + + def merge(a: Clause, b: Clause) = a ++ b + + def negationNormalFormNot(p: Prop): Prop = p match { + case And(ps) => Or(ps map negationNormalFormNot) + case Or(ps) => And(ps map negationNormalFormNot) + case Not(p) => negationNormalForm(p) + case True => False + case False => True + case s: Sym => Not(s) + } + + def negationNormalForm(p: Prop): Prop = p match { + case Or(ps) => Or(ps map negationNormalForm) + case And(ps) => And(ps map negationNormalForm) + case Not(negated) => negationNormalFormNot(negated) + case True + | False + | (_: Sym) => p + } + + val TrueF: Formula = Array() + val FalseF = Array(clause()) + def lit(sym: Sym) = Array(clause(symbolMapping.lit(sym))) + def negLit(sym: Sym) = Array(clause(-symbolMapping.lit(sym))) + + def conjunctiveNormalForm(p: Prop): Formula = { + def distribute(a: Formula, b: Formula): Formula = + (a, b) match { + // true \/ _ = true + // _ \/ true = true + case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF + // lit \/ lit + case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0))) + // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) + // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) + case (cs, ds) => + val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs) + big flatMap (c => distribute(formula(c), small)) + } + + p match { + case True => TrueF + case False => FalseF + case s: Sym => lit(s) + case Not(s: Sym) => negLit(s) + case And(ps) => + ps.toArray flatMap conjunctiveNormalForm + case Or(ps) => + ps map conjunctiveNormalForm reduceLeft { (a, b) => + distribute(a, b) + } + } + } + val cnf = conjunctiveNormalForm(negationNormalForm(p)) + Solvable(cnf, symbolMapping) + } + + } + +} + +/** + * Testing CNF conversion via Tseitin vs NNF & expansion. + */ +@RunWith(classOf[JUnit4]) +class SolvingTest { + + import scala.tools.nsc.transform.patmat.TestSolver.TestSolver._ + + implicit val Ord: Ordering[TestSolver.TestSolver.Model] = Ordering.by { + _.toSeq.sortBy(_.toString()).toIterable + } + + private def sym(name: String) = Sym(Var(Tree(name)), NullConst) + + @Test + def testSymCreation() { + val s1 = sym("hello") + val s2 = sym("hello") + assertEquals(s1, s2) + } + + /** + * Simplest possible test: solve a formula and check the solution(s) + */ + @Test + def testUnassigned() { + val pSym = sym("p") + val solvable = propToSolvable(Or(pSym, Not(pSym))) + val solutions = TestSolver.TestSolver.findAllModelsFor(solvable) + val expected = List(Solution(Map(), List(pSym))) + assertEquals(expected, solutions) + } + + /** + * Unassigned variables must be expanded + * for stable results + */ + @Test + def testNoUnassigned() { + val pSym = sym("p") + val qSym = sym("q") + val solvable = propToSolvable(Or(pSym, Not(qSym))) + val solutions = findAllModelsFor(solvable) + val expanded = solutions.flatMap(expandUnassigned).sorted + val expected = Seq( + Map(pSym -> false, qSym -> false), + Map(pSym -> true, qSym -> false), + Map(pSym -> true, qSym -> true) + ).sorted + + assertEquals(expected, expanded) + } + + @Test + def testTseitinVsExpansionFrom_t7020() { + val formulas = Seq( + And(And(And(Not(sym("V1=null")), + sym("V1=scala.collection.immutable.::[?]")), And(Not(sym("V1=null")), + And(Or(sym("V2=4"), Or(sym("V2=5"), sym("V2=6"))), sym("V3=Nil")))), + And(And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))))), + + And(And(And(Not(sym("V1=null")), + sym("V1=scala.collection.immutable.::[?]")), And(Not(sym("V1=null")), + And(sym("V2=7"), sym("V3=Nil")))), + And(And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), And(And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil")))))))), + + And(And(Not(sym("V1=null")), + sym("V1=scala.collection.immutable.::[?]")), And(Not(sym("V1=null")), + And(Or(sym("V2=4"), Or(sym("V2=5"), sym("V2=6"))), sym("V3=Nil")))), + + And(And(Not(sym("V1=null")), sym("V1=scala.collection.immutable.::[?]")), + And(Not(sym("V1=null")), And(sym("V2=7"), sym("V3=Nil")))), + + And(And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), And(And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))))), + + And(And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil"))))))), + + And(And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), And(sym("V1=Nil"), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil"))))))))), + + And(And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=7")), Not(sym("V3=Nil"))))), Not(sym("V1=Nil"))))), + + And(And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil")))))), + + And(And(Or(sym("V3=scala.collection.immutable.::[?]"), sym("V3=Nil")), + Or(sym("V1=scala.collection.immutable.::[?]"), sym("V1=Nil"))), + And(And(Or(Or(False, Not(sym("V1=scala.collection.immutable.::[?]"))), + Or(False, Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=7")), Not(sym("V3=Nil"))))), Not(sym("V1=Nil")))))), + + And(Not(sym("V1=null")), And(Or(sym("V2=4"), Or(sym("V2=5"), sym("V2=6"))), + sym("V3=Nil"))), + + And(Not(sym("V1=null")), And(sym("V2=7"), sym("V3=Nil"))), + + And(Not(sym("V1=null")), sym("V1=scala.collection.immutable.::[?]")), + + And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + + And(Not(sym("V2=5")), Not(sym("V2=6"))), + + And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))), + + And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), + + And(Or(Not(sym("V3=Nil")), Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))), + + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null"))))), + + And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=7")), Not(sym("V3=Nil"))))), Not(sym("V1=Nil")))), + + And(Or(Or(False, Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), + + And(Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=7")), Not(sym("V3=Nil"))))), Not(sym("V1=Nil"))), + + And(Or(Or(sym("V1=null"), Not(sym("V1=scala.collection.immutable.::[?]"))), + Or(sym("V1=null"), Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), + Not(sym("V2=6")))), Not(sym("V3=Nil"))))), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil"))))))), + + And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))), + + And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=7")), Not(sym("V3=Nil"))))), + And(And(Or(Not(sym("V1=scala.collection.immutable.::[?]")), + Not(sym("V1=null"))), And(Or(sym("V3=scala.collection.immutable.::[?]"), + Or(sym("V3=Nil"), sym("V3=null"))), And(Or(Not(sym("V3=Nil")), + Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null")))))))), And(sym("V1=Nil"), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))))))), + + And(Or(sym("V2=4"), Or(sym("V2=5"), sym("V2=6"))), sym("V3=Nil")), + + And(Or(sym("V3=scala.collection.immutable.::[?]"), Or(sym("V3=Nil"), + sym("V3=null"))), And(Or(Not(sym("V3=Nil")), Not(sym("V3=null"))), + And(Or(Not(sym("V3=scala.collection.immutable.::[?]")), + Not(sym("V3=null"))), And(Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + Or(sym("V1=scala.collection.immutable.::[?]"), Or(sym("V1=Nil"), + sym("V1=null"))))))), + + And(Or(sym("V3=scala.collection.immutable.::[?]"), + sym("V3=Nil")), Or(sym("V1=scala.collection.immutable.::[?]"), + sym("V1=Nil"))), + + And(sym("V1=Nil"), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), And(Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=2")), Not(sym("V3=Nil")))))))), + + And(sym("V2=7"), sym("V3=Nil")), + + False, + + Not(sym("V1=Nil")), + + Or(And(Not(sym("V2=4")), + And(Not(sym("V2=5")), Not(sym("V2=6")))), Not(sym("V3=Nil"))), + + Or(False, Not(sym("V1=scala.collection.immutable.::[?]"))), + + Or(False, + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil")))), + + Or(False, Or(Not(sym("V2=1")), Not(sym("V3=Nil")))), + + Or(Not(sym("V1=Nil")), Not(sym("V1=null"))), + + Or(Not(sym("V3=scala.collection.immutable.::[?]")), Not(sym("V3=null"))), + + Or(Or(False, Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), + + Or(Or(False, + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(False, + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), + + Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil"))))), + + Or(Or(sym("V1=null"), + Not(sym("V1=scala.collection.immutable.::[?]"))), Or(sym("V1=null"), + Or(Not(sym("V2=1")), Not(sym("V3=Nil"))))), + + Or(sym("V1=null"), Not(sym("V1=scala.collection.immutable.::[?]"))), + + Or(sym("V1=null"), + Or(And(Not(sym("V2=4")), And(Not(sym("V2=5")), Not(sym("V2=6")))), + Not(sym("V3=Nil")))), + + Or(sym("V1=null"), Or(Not(sym("V2=1")), Not(sym("V3=Nil")))), + + Or(sym("V1=scala.collection.immutable.::[?]"), + Or(sym("V1=Nil"), sym("V1=null"))), + + Or(sym("V1=scala.collection.immutable.::[?]"), sym("V1=Nil")), + + Or(sym("V2=4"), Or(sym("V2=5"), sym("V2=6"))), + + sym("V3=scala.collection.immutable.::[?]") + ) + + formulas foreach { + f => + // build CNF + val tseitinCnf = propToSolvable(f) + val expansionCnf = eqFreePropToSolvableViaDistribution(f) + + // ALL-SAT + val tseitinSolutions = findAllModelsFor(tseitinCnf) + val expansionSolutins = findAllModelsFor(expansionCnf) + + // expand unassigned variables + // (otherwise solutions can not be compared) + val tseitinNoUnassigned = tseitinSolutions.flatMap(expandUnassigned).sorted + val expansionNoUnassigned = expansionSolutins.flatMap(expandUnassigned).sorted + assertEquals(tseitinNoUnassigned, expansionNoUnassigned) + } + } +} + + |