Skip to content

Instantly share code, notes, and snippets.

@lyricallogical

lyricallogical/exhaustive.diff

Created January 9, 2016 19:45
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save lyricallogical/0e37adf140c62a0704e9 to your computer and use it in GitHub Desktop.
Save lyricallogical/0e37adf140c62a0704e9 to your computer and use it in GitHub Desktop.
Download ZIP
scalac -Ypatmat-debug exhaustive0.scala と scalac -Ypatmat-debug exhaustive1.scala の diff
Raw
exhaustive.diff
138c138
< enum class E sealed, subclasses: List(class Cons, trait L, object SNil)
---
> enum class E sealed, subclasses: List(class Cons, object SNil)
140d139
< checkableType(E.L): E.L
142,143c141
< enum sealed tp=E.E, tpApprox=E.E as: List(E.Cons, E.L, E.SNil.type)
< uniqued const: (E.L,E.L)
---
> enum sealed tp=E.E, tpApprox=E.E as: List(E.Cons, E.SNil.type)
147,148c145,146
< excluded: List(V2=null#7)
< implied: List(V2=E.L#6)
---
> excluded: List(V2=null#6)
> implied: List()
150,153c148
< excluded: List(V2=null#7)
< implied: List(V2=E.L#6)
< eq axioms for: null
< excluded: List(V2=E.L#6)
---
> excluded: List(V2=null#6)
155c150
< eq axioms for: E.L
---
> eq axioms for: null
159d153
< checkableType(E.L): E.L
162c156,161
< enum unsealed (E.L,trait L,false,false)
---
> enum trait L sealed, subclasses: List(class Cons, object SNil)
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> enum sealed tp=E.L, tpApprox=E.L as: List(E.Cons, E.SNil.type)
> unique const: (E.SNil.type,SNil)
> uniqued const: (E.L,E.L)
164c163
< excluded: List()
---
> excluded: List(V1=null#2)
167c166
< excluded: List()
---
> excluded: List(V1=null#2)
172c171,173
< enum unsealed (E.L,trait L,false,false)
---
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> unique const: (E.SNil.type,SNil)
174,177c175,178
< Or(Set(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
< Or(Set(Not(V2=E.Cons#5), V2=E.L#6))
< Or(Set(Not(V2=SNil#4), V2=E.L#6))
< AtMostOne(List(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
---
> Or(Set(V2=E.Cons#5, V2=SNil#4, V2=null#6))
> AtMostOne(List(V2=E.Cons#5, V2=SNil#4, V2=null#6))
> Or(Set(V1=E.Cons#3, V1=SNil#1, V1=null#2))
> AtMostOne(List(V1=E.Cons#3, V1=SNil#1, V1=null#2))
183,186c184,187
< Or(Set(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
< Or(Set(Not(V2=E.Cons#5), V2=E.L#6))
< Or(Set(Not(V2=SNil#4), V2=E.L#6))
< AtMostOne(List(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
---
> Or(Set(V2=E.Cons#5, V2=SNil#4, V2=null#6))
> AtMostOne(List(V2=E.Cons#5, V2=SNil#4, V2=null#6))
> Or(Set(V1=E.Cons#3, V1=SNil#1, V1=null#2))
> AtMostOne(List(V1=E.Cons#3, V1=SNil#1, V1=null#2))
191,192c192,193
< V1: E.L ::= E.Cons | SNil | null | ... // = x1
< V2: E.E ::= E.Cons | E.L | SNil | null// Set(E.Cons, SNil, null, E.L) // = x1.cdr
---
> V1: E.L ::= E.Cons | SNil | null// Set(E.Cons, SNil, null) // = x1
> V2: E.E ::= E.Cons | SNil | null// Set(E.Cons, SNil, null) // = x1.cdr
194c195,227
< And(Set(Or(Set(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7)), Or(Set(Not(V2=E.Cons#5), V2=E.L#6)), Or(Set(Not(V2=SNil#4), V2=E.L#6)), AtMostOne(List(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))))
---
> And(Set(Or(Set(V2=E.Cons#5, V2=SNil#4, V2=null#6)), AtMostOne(List(V2=E.Cons#5, V2=SNil#4, V2=null#6)), Or(Set(V1=E.Cons#3, V1=SNil#1, V1=null#2)), AtMostOne(List(V1=E.Cons#3, V1=SNil#1, V1=null#2))))
> DPLL
> Lit#1 \/ \/ /\
> Lit#-1 \/ Lit#-6 \/ /\
> Lit#-1 \/ Lit#-2 \/ /\
> Lit#-6 \/ Lit#-2 \/ /\
> Lit#1 \/ Lit#6 \/ Lit#2 /\
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#-6 \/ \/ /\
> Lit#4 \/ \/ /\
> Lit#-2 \/ \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3
> DPLL
> Lit#-6 \/ \/ /\
> Lit#-2 \/ \/ /\
> Lit#-6 \/ Lit#-2 \/ /\
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#-6 \/ \/ /\
> Lit#4 \/ \/ /\
> Lit#-2 \/ \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3
> DPLL
> Lit#-2 \/ \/ /\
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#4 \/ \/ /\
> Lit#-2 \/ \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3
196,242c229,236
< Lit#1 \/ \/ \/ /\
< Lit#-7 \/ \/ \/ /\
< Lit#6 \/ Lit#2 \/ Lit#5 \/ Lit#4 /\
< Lit#-5 \/ Lit#2 \/ \/ /\
< Lit#-6 \/ Lit#2 \/ \/ /\
< Lit#5 \/ \/ \/ /\
< Lit#-6 \/ Lit#-2 \/ \/ /\
< Lit#-6 \/ Lit#-5 \/ \/ /\
< Lit#-6 \/ Lit#-4 \/ \/ /\
< Lit#-2 \/ Lit#-5 \/ \/ /\
< Lit#-2 \/ Lit#-4 \/ \/ /\
< Lit#-5 \/ Lit#-4 \/ \/ /\
< Lit#-3 \/ \/ \/
< DPLL
< Lit#-7 \/ \/ \/ /\
< Lit#6 \/ Lit#2 \/ Lit#5 \/ Lit#4 /\
< Lit#-5 \/ Lit#2 \/ \/ /\
< Lit#-6 \/ Lit#2 \/ \/ /\
< Lit#5 \/ \/ \/ /\
< Lit#-6 \/ Lit#-2 \/ \/ /\
< Lit#-6 \/ Lit#-5 \/ \/ /\
< Lit#-6 \/ Lit#-4 \/ \/ /\
< Lit#-2 \/ Lit#-5 \/ \/ /\
< Lit#-2 \/ Lit#-4 \/ \/ /\
< Lit#-5 \/ Lit#-4 \/ \/ /\
< Lit#-3 \/ \/ \/
< DPLL
< Lit#6 \/ Lit#2 \/ Lit#5 \/ Lit#4 /\
< Lit#-5 \/ Lit#2 \/ \/ /\
< Lit#-6 \/ Lit#2 \/ \/ /\
< Lit#5 \/ \/ \/ /\
< Lit#-6 \/ Lit#-2 \/ \/ /\
< Lit#-6 \/ Lit#-5 \/ \/ /\
< Lit#-6 \/ Lit#-4 \/ \/ /\
< Lit#-2 \/ Lit#-5 \/ \/ /\
< Lit#-2 \/ Lit#-4 \/ \/ /\
< Lit#-5 \/ Lit#-4 \/ \/ /\
< Lit#-3 \/ \/ \/
< DPLL
< Lit#2 \/ /\
< Lit#-6 \/ Lit#2 /\
< Lit#-6 \/ Lit#-2 /\
< Lit#-6 \/ /\
< Lit#-6 \/ Lit#-4 /\
< Lit#-2 \/ /\
< Lit#-2 \/ Lit#-4 /\
< Lit#-4 \/ /\
---
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#4 \/ \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3
> DPLL
> Lit#-5 \/ /\
> Lit#-5 \/ Lit#-3 /\
245,255c239,376
< Lit#-6 \/ /\
< Lit#-6 \/ /\
< Lit#-6 \/ Lit#-4 /\
< \/ /\
< Lit#-4 \/ /\
< Lit#-4 \/ /\
< Lit#-3 \/
< todesking0.scala:9: warning: unreachable code
< case Cons(_, SNil) => 2
< ^
< enum unsealed (E.L,trait L,false,false)
---
> Lit#-3
> DPLL
>
> DPLL
> Lit#-2 \/ \/ /\
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#-6 \/ \/ /\
> Lit#1 \/ \/ /\
> Lit#2 \/ Lit#-1 \/ Lit#-4 /\
> Lit#-1 \/ Lit#-6 \/ /\
> Lit#-1 \/ Lit#-2 \/ /\
> Lit#-6 \/ Lit#-2 \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3 /\
> Lit#1 \/ Lit#6 \/ Lit#2
> DPLL
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#-6 \/ \/ /\
> Lit#1 \/ \/ /\
> Lit#-1 \/ Lit#-4 \/ /\
> Lit#-1 \/ Lit#-6 \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3 /\
> Lit#1 \/ Lit#6 \/
> DPLL
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#1 \/ \/ /\
> Lit#-1 \/ Lit#-4 \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3 /\
> Lit#1 \/ \/
> DPLL
> Lit#-5 \/ Lit#-4 \/ /\
> Lit#-5 \/ Lit#-3 \/ /\
> Lit#-4 \/ Lit#-3 \/ /\
> Lit#-4 \/ \/ /\
> Lit#5 \/ Lit#4 \/ Lit#3
> DPLL
> Lit#-5 \/ Lit#-3 /\
> Lit#5 \/ Lit#3
> DPLL
> Lit#-5 \/ Lit#-3 /\
> Lit#5 \/ Lit#3 /\
> Lit#-5 \/
> DPLL
> Lit#3
> DPLL
>
> enum trait L sealed, subclasses: List(class Cons, object SNil)
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> enum sealed tp=E.L, tpApprox=E.L as: List(E.Cons, E.SNil.type)
> checkableType(E.L): E.L
> checkableType(E.SNil.type): E.SNil.type
> uniqued const: (E.SNil.type,SNil)
> checkableType(E.Cons): E.Cons
> uniqued const: (E.Cons,E.Cons)
> checkableType(E.E): E.E
> analysing:
> treeMakers:
> ET(x1,E.this.SNil) >> B(1,Int) >> >>
> TT(E.Cons,x1,E.Cons) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
> TT(E.Cons,x1,E.Cons) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int) >>
> removeVarEq vars: Set(V1, V2)
> enum trait L sealed, subclasses: List(class Cons, object SNil)
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> enum sealed tp=E.L, tpApprox=E.L as: List(E.Cons, E.SNil.type)
> unique const: (E.SNil.type,SNil)
> uniqued const: (E.L,E.L)
> eq axioms for: E.Cons
> excluded: List()
> implied: List()
> eq axioms for: SNil
> excluded: List()
> implied: List()
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> unique const: (E.SNil.type,SNil)
> enum class E sealed, subclasses: List(class Cons, object SNil)
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> enum sealed tp=E.E, tpApprox=E.E as: List(E.Cons, E.SNil.type)
> unique const: (E.SNil.type,SNil)
> uniqued const: (E.E,E.E)
> eq axioms for: E.Cons
> excluded: List()
> implied: List()
> eq axioms for: SNil
> excluded: List()
> implied: List()
> checkableType(E.Cons): E.Cons
> checkableType(E.SNil.type): E.SNil.type
> unique const: (E.SNil.type,SNil)
> eqAxioms:
> Or(Set(V1=E.Cons#8, V1=SNil#7))
> AtMostOne(List(V1=E.Cons#8, V1=SNil#7))
> Or(Set(V2=E.Cons#10, V2=SNil#9))
> AtMostOne(List(V2=E.Cons#10, V2=SNil#9))
> pure:Not(Or(Set(And(Set(V1=SNil#7)), And(Set(And(Set(True, V1=E.Cons#8)), True, V2=SNil#9)), And(Set(And(Set(True, V1=E.Cons#8)), True)))))
> find all models for
> Lit#4 \/ Lit#3 /\
> Lit#-3 \/ /\
> Lit#-2 \/ Lit#-1 /\
> Lit#2 \/ Lit#1 /\
> Lit#-4 \/ Lit#-1 /\
> Lit#-4 \/ Lit#-3 /\
> Lit#-4 \/
> find all models for
> Lit#4 \/ Lit#3 /\
> Lit#-3 \/ /\
> Lit#-2 \/ Lit#-1 /\
> Lit#2 \/ Lit#1 /\
> Lit#-4 \/ Lit#-1 /\
> Lit#-4 \/ Lit#-3 /\
> Lit#-4 \/
> DPLL
> Lit#4 \/ Lit#3 /\
> Lit#-3 \/ /\
> Lit#-2 \/ Lit#-1 /\
> Lit#2 \/ Lit#1 /\
> Lit#-4 \/ Lit#-1 /\
> Lit#-4 \/ Lit#-3 /\
> Lit#-4 \/
> DPLL
> Lit#4 \/ /\
> Lit#-2 \/ Lit#-1 /\
> Lit#2 \/ Lit#1 /\
> Lit#-4 \/ Lit#-1 /\
> Lit#-4 \/
> DPLL
> Lit#-2 \/ Lit#-1 /\
> Lit#2 \/ Lit#1 /\
> Lit#-1 \/ /\
> \/
267,269c388,390
< dependencies: Map(T19C(Eq(V1,SNil)) -> Set(Eq(V1,SNil)), T21C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))) -> Set(Eq(V1,E.Cons)), T23C(Eq(V2,SNil)) -> Set(Eq(V2,SNil), Eq(V1,E.Cons)))
< sharedPrefix: List(T25C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
< suffix: List(T25C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
---
> dependencies: Map(T28C(Eq(V1,SNil)) -> Set(Eq(V1,SNil)), T30C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))) -> Set(Eq(V1,E.Cons)), T32C(Eq(V2,SNil)) -> Set(Eq(V1,E.Cons), Eq(V2,SNil)))
> sharedPrefix: List(T34C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
> suffix: List(T34C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
351d471
< one warning found
Raw
exhaustive0.log
translating {case _ => throw new IndexOutOfBoundsException(x$1.toString())}
combining cases: {B(throw new IndexOutOfBoundsException(x$1.toString()),Any)}
removeVarEq vars: Set()
eqAxioms:
pure:Not(True)
removeVarEq vars: Set()
eqAxioms:
pure:True
reachability, vars:
equality axioms:
And(Set())
enum unsealed (Int,class Int,false,true)
before CSE:
treeMakers:
B(throw new IndexOutOfBoundsException(x$1.toString()),Any)
dependencies: Map()
after CSE:
treeMakers:
B(throw new IndexOutOfBoundsException(x$1.toString()),Any)
def: (case <synthetic> val x1: Int = x$1,List(value x1),List(method productElement, object SNil, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: Int = x$1,class scala.reflect.internal.Trees$ValDef,List(value x1, method productElement, object SNil, object E, package <empty>, package <root>),List(method productElement, object SNil, object E, package <empty>, package <root>))
def: (case4(){
matchEnd3(throw new IndexOutOfBoundsException(x$1.toString()))
},List(method case4),List(method productElement, object SNil, object E, package <empty>, package <root>))
untouched (case4(){
matchEnd3(throw new IndexOutOfBoundsException(x$1.toString()))
},class scala.reflect.internal.Trees$LabelDef,List(method case4, method productElement, object SNil, object E, package <empty>, package <root>),List(method productElement, object SNil, object E, package <empty>, package <root>))
def: (matchEnd3(x){
x
},List(method matchEnd3),List(method productElement, object SNil, object E, package <empty>, package <root>))
untouched (matchEnd3(x){
x
},class scala.reflect.internal.Trees$LabelDef,List(method matchEnd3, method productElement, object SNil, object E, package <empty>, package <root>),List(method productElement, object SNil, object E, package <empty>, package <root>))
translating {case 0 => Cons.this.car
case 1 => Cons.this.cdr
case _ => throw new IndexOutOfBoundsException(x$1.toString())}
combining cases: {ET(x1,0) >> B(Cons.this.car,Any)
ET(x1,1) >> B(Cons.this.cdr,Any)
B(throw new IndexOutOfBoundsException(x$1.toString()),Any)}
def: (case <synthetic> val x1: Int = x$1,List(value x1),List(method productElement, class Cons, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: Int = x$1,class scala.reflect.internal.Trees$ValDef,List(value x1, method productElement, class Cons, object E, package <empty>, package <root>),List(method productElement, class Cons, object E, package <empty>, package <root>))
translating {case (_: E.Cons) => true
case _ => false}
TTTM(value x1,false,value x1,E.Cons,E.Cons)
combining cases: {TT(E.Cons,x1,E.Cons) >> B(true,Boolean)
B(false,Boolean)}
checkableType(Any): Any
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
removeVarEq vars: Set(V1)
enum unsealed (Any,class Any,false,false)
uniqued const: (Any,Any)
eq axioms for: E.Cons
excluded: List()
implied: List()
eq axioms for: null
excluded: List()
implied: List()
enum unsealed (Any,class Any,false,false)
eqAxioms:
pure:Not(And(Set(And(Set(Not(V1=null#1), V1=E.Cons#2)))))
Not(True)
removeVarEq vars: Set(V1)
eqAxioms:
pure:And(Set(And(Set(Not(V1=null#1), V1=E.Cons#2))))
True
reachability, vars:
V1: Any ::= E.Cons | null | ... // = x1
equality axioms:
And(Set())
DPLL
Lit#1 \/ Lit#-2
DPLL
enum unsealed (Any,class Any,false,false)
before CSE:
treeMakers:
TT(E.Cons,x1,E.Cons) >> B(true,Boolean)
B(false,Boolean) >>
checkableType(Any): Any
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
dependencies: Map(T7C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))) -> Set(Eq(V1,E.Cons)))
after CSE:
treeMakers:
TT(E.Cons,x1,E.Cons) >> B(true,Boolean)
B(false,Boolean) >>
def: (case <synthetic> val x1: Any = x$1,List(value x1),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: Any = x$1,class scala.reflect.internal.Trees$ValDef,List(value x1, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
def: (case5(){
if (x1.isInstanceOf[E.Cons])
matchEnd4(true)
else
case6()
},List(method case5),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (case5(){
if (x1.isInstanceOf[E.Cons])
matchEnd4(true)
else
case6()
},class scala.reflect.internal.Trees$LabelDef,List(method case5, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
def: (case6(){
matchEnd4(false)
},List(method case6),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (case6(){
matchEnd4(false)
},class scala.reflect.internal.Trees$LabelDef,List(method case6, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
def: (matchEnd4(x){
x
},List(method matchEnd4),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (matchEnd4(x){
x
},class scala.reflect.internal.Trees$LabelDef,List(method matchEnd4, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
translating {case E.this.SNil => 1
case (car: E.E, cdr: E.E)E.Cons(_, E.this.SNil) => 2
case (car: E.E, cdr: E.E)E.Cons(_, _) => 3}
TTTM(value x1,true,value x1,E.Cons,E.Cons)
changing val p3: <notype> to: E.E
changing val p4: <notype> to: E.E
TTTM(value x1,true,value x1,E.Cons,E.Cons)
changing val p6: <notype> to: E.E
changing val p7: <notype> to: E.E
combining cases: {ET(x1,E.this.SNil) >> B(1,Int)
TT(E.Cons,x1,E.Cons) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
TT(E.Cons,x1,E.Cons) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int)}
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
uniqued const: (E.SNil.type,SNil)
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
checkableType(E.E): E.E
removeVarEq vars: Set(V2, V1)
enum class E sealed, subclasses: List(class Cons, trait L, object SNil)
checkableType(E.Cons): E.Cons
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
enum sealed tp=E.E, tpApprox=E.E as: List(E.Cons, E.L, E.SNil.type)
uniqued const: (E.L,E.L)
unique const: (E.SNil.type,SNil)
uniqued const: (E.E,E.E)
eq axioms for: E.Cons
excluded: List(V2=null#7)
implied: List(V2=E.L#6)
eq axioms for: SNil
excluded: List(V2=null#7)
implied: List(V2=E.L#6)
eq axioms for: null
excluded: List(V2=E.L#6)
implied: List()
eq axioms for: E.L
excluded: List()
implied: List()
checkableType(E.Cons): E.Cons
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
unique const: (E.SNil.type,SNil)
enum unsealed (E.L,trait L,false,false)
eq axioms for: E.Cons
excluded: List()
implied: List()
eq axioms for: SNil
excluded: List()
implied: List()
eq axioms for: null
excluded: List()
implied: List()
enum unsealed (E.L,trait L,false,false)
eqAxioms:
Or(Set(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
Or(Set(Not(V2=E.Cons#5), V2=E.L#6))
Or(Set(Not(V2=SNil#4), V2=E.L#6))
AtMostOne(List(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
pure:Not(And(Set(V1=SNil#1)))
Not(And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2), V2=SNil#4)))
Not(And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2))))
removeVarEq vars: Set(V2, V1)
eqAxioms:
Or(Set(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
Or(Set(Not(V2=E.Cons#5), V2=E.L#6))
Or(Set(Not(V2=SNil#4), V2=E.L#6))
AtMostOne(List(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))
pure:And(Set(V1=SNil#1))
And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2), V2=SNil#4))
And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2)))
reachability, vars:
V1: E.L ::= E.Cons | SNil | null | ... // = x1
V2: E.E ::= E.Cons | E.L | SNil | null// Set(E.Cons, SNil, null, E.L) // = x1.cdr
equality axioms:
And(Set(Or(Set(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7)), Or(Set(Not(V2=E.Cons#5), V2=E.L#6)), Or(Set(Not(V2=SNil#4), V2=E.L#6)), AtMostOne(List(V2=E.Cons#5, V2=E.L#6, V2=SNil#4, V2=null#7))))
DPLL
Lit#1 \/ \/ \/ /\
Lit#-7 \/ \/ \/ /\
Lit#6 \/ Lit#2 \/ Lit#5 \/ Lit#4 /\
Lit#-5 \/ Lit#2 \/ \/ /\
Lit#-6 \/ Lit#2 \/ \/ /\
Lit#5 \/ \/ \/ /\
Lit#-6 \/ Lit#-2 \/ \/ /\
Lit#-6 \/ Lit#-5 \/ \/ /\
Lit#-6 \/ Lit#-4 \/ \/ /\
Lit#-2 \/ Lit#-5 \/ \/ /\
Lit#-2 \/ Lit#-4 \/ \/ /\
Lit#-5 \/ Lit#-4 \/ \/ /\
Lit#-3 \/ \/ \/
DPLL
Lit#-7 \/ \/ \/ /\
Lit#6 \/ Lit#2 \/ Lit#5 \/ Lit#4 /\
Lit#-5 \/ Lit#2 \/ \/ /\
Lit#-6 \/ Lit#2 \/ \/ /\
Lit#5 \/ \/ \/ /\
Lit#-6 \/ Lit#-2 \/ \/ /\
Lit#-6 \/ Lit#-5 \/ \/ /\
Lit#-6 \/ Lit#-4 \/ \/ /\
Lit#-2 \/ Lit#-5 \/ \/ /\
Lit#-2 \/ Lit#-4 \/ \/ /\
Lit#-5 \/ Lit#-4 \/ \/ /\
Lit#-3 \/ \/ \/
DPLL
Lit#6 \/ Lit#2 \/ Lit#5 \/ Lit#4 /\
Lit#-5 \/ Lit#2 \/ \/ /\
Lit#-6 \/ Lit#2 \/ \/ /\
Lit#5 \/ \/ \/ /\
Lit#-6 \/ Lit#-2 \/ \/ /\
Lit#-6 \/ Lit#-5 \/ \/ /\
Lit#-6 \/ Lit#-4 \/ \/ /\
Lit#-2 \/ Lit#-5 \/ \/ /\
Lit#-2 \/ Lit#-4 \/ \/ /\
Lit#-5 \/ Lit#-4 \/ \/ /\
Lit#-3 \/ \/ \/
DPLL
Lit#2 \/ /\
Lit#-6 \/ Lit#2 /\
Lit#-6 \/ Lit#-2 /\
Lit#-6 \/ /\
Lit#-6 \/ Lit#-4 /\
Lit#-2 \/ /\
Lit#-2 \/ Lit#-4 /\
Lit#-4 \/ /\
Lit#-3 \/
DPLL
Lit#-6 \/ /\
Lit#-6 \/ /\
Lit#-6 \/ Lit#-4 /\
\/ /\
Lit#-4 \/ /\
Lit#-4 \/ /\
Lit#-3 \/
todesking0.scala:9: warning: unreachable code
case Cons(_, SNil) => 2
^
enum unsealed (E.L,trait L,false,false)
before CSE:
treeMakers:
ET(x1,E.this.SNil) >> B(1,Int) >> >>
TT(E.Cons,x1,E.Cons) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
TT(E.Cons,x1,E.Cons) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int) >>
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
uniqued const: (E.SNil.type,SNil)
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
checkableType(E.E): E.E
dependencies: Map(T19C(Eq(V1,SNil)) -> Set(Eq(V1,SNil)), T21C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))) -> Set(Eq(V1,E.Cons)), T23C(Eq(V2,SNil)) -> Set(Eq(V2,SNil), Eq(V1,E.Cons)))
sharedPrefix: List(T25C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
suffix: List(T25C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
after CSE:
treeMakers:
ET(x1,E.this.SNil) >> B(1,Int) >> >>
Memo(x2,rc11,x1.isInstanceOf[E.Cons],(x1.asInstanceOf[E.Cons]: E.Cons),Substitution((x1,x2))) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
R(rc11,Substitution((x1,x2), (x5,x2))) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int) >>
def: (<synthetic> var rc11: Boolean = false,List(variable rc11),List(method foo, object E, package <empty>, package <root>))
untouched (<synthetic> var rc11: Boolean = false,class scala.reflect.internal.Trees$ValDef,List(variable rc11, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (<synthetic> var x2: E.Cons = null.asInstanceOf[E.Cons],List(variable x2),List(method foo, object E, package <empty>, package <root>))
untouched (<synthetic> var x2: E.Cons = null.asInstanceOf[E.Cons],class scala.reflect.internal.Trees$ValDef,List(variable x2, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case <synthetic> val x1: E.L = e,List(value x1),List(method foo, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: E.L = e,class scala.reflect.internal.Trees$ValDef,List(value x1, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case13(){
if (E.this.SNil.==(x1))
matchEnd12(1)
else
case14()
},List(method case13),List(method foo, object E, package <empty>, package <root>))
untouched (case13(){
if (E.this.SNil.==(x1))
matchEnd12(1)
else
case14()
},class scala.reflect.internal.Trees$LabelDef,List(method case13, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case14(){
if (x1.isInstanceOf[E.Cons])
{
rc11 = true;
x2 = (x1.asInstanceOf[E.Cons]: E.Cons);
{
<synthetic> val p4: E.E = x2.cdr;
if (E.this.SNil.==(p4))
matchEnd12(2)
else
case15()
}
}
else
case15()
},List(method case14),List(method foo, object E, package <empty>, package <root>))
untouched (case14(){
if (x1.isInstanceOf[E.Cons])
{
rc11 = true;
x2 = (x1.asInstanceOf[E.Cons]: E.Cons);
{
<synthetic> val p4: E.E = x2.cdr;
if (E.this.SNil.==(p4))
matchEnd12(2)
else
case15()
}
}
else
case15()
},class scala.reflect.internal.Trees$LabelDef,List(method case14, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (<synthetic> val p4: E.E = x2.cdr,List(value p4),List(method foo, object E, package <empty>, package <root>))
untouched (<synthetic> val p4: E.E = x2.cdr,class scala.reflect.internal.Trees$ValDef,List(value p4, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case15(){
if (rc11)
matchEnd12(3)
else
case16()
},List(method case15),List(method foo, object E, package <empty>, package <root>))
untouched (case15(){
if (rc11)
matchEnd12(3)
else
case16()
},class scala.reflect.internal.Trees$LabelDef,List(method case15, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case16(){
matchEnd12(throw new MatchError(x1))
},List(method case16),List(method foo, object E, package <empty>, package <root>))
untouched (case16(){
matchEnd12(throw new MatchError(x1))
},class scala.reflect.internal.Trees$LabelDef,List(method case16, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (matchEnd12(x){
x
},List(method matchEnd12),List(method foo, object E, package <empty>, package <root>))
untouched (matchEnd12(x){
x
},class scala.reflect.internal.Trees$LabelDef,List(method matchEnd12, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
one warning found
Java HotSpot(TM) 64-Bit Server VM
Raw
exhaustive0.scala
object E {
sealed abstract class E
trait L extends E
case object SNil extends L
case class Cons(car: E, cdr: E) extends L
def foo(e: L): Int = e match {
case SNil => 1
case Cons(_, SNil) => 2
case Cons(_, _) => 3
}
}
Raw
exhaustive1.log
translating {case _ => throw new IndexOutOfBoundsException(x$1.toString())}
combining cases: {B(throw new IndexOutOfBoundsException(x$1.toString()),Any)}
removeVarEq vars: Set()
eqAxioms:
pure:Not(True)
removeVarEq vars: Set()
eqAxioms:
pure:True
reachability, vars:
equality axioms:
And(Set())
enum unsealed (Int,class Int,false,true)
before CSE:
treeMakers:
B(throw new IndexOutOfBoundsException(x$1.toString()),Any)
dependencies: Map()
after CSE:
treeMakers:
B(throw new IndexOutOfBoundsException(x$1.toString()),Any)
def: (case <synthetic> val x1: Int = x$1,List(value x1),List(method productElement, object SNil, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: Int = x$1,class scala.reflect.internal.Trees$ValDef,List(value x1, method productElement, object SNil, object E, package <empty>, package <root>),List(method productElement, object SNil, object E, package <empty>, package <root>))
def: (case4(){
matchEnd3(throw new IndexOutOfBoundsException(x$1.toString()))
},List(method case4),List(method productElement, object SNil, object E, package <empty>, package <root>))
untouched (case4(){
matchEnd3(throw new IndexOutOfBoundsException(x$1.toString()))
},class scala.reflect.internal.Trees$LabelDef,List(method case4, method productElement, object SNil, object E, package <empty>, package <root>),List(method productElement, object SNil, object E, package <empty>, package <root>))
def: (matchEnd3(x){
x
},List(method matchEnd3),List(method productElement, object SNil, object E, package <empty>, package <root>))
untouched (matchEnd3(x){
x
},class scala.reflect.internal.Trees$LabelDef,List(method matchEnd3, method productElement, object SNil, object E, package <empty>, package <root>),List(method productElement, object SNil, object E, package <empty>, package <root>))
translating {case 0 => Cons.this.car
case 1 => Cons.this.cdr
case _ => throw new IndexOutOfBoundsException(x$1.toString())}
combining cases: {ET(x1,0) >> B(Cons.this.car,Any)
ET(x1,1) >> B(Cons.this.cdr,Any)
B(throw new IndexOutOfBoundsException(x$1.toString()),Any)}
def: (case <synthetic> val x1: Int = x$1,List(value x1),List(method productElement, class Cons, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: Int = x$1,class scala.reflect.internal.Trees$ValDef,List(value x1, method productElement, class Cons, object E, package <empty>, package <root>),List(method productElement, class Cons, object E, package <empty>, package <root>))
translating {case (_: E.Cons) => true
case _ => false}
TTTM(value x1,false,value x1,E.Cons,E.Cons)
combining cases: {TT(E.Cons,x1,E.Cons) >> B(true,Boolean)
B(false,Boolean)}
checkableType(Any): Any
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
removeVarEq vars: Set(V1)
enum unsealed (Any,class Any,false,false)
uniqued const: (Any,Any)
eq axioms for: E.Cons
excluded: List()
implied: List()
eq axioms for: null
excluded: List()
implied: List()
enum unsealed (Any,class Any,false,false)
eqAxioms:
pure:Not(And(Set(And(Set(Not(V1=null#1), V1=E.Cons#2)))))
Not(True)
removeVarEq vars: Set(V1)
eqAxioms:
pure:And(Set(And(Set(Not(V1=null#1), V1=E.Cons#2))))
True
reachability, vars:
V1: Any ::= E.Cons | null | ... // = x1
equality axioms:
And(Set())
DPLL
Lit#1 \/ Lit#-2
DPLL
enum unsealed (Any,class Any,false,false)
before CSE:
treeMakers:
TT(E.Cons,x1,E.Cons) >> B(true,Boolean)
B(false,Boolean) >>
checkableType(Any): Any
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
dependencies: Map(T7C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))) -> Set(Eq(V1,E.Cons)))
after CSE:
treeMakers:
TT(E.Cons,x1,E.Cons) >> B(true,Boolean)
B(false,Boolean) >>
def: (case <synthetic> val x1: Any = x$1,List(value x1),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: Any = x$1,class scala.reflect.internal.Trees$ValDef,List(value x1, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
def: (case5(){
if (x1.isInstanceOf[E.Cons])
matchEnd4(true)
else
case6()
},List(method case5),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (case5(){
if (x1.isInstanceOf[E.Cons])
matchEnd4(true)
else
case6()
},class scala.reflect.internal.Trees$LabelDef,List(method case5, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
def: (case6(){
matchEnd4(false)
},List(method case6),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (case6(){
matchEnd4(false)
},class scala.reflect.internal.Trees$LabelDef,List(method case6, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
def: (matchEnd4(x){
x
},List(method matchEnd4),List(method equals, class Cons, object E, package <empty>, package <root>))
untouched (matchEnd4(x){
x
},class scala.reflect.internal.Trees$LabelDef,List(method matchEnd4, method equals, class Cons, object E, package <empty>, package <root>),List(method equals, class Cons, object E, package <empty>, package <root>))
translating {case E.this.SNil => 1
case (car: E.E, cdr: E.E)E.Cons(_, E.this.SNil) => 2
case (car: E.E, cdr: E.E)E.Cons(_, _) => 3}
TTTM(value x1,true,value x1,E.Cons,E.Cons)
changing val p3: <notype> to: E.E
changing val p4: <notype> to: E.E
TTTM(value x1,true,value x1,E.Cons,E.Cons)
changing val p6: <notype> to: E.E
changing val p7: <notype> to: E.E
combining cases: {ET(x1,E.this.SNil) >> B(1,Int)
TT(E.Cons,x1,E.Cons) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
TT(E.Cons,x1,E.Cons) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int)}
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
uniqued const: (E.SNil.type,SNil)
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
checkableType(E.E): E.E
removeVarEq vars: Set(V2, V1)
enum class E sealed, subclasses: List(class Cons, object SNil)
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
enum sealed tp=E.E, tpApprox=E.E as: List(E.Cons, E.SNil.type)
unique const: (E.SNil.type,SNil)
uniqued const: (E.E,E.E)
eq axioms for: E.Cons
excluded: List(V2=null#6)
implied: List()
eq axioms for: SNil
excluded: List(V2=null#6)
implied: List()
eq axioms for: null
excluded: List()
implied: List()
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
unique const: (E.SNil.type,SNil)
enum trait L sealed, subclasses: List(class Cons, object SNil)
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
enum sealed tp=E.L, tpApprox=E.L as: List(E.Cons, E.SNil.type)
unique const: (E.SNil.type,SNil)
uniqued const: (E.L,E.L)
eq axioms for: E.Cons
excluded: List(V1=null#2)
implied: List()
eq axioms for: SNil
excluded: List(V1=null#2)
implied: List()
eq axioms for: null
excluded: List()
implied: List()
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
unique const: (E.SNil.type,SNil)
eqAxioms:
Or(Set(V2=E.Cons#5, V2=SNil#4, V2=null#6))
AtMostOne(List(V2=E.Cons#5, V2=SNil#4, V2=null#6))
Or(Set(V1=E.Cons#3, V1=SNil#1, V1=null#2))
AtMostOne(List(V1=E.Cons#3, V1=SNil#1, V1=null#2))
pure:Not(And(Set(V1=SNil#1)))
Not(And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2), V2=SNil#4)))
Not(And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2))))
removeVarEq vars: Set(V2, V1)
eqAxioms:
Or(Set(V2=E.Cons#5, V2=SNil#4, V2=null#6))
AtMostOne(List(V2=E.Cons#5, V2=SNil#4, V2=null#6))
Or(Set(V1=E.Cons#3, V1=SNil#1, V1=null#2))
AtMostOne(List(V1=E.Cons#3, V1=SNil#1, V1=null#2))
pure:And(Set(V1=SNil#1))
And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2), V2=SNil#4))
And(Set(And(Set(Not(V1=null#2), V1=E.Cons#3)), Not(V1=null#2)))
reachability, vars:
V1: E.L ::= E.Cons | SNil | null// Set(E.Cons, SNil, null) // = x1
V2: E.E ::= E.Cons | SNil | null// Set(E.Cons, SNil, null) // = x1.cdr
equality axioms:
And(Set(Or(Set(V2=E.Cons#5, V2=SNil#4, V2=null#6)), AtMostOne(List(V2=E.Cons#5, V2=SNil#4, V2=null#6)), Or(Set(V1=E.Cons#3, V1=SNil#1, V1=null#2)), AtMostOne(List(V1=E.Cons#3, V1=SNil#1, V1=null#2))))
DPLL
Lit#1 \/ \/ /\
Lit#-1 \/ Lit#-6 \/ /\
Lit#-1 \/ Lit#-2 \/ /\
Lit#-6 \/ Lit#-2 \/ /\
Lit#1 \/ Lit#6 \/ Lit#2 /\
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#-6 \/ \/ /\
Lit#4 \/ \/ /\
Lit#-2 \/ \/ /\
Lit#5 \/ Lit#4 \/ Lit#3
DPLL
Lit#-6 \/ \/ /\
Lit#-2 \/ \/ /\
Lit#-6 \/ Lit#-2 \/ /\
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#-6 \/ \/ /\
Lit#4 \/ \/ /\
Lit#-2 \/ \/ /\
Lit#5 \/ Lit#4 \/ Lit#3
DPLL
Lit#-2 \/ \/ /\
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#4 \/ \/ /\
Lit#-2 \/ \/ /\
Lit#5 \/ Lit#4 \/ Lit#3
DPLL
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#4 \/ \/ /\
Lit#5 \/ Lit#4 \/ Lit#3
DPLL
Lit#-5 \/ /\
Lit#-5 \/ Lit#-3 /\
Lit#-3 \/
DPLL
Lit#-3
DPLL
DPLL
Lit#-2 \/ \/ /\
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#-6 \/ \/ /\
Lit#1 \/ \/ /\
Lit#2 \/ Lit#-1 \/ Lit#-4 /\
Lit#-1 \/ Lit#-6 \/ /\
Lit#-1 \/ Lit#-2 \/ /\
Lit#-6 \/ Lit#-2 \/ /\
Lit#5 \/ Lit#4 \/ Lit#3 /\
Lit#1 \/ Lit#6 \/ Lit#2
DPLL
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#-6 \/ \/ /\
Lit#1 \/ \/ /\
Lit#-1 \/ Lit#-4 \/ /\
Lit#-1 \/ Lit#-6 \/ /\
Lit#5 \/ Lit#4 \/ Lit#3 /\
Lit#1 \/ Lit#6 \/
DPLL
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#1 \/ \/ /\
Lit#-1 \/ Lit#-4 \/ /\
Lit#5 \/ Lit#4 \/ Lit#3 /\
Lit#1 \/ \/
DPLL
Lit#-5 \/ Lit#-4 \/ /\
Lit#-5 \/ Lit#-3 \/ /\
Lit#-4 \/ Lit#-3 \/ /\
Lit#-4 \/ \/ /\
Lit#5 \/ Lit#4 \/ Lit#3
DPLL
Lit#-5 \/ Lit#-3 /\
Lit#5 \/ Lit#3
DPLL
Lit#-5 \/ Lit#-3 /\
Lit#5 \/ Lit#3 /\
Lit#-5 \/
DPLL
Lit#3
DPLL
enum trait L sealed, subclasses: List(class Cons, object SNil)
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
enum sealed tp=E.L, tpApprox=E.L as: List(E.Cons, E.SNil.type)
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
uniqued const: (E.SNil.type,SNil)
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
checkableType(E.E): E.E
analysing:
treeMakers:
ET(x1,E.this.SNil) >> B(1,Int) >> >>
TT(E.Cons,x1,E.Cons) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
TT(E.Cons,x1,E.Cons) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int) >>
removeVarEq vars: Set(V1, V2)
enum trait L sealed, subclasses: List(class Cons, object SNil)
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
enum sealed tp=E.L, tpApprox=E.L as: List(E.Cons, E.SNil.type)
unique const: (E.SNil.type,SNil)
uniqued const: (E.L,E.L)
eq axioms for: E.Cons
excluded: List()
implied: List()
eq axioms for: SNil
excluded: List()
implied: List()
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
unique const: (E.SNil.type,SNil)
enum class E sealed, subclasses: List(class Cons, object SNil)
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
enum sealed tp=E.E, tpApprox=E.E as: List(E.Cons, E.SNil.type)
unique const: (E.SNil.type,SNil)
uniqued const: (E.E,E.E)
eq axioms for: E.Cons
excluded: List()
implied: List()
eq axioms for: SNil
excluded: List()
implied: List()
checkableType(E.Cons): E.Cons
checkableType(E.SNil.type): E.SNil.type
unique const: (E.SNil.type,SNil)
eqAxioms:
Or(Set(V1=E.Cons#8, V1=SNil#7))
AtMostOne(List(V1=E.Cons#8, V1=SNil#7))
Or(Set(V2=E.Cons#10, V2=SNil#9))
AtMostOne(List(V2=E.Cons#10, V2=SNil#9))
pure:Not(Or(Set(And(Set(V1=SNil#7)), And(Set(And(Set(True, V1=E.Cons#8)), True, V2=SNil#9)), And(Set(And(Set(True, V1=E.Cons#8)), True)))))
find all models for
Lit#4 \/ Lit#3 /\
Lit#-3 \/ /\
Lit#-2 \/ Lit#-1 /\
Lit#2 \/ Lit#1 /\
Lit#-4 \/ Lit#-1 /\
Lit#-4 \/ Lit#-3 /\
Lit#-4 \/
find all models for
Lit#4 \/ Lit#3 /\
Lit#-3 \/ /\
Lit#-2 \/ Lit#-1 /\
Lit#2 \/ Lit#1 /\
Lit#-4 \/ Lit#-1 /\
Lit#-4 \/ Lit#-3 /\
Lit#-4 \/
DPLL
Lit#4 \/ Lit#3 /\
Lit#-3 \/ /\
Lit#-2 \/ Lit#-1 /\
Lit#2 \/ Lit#1 /\
Lit#-4 \/ Lit#-1 /\
Lit#-4 \/ Lit#-3 /\
Lit#-4 \/
DPLL
Lit#4 \/ /\
Lit#-2 \/ Lit#-1 /\
Lit#2 \/ Lit#1 /\
Lit#-4 \/ Lit#-1 /\
Lit#-4 \/
DPLL
Lit#-2 \/ Lit#-1 /\
Lit#2 \/ Lit#1 /\
Lit#-1 \/ /\
\/
before CSE:
treeMakers:
ET(x1,E.this.SNil) >> B(1,Int) >> >>
TT(E.Cons,x1,E.Cons) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
TT(E.Cons,x1,E.Cons) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int) >>
checkableType(E.L): E.L
checkableType(E.SNil.type): E.SNil.type
uniqued const: (E.SNil.type,SNil)
checkableType(E.Cons): E.Cons
uniqued const: (E.Cons,E.Cons)
checkableType(E.E): E.E
dependencies: Map(T28C(Eq(V1,SNil)) -> Set(Eq(V1,SNil)), T30C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))) -> Set(Eq(V1,E.Cons)), T32C(Eq(V2,SNil)) -> Set(Eq(V1,E.Cons), Eq(V2,SNil)))
sharedPrefix: List(T34C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
suffix: List(T34C(And(Set(Not(Eq(V1,null)), Eq(V1,E.Cons)))))
after CSE:
treeMakers:
ET(x1,E.this.SNil) >> B(1,Int) >> >>
Memo(x2,rc11,x1.isInstanceOf[E.Cons],(x1.asInstanceOf[E.Cons]: E.Cons),Substitution((x1,x2))) >> P(x2,,Substitution((p3,x2.car))) >> ET(p4,E.this.SNil) >> B(2,Int)
R(rc11,Substitution((x1,x2), (x5,x2))) >> P(x5,,Substitution((p6,x5.car), (p7,x5.cdr))) >> B(3,Int) >>
def: (<synthetic> var rc11: Boolean = false,List(variable rc11),List(method foo, object E, package <empty>, package <root>))
untouched (<synthetic> var rc11: Boolean = false,class scala.reflect.internal.Trees$ValDef,List(variable rc11, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (<synthetic> var x2: E.Cons = null.asInstanceOf[E.Cons],List(variable x2),List(method foo, object E, package <empty>, package <root>))
untouched (<synthetic> var x2: E.Cons = null.asInstanceOf[E.Cons],class scala.reflect.internal.Trees$ValDef,List(variable x2, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case <synthetic> val x1: E.L = e,List(value x1),List(method foo, object E, package <empty>, package <root>))
untouched (case <synthetic> val x1: E.L = e,class scala.reflect.internal.Trees$ValDef,List(value x1, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case13(){
if (E.this.SNil.==(x1))
matchEnd12(1)
else
case14()
},List(method case13),List(method foo, object E, package <empty>, package <root>))
untouched (case13(){
if (E.this.SNil.==(x1))
matchEnd12(1)
else
case14()
},class scala.reflect.internal.Trees$LabelDef,List(method case13, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case14(){
if (x1.isInstanceOf[E.Cons])
{
rc11 = true;
x2 = (x1.asInstanceOf[E.Cons]: E.Cons);
{
<synthetic> val p4: E.E = x2.cdr;
if (E.this.SNil.==(p4))
matchEnd12(2)
else
case15()
}
}
else
case15()
},List(method case14),List(method foo, object E, package <empty>, package <root>))
untouched (case14(){
if (x1.isInstanceOf[E.Cons])
{
rc11 = true;
x2 = (x1.asInstanceOf[E.Cons]: E.Cons);
{
<synthetic> val p4: E.E = x2.cdr;
if (E.this.SNil.==(p4))
matchEnd12(2)
else
case15()
}
}
else
case15()
},class scala.reflect.internal.Trees$LabelDef,List(method case14, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (<synthetic> val p4: E.E = x2.cdr,List(value p4),List(method foo, object E, package <empty>, package <root>))
untouched (<synthetic> val p4: E.E = x2.cdr,class scala.reflect.internal.Trees$ValDef,List(value p4, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case15(){
if (rc11)
matchEnd12(3)
else
case16()
},List(method case15),List(method foo, object E, package <empty>, package <root>))
untouched (case15(){
if (rc11)
matchEnd12(3)
else
case16()
},class scala.reflect.internal.Trees$LabelDef,List(method case15, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (case16(){
matchEnd12(throw new MatchError(x1))
},List(method case16),List(method foo, object E, package <empty>, package <root>))
untouched (case16(){
matchEnd12(throw new MatchError(x1))
},class scala.reflect.internal.Trees$LabelDef,List(method case16, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
def: (matchEnd12(x){
x
},List(method matchEnd12),List(method foo, object E, package <empty>, package <root>))
untouched (matchEnd12(x){
x
},class scala.reflect.internal.Trees$LabelDef,List(method matchEnd12, method foo, object E, package <empty>, package <root>),List(method foo, object E, package <empty>, package <root>))
Java HotSpot(TM) 64-Bit Server VM warning: ignoring option MaxPermSize=512M; support was removed in 8.0
Raw
exhaustive1.scala
object E {
sealed abstract class E
sealed trait L extends E
case object SNil extends L
case class Cons(car: E, cdr: E) extends L
def foo(e: L): Int = e match {
case SNil => 1
case Cons(_, SNil) => 2
case Cons(_, _) => 3
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment