move code around

src/purescala/FairZ3Solver.scala

@@ -38,54 +38,6 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   private var toCheckAgainstModels: Expr = BooleanLiteral(true)
   private var varsInVC: Set[Identifier] = Set.empty
 
-  private val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
-  private val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
-  private val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
-  private val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
-  private val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
-  private val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
-
-  private def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
-    case Some(z3sort) => z3sort
-    case None => {
-      import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
-      intSort = z3.mkIntSort
-      boolSort = z3.mkBoolSort
-
-      def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
-        case BooleanType => RegularSort(boolSort)
-        case Int32Type => RegularSort(intSort)
-        case AbstractClassType(d) => RegularSort(adtSorts(d))
-        case CaseClassType(d) => RegularSort(adtSorts(d))
-        case _ => throw UntranslatableTypeException("Can't handle type " + tt)
-      }
-
-      val z3info = z3.mkADTSorts(
-        Seq(
-          (
-            toType.toString + "Option",
-            Seq(toType.toString + "Some", toType.toString + "None"),
-            Seq(
-              Seq(("value", typeToSortRef(toType))),
-              Seq()
-            )
-          )
-        )
-      )
-
-      z3info match {
-        case Seq((optionSort, Seq(someCons, noneCons), Seq(someTester, noneTester), Seq(Seq(valueSelector), Seq()))) =>
-          mapRangeSorts += ((toType, optionSort))
-          mapRangeSomeConstructors += ((toType, someCons))
-          mapRangeNoneConstructors += ((toType, noneCons))
-          mapRangeSomeTesters += ((toType, someTester))
-          mapRangeNoneTesters += ((toType, noneTester))
-          mapRangeValueSelectors += ((toType, valueSelector))
-          optionSort
-      }
-    }
-  }
-
   override def setProgram(prog: Program): Unit = {
     program = prog
   }
@@ -148,6 +100,54 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
   private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
 
+  private val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
+  private val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+  private val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+  private val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+  private val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+  private val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+
+  private def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
+    case Some(z3sort) => z3sort
+    case None => {
+      import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
+      intSort = z3.mkIntSort
+      boolSort = z3.mkBoolSort
+
+      def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
+        case BooleanType => RegularSort(boolSort)
+        case Int32Type => RegularSort(intSort)
+        case AbstractClassType(d) => RegularSort(adtSorts(d))
+        case CaseClassType(d) => RegularSort(adtSorts(d))
+        case _ => throw UntranslatableTypeException("Can't handle type " + tt)
+      }
+
+      val z3info = z3.mkADTSorts(
+        Seq(
+          (
+            toType.toString + "Option",
+            Seq(toType.toString + "Some", toType.toString + "None"),
+            Seq(
+              Seq(("value", typeToSortRef(toType))),
+              Seq()
+            )
+          )
+        )
+      )
+
+      z3info match {
+        case Seq((optionSort, Seq(someCons, noneCons), Seq(someTester, noneTester), Seq(Seq(valueSelector), Seq()))) =>
+          mapRangeSorts += ((toType, optionSort))
+          mapRangeSomeConstructors += ((toType, someCons))
+          mapRangeNoneConstructors += ((toType, noneCons))
+          mapRangeSomeTesters += ((toType, someTester))
+          mapRangeNoneTesters += ((toType, noneTester))
+          mapRangeValueSelectors += ((toType, valueSelector))
+          optionSort
+      }
+    }
+  }
+
   case class UntranslatableTypeException(msg: String) extends Exception(msg)
   private def prepareSorts: Unit = {
     import Z3Context.{ADTSortReference, RecursiveType, RegularSort}