From 148dfaad16e49583e624ff0a6254dae3c0a8d542 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 16 Dec 2015 17:42:33 +0100
Subject: [PATCH] Corrected compilation errors after merge
---
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 6 +++---
.../scala/leon/synthesis/disambiguation/ExamplesAdder.scala | 2 +-
src/main/scala/leon/synthesis/rules/StringRender.scala | 4 ++--
3 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 5fd738518..f0b7d5f91 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -607,15 +607,15 @@ trait AbstractZ3Solver extends Solver {
case _ =>
reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
}
- } else
- _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
+ } else {
+ _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
case Some(hexa) =>
tpe match {
case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar)
case _ => unsound(t, "unexpected target type for BV value: " + tpe.asString)
}
- case None => unsound(t, "could not translate Z3NumeralIntAST numeral")
+ case None => unsound(t, "could not translate Z3NumeralIntAST numeral")
}
}
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 51e88cfef..cfe8f456a 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -58,7 +58,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
}
case None =>
val id = FreshIdentifier("res", fd.returnType, false)
- fd.postcondition = Some(Lambda(Seq(ValDef(id, None)), Passes(inputVariables, Variable(id), newCases)))
+ fd.postcondition = Some(Lambda(Seq(ValDef(id, false)), Passes(inputVariables, Variable(id), newCases)))
//ctx0.reporter.info("No postcondition, adding it: " + fd)
}
fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 3604808df..d5c0b21e6 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -325,7 +325,7 @@ case object StringRender extends Rule("StringRender") {
: (Stream[WithIds[MatchCase]], StringSynthesisResult) = cct match {
case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
val typeMap = tparams.zip(tparams2).toMap
- val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id )
+ val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd.id, typeMap) )
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val (rhs, result) = createFunDefsTemplates(ctx.copy(currentCaseClassParent=Some(cct)), fields.map(Variable)) // Invoke functions for each of the fields.
val newCases = rhs.map(e => (MatchCase(pattern, None, e._1), e._2))
@@ -351,7 +351,7 @@ case object StringRender extends Rule("StringRender") {
val cases = (ListBuffer[WithIds[MatchCase]]() /: act.knownCCDescendants) {
case (acc, cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
val typeMap = tparams.zip(tparams2).toMap
- val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id )
+ val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd.id, typeMap) )
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val rhs = StringLiteral(id.asString)
MatchCase(pattern, None, rhs)
--
GitLab