Re-introduce secific CVC4 implementations, fix scala-smtlib

project/Build.scala

@@ -80,6 +80,6 @@ object Leon extends Build {
     def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
     lazy val bonsai      = project("git://github.com/colder/bonsai.git",     "8f485605785bda98ac61885b0c8036133783290a")
-    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e676aab157382847b27eb436b43d2e0abd8e29ba")
+    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "acd60b52bac56e47ef1b855d91a1515a6d9178de")
   }
 }

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala

@@ -60,42 +60,42 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
   }
 
   override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]) = e match {
-    //case a @ FiniteArray(elems) =>
-    //  val tpe @ ArrayType(base) = normalizeType(a.getType)
-    //  declareSort(tpe)
+    case a @ FiniteArray(elems) =>
+      val tpe @ ArrayType(base) = normalizeType(a.getType)
+      declareSort(tpe)
 
-    //  var ar: SExpr = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
+      var ar: Term = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
 
-    //  for ((e, i) <- elems.zipWithIndex) {
-    //    ar = SList(SSymbol("store"), ar, toSMT(IntLiteral(i)), toSMT(e))
-    //  }
+      for ((e, i) <- elems.zipWithIndex) {
+        ar = FunctionApplication(SSymbol("store"), Seq(ar, toSMT(IntLiteral(i)), toSMT(e)))
+      }
 
-    //  SList(constructors.toB(tpe), toSMT(IntLiteral(elems.size)), ar)
+      FunctionApplication(constructors.toB(tpe), Seq(toSMT(IntLiteral(elems.size)), ar))
 
-    ///**
-    // * ===== Set operations =====
-    // */
-    //case fs @ FiniteSet(elems) =>
-    //  if (elems.isEmpty) {
-    //    SList(SSymbol("as"), SSymbol("emptyset"), declareSort(fs.getType))
-    //  } else {
-    //    SList(SSymbol("setenum") :: elems.map(toSMT).toList)
-    //  }
+    /**
+     * ===== Set operations =====
+     */
+    case fs @ FiniteSet(elems) =>
+      if (elems.isEmpty) {
+        QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset")), Some(declareSort(fs.getType)))
+      } else {
+        FunctionApplication(SSymbol("singleton"), elems.toSeq.map(toSMT))
+      }
 
-    //case SubsetOf(ss, s) =>
-    //  SList(SSymbol("subseteq"), toSMT(ss), toSMT(s))
+    case SubsetOf(ss, s) =>
+      FunctionApplication(SSymbol("subseteq"), Seq(toSMT(ss), toSMT(s)))
 
-    //case ElementOfSet(e, s) =>
-    //  SList(SSymbol("in"), toSMT(e), toSMT(s))
+    case ElementOfSet(e, s) =>
+      FunctionApplication(SSymbol("in"), Seq(toSMT(e), toSMT(s)))
 
-    //case SetDifference(a, b) =>
-    //  SList(SSymbol("setminus"), toSMT(a), toSMT(b))
+    case SetDifference(a, b) =>
+      FunctionApplication(SSymbol("setminus"), Seq(toSMT(a), toSMT(b)))
 
-    //case SetUnion(a, b) =>
-    //  SList(SSymbol("union"), toSMT(a), toSMT(b))
+    case SetUnion(a, b) =>
+      FunctionApplication(SSymbol("union"), Seq(toSMT(a), toSMT(b)))
 
-    //case SetIntersection(a, b) =>
-    //  SList(SSymbol("intersection"), toSMT(a), toSMT(b))
+    case SetIntersection(a, b) =>
+      FunctionApplication(SSymbol("intersection"), Seq(toSMT(a), toSMT(b)))
 
     case _ =>
       super[SMTLIBTarget].toSMT(e)