No commit message

No commit message

src/funcheck/CodeExtraction.scala

@@ -109,9 +109,9 @@ trait CodeExtraction extends Extractors {
 
       scalaClassSyms.foreach(p => {
           if(p._1.isAbstractClass) {
-            classesToClasses += (p._1 -> new AbstractClassDef(p._2, None))
+            classesToClasses += (p._1 -> new AbstractClassDef(p._2))
           } else if(p._1.isCase) {
-            classesToClasses += (p._1 -> new CaseClassDef(p._2, None))
+            classesToClasses += (p._1 -> new CaseClassDef(p._2))
           }
       })
 
@@ -132,7 +132,7 @@ trait CodeExtraction extends Extractors {
         }
 
         if(superAC.length == 1) {
-            p._2.parent = Some(superAC.head)
+            p._2.setParent(superAC.head)
         }
 
         if(p._2.isInstanceOf[CaseClassDef]) {

src/purescala/Definitions.scala

@@ -38,14 +38,24 @@ object Definitions {
   /** Objects work as containers for class definitions, functions (def's) and
    * val's. */
   case class ObjectDef(id: Identifier, defs : Seq[Definition], invariants: Seq[Expr]) extends Definition {
-    def getDefinedClasses : Seq[ClassTypeDef] = defs.filter(_.isInstanceOf[ClassTypeDef]).map(_.asInstanceOf[ClassTypeDef])
+    // Watch out ! Use only when object is completely built !
+    lazy val getDefinedClasses = computeDefinedClasses
+    // ...this one can be used safely at anytime.
+    def computeDefinedClasses : Seq[ClassTypeDef] = defs.filter(_.isInstanceOf[ClassTypeDef]).map(_.asInstanceOf[ClassTypeDef])
+
+    lazy val getClassHierarchyRoots = computeClassHierarchyRoots
+    def computeClassHierarchyRoots : Seq[ClassTypeDef] = defs.filter(_.isInstanceOf[ClassTypeDef]).map(_.asInstanceOf[ClassTypeDef]).filter(!_.hasParent)
   }
 
   /** Useful because case classes and classes are somewhat unified in some
    * patterns (of pattern-matching, that is) */
   sealed trait ClassTypeDef extends Definition {
+    self =>
+
     val id: Identifier
-    var parent: Option[AbstractClassDef]
+    def parent: Option[AbstractClassDef]
+    def setParent(parent: AbstractClassDef) : self.type
+    def hasParent: Boolean = parent.isDefined
     val isAbstract: Boolean
     // val fields: VarDecls
   }
@@ -60,9 +70,37 @@ object Definitions {
       if(acd == null) None else Some((acd.id, acd.parent))
     }
   }
-  class AbstractClassDef(val id: Identifier, var parent: Option[AbstractClassDef]) extends ClassTypeDef {
+  class AbstractClassDef(val id: Identifier, prnt: Option[AbstractClassDef] = None) extends ClassTypeDef {
+    private var parent_ = prnt
     var fields: VarDecls = Nil
     val isAbstract = true
+
+    private var children : List[ClassTypeDef] = Nil
+
+    private[purescala] def registerChild(child: ClassTypeDef) : Unit = {
+      children = child :: children
+    }
+
+    def knownChildren : Seq[ClassTypeDef] = {
+      children
+    }
+
+    def knownDescendents : Seq[ClassTypeDef] = {
+      knownChildren ++ (knownChildren.map(c => c match {
+        case acd: AbstractClassDef => acd.knownDescendents
+        case _ => Nil
+      }).reduceLeft(_ ++ _))
+    }
+
+    def setParent(newParent: AbstractClassDef) = {
+      if(parent_.isDefined) {
+        scala.Predef.error("Resetting parent is forbidden.")
+      }
+      newParent.registerChild(this)
+      parent_ = Some(newParent)
+      this
+    }
+    def parent = parent_
   }
 
   /** Case classes. */
@@ -71,9 +109,21 @@ object Definitions {
       if(ccd == null) None else Some((ccd.id, ccd.parent, ccd.fields))
     }
   }
-  class CaseClassDef(val id: Identifier, var parent: Option[AbstractClassDef]) extends ClassTypeDef with ExtractorTypeDef {
+
+  class CaseClassDef(val id: Identifier, prnt: Option[AbstractClassDef] = None) extends ClassTypeDef with ExtractorTypeDef {
+    private var parent_ = prnt
     var fields: VarDecls = Nil
     val isAbstract = false
+
+    def setParent(newParent: AbstractClassDef) = {
+      if(parent_.isDefined) {
+        scala.Predef.error("Resetting parent is forbidden.")
+      }
+      newParent.registerChild(this)
+      parent_ = Some(newParent)
+      this
+    }
+    def parent = parent_
   }
 
   /** "Regular" classes */

src/purescala/Z3Solver.scala

@@ -12,12 +12,12 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
   override val shortDescription = "Z3"
 
   // this is fixed
-  val z3cfg = new Z3Config()
+  private val z3cfg = new Z3Config()
   z3cfg.setParamValue("MODEL", "true")
 
   // we restart Z3 for each new program
-  var z3: Z3Context = null
-  var program: Program = null
+  private var z3: Z3Context = null
+  private var program: Program = null
   private var neverInitialized = true
 
   override def setProgram(prog: Program) : Unit = {
@@ -32,14 +32,27 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
     prepareSorts
   }
 
-  var intSort : Z3Sort  = null
-  var boolSort : Z3Sort = null
+  private var intSort : Z3Sort  = null
+  private var boolSort : Z3Sort = null
 
-  def prepareSorts : Unit = {
+  private def prepareSorts : Unit = {
+    // NOTE THAT abstract classes that extend abstract classes are not
+    // currently supported in the translation
     intSort  = z3.mkIntSort
     boolSort = z3.mkBoolSort
 
-    val classDefs = program.mainObject.getDefinedClasses
+    val roots = program.mainObject.getClassHierarchyRoots
+    val indexMap: Map[ClassTypeDef,Int] = Map(roots.zipWithIndex: _*)
+    println("indexMap: " + indexMap)
+    val childrenLists: Seq[List[CaseClassDef]] = roots.map(_ match {
+      case c: CaseClassDef => Nil
+      case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList
+    })
+    println("children lists: " + childrenLists.toList.mkString("\n"))
+
+    //val caseClassRoots = roots.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef])
+    //val absClassRoots  = roots.filter(_.isInstanceOf[AbstractClassDef]).map(_.asInstanceOf[AbstractClassDef])
+
 
     // Abstract classes with no subclasses.. do we care? :)
     //  - we can build an uninterpreted type for them.

testcases/BinarySearchTree.scala

@@ -5,6 +5,8 @@ object BinarySearchTree {
     case class Node(left: Tree, value: Int, right: Tree) extends Tree
     case class Leaf() extends Tree
 
+    case class IntWrapper(value: Int)
+
     def emptySet() : Tree = Leaf()
 
     def insert(tree: Tree, value: Int) : Node = (tree match {