From be404ffceabde9c6cffaa5bf5efb09f5e266a451 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Mon, 23 May 2011 08:29:39 +0000
Subject: [PATCH] move code around
---
src/purescala/FairZ3Solver.scala | 96 ++++++++++++++++----------------
1 file changed, 48 insertions(+), 48 deletions(-)
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index c93a7f7ea..4822702df 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/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}
--
GitLab