From 3356211a71d83230fcf500b1983c895afe97999b Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 12 Jul 2010 21:46:52 +0000
Subject: [PATCH]
---
src/multisets/Main.scala | 1 +
src/orderedsets/UnifierMain.scala | 1 +
src/purescala/Analysis.scala | 29 ++++++++++++++++++-----------
src/purescala/Extensions.scala | 1 +
4 files changed, 21 insertions(+), 11 deletions(-)
diff --git a/src/multisets/Main.scala b/src/multisets/Main.scala
index 254b33c46..3da74362d 100644
--- a/src/multisets/Main.scala
+++ b/src/multisets/Main.scala
@@ -6,6 +6,7 @@ import purescala.Trees._
class Main(reporter: Reporter) extends Solver(reporter) {
val description = "Multiset Solver"
+ override def shortDescription = "MUNCH"
def solve(expr: Expr) : Option[Boolean] = {
reporter.info("Don't know how to solve anything.")
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index 91ac3df33..ede3dba52 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/src/orderedsets/UnifierMain.scala
@@ -22,6 +22,7 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
val description = "Unifier for ADTs with abstractions"
override val shortDescription = "Unifier"
+ override def superseeds = List("BAPA<", "MUNCH")
var program: Program = null
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index d8e930b71..d940dd70f 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -61,19 +61,26 @@ class Analysis(val program: Program) {
// reporter.info(exp)
// try all solvers until one returns a meaningful answer
+ var superseeded : Set[String] = Set.empty[String]
solverExtensions.find(se => {
reporter.info("Trying with solver: " + se.shortDescription)
- se.solve(vc) match {
- case None => false
- case Some(true) => {
- reporter.info("==== VALID ====")
- verifiedVCs = (funDef.id.toString, "postcondition", "valid", se.shortDescription) :: verifiedVCs
- true
- }
- case Some(false) => {
- reporter.error("==== INVALID ====")
- verifiedVCs = (funDef.id.toString, "postcondition", "invalid", se.shortDescription) :: verifiedVCs
- true
+ if(superseeded(se.shortDescription) || superseeded(se.description)) {
+ reporter.info("Solver was superseeded. Skipping.")
+ false
+ } else {
+ superseeded = superseeded ++ Set(se.superseeds: _*)
+ se.solve(vc) match {
+ case None => false
+ case Some(true) => {
+ reporter.info("==== VALID ====")
+ verifiedVCs = (funDef.id.toString, "postcondition", "valid", se.shortDescription) :: verifiedVCs
+ true
+ }
+ case Some(false) => {
+ reporter.error("==== INVALID ====")
+ verifiedVCs = (funDef.id.toString, "postcondition", "invalid", se.shortDescription) :: verifiedVCs
+ true
+ }
}
}
}) match {
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index 0a3732fde..99c0cf8b8 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -20,6 +20,7 @@ object Extensions {
def solve(expression: Expr) : Option[Boolean]
def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
+ def superseeds : Seq[String] = Nil
}
abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
--
GitLab