From d3f14b3153e766c0c5c54718130b654cd3bbe6c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 27 Apr 2012 00:05:51 +0000
Subject: [PATCH] Better return results when it is impossible to compute the
model
---
src/main/scala/leon/Evaluator.scala | 8 ++++----
src/main/scala/leon/FairZ3Solver.scala | 4 ++--
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 6bb9ef1b3..e8409aa31 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -24,7 +24,7 @@ object Evaluator {
case class InfiniteComputation() extends EvaluationResult {
val finalResult = None
}
- case class PostconditionViolationFunctionFromModel() extends EvaluationResult {
+ case class ImpossibleComputation() extends EvaluationResult {
val finalResult = None
}
@@ -33,7 +33,7 @@ object Evaluator {
case class RuntimeErrorEx(msg: String) extends Exception
case class InfiniteComputationEx() extends Exception
case class TypeErrorEx(typeError: TypeError) extends Exception
- case class PostconditionViolationFunctionFromModelEx() extends Exception
+ case class ImpossibleComputationEx() extends Exception
var left: Int = maxSteps
@@ -101,7 +101,7 @@ object Evaluator {
val postBody = replace(Map(ResultVariable() -> Variable(freshResID)), matchToIfThenElse(fd.postcondition.get))
rec(frame + ((freshResID -> callResult)), postBody) match {
case BooleanLiteral(true) => ;
- case BooleanLiteral(false) if !fd.hasImplementation => throw PostconditionViolationFunctionFromModelEx()
+ case BooleanLiteral(false) if !fd.hasImplementation => throw ImpossibleComputationEx()
case BooleanLiteral(false) => throw RuntimeErrorEx("Postcondition violation for " + fd.id.name + " reached in evaluation.")
case other => throw TypeErrorEx(TypeError(other, BooleanType))
}
@@ -313,7 +313,7 @@ object Evaluator {
case RuntimeErrorEx(msg) => RuntimeError(msg)
case InfiniteComputationEx() => InfiniteComputation()
case TypeErrorEx(te) => te
- case PostconditionViolationFunctionFromModelEx() => PostconditionViolationFunctionFromModel()
+ case ImpossibleComputationEx() => ImpossibleComputation()
}
}
}
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index ebca10ab2..919b5b4f9 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -827,8 +827,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info("- Invalid model.")
(false, asMap)
}
- case PostconditionViolationFunctionFromModel() => {
- reporter.info("- Invalid Model: postcondition violation of a function that whose implementation was specified by the model")
+ case ImpossibleComputation() => {
+ reporter.info("- Invalid Model: the model could not be verified because of insufficient information.")
(false, asMap)
}
case other => {
--
GitLab