From 716b0395c6d89121b7b0d98807a152bb7c347562 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 3 Oct 2016 15:25:06 +0200
Subject: [PATCH] More solver tests (+fixes) and start on TIP test
---
src/it/scala/inox/InoxTestSuite.scala | 1 -
src/it/scala/inox/ResourceUtils.scala | 30 ++
.../unrolling/InductiveUnrollingSuite.scala | 41 ++-
src/it/scala/inox/tip/TIPTestSuite.scala | 37 +++
src/main/scala/inox/parsers/TIPParser.scala | 309 +++++++++---------
.../scala/inox/solvers/smtlib/Z3Target.scala | 33 +-
6 files changed, 285 insertions(+), 166 deletions(-)
create mode 100644 src/it/scala/inox/ResourceUtils.scala
create mode 100644 src/it/scala/inox/tip/TIPTestSuite.scala
diff --git a/src/it/scala/inox/InoxTestSuite.scala b/src/it/scala/inox/InoxTestSuite.scala
index 9abb984f9..89b1d0649 100644
--- a/src/it/scala/inox/InoxTestSuite.scala
+++ b/src/it/scala/inox/InoxTestSuite.scala
@@ -8,7 +8,6 @@ import org.scalatest.concurrent._
import utils._
trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
- type FixtureParam = InoxContext
val configurations: Seq[Seq[InoxOption[Any]]] = Seq(Seq.empty)
diff --git a/src/it/scala/inox/ResourceUtils.scala b/src/it/scala/inox/ResourceUtils.scala
new file mode 100644
index 000000000..3297b44f6
--- /dev/null
+++ b/src/it/scala/inox/ResourceUtils.scala
@@ -0,0 +1,30 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+
+import org.scalatest._
+import org.scalatest.concurrent._
+
+import java.io.File
+
+import utils._
+
+trait ResourceUtils {
+
+ val resourcesDir = "src/it/resources"
+
+ def resourceFiles(dir: String, filter: String => Boolean = (s: String) => true, recursive: Boolean = false): Seq[File] = {
+ val baseDir = new File(getClass.getResource(s"/$dir").getPath)
+
+ def rec(f: File): Seq[File] = Option(f.listFiles()).getOrElse(Array()).flatMap { f =>
+ if (f.isDirectory) {
+ if (recursive) rec(f)
+ else Nil
+ } else {
+ List(f)
+ }
+ }
+
+ rec(baseDir).filter(f => filter(f.getPath)).toSeq.sortBy(_.getPath)
+ }
+}
diff --git a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
index 50182a30f..70fcc7b3a 100644
--- a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
@@ -22,6 +22,15 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
}
val sizeID = FreshIdentifier("size")
+ val appendID = FreshIdentifier("append")
+ val flatMapID = FreshIdentifier("flatMap")
+ val assocID = FreshIdentifier("associative_lemma")
+
+ val forallID = FreshIdentifier("forall")
+ val contentID = FreshIdentifier("content")
+ val partitionID = FreshIdentifier("partition")
+ val sortID = FreshIdentifier("sort")
+
val sizeFd = mkFunDef(sizeID)("A") { case Seq(aT) => (
Seq("l" :: T(listID)(aT)), IntegerType, { case Seq(l) =>
if_ (l.isInstOf(T(consID)(aT))) {
@@ -34,20 +43,18 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
- val appendID = FreshIdentifier("append")
val append = mkFunDef(appendID)("A") { case Seq(aT) => (
Seq("l1" :: T(listID)(aT), "l2" :: T(listID)(aT)), T(listID)(aT), { case Seq(l1, l2) =>
- if_ (l1.isInstOf(T(consID)(aT))) {
+ let("res" :: T(listID)(aT), if_ (l1.isInstOf(T(consID)(aT))) {
let("c" :: T(consID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
T(consID)(aT)(c.getField(head), E(appendID)(aT)(c.getField(tail), l2))
}
} else_ {
l2
- }
+ }) { res => Assume(E(contentID)(aT)(res) === E(contentID)(aT)(l1) ++ E(contentID)(aT)(l2), res) }
})
}
- val flatMapID = FreshIdentifier("flatMap")
val flatMap = mkFunDef(flatMapID)("A","B") { case Seq(aT, bT) => (
Seq("l" :: T(listID)(aT), "f" :: (aT =>: T(listID)(bT))), T(listID)(bT), { case Seq(l, f) =>
if_ (l.isInstOf(T(consID)(aT))) {
@@ -60,7 +67,6 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
- val assocID = FreshIdentifier("associative_lemma")
val associative = mkFunDef(assocID)("A","B","C") { case Seq(aT, bT, cT) => (
Seq("l1" :: T(listID)(aT), "l2" :: T(listID)(bT), "l3" :: T(listID)(cT),
"f" :: (aT =>: T(listID)(bT)), "g" :: (bT =>: T(listID)(cT))), BooleanType,
@@ -88,7 +94,6 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
- val forallID = FreshIdentifier("forall")
val forall = mkFunDef(forallID)("A") { case Seq(aT) => (
Seq("l" :: T(listID)(aT), "p" :: (aT =>: BooleanType)), BooleanType, { case Seq(l, p) =>
if_ (l.isInstOf(T(consID)(aT))) {
@@ -101,7 +106,6 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
- val contentID = FreshIdentifier("content")
val content = mkFunDef(contentID)("A") { case Seq(aT) => (
Seq("l" :: T(listID)(aT)), SetType(aT), { case Seq(l) =>
if_ (l.isInstOf(T(consID)(aT))) {
@@ -114,7 +118,6 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
- val partitionID = FreshIdentifier("partition")
val partition = mkFunDef(partitionID)("A") { case Seq(aT) => (
Seq("l" :: T(listID)(aT), "p" :: (aT =>: BooleanType)), T(T(listID)(aT), T(listID)(aT)), { case Seq(l, p) =>
let("res" :: T(T(listID)(aT), T(listID)(aT)), if_ (l.isInstOf(T(consID)(aT))) {
@@ -139,7 +142,6 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
- val sortID = FreshIdentifier("sort")
val sort = mkFunDef(sortID)("A") { case Seq(aT) => (
Seq("l" :: T(listID)(aT), "lt" :: ((aT, aT) =>: BooleanType)), T(listID)(aT), { case Seq(l, lt) =>
let("res" :: T(listID)(aT), if_ (l.isInstOf(T(consID)(aT))) {
@@ -148,13 +150,12 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
E(partitionID)(aT)(cons.getField(tail), \("x" :: aT)(x => lt(x, cons.getField(head))))) { part =>
let("less" :: T(listID)(aT), E(sortID)(aT)(part._1, lt)) { less =>
let("more" :: T(listID)(aT), E(sortID)(aT)(part._2, lt)) { more =>
- let("res" :: T(listID)(aT), E(appendID)(aT)(less, T(consID)(aT)(cons.getField(head), more))) { res =>
Assume(E(forallID)(aT)(part._1, \("x" :: aT)(x => lt(x, cons.getField(head)))),
- Assume(E(contentID)(aT)(less) === E(contentID)(aT)(part._1),
+ Assume(E(contentID)(aT)(part._1) === E(contentID)(aT)(less),
Assume(E(forallID)(aT)(less, \("x" :: aT)(x => lt(x, cons.getField(head)))),
- res
+ E(appendID)(aT)(less, T(consID)(aT)(cons.getField(head), more))
)))
- }}}}}
+ }}}}
} else_ {
l
}) { res =>
@@ -190,7 +191,7 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(Not(associative.fullBody)).isUNSAT)
}
- test("sort preserves content") { ctx =>
+ test("sort preserves content 1") { ctx =>
val program = InoxProgram(ctx, symbols)
val (l,p) = ("l" :: T(listID)(IntegerType), "p" :: ((IntegerType, IntegerType) =>: BooleanType))
val clause = E(contentID)(IntegerType)(E(sortID)(IntegerType)(l.toVariable, p.toVariable)) ===
@@ -198,4 +199,16 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(Not(clause)).isUNSAT)
}
+ test("sort preserves content 2") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+ import program._
+
+ val clause = sort.fullBody match {
+ case Let(res, body, Assume(pred, resVar)) if res.toVariable == resVar =>
+ Let(res, body, pred)
+ case e => fail("Unexpected fullBody of `sort`: " + e.asString)
+ }
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(Not(clause)).isUNSAT)
+ }
+
}
diff --git a/src/it/scala/inox/tip/TIPTestSuite.scala b/src/it/scala/inox/tip/TIPTestSuite.scala
new file mode 100644
index 000000000..19f91fe85
--- /dev/null
+++ b/src/it/scala/inox/tip/TIPTestSuite.scala
@@ -0,0 +1,37 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import org.scalatest._
+import org.scalatest.concurrent._
+
+import solvers._
+import utils._
+
+trait TIPTestSuite extends InoxTestSuite with ResourceUtils {
+
+ val tipDir = "tip-benchmarks"
+
+ def makeTests(base: String) = {
+ val files = resourceFiles(s"$tipDir/$base")
+
+ if (files.isEmpty) {
+ ignore(s"tip-benchmarks: $base directory not found (missing git submodule?") {_ => ()}
+ } else {
+ for (file <- files) {
+ test(s"Verifying tip-benchmarks/$base") { ctx =>
+ val (syms, clause) = parsers.TIPParser.parse(file)
+ val program = InoxProgram(ctx, syms)
+
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
+ }
+ }
+ }
+ }
+
+ makeTests("grammars")
+ makeTests("isaplanner")
+ makeTests("prod")
+ makeTests("tip2015")
+}
diff --git a/src/main/scala/inox/parsers/TIPParser.scala b/src/main/scala/inox/parsers/TIPParser.scala
index 6f0897b17..8af28f8f1 100644
--- a/src/main/scala/inox/parsers/TIPParser.scala
+++ b/src/main/scala/inox/parsers/TIPParser.scala
@@ -18,7 +18,20 @@ import utils._
import scala.language.implicitConversions
trait TIPParser {
- import inox.trees._
+ val trees: ast.Trees
+ import trees._
+
+ def parse(file: File): (Symbols, Expr) = {
+ val pos = new PositionProvider(new java.io.BufferedReader(new java.io.FileReader(file)), Some(file))
+ val parser = new Parser(new Lexer(pos.reader), pos)
+ parser.parseTIPScript
+ }
+
+ def parse(reader: Reader): (Symbols, Expr) = {
+ val pos = new PositionProvider(reader, None)
+ val parser = new Parser(new Lexer(pos.reader), pos)
+ parser.parseTIPScript
+ }
private class PositionProvider(_reader: Reader, _file: Option[File]) {
val (reader, file): (Reader, File) = _file match {
@@ -48,13 +61,13 @@ trait TIPParser {
class MissformedTIPException(reason: String, pos: Position)
extends Exception("Missfomed TIP source @" + pos + ":\n" + reason)
- private class Parser(lex: Lexer, positions: PositionProvider) extends SMTParser(lex) {
+ protected class Parser(lex: Lexer, positions: PositionProvider) extends SMTParser(lex) {
implicit def smtlibPositionToPosition(pos: _root_.smtlib.common.Position): Position = {
positions.get(pos.line, pos.col)
}
- private class Locals private(
+ protected class Locals (
funs: Map[SSymbol, Identifier],
adts: Map[SSymbol, Identifier],
selectors: Map[SSymbol, Identifier],
@@ -109,176 +122,168 @@ trait TIPParser {
new Locals(funs, adts, selectors, vars, tps, symbols.withADTs(defs))
}
- private object Locals {
- def empty = new Locals(Map.empty, Map.empty, Map.empty, Map.empty, Map.empty, NoSymbols)
- }
+ protected val NoLocals: Locals = new Locals(
+ Map.empty, Map.empty, Map.empty, Map.empty, Map.empty, NoSymbols)
- private def getIdentifier(sym: SSymbol): Identifier = {
+ protected def getIdentifier(sym: SSymbol): Identifier = {
// TODO: check keywords!
FreshIdentifier(sym.name)
}
- def parseTIPScript: (InoxProgram, Expr) = {
+ protected def parseTIPCommand(token: Tokens.Token)
+ (implicit locals: Locals): (Option[Expr], Locals) = token match {
+ case Tokens.SymbolLit("assert-not") =>
+ (Some(Not(extractExpr(parseTerm))), locals)
- val ctx: InoxContext = InoxContext.empty
- var assertions: Seq[Expr] = Seq.empty
- implicit var locals: Locals = Locals.empty
+ case Tokens.Token(Tokens.Assert) =>
+ (Some(extractExpr(parseTerm)), locals)
- while (peekToken != null) {
- eat(Tokens.OParen)
-
- peekToken match {
- case Tokens.SymbolLit("assert-not") =>
- nextToken // eat the "assert-not" token
- assertions :+= Not(extractExpr(parseTerm))
-
- case Tokens.Token(Tokens.Assert) =>
- nextToken // eat the "assert" token
- assertions :+= extractExpr(parseTerm)
-
- case Tokens.Token(Tokens.DefineFun) | Tokens.Token(Tokens.DefineFunRec) =>
- // eats the "define-fun" or "define-fun-rec" token
- val isRec = nextToken == Tokens.Token(Tokens.DefineFunRec)
- val (tps, funDef) = getPeekToken.kind match {
- case Tokens.OParen =>
- eat(Tokens.OParen)
- eat(Tokens.Par)
- val tps = parseMany(parseSymbol _)
- val res = parseWithin(Tokens.OParen, Tokens.CParen)(parseFunDef _)
- eat(Tokens.CParen)
- (tps, res)
-
- case _ =>
- (Seq.empty[SSymbol], parseFunDef)
- }
+ case Tokens.Token(Tokens.DefineFun) | Tokens.Token(Tokens.DefineFunRec) =>
+ val isRec = token == Tokens.Token(Tokens.DefineFunRec)
+ val (tps, funDef) = getPeekToken.kind match {
+ case Tokens.OParen =>
+ eat(Tokens.OParen)
+ eat(Tokens.Par)
+ val tps = parseMany(parseSymbol _)
+ val res = parseWithin(Tokens.OParen, Tokens.CParen)(parseFunDef _)
+ eat(Tokens.CParen)
+ (tps, res)
- val tpsLocals = locals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
- val fdsLocals = if (!isRec) tpsLocals else {
- tpsLocals.withFunction(funDef.name, extractSignature(funDef, tps)(tpsLocals))
- }
- val fd = extractFunction(funDef, tps)(fdsLocals)
- locals = locals.withFunction(funDef.name, fd)
-
- case Tokens.Token(Tokens.DefineFunsRec) =>
- nextToken // eat the "define-funs-rec" token
- val (funDec, funDecs) = parseOneOrMore(() => {
- eat(Tokens.OParen)
- val (tps, funDec) = getPeekToken.kind match {
- case Tokens.Par =>
- eat(Tokens.Par)
- val tps = parseMany(parseSymbol _)
- val funDec = parseWithin(Tokens.OParen, Tokens.CParen)(parseFunDec _)
- (tps -> funDec)
-
- case _ =>
- (Seq.empty[SSymbol], parseFunDec)
- }
- eat(Tokens.CParen)
- (tps, funDec)
- })
+ case _ =>
+ (Seq.empty[SSymbol], parseFunDef)
+ }
- val (body, bodies) = parseOneOrMore(parseTerm _)
- assert(funDecs.size == bodies.size)
+ val tpsLocals = locals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
+ val fdsLocals = if (!isRec) tpsLocals else {
+ tpsLocals.withFunction(funDef.name, extractSignature(funDef, tps)(tpsLocals))
+ }
+ val fd = extractFunction(funDef, tps)(fdsLocals)
+ (None, locals.withFunction(funDef.name, fd))
+
+ case Tokens.Token(Tokens.DefineFunsRec) =>
+ val (funDec, funDecs) = parseOneOrMore(() => {
+ eat(Tokens.OParen)
+ val (tps, funDec) = getPeekToken.kind match {
+ case Tokens.Par =>
+ eat(Tokens.Par)
+ val tps = parseMany(parseSymbol _)
+ val funDec = parseWithin(Tokens.OParen, Tokens.CParen)(parseFunDec _)
+ (tps -> funDec)
+
+ case _ =>
+ (Seq.empty[SSymbol], parseFunDec)
+ }
+ eat(Tokens.CParen)
+ (tps, funDec)
+ })
- val funDefs = ((funDec -> body) +: (funDecs zip bodies)).map {
- case ((tps, FunDec(name, params, returnSort)), body) =>
- tps -> SMTFunDef(name, params, returnSort, body)
- }
+ val (body, bodies) = parseOneOrMore(parseTerm _)
+ assert(funDecs.size == bodies.size)
- val bodyLocals = locals.withFunctions(for ((tps, funDef) <- funDefs) yield {
- val tpsLocals = locals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
- funDef.name -> extractSignature(funDef, tps)(tpsLocals)
- })
+ val funDefs = ((funDec -> body) +: (funDecs zip bodies)).map {
+ case ((tps, FunDec(name, params, returnSort)), body) =>
+ tps -> SMTFunDef(name, params, returnSort, body)
+ }
- locals = locals.withFunctions(for ((tps, funDef) <- funDefs) yield {
- val tpsLocals = bodyLocals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
- funDef.name -> extractFunction(funDef, tps)(tpsLocals)
- })
+ val bodyLocals = locals.withFunctions(for ((tps, funDef) <- funDefs) yield {
+ val tpsLocals = locals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
+ funDef.name -> extractSignature(funDef, tps)(tpsLocals)
+ })
+
+ (None, locals.withFunctions(for ((tps, funDef) <- funDefs) yield {
+ val tpsLocals = bodyLocals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
+ funDef.name -> extractFunction(funDef, tps)(tpsLocals)
+ }))
+
+ case Tokens.Token(Tokens.DeclareDatatypes) =>
+ val tps = parseMany(parseSymbol _)
+ val datatypes = parseMany(parseDatatypes _)
+
+ var locs = locals.withADTs(datatypes
+ .flatMap { case (sym, conss) => sym +: conss.map(_.sym) }
+ .map(sym => sym -> getIdentifier(sym)))
+
+ val adtLocals = locs.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
+ for ((sym, conss) <- datatypes) {
+ val children = for (Constructor(sym, fields) <- conss) yield {
+ val id = locs.getADT(sym)
+ val vds = fields.map { case (s, sort) =>
+ ValDef(getIdentifier(s), extractType(sort)(adtLocals)).setPos(s.getPos)
+ }
- case Tokens.Token(Tokens.DeclareDatatypes) =>
- nextToken // eat the "declare-datatypes" token
- val tps = parseMany(parseSymbol _)
- val datatypes = parseMany(parseDatatypes _)
+ (id, vds)
+ }
- locals = locals.withADTs(datatypes
- .flatMap { case (sym, conss) => sym +: conss.map(_.sym) }
- .map(sym => sym -> getIdentifier(sym)))
+ val allVds: Set[ValDef] = children.flatMap(_._2).toSet
+ val allTparams: Set[TypeParameter] = children.flatMap(_._2).toSet.flatMap {
+ (vd: ValDef) => locs.symbols.typeParamsOf(vd.tpe): Set[TypeParameter]
+ }
- val adtLocals = locals.withGenerics(tps.map(s => s -> TypeParameter.fresh(s.name).setPos(s.getPos)))
- for ((sym, conss) <- datatypes) {
- val children = for (Constructor(sym, fields) <- conss) yield {
- val id = locals.getADT(sym)
- val vds = fields.map { case (s, sort) =>
- ValDef(getIdentifier(s), extractType(sort)(adtLocals)).setPos(s.getPos)
- }
+ val tparams: Seq[TypeParameterDef] = tps.flatMap { sym =>
+ val tp = adtLocals.getGeneric(sym)
+ if (allTparams(tp)) Some(TypeParameterDef(tp).setPos(sym.getPos)) else None
+ }
- (id, vds)
- }
+ val parent = if (children.size > 1) {
+ val id = adtLocals.getADT(sym)
+ locs = locs.registerADT(
+ new ADTSort(id, tparams, children.map(_._1), Set.empty).setPos(sym.getPos))
+ Some(id)
+ } else {
+ None
+ }
- val allVds: Set[ValDef] = children.flatMap(_._2).toSet
- val allTparams: Set[TypeParameter] = children.flatMap(_._2).toSet.flatMap {
- (vd: ValDef) => locals.symbols.typeParamsOf(vd.tpe): Set[TypeParameter]
- }
+ locs = locals.registerADTs((conss zip children).map { case (cons, (cid, vds)) =>
+ new ADTConstructor(cid, tparams, parent, vds, Set.empty).setPos(cons.sym.getPos)
+ }).withADTSelectors((conss zip children).flatMap { case (Constructor(_, fields), (_, vds)) =>
+ (fields zip vds).map(p => p._1._1 -> p._2.id)
+ })
+ }
- val tparams: Seq[TypeParameterDef] = tps.flatMap { sym =>
- val tp = adtLocals.getGeneric(sym)
- if (allTparams(tp)) Some(TypeParameterDef(tp).setPos(sym.getPos)) else None
- }
+ (None, locs)
+
+ case Tokens.Token(Tokens.DeclareConst) =>
+ val sym = parseSymbol
+ val sort = parseSort
+ (None, locals.withVariable(sym,
+ Variable(getIdentifier(sym), extractType(sort)).setPos(sym.getPos)))
+
+ case Tokens.Token(Tokens.DeclareSort) =>
+ val sym = parseSymbol
+ val arity = parseNumeral.value.toInt
+ val id = getIdentifier(sym)
+ (None, locals.withADT(sym, id).registerADT {
+ val tparams = List.range(0, arity).map {
+ i => TypeParameterDef(TypeParameter.fresh("A" + i).setPos(sym.getPos)).setPos(sym.getPos)
+ }
+ val field = ValDef(FreshIdentifier("val"), IntegerType).setPos(sym.getPos)
- val parent = if (children.size > 1) {
- val id = adtLocals.getADT(sym)
- locals = locals.registerADT(
- new ADTSort(id, tparams, children.map(_._1), Set.empty).setPos(sym.getPos))
- Some(id)
- } else {
- None
- }
+ new ADTConstructor(id, tparams, None, Seq(field), Set.empty)
+ })
- locals = locals.registerADTs((conss zip children).map { case (cons, (cid, vds)) =>
- new ADTConstructor(cid, tparams, parent, vds, Set.empty).setPos(cons.sym.getPos)
- }).withADTSelectors((conss zip children).flatMap { case (Constructor(_, fields), (_, vds)) =>
- (fields zip vds).map(p => p._1._1 -> p._2.id)
- })
- }
+ case Tokens.Token(Tokens.CheckSat) =>
+ // TODO: what do I do with this??
+ (None, locals)
- case Tokens.Token(Tokens.DeclareConst) =>
- nextToken // eat the "declare-const" token
- val sym = parseSymbol
- val sort = parseSort
- locals = locals.withVariable(sym,
- Variable(getIdentifier(sym), extractType(sort)).setPos(sym.getPos))
-
- case Tokens.Token(Tokens.DeclareSort) =>
- nextToken // eat the "declare-const" token
- val sym = parseSymbol
- val arity = parseNumeral.value.toInt
- locals = if (arity == 0) {
- locals.withGeneric(sym, TypeParameter.fresh(sym.name))
- } else {
- val id = getIdentifier(sym)
- locals.withADT(sym, id).registerADT {
- val tparams = List.range(0, arity).map {
- i => TypeParameterDef(TypeParameter.fresh("A" + i).setPos(sym.getPos)).setPos(sym.getPos)
- }
- val field = ValDef(FreshIdentifier("val"), IntegerType).setPos(sym.getPos)
-
- new ADTConstructor(id, tparams, None, Seq(field), Set.empty)
- }
- }
+ case token =>
+ throw new MissformedTIPException("unknown TIP command " + token, token.getPos)
+ }
- case Tokens.Token(Tokens.CheckSat) =>
- // TODO: what do I do with this??
+ def parseTIPScript: (Symbols, Expr) = {
- case token =>
- throw new MissformedTIPException("unknown TIP command " + token, token.getPos)
- }
+ var assertions: Seq[Expr] = Seq.empty
+ implicit var locals: Locals = NoLocals
+ while (peekToken != null) {
+ eat(Tokens.OParen)
+ val (newAssertions, newLocals) = parseTIPCommand(nextToken)
+ assertions ++= newAssertions
+ locals = newLocals
eat(Tokens.CParen)
}
val expr: Expr = locals.symbols.andJoin(assertions)
- val program = InoxProgram(ctx, locals.symbols)
- (program, expr)
+ (locals.symbols, expr)
}
override protected def parseTermWithoutParens: Term = getPeekToken match {
@@ -372,7 +377,7 @@ trait TIPParser {
}
}
- private def extractExpr(term: Term)(implicit locals: Locals): Expr = (term match {
+ protected def extractExpr(term: Term)(implicit locals: Locals): Expr = (term match {
case FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("assume")), None), Seq(pred, body)) =>
Assume(extractExpr(pred), extractExpr(body))
@@ -594,7 +599,7 @@ trait TIPParser {
}).setPos(term.getPos)
- private def extractType(sort: Sort)(implicit locals: Locals): Type = (sort match {
+ protected def extractType(sort: Sort)(implicit locals: Locals): Type = (sort match {
case Sort(SMTIdentifier(SSymbol("bitvector"), Seq(SNumeral(n))), Seq()) => BVType(n.toInt)
case Sort(SimpleIdentifier(SSymbol("Bool")), Seq()) => BooleanType
case Sort(SimpleIdentifier(SSymbol("Int")), Seq()) => IntegerType
@@ -621,3 +626,13 @@ trait TIPParser {
}).setPos(sort.id.symbol.getPos)
}
}
+
+object TIPParser {
+ def parse(file: File): (inox.trees.Symbols, inox.trees.Expr) = new TIPParser {
+ val trees: inox.trees.type = inox.trees
+ }.parse(file)
+
+ def parse(reader: Reader): (inox.trees.Symbols, inox.trees.Expr) = new TIPParser {
+ val trees: inox.trees.type = inox.trees
+ }.parse(reader)
+}
diff --git a/src/main/scala/inox/solvers/smtlib/Z3Target.scala b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
index ccff47697..5d8e30703 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
@@ -66,9 +66,8 @@ trait Z3Target extends SMTLIBTarget {
override protected def fromSMT(t: Term, otpe: Option[Type] = None)
(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
(t, otpe) match {
- case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe)) =>
+ case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe @ MapType(keyType, valueType))) =>
if (letDefs contains k) {
- val MapType(keyType, valueType) = tpe
val DefineFun(SMTFunDef(a, Seq(SortedVar(arg, akind)), rkind, body)) = letDefs(k)
def extractCases(e: Term): (Map[Expr, Expr], Expr) = e match {
@@ -85,13 +84,39 @@ trait Z3Target extends SMTLIBTarget {
throw FatalError("Array on non-function or unknown symbol "+k)
}
+ case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe @ SetType(base))) =>
+ val fm @ FiniteMap(cases, dflt, _) = fromSMT(t, Some(MapType(base, BooleanType)))
+ if (dflt != BooleanLiteral(false)) unsupported(fm, "Solver returned a co-finite set which is not supported")
+ FiniteSet(cases.collect { case (k, BooleanLiteral(true)) => k }, base)
+
+ case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe @ BagType(base))) =>
+ val fm @ FiniteMap(cases, dflt, _) = fromSMT(t, Some(MapType(base, IntegerType)))
+ if (dflt != IntegerLiteral(0)) unsupported(fm, "Solver returned a co-finite bag which is not supported")
+ FiniteBag(cases.filter(_._2 != IntegerLiteral(BigInt(0))), base)
+
case (FunctionApplication(
QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), Some(ArraysEx.ArraySort(k, v))),
Seq(defV)
- ), Some(tpe)) =>
+ ), Some(tpe: MapType)) =>
val ktpe = sorts.fromB(k)
val vtpe = sorts.fromB(v)
- FiniteMap(Seq(), fromSMT(defV), ktpe)
+ FiniteMap(Seq(), fromSMT(defV, Some(vtpe)), ktpe)
+
+ case (FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), Some(ArraysEx.ArraySort(k, v))),
+ Seq(defV)
+ ), Some(tpe @ SetType(base))) =>
+ val dflt = fromSMT(defV, Some(BooleanType))
+ if (dflt != BooleanLiteral(false)) unsupported(dflt, "Solver returned a co-finite set which is not supported")
+ FiniteSet(Seq.empty, base)
+
+ case (FunctionApplication(
+ QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), Some(ArraysEx.ArraySort(k, v))),
+ Seq(defV)
+ ), Some(tpe @ BagType(base))) =>
+ val dflt = fromSMT(defV, Some(IntegerType))
+ if (dflt != IntegerLiteral(BigInt(0))) unsupported(dflt, "Solver returned a co-finite bag which is not supported")
+ FiniteBag(Seq.empty, base)
case _ =>
super.fromSMT(t, otpe)
--
GitLab