diff --git a/src/multisets/Main.scala b/src/multisets/Main.scala index 254b33c466698f84927e6ecef4e1b6a3e4502b67..3da74362d84ccc9d7bc38ba4bb24b0aee393a0e0 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 91ac3df336a9ed28d9c95ffe018f14e0662cd609..ede3dba52801df5de5803f2f22302c7f6502e944 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 d8e930b71d9894fd9c1dbcaea3872ed7a710fe2b..d940dd70f7ceda09242457555ece0fff85514a38 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 0a3732fde7ac3575019918ef32605c55d9b6b202..99c0cf8b8301fb0fa0f658d2701790d414921e9a 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) {