From bed6d83389c8dc22c847a05b4870462b1802a1f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Mon, 18 Apr 2011 09:34:17 +0000
Subject: [PATCH] On restarting, FairZ3Solver needs to purge its function maps
---
src/cp/CallTransformation.scala | 2 +-
src/cp/CodeExtraction.scala | 2 +-
src/purescala/FairZ3Solver.scala | 2 ++
3 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/cp/CallTransformation.scala b/src/cp/CallTransformation.scala
index b0a0880ec..ab8a96f58 100644
--- a/src/cp/CallTransformation.scala
+++ b/src/cp/CallTransformation.scala
@@ -552,7 +552,7 @@ object CallTransformation {
case None => expr
case Some(b) => And(expr, GreaterThan(minExpr, IntLiteral(b)))
}
- println("Now calling findAllMinimizing with " + toCheck)
+ // purescala.Settings.reporter.info("Now calling findAllMinimizing with " + toCheck)
val minValue = chooseMinimizingModelAndValue(program, toCheck, outputVars, minExpr, inputConstraints)._2
val minValConstraint = And(expr, Equals(minExpr, IntLiteral(minValue)))
diff --git a/src/cp/CodeExtraction.scala b/src/cp/CodeExtraction.scala
index 4d9ab2e5f..13253aacc 100644
--- a/src/cp/CodeExtraction.scala
+++ b/src/cp/CodeExtraction.scala
@@ -650,7 +650,7 @@ trait CodeExtraction extends Extractors {
if (tolerant) {
val varTpe = scalaType2PureScala(unit, silent)(sym.tpe)
val newID = FreshIdentifier(sym.name.toString).setType(varTpe)
- externalSubsts(i) = (() => Variable(newID))
+ varSubsts(sym) = (() => Variable(newID))
Variable(newID)
} else {
unit.error(tr.pos, "Unidentified variable.")
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 134af4730..484d1b101 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -177,6 +177,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
private var reverseFunctionMap: Map[Z3FuncDecl, FunDef] = Map.empty
def prepareFunctions: Unit = {
+ functionMap = Map.empty
+ reverseFunctionMap = Map.empty
for (funDef <- program.definedFunctions) {
val sortSeq = funDef.args.map(vd => typeToSort(vd.tpe))
val returnSort = typeToSort(funDef.returnType)
--
GitLab