Changelist:

1. Added isUnsat to Extensions.scala
2. Added a few more conditions to BinarySearchTree.scala
3. Made calls to underlying solvers (involving double negation, etc) from the unifier
4. Fixed a minor bug in Expression Parsing in Main.scala

src/orderedsets/Main.scala

@@ -208,7 +208,7 @@ object ExprToASTConverter {
     formulaRelaxed = false;
     expr match {
       case And(exprs) => AST.And((exprs map toRelaxedFormula).toList)
-      case _ => toFormula(expr)
+      case _ => toRelaxedFormula(expr)
     }
   }
 

src/orderedsets/UnifierMain.scala

@@ -50,14 +50,9 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
           val (varMap, restFormula) = solve(conjunction)
           // TODO: Might contain multiple c_i ~= {} for a fixed i
           val noAlphas = And(restFormula flatMap expandAlphas(varMap))
-          //reporter.info("The resulting formula is\n" + rpp(noAlphas))
-          // OrdBAPA finds the formula satisfiable
-          if ((new Main(reporter)).solve(ExprToASTConverter(noAlphas))) {
-            throw (new SatException(null))
-          } else {
-            reporter.info("Conjunction " + counter + " is UNSAT, proved by BAPA<")
-          }
-        } catch {
+          reporter.info("The resulting formula is\n" + rpp(noAlphas))
+          tryAllSolvers(noAlphas)
+          } catch {
           case ex@ConversionException(badExpr, msg) =>
             reporter.info("Conjunction " + counter + " is UNKNOWN, could not be parsed")
             throw ex
@@ -68,7 +63,7 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
           case UnificationImpossible(msg) =>
             reporter.info("Conjunction " + counter + " is UNSAT, proved by Unifier") // (" + msg + ")")
           case ex@SatException(_) =>
-            reporter.info("Conjunction " + counter + " is SAT, proved by BAPA<")
+            reporter.info("Conjunction " + counter + " is SAT")
             throw ex
         }
       }
@@ -93,6 +88,21 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
     }
   }
 
+  def tryAllSolvers(f : Expr): Unit = {
+    for(solver <- Extensions.loadedSolverExtensions; if solver != this) {
+          reporter.info("Trying solver: " + solver.shortDescription + " from inside the unifier.")
+          solver.isUnsat(f) match {
+            case Some(true) => 
+                reporter.info("Solver: " + solver.shortDescription + " proved the formula unsatisfiable") 
+                return
+            case Some(false) => 
+                reporter.warning("Solver: " + solver.shortDescription + " proved the formula satisfiable")
+                throw (new SatException(null))
+            case None =>
+                reporter.info("Solver: " + solver.shortDescription + " was unable to conclusively determine the correctness of the formula") 
+          }
+    }; throw IncompleteException("All the solvers were unable to prove the formula unsatisfiable, giving up.") }
+
   def checkIsSupported(expr: Expr) {
     def check(ex: Expr): Option[Expr] = ex match {
       case Let(_, _, _) | MatchExpr(_, _) =>
@@ -229,7 +239,7 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
           //reporter.warning("Result:\n" + rpp(res))
           Some(res)
         }
-        case _ => error("Bad argument/substitution to catamorphism")
+        case _ => error("Bad argument/substitution to catamorphism: " + substArg(arg))
       }
       case None => // Not a catamorphism
         warning("Function " + fd.id + " is not a catamorphism.")

src/purescala/Extensions.scala

@@ -19,7 +19,7 @@ object Extensions {
     // None if unknown.
     def solve(expression: Expr) : Option[Boolean]
 
-    def isSat(expression: Expr) : Option[Boolean] = solve(expression).map(!_)
+    def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
   }
   
   abstract class Analyser(reporter: Reporter) extends Extension(reporter) {

testcases/BinarySearchTree.scala

@@ -57,22 +57,24 @@ object BinarySearchTree {
     }
   
 
-  def treeMin(tree: Node): Int = tree match {
+  def treeMin(tree: Node): Int = {
+    require(isSorted(tree).sorted)
+    tree match {
     case Node(left, v, _) => left match {
       case Leaf() => v
       case n@Node(_, _, _) => treeMin(n)
     }
-  }
+  }} ensuring (_ == contents(tree).min)
 
   def treeMax(tree: Node): Int = {
-    // requires(isSorted(tree))
+    require(isSorted(tree).sorted)
     tree match {
       case Node(_, v, right) => right match {
         case Leaf() => v
         case n@Node(_, _, _) => treeMax(n)
       }
     }
-  } //ensuring (_ == contents(tree).max)
+  } ensuring (_ == contents(tree).max)
 
   def insert(tree: Tree, value: Int): Node = {
     require(isSorted(tree).sorted)