From 59478b045879ee3356b36d2a1a952233ba55df93 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 11 Nov 2016 16:10:16 +0100
Subject: [PATCH] Added choose to TIP and fixes in templates for beter
q-instantiation heuristics
---
.../solvers/unrolling/DatatypeTemplates.scala | 3 ++-
src/main/scala/inox/tip/Parser.scala | 6 +++++-
src/main/scala/inox/tip/Printer.scala | 7 ++++++-
src/main/scala/inox/tip/TipExtensions.scala | 21 +++++++++++++++++++
4 files changed, 34 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 8f33f9bb3..5106ccfef 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -183,7 +183,8 @@ trait DatatypeTemplates { self: Templates =>
storeCond(pathVar, newBool)
for (vd <- tcons.fields) {
- rec(newBool, ADTSelector(AsInstanceOf(expr, tpe), vd.id), state.copy(recurseSort = false))
+ val ex = if (adt != tpe) AsInstanceOf(expr, tpe) else expr
+ rec(newBool, ADTSelector(ex, vd.id), state.copy(recurseSort = false))
}
val vars = tpes.keys.toSet ++ functions.keys ++
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 52f8fa69d..0a5af026d 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -13,7 +13,7 @@ import smtlib.theories.experimental._
import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTApplication, _}
import smtlib.extensions.tip.Commands._
-import Terms.{Assume => SMTAssume}
+import Terms.{Assume => SMTAssume, Choose => SMTChoose}
import Commands._
import scala.collection.BitSet
@@ -407,6 +407,10 @@ class Parser(file: File) {
case SMTAssume(pred, body) =>
Assume(extractTerm(pred), extractTerm(body))
+ case SMTChoose(sym, sort, pred) =>
+ val vd = ValDef(FreshIdentifier(sym.name), extractSort(sort))
+ Choose(vd, extractTerm(pred)(locals.withVariable(sym, vd.toVariable)))
+
case SMTLet(binding, bindings, term) =>
var locs = locals
val mapping = for (VarBinding(name, term) <- (binding +: bindings)) yield {
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 5d76756b2..1761d5db3 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -11,7 +11,7 @@ import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTAppli
import smtlib.extensions.tip.Commands._
import smtlib.Interpreter
-import Terms.{Assume => SMTAssume}
+import Terms.{Assume => SMTAssume, Choose => SMTChoose}
import Commands._
import java.io.Writer
@@ -356,6 +356,11 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
Some(declareSort(fi.tfd.returnType))
)
+ case Choose(vd, pred) =>
+ val sym = id2sym(vd.id)
+ val sort = declareSort(vd.tpe)
+ SMTChoose(sym, declareSort(vd.tpe), toSMT(pred)(bindings + (vd.id -> (sym: Term))))
+
case _ => super.toSMT(e)
}
}
diff --git a/src/main/scala/inox/tip/TipExtensions.scala b/src/main/scala/inox/tip/TipExtensions.scala
index 0f22f3d8a..48f942e30 100644
--- a/src/main/scala/inox/tip/TipExtensions.scala
+++ b/src/main/scala/inox/tip/TipExtensions.scala
@@ -13,6 +13,7 @@ object Tokens {
import LT.ReservedWord
case object Assume extends ReservedWord
+ case object Choose extends ReservedWord
case object DatatypeInvariant extends ReservedWord
}
@@ -26,6 +27,18 @@ object Terms {
ctx.print(")")
}
}
+
+ case class Choose(name: SSymbol, sort: Sort, pred: Term) extends TermExtension {
+ def print(ctx: PrintingContext): Unit = {
+ ctx.print("(choose ")
+ ctx.print(name)
+ ctx.print(" ")
+ ctx.print(sort)
+ ctx.print(" ")
+ ctx.print(pred)
+ ctx.print(")")
+ }
+ }
}
object Commands {
@@ -60,6 +73,7 @@ class TipLexer(reader: java.io.Reader) extends SMTLexer(reader) {
override protected def toReserved(s: String): Option[Token] = s match {
case "assume" => Some(Token(Tokens.Assume))
+ case "choose" => Some(Token(Tokens.Choose))
case "datatype-invariant" => Some(Token(Tokens.DatatypeInvariant))
case _ => super.toReserved(s)
}
@@ -76,6 +90,13 @@ class TipParser(lexer: TipLexer) extends SMTParser(lexer) {
val body = parseTerm
Assume(pred, body)
+ case Tokens.Choose =>
+ eat(Tokens.Choose)
+ val name = parseSymbol
+ val sort = parseSort
+ val pred = parseTerm
+ Choose(name, sort, pred)
+
case _ => super.parseTermWithoutParens
}
--
GitLab