diff --git a/src/it/scala/inox/TestSilentReporter.scala b/src/it/scala/inox/TestSilentReporter.scala
index 96deee1c47d6b20025c24707fffc9c3e15c73b37..6cb2bd95f5ddb21ee42a18cf05085269b1d66449 100644
--- a/src/it/scala/inox/TestSilentReporter.scala
+++ b/src/it/scala/inox/TestSilentReporter.scala
@@ -13,6 +13,7 @@ class TestSilentReporter extends DefaultReporter(Set()) {
override def debug(pos: utils.Position, msg: => Any)(implicit section: DebugSection): Unit = {
//println(msg)
+ super.debug(pos, msg)
}
}
diff --git a/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala b/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ad8c11268ba74b1cb249ceca3fc171a33cb83866
--- /dev/null
+++ b/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala
@@ -0,0 +1,50 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package solvers
+package unrolling
+
+class FunctionEqualitySuite extends SolvingTestSuite {
+ import inox.trees._
+ import dsl._
+
+ val v = FreshIdentifier("value")
+
+ val optionID = FreshIdentifier("Option")
+ val someID = FreshIdentifier("Some")
+ val noneID = FreshIdentifier("None")
+
+ val option = mkSort(optionID)("A")(Seq(someID, noneID))
+ val none = mkConstructor(noneID)("A")(Some(optionID))(_ => Seq.empty)
+ val some = mkConstructor(someID)("A")(Some(optionID)) {
+ case Seq(aT) => Seq(ValDef(v, aT))
+ }
+
+ val f = FreshIdentifier("f")
+ val mmapID = FreshIdentifier("MMap")
+ val mmap = mkConstructor(mmapID)("A","B")(None) {
+ case Seq(aT, bT) => Seq(ValDef(f, aT =>: T(optionID)(bT)))
+ }
+
+ val containsID = FreshIdentifier("contains")
+ val contains = mkFunDef(containsID)("A", "B") { case Seq(aT, bT) => (
+ Seq("m" :: T(mmapID)(aT, bT), "k" :: aT), BooleanType, { case Seq(m, k) =>
+ m.getField(f)(k).isInstOf(T(someID)(bT))
+ })
+ }
+
+ val symbols = new Symbols(
+ Map(containsID -> contains),
+ Map(optionID -> option, someID -> some, noneID -> none, mmapID -> mmap)
+ )
+
+ test("simple theorem") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+ val clause = let(
+ "states" :: T(mmapID)(IntegerType, IntegerType =>: IntegerType),
+ T(mmapID)(IntegerType, IntegerType =>: IntegerType)(\("i" :: IntegerType)(i => T(someID)(IntegerType =>: IntegerType)(\("x" :: IntegerType)(x => IntegerLiteral(0)))))
+ )(states => contains(IntegerType, IntegerType =>: IntegerType)(states, IntegerLiteral(0)) && E(false))
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(Not(clause)).isSAT)
+ }
+}
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index e54a768cc37b513f1d03806f9c55071064781795..cac42a3e01e79aa6b9efbd8bc42632d94d355638 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -131,9 +131,9 @@ trait Definitions { self: Trees =>
override def toString: String = asString(PrinterOptions.fromSymbols(this, InoxContext.printNames))
override def asString(implicit opts: PrinterOptions): String = {
- adts.map(p => PrettyPrinter(p._2, opts)).mkString("\n\n") +
+ adts.map(p => prettyPrint(p._2, opts)).mkString("\n\n") +
"\n\n-----------\n\n" +
- functions.map(p => PrettyPrinter(p._2, opts)).mkString("\n\n")
+ functions.map(p => prettyPrint(p._2, opts)).mkString("\n\n")
}
def transform(t: TreeTransformer): Symbols = NoSymbols.withFunctions {
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index fecbe01df372c03eee42972cdd1cdcf63aa16cdf..cde78421cb5803350e2ac03ca70cec2f73ecda95 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -17,7 +17,8 @@ trait Printers {
case class PrinterContext(current: Tree,
parents: List[Tree],
lvl: Int,
- printer: PrettyPrinter) {
+ opts: PrinterOptions,
+ sb: StringBuffer = new StringBuffer) {
def parent = parents.headOption
}
@@ -61,348 +62,357 @@ trait Printers {
val sb: StringBuffer = new StringBuffer) {
override def toString = sb.toString
+ }
- protected def optP(body: => Any)(implicit ctx: PrinterContext) = {
- if (requiresParentheses(ctx.current, ctx.parent)) {
- sb.append("(")
- body
- sb.append(")")
- } else {
- body
- }
+ protected def optP(body: => Any)(implicit ctx: PrinterContext) = {
+ if (requiresParentheses(ctx.current, ctx.parent)) {
+ ctx.sb.append("(")
+ body
+ ctx.sb.append(")")
+ } else {
+ body
}
+ }
- private val dbquote = "\""
+ private val dbquote = "\""
- def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+ def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+ ppPrefix(tree)
+ ppBody(tree)
+ ppSuffix(tree)
+ }
- if (requiresBraces(tree, ctx.parent) && !ctx.parent.contains(tree)) {
- p"""|{
- | $tree
- |}"""
- return
- }
+ protected def ppPrefix(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+ if (requiresBraces(tree, ctx.parent) && !ctx.parent.contains(tree)) {
+ p"""|{
+ | $tree
+ |}"""
+ return
+ }
- if (opts.printTypes) {
- tree match {
- case t: Expr =>
- p"⟨"
+ if (ctx.opts.printTypes) {
+ tree match {
+ case t: Expr =>
+ p"⟨"
- case _ =>
- }
+ case _ =>
}
- tree match {
- case Variable(id, _) =>
- p"$id"
+ }
+ }
- case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd.toVariable == v2 && v2 == v3 =>
- p"$expr.substring($start)"
+ protected def ppBody(tree: Tree)(implicit ctx: PrinterContext): Unit = tree match {
+ case Variable(id, _) =>
+ p"$id"
- case Let(b, d, e) =>
- p"""|val $b = $d
- |$e"""
+ case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd.toVariable == v2 && v2 == v3 =>
+ p"$expr.substring($start)"
- case Forall(args, e) =>
- p"\u2200${nary(args)}. $e"
+ case Let(b, d, e) =>
+ p"""|val $b = $d
+ |$e"""
- case Choose(res, pred) =>
- p"choose(($res) => $pred)"
+ case Forall(args, e) =>
+ p"\u2200${nary(args)}. $e"
- case e @ ADT(adt, args) =>
- p"$adt($args)"
+ case Choose(res, pred) =>
+ p"choose(($res) => $pred)"
- case And(exprs) => optP {
- p"${nary(exprs, " && ")}"
- }
- case Or(exprs) => optP {
- p"${nary(exprs, "| || ")}"
- } // Ugliness award! The first | is there to shield from stripMargin()
- case Not(Equals(l, r)) => optP {
- p"$l \u2260 $r"
- }
- case Implies(l, r) => optP {
- p"$l ==> $r"
- }
- case UMinus(expr) => p"-$expr"
- case Equals(l, r) => optP {
- p"$l == $r"
- }
+ case e @ ADT(adt, args) =>
+ p"$adt($args)"
- case StringConcat(lhs, rhs) => optP {
- p"$lhs + $rhs"
- }
- case SubString(expr, start, end) => p"$expr.substring($start, $end)"
- case StringLength(expr) => p"$expr.length"
-
- case IntLiteral(v) => p"$v"
- case BVLiteral(bits, size) => p"x${(size to 1 by -1).map(i => if (bits(i)) "1" else "0")}"
- case IntegerLiteral(v) => p"$v"
- case FractionLiteral(n, d) =>
- if (d == 1) p"$n"
- else p"$n/$d"
- case CharLiteral(v) => p"$v"
- case BooleanLiteral(v) => p"$v"
- case UnitLiteral() => p"()"
- case StringLiteral(v) =>
- if (v.count(c => c == '\n') >= 1 && v.length >= 80 && v.indexOf("\"\"\"") == -1) {
- p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
- } else {
- val escaped = StringEscapeUtils.escapeJava(v)
- p"$dbquote$escaped$dbquote"
- }
- case GenericValue(tp, id) => p"$tp#$id"
- case Tuple(exprs) => p"($exprs)"
- case TupleSelect(t, i) => p"$t._$i"
- case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
- case IsInstanceOf(e, cct) => p"$e.isInstanceOf[$cct]"
- case ADTSelector(e, id) => p"$e.$id"
-
- case FunctionInvocation(id, tps, args) =>
- p"$id${nary(tps, ", ", "[", "]")}"
- if (args.nonEmpty) {
- p"($args)"
- }
+ case And(exprs) => optP {
+ p"${nary(exprs, " && ")}"
+ }
+ case Or(exprs) => optP {
+ p"${nary(exprs, "| || ")}"
+ } // Ugliness award! The first | is there to shield from stripMargin()
+ case Not(Equals(l, r)) => optP {
+ p"$l \u2260 $r"
+ }
+ case Implies(l, r) => optP {
+ p"$l ==> $r"
+ }
+ case UMinus(expr) => p"-$expr"
+ case Equals(l, r) => optP {
+ p"$l == $r"
+ }
- case Application(caller, args) =>
- p"$caller($args)"
+ case StringConcat(lhs, rhs) => optP {
+ p"$lhs + $rhs"
+ }
+ case SubString(expr, start, end) => p"$expr.substring($start, $end)"
+ case StringLength(expr) => p"$expr.length"
+
+ case IntLiteral(v) => p"$v"
+ case BVLiteral(bits, size) => p"x${(size to 1 by -1).map(i => if (bits(i)) "1" else "0")}"
+ case IntegerLiteral(v) => p"$v"
+ case FractionLiteral(n, d) =>
+ if (d == 1) p"$n"
+ else p"$n/$d"
+ case CharLiteral(v) => p"$v"
+ case BooleanLiteral(v) => p"$v"
+ case UnitLiteral() => p"()"
+ case StringLiteral(v) =>
+ if (v.count(c => c == '\n') >= 1 && v.length >= 80 && v.indexOf("\"\"\"") == -1) {
+ p"$dbquote$dbquote$dbquote$v$dbquote$dbquote$dbquote"
+ } else {
+ val escaped = StringEscapeUtils.escapeJava(v)
+ p"$dbquote$escaped$dbquote"
+ }
+ case GenericValue(tp, id) => p"$tp#$id"
+ case Tuple(exprs) => p"($exprs)"
+ case TupleSelect(t, i) => p"$t._$i"
+ case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
+ case IsInstanceOf(e, cct) => p"$e.isInstanceOf[$cct]"
+ case ADTSelector(e, id) => p"$e.$id"
+
+ case FunctionInvocation(id, tps, args) =>
+ p"$id${nary(tps, ", ", "[", "]")}"
+ if (args.nonEmpty) {
+ p"($args)"
+ }
- case Lambda(Seq(vd), FunctionInvocation(id, Seq(), Seq(arg))) if vd.toVariable == arg =>
- p"$id"
+ case Application(caller, args) =>
+ p"$caller($args)"
- case Lambda(args, body) =>
- optP {
- p"($args) => $body"
- }
+ case Lambda(Seq(vd), FunctionInvocation(id, Seq(), Seq(arg))) if vd.toVariable == arg =>
+ p"$id"
- case Plus(l, r) => optP {
- p"$l + $r"
- }
- case Minus(l, r) => optP {
- p"$l - $r"
- }
- case Times(l, r) => optP {
- p"$l * $r"
- }
- case Division(l, r) => optP {
- p"$l / $r"
- }
- case Remainder(l, r) => optP {
- p"$l % $r"
- }
- case Modulo(l, r) => optP {
- p"$l mod $r"
- }
- case LessThan(l, r) => optP {
- p"$l < $r"
- }
- case GreaterThan(l, r) => optP {
- p"$l > $r"
- }
- case LessEquals(l, r) => optP {
- p"$l <= $r"
- }
- case GreaterEquals(l, r) => optP {
- p"$l >= $r"
- }
- case BVNot(e) => optP {
- p"~$e"
- }
- case BVXor(l, r) => optP {
- p"$l ^ $r"
- }
- case BVOr(l, r) => optP {
- p"$l | $r"
- }
- case BVAnd(l, r) => optP {
- p"$l & $r"
- }
- case BVShiftLeft(l, r) => optP {
- p"$l << $r"
- }
- case BVAShiftRight(l, r) => optP {
- p"$l >> $r"
- }
- case BVLShiftRight(l, r) => optP {
- p"$l >>> $r"
- }
- case fs@FiniteSet(rs, _) => p"{${rs.distinct}}"
- case fs@FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
- case fm@FiniteMap(rs, _, _) => p"{${rs.toMap.toSeq}}"
- case Not(ElementOfSet(e, s)) => p"$e \u2209 $s"
- case ElementOfSet(e, s) => p"$e \u2208 $s"
- case SubsetOf(l, r) => p"$l \u2286 $r"
- case Not(SubsetOf(l, r)) => p"$l \u2288 $r"
- case SetAdd(s, e) => p"$s \u222A {$e}"
- case SetUnion(l, r) => p"$l \u222A $r"
- case BagUnion(l, r) => p"$l \u222A $r"
- case SetDifference(l, r) => p"$l \\ $r"
- case BagDifference(l, r) => p"$l \\ $r"
- case SetIntersection(l, r) => p"$l \u2229 $r"
- case BagIntersection(l, r) => p"$l \u2229 $r"
- case BagAdd(b, e) => p"$b + $e"
- case MultiplicityInBag(e, b) => p"$b($e)"
- case MapApply(m, k) => p"$m($k)"
-
- case Not(expr) => p"\u00AC$expr"
-
- case vd@ValDef(id, tpe) =>
- p"$id : $tpe"
-
- case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
- case TypeParameterDef(tp) => p"$tp"
- case TypeParameter(id) => p"$id"
-
-
- case IfExpr(c, t, ie: IfExpr) =>
- optP {
- p"""|if ($c) {
- | $t
- |} else $ie"""
- }
+ case Lambda(args, body) =>
+ optP {
+ p"($args) => $body"
+ }
- case IfExpr(c, t, e) =>
- optP {
- p"""|if ($c) {
- | $t
- |} else {
- | $e
- |}"""
- }
+ case Plus(l, r) => optP {
+ p"$l + $r"
+ }
+ case Minus(l, r) => optP {
+ p"$l - $r"
+ }
+ case Times(l, r) => optP {
+ p"$l * $r"
+ }
+ case Division(l, r) => optP {
+ p"$l / $r"
+ }
+ case Remainder(l, r) => optP {
+ p"$l % $r"
+ }
+ case Modulo(l, r) => optP {
+ p"$l mod $r"
+ }
+ case LessThan(l, r) => optP {
+ p"$l < $r"
+ }
+ case GreaterThan(l, r) => optP {
+ p"$l > $r"
+ }
+ case LessEquals(l, r) => optP {
+ p"$l <= $r"
+ }
+ case GreaterEquals(l, r) => optP {
+ p"$l >= $r"
+ }
+ case BVNot(e) => optP {
+ p"~$e"
+ }
+ case BVXor(l, r) => optP {
+ p"$l ^ $r"
+ }
+ case BVOr(l, r) => optP {
+ p"$l | $r"
+ }
+ case BVAnd(l, r) => optP {
+ p"$l & $r"
+ }
+ case BVShiftLeft(l, r) => optP {
+ p"$l << $r"
+ }
+ case BVAShiftRight(l, r) => optP {
+ p"$l >> $r"
+ }
+ case BVLShiftRight(l, r) => optP {
+ p"$l >>> $r"
+ }
+ case fs@FiniteSet(rs, _) => p"{${rs.distinct}}"
+ case fs@FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
+ case fm@FiniteMap(rs, _, _) => p"{${rs.toMap.toSeq}}"
+ case Not(ElementOfSet(e, s)) => p"$e \u2209 $s"
+ case ElementOfSet(e, s) => p"$e \u2208 $s"
+ case SubsetOf(l, r) => p"$l \u2286 $r"
+ case Not(SubsetOf(l, r)) => p"$l \u2288 $r"
+ case SetAdd(s, e) => p"$s \u222A {$e}"
+ case SetUnion(l, r) => p"$l \u222A $r"
+ case BagUnion(l, r) => p"$l \u222A $r"
+ case SetDifference(l, r) => p"$l \\ $r"
+ case BagDifference(l, r) => p"$l \\ $r"
+ case SetIntersection(l, r) => p"$l \u2229 $r"
+ case BagIntersection(l, r) => p"$l \u2229 $r"
+ case BagAdd(b, e) => p"$b + $e"
+ case MultiplicityInBag(e, b) => p"$b($e)"
+ case MapApply(m, k) => p"$m($k)"
+
+ case Not(expr) => p"\u00AC$expr"
+
+ case vd@ValDef(id, tpe) =>
+ p"$id : $tpe"
+
+ case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
+ case TypeParameterDef(tp) => p"$tp"
+ case TypeParameter(id) => p"$id"
+
+
+ case IfExpr(c, t, ie: IfExpr) =>
+ optP {
+ p"""|if ($c) {
+ | $t
+ |} else $ie"""
+ }
- // Types
- case Untyped => p"<untyped>"
- case UnitType => p"Unit"
- case Int32Type => p"Int"
- case IntegerType => p"BigInt"
- case RealType => p"Real"
- case CharType => p"Char"
- case BooleanType => p"Boolean"
- case StringType => p"String"
- case SetType(bt) => p"Set[$bt]"
- case BagType(bt) => p"Bag[$bt]"
- case MapType(ft, tt) => p"Map[$ft, $tt]"
- case TupleType(tpes) => p"($tpes)"
- case FunctionType(fts, tt) => p"($fts) => $tt"
- case adt: ADTType =>
- p"${adt.id}${nary(adt.tps, ", ", "[", "]")}"
-
- // Definitions
- case sort: ADTSort =>
- p"abstract class ${sort.id}${nary(sort.tparams, ", ", "[", "]")}"
-
- case cons: ADTConstructor =>
- p"case class ${cons.id}"
- p"${nary(cons.tparams, ", ", "[", "]")}"
- p"(${cons.fields})"
-
- cons.sort.foreach { s =>
- // Remember child and parents tparams are simple bijection
- p" extends $s${nary(cons.tparams, ", ", "[", "]")}"
- }
+ case IfExpr(c, t, e) =>
+ optP {
+ p"""|if ($c) {
+ | $t
+ |} else {
+ | $e
+ |}"""
+ }
- case fd: FunDef =>
- for (an <- fd.flags) {
- p"""|@$an
- |"""
- }
+ // Types
+ case Untyped => p"<untyped>"
+ case UnitType => p"Unit"
+ case Int32Type => p"Int"
+ case IntegerType => p"BigInt"
+ case RealType => p"Real"
+ case CharType => p"Char"
+ case BooleanType => p"Boolean"
+ case StringType => p"String"
+ case SetType(bt) => p"Set[$bt]"
+ case BagType(bt) => p"Bag[$bt]"
+ case MapType(ft, tt) => p"Map[$ft, $tt]"
+ case TupleType(tpes) => p"($tpes)"
+ case FunctionType(fts, tt) => p"($fts) => $tt"
+ case adt: ADTType =>
+ p"${adt.id}${nary(adt.tps, ", ", "[", "]")}"
+
+ // Definitions
+ case sort: ADTSort =>
+ p"abstract class ${sort.id}${nary(sort.tparams, ", ", "[", "]")}"
+
+ case cons: ADTConstructor =>
+ p"case class ${cons.id}"
+ p"${nary(cons.tparams, ", ", "[", "]")}"
+ p"(${cons.fields})"
+
+ cons.sort.foreach { s =>
+ // Remember child and parents tparams are simple bijection
+ p" extends $s${nary(cons.tparams, ", ", "[", "]")}"
+ }
- p"def ${fd.id}${nary(fd.tparams, ", ", "[", "]")}"
- if (fd.params.nonEmpty) {
- p"(${fd.params}): "
- }
+ case fd: FunDef =>
+ for (an <- fd.flags) {
+ p"""|@$an
+ |"""
+ }
- p"${fd.returnType} = "
- p"${fd.fullBody}"
+ p"def ${fd.id}${nary(fd.tparams, ", ", "[", "]")}"
+ if (fd.params.nonEmpty) {
+ p"(${fd.params}): "
+ }
- case (tree: PrettyPrintable) => tree.printWith(ctx)
+ p"${fd.returnType} = "
+ p"${fd.fullBody}"
- case _ => sb.append("Tree? (" + tree.getClass + ")")
- }
- if (opts.printTypes) {
- tree match {
- case t: Expr =>
- p" : ${t.getType(opts.symbols.get)} ⟩"
+ case (tree: PrettyPrintable) => tree.printWith(ctx)
- case _ =>
- }
+ case _ => ctx.sb.append("Tree? (" + tree.getClass + ")")
+ }
+
+ protected def ppSuffix(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+ if (ctx.opts.printTypes) {
+ tree match {
+ case t: Expr =>
+ p" : ${t.getType(ctx.opts.symbols.get)} ⟩"
+
+ case _ =>
}
- if (opts.printPositions) {
- tree.getPos match {
- case op: OffsetPosition =>
- p"@($op)"
- case rp: RangePosition =>
- if (rp.lineFrom == rp.lineTo) {
- if (rp.colFrom == rp.colTo) {
- p"@(${rp.lineFrom}:${rp.colFrom})"
- } else {
- p"@(${rp.lineFrom}:${rp.colFrom}-${rp.colTo})"
- }
+ }
+ if (ctx.opts.printPositions) {
+ tree.getPos match {
+ case op: OffsetPosition =>
+ p"@($op)"
+ case rp: RangePosition =>
+ if (rp.lineFrom == rp.lineTo) {
+ if (rp.colFrom == rp.colTo) {
+ p"@(${rp.lineFrom}:${rp.colFrom})"
} else {
- p"@(${rp.focusBegin}-${rp.focusEnd})"
+ p"@(${rp.lineFrom}:${rp.colFrom}-${rp.colTo})"
}
- case _ =>
- p"@(?)"
- }
+ } else {
+ p"@(${rp.focusBegin}-${rp.focusEnd})"
+ }
+ case _ =>
+ p"@(?)"
}
}
+ }
- protected def isSimpleExpr(e: Expr): Boolean = e match {
- case _: Let => false
- case p: PrettyPrintable => p.isSimpleExpr
- case _ => true
- }
+ protected def isSimpleExpr(e: Expr): Boolean = e match {
+ case _: Let => false
+ case p: PrettyPrintable => p.isSimpleExpr
+ case _ => true
+ }
- protected def noBracesSub(e: Expr): Seq[Expr] = e match {
- case Let(_, _, bd) => Seq(bd)
- case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
- case _ => Seq()
- }
+ protected def noBracesSub(e: Expr): Seq[Expr] = e match {
+ case Let(_, _, bd) => Seq(bd)
+ case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
+ case _ => Seq()
+ }
- protected def requiresBraces(ex: Tree, within: Option[Tree]) = (ex, within) match {
- case (e: Expr, _) if isSimpleExpr(e) => false
- case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
- case (e: Expr, Some(_)) => true
- case _ => false
- }
+ protected def requiresBraces(ex: Tree, within: Option[Tree]) = (ex, within) match {
+ case (e: Expr, _) if isSimpleExpr(e) => false
+ case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
+ case (e: Expr, Some(_)) => true
+ case _ => false
+ }
- protected def precedence(ex: Expr): Int = ex match {
- case (pa: PrettyPrintable) => pa.printPrecedence
- // 0: Letters
- case (_: ElementOfSet | _: Modulo) => 0
- // 1: |
- case (_: Or | _: BVOr) => 1
- // 2: ^
- case (_: BVXor) => 2
- // 3: &
- case (_: And | _: BVAnd | _: SetIntersection) => 3
- // 4: < >
- case (
- _: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan |
- _: BVAShiftRight | _: BVLShiftRight | _: BVShiftLeft
- ) => 4
- // 5: = !
- case (_: Equals | _: Not | _: Implies) => 5
- // 6: :
- // 7: + -
- case (_: Plus | _: Minus | _: SetUnion | _: SetDifference | _: StringConcat) => 7
- // 8: * / %
- case (_: Times | _: Division | _: Remainder) => 8
- // 9: Other special characters
- case _ => 9
- }
+ protected def precedence(ex: Expr): Int = ex match {
+ case (pa: PrettyPrintable) => pa.printPrecedence
+ // 0: Letters
+ case (_: ElementOfSet | _: Modulo) => 0
+ // 1: |
+ case (_: Or | _: BVOr) => 1
+ // 2: ^
+ case (_: BVXor) => 2
+ // 3: &
+ case (_: And | _: BVAnd | _: SetIntersection) => 3
+ // 4: < >
+ case (
+ _: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan |
+ _: BVAShiftRight | _: BVLShiftRight | _: BVShiftLeft
+ ) => 4
+ // 5: = !
+ case (_: Equals | _: Not | _: Implies) => 5
+ // 6: :
+ // 7: + -
+ case (_: Plus | _: Minus | _: SetUnion | _: SetDifference | _: StringConcat) => 7
+ // 8: * / %
+ case (_: Times | _: Division | _: Remainder) => 8
+ // 9: Other special characters
+ case _ => 9
+ }
- protected def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
- case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
- case (_, None) => false
- case (_, Some(
- _: Definition | _: Let | _: IfExpr | _: ADT | _: Lambda | _: Choose | _: Tuple
- )) => false
- case (ex: StringConcat, Some(_: StringConcat)) => false
- case (_, Some(_: FunctionInvocation)) => false
- case (ie: IfExpr, _) => true
- case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
- case (_, _) => true
- }
+ protected def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
+ case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
+ case (_, None) => false
+ case (_, Some(
+ _: Definition | _: Let | _: IfExpr | _: ADT | _: Lambda | _: Choose | _: Tuple
+ )) => false
+ case (ex: StringConcat, Some(_: StringConcat)) => false
+ case (_, Some(_: FunctionInvocation)) => false
+ case (ie: IfExpr, _) => true
+ case (e1: Expr, Some(e2: Expr)) if precedence(e1) > precedence(e2) => false
+ case (_, _) => true
}
implicit class PrintWrapper(val f: PrinterContext => Any) {
@@ -412,8 +422,7 @@ trait Printers {
implicit class PrintingHelper(val sc: StringContext) {
def p(args: Any*)(implicit ctx: PrinterContext): Unit = {
- val printer = ctx.printer
- val sb = printer.sb
+ val sb = ctx.sb
val strings = sc.parts.iterator
val expressions = args.iterator
@@ -464,10 +473,10 @@ trait Printers {
nctx.current :: nctx.parents
}
val nctx2 = nctx.copy(parents = parents, current = t)
- printer.pp(t)(nctx2)
+ pp(t)(nctx2)
case id: Identifier =>
- val name = if (ctx.printer.opts.printUniqueIds) {
+ val name = if (ctx.opts.printUniqueIds) {
id.uniqueName
} else {
id.toString
@@ -514,29 +523,10 @@ trait Printers {
def isSimpleExpr: Boolean = false
}
- abstract class PrettyPrinterFactory {
- def create(opts: PrinterOptions, osym: Option[Symbols]): PrettyPrinter
-
- def apply(tree: Tree, opts: PrinterOptions = PrinterOptions(), osym: Option[Symbols] = None): String = {
- val printer = create(opts, osym)
- val ctx = PrinterContext(tree, Nil, opts.baseIndent, printer)
- printer.pp(tree)(ctx)
- printer.toString
- }
-
- def apply(tree: Tree, ctx: InoxContext): String = {
- val opts = PrinterOptions.fromContext(ctx)
- apply(tree, opts, None)
- }
-
- def apply(tree: Tree, ctx: InoxContext, sym: Symbols): String = {
- val opts = PrinterOptions.fromContext(ctx)
- apply(tree, opts, Some(sym))
- }
- }
-
- object PrettyPrinter extends PrettyPrinterFactory {
- def create(opts: PrinterOptions, osym: Option[Symbols]) = new PrettyPrinter(opts, osym)
+ def prettyPrint(tree: Tree, opts: PrinterOptions = PrinterOptions()): String = {
+ val ctx = PrinterContext(tree, Nil, opts.baseIndent, opts)
+ pp(tree)(ctx)
+ ctx.sb.toString
}
}
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 5f342c5a85fa8895e3c3440fc556de2adbacb459..ac08971ac895faa1befb1246efba8f007d636be2 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -27,7 +27,7 @@ trait Trees
// @EK: toString is considered harmful for non-internal things. Use asString(ctx) instead.
- def asString(implicit opts: PrinterOptions): String = PrettyPrinter(this, opts)
+ def asString(implicit opts: PrinterOptions): String = prettyPrint(this, opts)
override def toString = asString(PrinterOptions.fromContext(InoxContext.printNames))
}
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index caa22aeb8fdc1cb6311e408a3236f56d0e4c675e..d9e5836ddbd499e3da88424d2cf046537052256f 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -128,10 +128,16 @@ trait DatatypeTemplates { self: Templates =>
val newBool: Variable = Variable(FreshIdentifier("b", true), BooleanType)
storeCond(pathVar, newBool)
- iff(and(pathVar, IsInstanceOf(expr, tpe)), newBool)
for (vd <- tcons.fields) {
rec(newBool, ADTSelector(AsInstanceOf(expr, tpe), vd.id))
}
+
+ val vars = types.keys.toSet ++ functions.keys
+ guardedExprs.flatMap(_._2.flatMap(exprOps.variablesOf))
+
+ if (vars(newBool)) {
+ iff(and(pathVar, IsInstanceOf(expr, tpe)), newBool)
+ }
}
}
}
@@ -253,6 +259,7 @@ trait DatatypeTemplates { self: Templates =>
}
def unroll: Clauses = if (typeInfos.isEmpty) Seq.empty else {
+ println("unrolling datatypes")
val blockers = typeInfos.filter(_._2._1 <= currentGeneration).toSeq.map(_._1)
val newClauses = new scala.collection.mutable.ListBuffer[Encoded]
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 942fa17da1e4cebf6f5d819a0e2e8e9527d27dd5..d6ba9205cea613f26384340a1713076e026bf011 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -271,8 +271,6 @@ trait LambdaTemplates { self: Templates =>
val typeBlocker = encodeSymbol(Variable(FreshIdentifier("t"), BooleanType))
typeBlockers += value -> typeBlocker
- val clauses = registerSymbol(typeBlocker, value, to)
-
val (b, extClauses) = if (knownFree(tpe) contains caller) {
(blocker, Seq.empty)
} else {
@@ -289,6 +287,9 @@ trait LambdaTemplates { self: Templates =>
(firstB, Seq(clause))
}
+ registerParent(typeBlocker, b)
+ val clauses = registerSymbol(typeBlocker, value, to)
+
clauses ++ extClauses :+ mkImplies(b, typeBlocker)
}
}
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 24339f73fdf43eb2c58ebe3505e6430833598053..62c214b6915791cef732950c83b661999390e5f5 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -188,7 +188,7 @@ trait TemplateGenerator { self: Templates =>
val xrec = rec(pathVar, x, pol)
iff(and(pathVar, xrec), newBool)
- iff(and(pathVar, not(xrec)), not(newExpr))
+ storeGuarded(pathVar, implies(not(xrec), not(newExpr)))
recAnd(newBool, xs)
@@ -216,7 +216,7 @@ trait TemplateGenerator { self: Templates =>
storeCond(pathVar, newBool)
val xrec = rec(pathVar, x, None)
- iff(and(pathVar, xrec), newExpr)
+ storeGuarded(pathVar, implies(xrec, newExpr))
iff(and(pathVar, not(xrec)), newBool)
recOr(newBool, xs)
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index 3e0af30b5d11fb73d77e5fd5068bbe289049ebc9..fd358008adaa9370af658090676464e04c36ad45 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -120,6 +120,10 @@ trait Templates extends TemplateGenerator
}
}
+ protected def registerParent(child: Encoded, parent: Encoded): Unit = {
+ condImplied += child -> (condImplied(child) + parent)
+ }
+
protected def blockerParents(b: Encoded): Set[Encoded] = condImplied(b)
protected def blockerChildren(b: Encoded): Set[Encoded] = condImplies(b)