First Set involving program verified!

src/orderedsets/Main.scala

 package orderedsets
 
 import purescala.Reporter
+import Phase3._
+import Reconstruction._
 import purescala.TypeTrees._
 import purescala.Common._
 import purescala.Extensions._
@@ -14,7 +16,7 @@ class Main(reporter: Reporter) extends Solver(reporter) {
     // TODO: Use id.getType as Symbol's type, this _has_ to be a set variable
     case Variable(id) if id.getType == SetType(Int32Type) => Symbol(id.name, Symbol.SetType) 
     case EmptySet(_) => AST.emptyset
-    case FiniteSet(elems) => { reporter.error(expr, "TODO!"); error("TODO!") }
+    case FiniteSet(elems) => AST.Op(UNION, ( elems map convertToIntTerm map {_.singleton} ).toList)
     case SetCardinality(set) => convertToSetTerm(set).card
     case SetIntersection(set1, set2) => convertToSetTerm(set1) ** convertToSetTerm(set2)
     case SetUnion(set1, set2) => convertToSetTerm(set1) ++ convertToSetTerm(set2)
@@ -36,6 +38,7 @@ class Main(reporter: Reporter) extends Solver(reporter) {
     // TODO: Throwing own exception here?
     case Division(_, _) => reporter.error(expr, "Division is not supported."); error("Division is not supported.")
     case UMinus(e) => AST.zero - convertToIntTerm(e)
+    case SetCardinality(e) => convertToSetTerm(e).card
     case _ => reporter.error(expr, "Not an integer expression!"); error("Not an integer expression.")
   }
 
@@ -69,16 +72,73 @@ class Main(reporter: Reporter) extends Solver(reporter) {
     case _ => reporter.error(expr, "Cannot be handled by Ordered BAPA."); error("Cannot be handled")
   }
 
+  var allModels: Set[ReconstructedValues] = Set()
+  var outSetVars: Set[Symbol] = null
+  var outIntVars: Set[Symbol] = null
+
+  def callZ3(z3: MyZ3Context, paForm: AST.Formula, eq: List[EquiClass]): Phase2.Hint = {
+
+    z3.push
+    z3.impose(paForm)
+
+    val result = z3.getModel match {
+      case s@Sat(deleteModel, bools, ints) => {
+        reporter.info("Formula satisfiable")
+        allModels += Reconstruction.getReconstruction(s, outSetVars.toList, outIntVars.toList, eq)
+        deleteModel()
+        true
+      }
+      case Unsat => reporter.info("Formula unsatisfiable"); false
+      case Z3Failure(e) => error("Z3 not executed.  " + e);
+    }
+    z3.pop
+    result
+  }
+
   // checks for V-A-L-I-D-I-T-Y !
   // Some(true) means formula is valid (negation is unsat)
   // None means you don't know.
   def solve(expr: Expr) : Option[Boolean] = {
     try {
-      reporter.info("OrdBAPA conversion = " + convertToAST(expr).toString)
+      val form = NormalForms.nnf(convertToAST(expr))
+      outIntVars = ASTUtil.intvars(form)
+      outSetVars = ASTUtil.setvars(form)
+
+      reporter.info("OrdBAPA conversion = " + form.toString)
+      val start = System.nanoTime
+      for (conj <- NormalForms(!form)) {
+        //println("Conjunction:")
+        //conj.print
+        try {
+            Phase2(Phase3.segment(callZ3))(conj)
+        } catch {
+          case Phase2.UnsatException(msg) =>
+            reporter.error("  " + msg)
+        }
+      }
+      val end = System.nanoTime
+      var toReturn : Boolean = false
+      val total = ((end - start) / 1000000) / 1000.0
+      if (!allModels.isEmpty) {
+        reporter.info("Models after reconstruction:")
+        toReturn = true
+      } else {
+        toReturn = false
+      }
+        
+      for (ReconstructedValues(intMap, setMap) <- allModels) {
+
+        intMap.toList.sortWith {_._1.name < _._1.name}.foreach(x => reporter.info("\t\t " + x._1.toString + " -> " + x._2))
+        setMap.toList.sortWith {_._1.name < _._1.name}.foreach(x => reporter.info("\t\t " + x._1.toString + " -> " + x._2.toList.sortWith {_ < _}.mkString("Set { ", ", ", " }")))
+      }
+
+      reporter.info("Total time : " + total)
+      Some(!toReturn)
     } catch {
-      case e => reporter.info(e.toString)
+      case e => 
+        reporter.info("OrdBAPA exception = " + e.toString)
+        reporter.info(expr, "OrdBAPA has no idea how to solve this :(")
+        None
     }
-    reporter.info(expr, "I have no idea how to solve this :(")
-    None
   }
 }

src/orderedsets/Phase3.scala

@@ -110,8 +110,8 @@ object Phase3 {
       equiCls.allSets = Some(setvars(nnfForm).toList)
       continuationZ3call(z3, paFormula && paForm, List(equiCls))
     } else {
-      println
-      println("Order " + orderCount + "      " + Phase2.order2string(order))
+      // println
+      // println("Order " + orderCount + "      " + Phase2.order2string(order))
 
       val classes = new ArrayBuffer[EquiClass]
       val sets = new MutableSet[Symbol]

src/orderedsets/Z3LibConverter.scala

@@ -70,8 +70,9 @@ class MyZ3Context {
   }
 
   def impose(form: Formula) {
-    debug_stack.head += form
-    z3.assertCnstr(mkAST(form))
+    val nnfForm = NormalForms.nnf( form )
+    debug_stack.head += nnfForm
+    z3.assertCnstr(mkAST(nnfForm))
   }
 
   def push {

testcases/SetOperations.scala

@@ -7,5 +7,5 @@ object SetOperations {
     def add(a: Set[Int], b: Int) : Set[Int] = {
         require(a.size >= 0)
         a ++ Set(b)
-    } ensuring((x:Set[Int]) => x.size == a.size + 1)
+      } ensuring((x:Set[Int]) => x.size >= a.size)
 }