From 8679204a13b1f9135ef778abdb3b20db2ac53194 Mon Sep 17 00:00:00 2001
From: Utkarsh Upadhyay <musically.ut@gmail.com>
Date: Mon, 12 Jul 2010 18:16:17 +0000
Subject: [PATCH] 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 | 2 +-
src/orderedsets/UnifierMain.scala | 30 ++++++++++++++++++++----------
src/purescala/Extensions.scala | 2 +-
testcases/BinarySearchTree.scala | 10 ++++++----
4 files changed, 28 insertions(+), 16 deletions(-)
diff --git a/src/orderedsets/Main.scala b/src/orderedsets/Main.scala
index 187d077f0..e20188413 100644
--- a/src/orderedsets/Main.scala
+++ b/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)
}
}
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index f51e4a7fc..099d306ac 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/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.")
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index a7744567f..0a3732fde 100644
--- a/src/purescala/Extensions.scala
+++ b/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) {
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index c2e4566f4..859a5eb29 100644
--- a/testcases/BinarySearchTree.scala
+++ b/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)
--
GitLab