Skip to content
Snippets Groups Projects
Commit 148dfaad authored by Mikaël Mayer's avatar Mikaël Mayer
Browse files

Corrected compilation errors after merge

parent bf565df3
No related branches found
No related tags found
No related merge requests found
...@@ -607,15 +607,15 @@ trait AbstractZ3Solver extends Solver { ...@@ -607,15 +607,15 @@ trait AbstractZ3Solver extends Solver {
case _ => case _ =>
reporter.fatalError("Unexpected target type for BV value: " + tpe.asString) reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
} }
} else } else {
_root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match { _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
case Some(hexa) => case Some(hexa) =>
tpe match { tpe match {
case Int32Type => IntLiteral(hexa.toInt) case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar) case CharType => CharLiteral(hexa.toInt.toChar)
case _ => unsound(t, "unexpected target type for BV value: " + tpe.asString) 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")
} }
} }
......
...@@ -58,7 +58,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) { ...@@ -58,7 +58,7 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
} }
case None => case None =>
val id = FreshIdentifier("res", fd.returnType, false) 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) //ctx0.reporter.info("No postcondition, adding it: " + fd)
} }
fd.body match { // TODO: Is it correct to discard the choose construct inside the body? fd.body match { // TODO: Is it correct to discard the choose construct inside the body?
......
...@@ -325,7 +325,7 @@ case object StringRender extends Rule("StringRender") { ...@@ -325,7 +325,7 @@ case object StringRender extends Rule("StringRender") {
: (Stream[WithIds[MatchCase]], StringSynthesisResult) = cct match { : (Stream[WithIds[MatchCase]], StringSynthesisResult) = cct match {
case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) => case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
val typeMap = tparams.zip(tparams2).toMap 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 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 (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)) val newCases = rhs.map(e => (MatchCase(pattern, None, e._1), e._2))
...@@ -351,7 +351,7 @@ case object StringRender extends Rule("StringRender") { ...@@ -351,7 +351,7 @@ case object StringRender extends Rule("StringRender") {
val cases = (ListBuffer[WithIds[MatchCase]]() /: act.knownCCDescendants) { val cases = (ListBuffer[WithIds[MatchCase]]() /: act.knownCCDescendants) {
case (acc, cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) => case (acc, cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
val typeMap = tparams.zip(tparams2).toMap 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 pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val rhs = StringLiteral(id.asString) val rhs = StringLiteral(id.asString)
MatchCase(pattern, None, rhs) MatchCase(pattern, None, rhs)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment