From 584168d714d3dee458670cbfc1aa62a16571abe7 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 13 Nov 2015 15:01:25 +0100
Subject: [PATCH] use experimental sets
---
build.sbt | 2 +-
.../solvers/smtlib/SMTLIBCVC4Target.scala | 31 ++++++-------------
2 files changed, 11 insertions(+), 22 deletions(-)
diff --git a/build.sbt b/build.sbt
index ac8fae6e2..6517cf1e6 100644
--- a/build.sbt
+++ b/build.sbt
@@ -143,7 +143,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
-lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "3b6ef4992b6af15d08a7320fd12202f35e97b905")
+lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "372bb14d0c84953acc17f9a7e1592087adb0a3e1")
lazy val root = (project in file(".")).
configs(RegressionTest, IsabelleTest, IntegrTest).
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 3173dd652..6e131fda7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -12,6 +12,7 @@ import purescala.Types._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Forall => SMTForall, _}
import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
+import _root_.smtlib.theories.experimental.Sets
trait SMTLIBCVC4Target extends SMTLIBTarget {
@@ -27,7 +28,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
sorts.cachedB(tpe) {
tpe match {
case SetType(base) =>
- Sort(SMTIdentifier(SSymbol("Set")), Seq(declareSort(base)))
+ Sets.SetSort(declareSort(base))
case _ =>
super.declareSort(t)
@@ -119,36 +120,24 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
*/
case fs @ FiniteSet(elems, _) =>
if (elems.isEmpty) {
- QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset")), Some(declareSort(fs.getType)))
+ Sets.EmptySet(declareSort(fs.getType))
} else {
val selems = elems.toSeq.map(toSMT)
- val sgt = FunctionApplication(SSymbol("singleton"), Seq(selems.head))
+ val sgt = Sets.Singleton(selems.head)
if (selems.size > 1) {
- FunctionApplication(SSymbol("insert"), selems.tail :+ sgt)
+ Sets.Insert(selems.tail :+ sgt)
} else {
sgt
}
}
- case SubsetOf(ss, s) =>
- FunctionApplication(SSymbol("subset"), Seq(toSMT(ss), toSMT(s)))
-
- case ElementOfSet(e, s) =>
- FunctionApplication(SSymbol("member"), Seq(toSMT(e), toSMT(s)))
-
- case SetCardinality(s) =>
- FunctionApplication(SSymbol("card"), Seq(toSMT(s)))
-
- case SetDifference(a, b) =>
- FunctionApplication(SSymbol("setminus"), Seq(toSMT(a), toSMT(b)))
-
- case SetUnion(a, b) =>
- FunctionApplication(SSymbol("union"), Seq(toSMT(a), toSMT(b)))
-
- case SetIntersection(a, b) =>
- FunctionApplication(SSymbol("intersection"), Seq(toSMT(a), toSMT(b)))
+ case SubsetOf(ss, s) => Sets.Subset(toSMT(ss), toSMT(s))
+ case ElementOfSet(e, s) => Sets.Member(toSMT(e), toSMT(s))
+ case SetDifference(a, b) => Sets.Setminus(toSMT(a), toSMT(b))
+ case SetUnion(a, b) => Sets.Union(toSMT(a), toSMT(b))
+ case SetIntersection(a, b) => Sets.Intersection(toSMT(a), toSMT(b))
case _ =>
super.toSMT(e)
--
GitLab