summaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Add an IntelliJ module for the Pax Exam based OSGi testsJason Zaugg2015-01-282-0/+24
| | | | We can now edit these in IntelliJ, as per the regular JUnit tests.
* Merge pull request #4214 from som-snytt/issue/5154Jason Zaugg2015-01-221-4/+3
|\ | | | | SI-5154 Parse leading literal brace in XML pattern
| * SI-5154 Parse leading literal brace in XML patternSom Snytt2014-12-161-4/+3
| | | | | | | | | | | | | | Don't consume literal brace as Scala pattern. Previously, leading space would let the text parser `xText` handle it correctly instead.
* | Merge pull request #4190 from kanielc/SI-5817Jason Zaugg2015-01-222-0/+20
|\ \ | | | | | | SI-5817: Add header to language.scala and languageFeature.scala
| * | SI-5817: Add header to language.scala and languageFeature.scalaDenton Cockburn2014-12-052-0/+20
| | | | | | | | | | | | | | | | | | These two files were missing headers. There is other work on-going to automate updating of the headers, but that likely won't crossover with this.
* | | Merge pull request #4253 from retronym/ticket/9087Grzegorz Kossakowski2015-01-201-0/+5
|\ \ \ | | | | | | | | SI-9087 Fix min/max of reversed Double/Float orderings
| * | | SI-9087 Fix min/max of reversed Double/Float orderingsJason Zaugg2015-01-201-0/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As diagnosed by the reporter, we needed additional overrides due to the way these orderings are implemented. I've added tests to show other methods and other orderings are working correctly. After writing that, I found a scalacheck test related to NaN handling that also covers `Ordering`. I had to correct the assertion in the tests of `reverse.{min,max}`.
* | | | Address review feedbackLukas Rytz2015-01-164-19/+44
| | | | | | | | | | | | | | | | | | | | | | | | - Rename CodeRepository to ByteCodeRepository - Scaladoc on OptimizerReporting - Scaladoc on ByteCodeRepository
* | | | Construct ClassBTypes from parsed classfilesLukas Rytz2015-01-168-80/+306
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This infrastructure is required for the inliner: when inlining code from a classfile, the corresponding ClassBType is needed for various things (eg access checks, InnerClass attribute). The test creates two ClassBTypes for the same class: once using the (unpickled) Symbol, once using the parsed ASM ClassNode, and verifies that the two are the same. There's a cleanup to the InnerClass attribute: object T { class Member; def foo = { class Local } } class T For Java compatibility the InnerClass entry for Member says the class is nested in T (not in the module class T$). We now make sure to add that entry only to T, not to T$ (unless Member is actually referenced in the classfile T$, in that case it will be added, as required).
* | | | Cleanup asm-to-string debug helpersLukas Rytz2015-01-161-14/+56
| | | | | | | | | | | | | | | | | | | | Introduces methods for textifying classes, methods, InsnLists and individual AbstractInsnNodes.
* | | | Remove an unnecessary hash map in BTypesFromSymbolsLukas Rytz2015-01-161-12/+5
| | | | | | | | | | | | | | | | | | | | There's already the map classBTypeFromInternalNameMap in BTypes which stores all ClassBTypes.
* | | | Type alias for InternalNameLukas Rytz2015-01-162-5/+17
| | | |
* | | | Make ClassBType independent of the name tableLukas Rytz2015-01-163-60/+12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Each ClassBType is identified by its internalName, the fully qualified JVM class name. Before this change, the name was stored in the `chrs` array of the compiler name table (hash consed), with the idea to avoid materializing the string. However, we materialize the string anyway, because each ClassBType is stored in the classBTypeFromInternalNameMap, indexed by the string. If string equality turns out to be too slow we can use interning. For the inliner, we read classes from bytecode and create ClassBTypes for them. The names of these classes would not yet exist in the name table, so the backend would need to be able to create new names. Using Strings removes this dependency.
* | | | Merge pull request #4249 from retronym/ticket/9089Vlad Ureche2015-01-161-1/+0
|\ \ \ \ | |/ / / |/| | | SI-9089 Another REPL/FSC + specialization bug fix
| * | | SI-9089 Another REPL/FSC + specialization bug fixJason Zaugg2015-01-151-1/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The enclosed test case stopped working in 2.11.5 on the back of https://github.com/scala/scala/pull/4040. The key change was that we ran all post-typer info transformers on each run of the compiler, rather than trying to reuse the results of the previous run. In that patch, I noticed one place [1] in specialization that aggressively entered specialized members into the owning scope, rather than relying on `transformInfo` to place the new members in the scope of the newly created element of the info history. I made that change after noticing that this code could actually mutated scopes of specializaed types at the parser phase, which led to fairly obscure failures. This bug is another one of these obscure failures, and has the same root cause. We effectively "double specialiaze" Function0, which trips an assertion when `method apply$mcI$sp` is found twice in a scope. I have found another spot that was directly manipulating the scope, and removed the offending code. [1] https://github.com/scala/scala/pull/4040#commitcomment-8531516
* | | | Merge pull request #4201 from mpociecha/fix-typos-in-docs-and-commentsGrzegorz Kossakowski2015-01-14112-196/+196
|\ \ \ \ | | | | | | | | | | Fix many typos in docs and comments
| * | | | Fix many typos in docs and commentsmpociecha2014-12-14113-197/+197
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit corrects many typos found in scaladocs, comments and documentation. It should reduce a bit number of PRs which fix one typo. There are no changes in the 'real' code except one corrected name of a JUnit test method and some error messages in exceptions. In the case of typos in other method or field names etc., I just skipped them. Obviously this commit doesn't fix all existing typos. I just generated in IntelliJ the list of potential typos and looked through it quickly.
* | | | | Merge pull request #4234 from JanBessai/ShowCodeEscapeFixGrzegorz Kossakowski2015-01-141-1/+2
|\ \ \ \ \ | |_|/ / / |/| | | | SI-9057 - fix `showCode` to put backticks around names including dots
| * | | | SI-9057 - fix `showCode` to put backticks around names including dotsJan Bessai2015-01-071-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Missing backticks cause the parser to treat names as paths, which is obviously invalid. A unit test is included.
* | | | | Merge pull request #4200 from er1c/typoJason Zaugg2015-01-091-1/+1
|\ \ \ \ \ | | | | | | | | | | | | Fix scaladoc OutpuStream typo
| * | | | | Fix scaladoc OutpuStream typoEric Peters2014-12-121-1/+1
| | |/ / / | |/| | |
* | | | | Merge pull request #4229 from ↵Grzegorz Kossakowski2015-01-081-1/+2
|\ \ \ \ \ | |_|/ / / |/| | | | | | | | | | | | | | Kornel/feature/SI-9067-enumeration-with-name-improvement SI-9067: Enumeration withName improvement
| * | | | SI-9067: Enumeration withName improvementKornel Kielczewski2015-01-051-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Enumeration#withName in case of a failed approach to resolve the Enumeration value fails with a meaningless NoSuchElementException. Would be nice to know what exactly is not found
* | | | | Bugfix: Implement missing `equals` method for `Sym`.Gerard Basler2014-12-291-1/+12
|/ / / /
* | | | Merge pull request #4139 from retronym/ticket/7965Adriaan Moors2014-12-234-0/+23
|\ \ \ \ | | | | | | | | | | SI-7965 Support calls to MethodHandle.{invoke,invokeExact}
| * | | | SI-7965 Support calls to MethodHandle.{invoke,invokeExact}Jason Zaugg2014-12-034-0/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | These methods are "signature polymorphic", which means that compiler should not: 1. adapt the arguments to `Object` 2. wrap the repeated parameters in an array 3. adapt the result type to `Object`, but instead treat it as it it already conforms to the expected type. Dispiritingly, my initial attempt to implement this touched the type checker, uncurry, erasure, and the backend. However, I realized we could centralize handling of this in the typer if at each application we substituted the signature polymorphic symbol with a clone that carried its implied signature, which is derived from the types of the arguments (typechecked without an expected type) and position within and enclosing cast or block. The test case requires Java 7+ to compile so is currently embedded in a conditionally compiled block of code in a run test. We ought to create a partest category for modern JVMs so we can write such tests in a more natural style. Here's how this looks in bytecode. Note the `bipush` / `istore` before/after the invocation of `invokeExact`, and the descriptor `(LO$;I)I`. ``` % cat sandbox/poly-sig.scala && qscala Test && echo ':javap Test$#main' | qscala import java.lang.invoke._ object O { def bar(x: Int): Int = -x } object Test { def main(args: Array[String]): Unit = { def lookup(name: String, params: Array[Class[_]], ret: Class[_]) = { val lookup = java.lang.invoke.MethodHandles.lookup val mt = MethodType.methodType(ret, params) lookup.findVirtual(O.getClass, name, mt) } def lookupBar = lookup("bar", Array(classOf[Int]), classOf[Int]) val barResult: Int = lookupBar.invokeExact(O, 42) () } } scala> :javap Test$#main public void main(java.lang.String[]); descriptor: ([Ljava/lang/String;)V flags: ACC_PUBLIC Code: stack=3, locals=3, args_size=2 0: aload_0 1: invokespecial #18 // Method lookupBar$1:()Ljava/lang/invoke/MethodHandle; 4: getstatic #23 // Field O$.MODULE$:LO$; 7: bipush 42 9: invokevirtual #29 // Method java/lang/invoke/MethodHandle.invokeExact:(LO$;I)I 12: istore_2 13: return LocalVariableTable: Start Length Slot Name Signature 0 14 0 this LTest$; 0 14 1 args [Ljava/lang/String; 13 0 2 barResult I LineNumberTable: line 16: 0 } ``` I've run this test across our active JVMs: ``` % for v in 1.6 1.7 1.8; do java_use $v; pt --terse test/files/run/t7965.scala || break; done java version "1.6.0_65" Java(TM) SE Runtime Environment (build 1.6.0_65-b14-466.1-11M4716) Java HotSpot(TM) 64-Bit Server VM (build 20.65-b04-466.1, mixed mode) Selected 1 tests drawn from specified tests . 1/1 passed (elapsed time: 00:00:02) Test Run PASSED java version "1.7.0_71" Java(TM) SE Runtime Environment (build 1.7.0_71-b14) Java HotSpot(TM) 64-Bit Server VM (build 24.71-b01, mixed mode) Selected 1 tests drawn from specified tests . 1/1 passed (elapsed time: 00:00:07) Test Run PASSED java version "1.8.0_25" Java(TM) SE Runtime Environment (build 1.8.0_25-b17) Java HotSpot(TM) 64-Bit Server VM (build 25.25-b02, mixed mode) Selected 1 tests drawn from specified tests . 1/1 passed (elapsed time: 00:00:05) Test Run PASSED ```
* | | | | Merge pull request #4208 from lrytz/t9044Adriaan Moors2014-12-234-49/+39
|\ \ \ \ \ | | | | | | | | | | | | SI-9044 Fix order of interfaces in classfiles
| * | | | | SI-9044 Fix order of interfaces in classfilesLukas Rytz2014-12-184-49/+39
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was reversed since ced3ca8ae1. The reason is that the backend used `mixinClasses` to obtain the parents of a class, which returns them in linearization order. `mixinClasses` als returns all ancestors (not only direct parents), which means more work for `minimizeInterfaces`. This was introduced in cd62f52 for unclear reasons. So we switch back to using `parents`.
* | | | | | Merge pull request #4205 from retronym/ticket/9011Adriaan Moors2014-12-231-1/+5
|\ \ \ \ \ \ | | | | | | | | | | | | | | SI-9011 Speculative fix for CCE in Scala IDE
| * | | | | | SI-9011 Speculative fix for CCE in Scala IDEJason Zaugg2014-12-151-1/+5
| | |_|/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Based on the reported stack trace and what I know of Scala IDE, I've changed `InteractiveNamer#enterExistingSymbol` to be `DocDef` aware. I haven't provided a test as this was not minimized from Scala IDE.
* | | | | | Merge pull request #4199 from adriaanm/rebase-4193Adriaan Moors2014-12-183-62/+122
|\ \ \ \ \ \ | | | | | | | | | | | | | | SI-8999 Reduce memory usage in exhaustivity check
| * | | | | | SI-8999 Reduce memory usage in exhaustivity checkGerard Basler2014-12-123-62/+122
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The OOM could occur when all models are forcibly expanded in the DPLL solver. The simplest solution would be to limit the number of returned models but then we are back in non-determinism land (since the subset we get back depends on which models were found first). A better alternative is to create only the models that have corresponding counter examples. If this does not ring a bell, here's a longer explanation: TThe models we get from the DPLL solver need to be mapped back to counter examples. However there's no precalculated mapping model -> counter example. Even worse, not every valid model corresponds to a valid counter example. The reason is that restricting the valid models further would for example require a quadratic number of additional clauses. So to keep the optimistic case fast (i.e., all cases are covered in a pattern match), the infeasible counter examples are filtered later. The DPLL procedure keeps the literals that do not contribute to the solution unassigned, e.g., for `(a \/ b)` only {a = true} or {b = true} is required and the other variable can have any value. This function does a smart expansion of the model and avoids models that have conflicting mappings. For example for in case of the given set of symbols (taken from `t7020.scala`): "V2=2#16" "V2=6#19" "V2=5#18" "V2=4#17" "V2=7#20" One possibility would be to group the symbols by domain but this would only work for equality tests and would not be compatible with type tests. Another observation leads to a much simpler algorithm: Only one of these symbols can be set to true, since `V2` can at most be equal to one of {2,6,5,4,7}. TODO: How does this fare with mixed TypeConst/ValueConst assignments? When the assignments are e.g., V2=Int | V2=2 | V2=4, only the assignments to value constants are mutually exclusive.
* | | | | | Merge pull request #4122 from retronym/ticket/7459-2Adriaan Moors2014-12-185-13/+53
|\ \ \ \ \ \ | | | | | | | | | | | | | | SI-7459 Handle pattern binders used as prefixes in TypeTrees.
| * | | | | | SI-7459 Handle pattern binders used as prefixes in TypeTrees.Jason Zaugg2014-11-145-13/+53
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Match translation was incorrect for: case t => new t.C case D(t) => new d.C We would end up with Types in TypeTrees referring to the wrong symbols, e.g: // t7459a.scala ((x0$1: this.LM) => { case <synthetic> val x1: this.LM = x0$1; case4(){ matchEnd3(new tttt.Node[Any]()) }; matchEnd3(x: Any){ x } Or: // t7459b.scala ((x0$1: CC) => { case <synthetic> val x1: CC = x0$1; case4(){ if (x1.ne(null)) matchEnd3(new tttt.Node[Any]()) else case5() }; This commit: - Changes `bindSubPats` to traverse types, as well as terms, in search of references to bound symbols - Changes `Substitution` to reuse `Tree#substituteSymbols` rather than the home-brew substitution from `Tree`s to `Tree`s, if the `to` trees are all `Ident`s - extends `substIdentsForTrees` to substitute selections like `x1.caseField` into types. I had to dance around the awkward handling of "swatches" (exception handlers that can be implemented with JVM native type switches) by duplicating trees to avoid seeing the results of `substituteSymbols` in `caseDefs` after we abandon that approach if we detect the patterns are too complex late in the game. I also had to add an escape hatch for the "type selection from volatile type" check in the type checker. Without this, the translation of `pos/t7459c.scala`: case <synthetic> val x1: _$1 = (null: Test.Mirror[_]).universe; case5(){ if (x1.isInstanceOf[Test.JavaUniverse]) { <synthetic> val x2: _$1 with Test.JavaUniverse = (x1.asInstanceOf[_$1 with Test.JavaUniverse]: _$1 with Test.JavaUniverse); matchEnd4({ val ju1: Test.JavaUniverse = x2; val f: () => x2.Type = (() => (null: x2.TypeTag[Nothing]).tpe); .. triggers that error at `x2.TypeTag`.
* | | | | | | Merge pull request #4085 from adriaanm/patmat-suppressLukas Rytz2014-12-183-6/+7
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | Suppress match analysis under -Xno-patmat-analysis
| * | | | | | | Suppress match analysis under -Xno-patmat-analysisAdriaan Moors2014-12-123-6/+7
| | |/ / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | NoSuppression doesn't suppress. FullSuppression does. Now using the latter when running under `-Xno-patmat-analysis`. I should really have tested. /me hides under a rock
* | | | | | | Merge pull request #4191 from som-snytt/issue/8538Lukas Rytz2014-12-181-3/+14
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | SI-8538 Test or example for Source.report
| * | | | | | | SI-8538 Document extensionSom Snytt2014-12-151-3/+14
| |/ / / / / / | | | | | | | | | | | | | | | | | | | | | Scaladoc for report extension point.
* | | | | | | Merge pull request #4211 from lrytz/bcode-buildGrzegorz Kossakowski2014-12-182-1/+2
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | Run dead code elimination by default in GenBCode
| * | | | | | | Run dead code elimination by default in GenBCodeLukas Rytz2014-12-162-1/+2
| | |_|/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was disabled by mistake. Settings are still a challenge. This fixes the bcode-delambdafy-method build (https://scala-webapps.epfl.ch/jenkins/view/2.11.x/job/scala-nightly-genbcode-2.11.x/)
* | | | | | | Merge pull request #4196 from lrytz/t9030-2.11Lukas Rytz2014-12-172-2/+2
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | | [nomerge] SI-9030 don't call private BoxesRunTime.equalsNumChar
| * | | | | | [nomerge] SI-9030 don't call private BoxesRunTime.equalsNumCharLukas Rytz2014-12-112-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When comparing a Number and a Character, the would emit a call to the private method. For binary compatibility, this method remains private in 2.11, so we just use equalsNumObject instead.
* | | | | | | Merge pull request #4202 from kanielc/SI-9043Grzegorz Kossakowski2014-12-151-6/+7
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | SI-9043 ArrayBuffer.insert and insertAll are very slow
| * | | | | | | SI-9043 ArrayBuffer.insert and insertAll are very slowDenton Cockburn2014-12-141-6/+7
| | |_|/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | insert and insertAll were slower than their java equivalents by factors of 5 and 10 respectively. Benchmark code was provided here: https://gist.github.com/rklaehn/3e9290118fcf63d1feae We are using a toList to the source Traversable Then doing a length and a copy on that collection. By using an array, we can make use of faster methods. Managed to get the ratios down to 1.5 and 1.5 respectively. In addition to this, I think we should consider breaking insert into 2 separate methods, one for a single item and one for a collection. The varags version is very expensive when a single item is being inserted. @phaller @axel22
* / | | | | | fix ByteCodecs scaladocxuwei-k2014-12-141-2/+2
|/ / / / / /
* | | | | | Merge pull request #4078 from gbasler/topic/fix-analysis-budgetAdriaan Moors2014-12-128-277/+600
|\ \ \ \ \ \ | | | | | | | | | | | | | | Avoid the `CNF budget exceeded` exception via smarter translation into CNF.
| * | | | | | Avoid the `CNF budget exceeded` exception via smarter translation into CNF.Gerard Basler2014-10-277-268/+573
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The exhaustivity checks in the pattern matcher build a propositional formula that must be converted into conjunctive normal form (CNF) in order to be amenable to the following DPLL decision procedure. However, the simple conversion into CNF via negation normal form and Shannon expansion that was used has exponential worst-case complexity and thus even simple problems could become untractable. A better approach is to use a transformation into an _equisatisfiable_ CNF-formula (by generating auxiliary variables) that runs with linear complexity. The commonly known Tseitin transformation uses bi- implication. I have choosen for an enhancement: the Plaisted transformation which uses implication only, thus the resulting CNF formula has (on average) only half of the clauses of a Tseitin transformation. The Plaisted transformation uses the polarities of sub-expressions to figure out which part of the bi-implication can be omitted. However, if all sub-expressions have positive polarity (e.g., after transformation into negation normal form) then the conversion is rather simple and the pseudo-normalization via NNF increases chances only one side of the bi-implication is needed. I implemented only optimizations that had a substantial effect on formula size: - formula simplification, extraction of multi argument operands - if a formula is already in CNF then the Tseitin/Plaisted transformation is omitted - Plaisted via NNF - omitted: (sharing of sub-formulas is also not implemented) - omitted: (clause subsumption)
| * | | | | | Debug printing for Any, not AnyRef, to include primitivesAdriaan Moors2014-10-261-3/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Signed-off-by: Gerard Basler <gerard.basler@gmail.com>
| * | | | | | And, Or take sets of PropsGerard Basler2014-10-263-39/+57
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Remove redundant UniqueSym class.
* | | | | | | Merge pull request #4192 from Ichoran/issue/8950Lukas Rytz2014-12-112-2/+2
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | | | | SI-8950 SeqView and StreamView allow indexing out of a slice