From 4724ce5d2d6b7e9889815e35337aaf9b765e570f Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 18 Nov 2010 17:13:34 +0000
Subject: [PATCH] support for div
---
src/purescala/Analysis.scala | 4 ++--
src/purescala/DefaultTactic.scala | 6 +++---
src/purescala/Z3Solver.scala | 8 ++++++++
3 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index c29a2b19e..2c62fb5d4 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -82,9 +82,9 @@ class Analysis(val program: Program) {
val vc = vcInfo.condition
reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
- // reporter.info("Verification condition (post) for ==== " + funDef.id + " ====")
+ reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
// if(Settings.unrollingLevel == 0) {
- // reporter.info(simplifyLets(vc))
+ reporter.info(simplifyLets(vc))
// } else {
// reporter.info("(not showing unrolled VCs)")
// }
diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala
index b7e586a39..5b16ad4ea 100644
--- a/src/purescala/DefaultTactic.scala
+++ b/src/purescala/DefaultTactic.scala
@@ -77,7 +77,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
expr2
}
}
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this))
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
}
}
@@ -110,7 +110,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrecIfDefined(path, newCall),
function,
VCKind.Precondition,
- this).setPosInfo(fi)
+ this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
}).toSeq
} else {
Seq.empty
@@ -142,7 +142,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrecIfDefined(pc._1),
function,
VCKind.ExhaustiveMatch,
- this).setPosInfo(pc._2.asInstanceOf[Error])
+ this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
} else {
Seq.empty
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 967899a1e..c9054fc08 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -726,6 +726,14 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
assert(argsSize == 2)
Times(rargs(0), rargs(1))
}
+ case OpDiv => {
+ assert(argsSize == 2)
+ Division(rargs(0), rargs(1))
+ }
+ case OpIDiv => {
+ assert(argsSize == 2)
+ Division(rargs(0), rargs(1))
+ }
case other => {
System.err.println("Don't know what to do with this declKind : " + other)
throw new CantTranslateException(t)
--
GitLab