Merge pull request #132 from jad-hamza/cvc4-1.8

Minor fixes for CVC4 1.8
epfl-lara · Apr 15, 2021 · 93550f1 · 93550f1
2 parents 6dfb351 + d51ea2c
commit 93550f1
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 24 deletions.
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
@@ -24,7 +24,6 @@ trait CVC4Solver extends SMTLIBSolver with CVC4Target {
       "--produce-models",
       "--incremental",
       // "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
-      "--rewrite-divk",
       "--print-success",
       "--lang", "smt2.5"
     ) ++ options.findOptionOrDefault(optCVC4Options)

diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala
@@ -81,15 +81,20 @@ trait SMTLIBParser {
       case _ => IntegerLiteral(n)
     }
 
-    case FixedSizeBitVectors.BitVectorLit(bs) => otpe match {
-      case Some(BVType(signed, _)) =>
-        BVLiteral(signed, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size)
-      case _ =>
-        BVLiteral(true, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size)
-    }
+    case FixedSizeBitVectors.BitVectorLit(bs) =>
+      otpe match {
+        case Some(BVType(signed, _)) =>
+          BVLiteral(signed, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size)
+        case Some(CharType()) =>
+          val bv = BVLiteral(true, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, 16)
+          CharLiteral(bv.toBigInt.toInt.toChar)
+        case _ =>
+          BVLiteral(true, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size)
+      }
 
     case FixedSizeBitVectors.BitVectorConstant(n, size) => otpe match {
       case Some(BVType(signed, _)) => BVLiteral(signed, n, size.intValue)
+      case Some(CharType()) => CharLiteral(n.toChar)
       case _ => BVLiteral(true, n, size.intValue)
     }
 

diff --git a/src/main/scala/inox/utils/ASCIIHelpers.scala b/src/main/scala/inox/utils/ASCIIHelpers.scala
@@ -72,23 +72,23 @@ object ASCIIHelpers {
 
       val sb = new StringBuffer
 
-      val barH = if (asciiOnly) "#" else "─"
-      val topLeft = if (asciiOnly) "#" else "┌"
-      val topRight = if (asciiOnly) "#" else "┐"
-      val bottomLeft = if (asciiOnly) "#" else "└"
-      val bottomRight = if (asciiOnly) "#" else "┘"
+      val barH = if (asciiOnly) "" else "─"
+      val topLeft = if (asciiOnly) "" else "┌"
+      val topRight = if (asciiOnly) "" else "┐"
+      val bottomLeft = if (asciiOnly) "" else "└"
+      val bottomRight = if (asciiOnly) "" else "┘"
       val dots = if (asciiOnly) "." else "┄"
-      val doubleBarH = if (asciiOnly) "#" else "═"
-      val doubleBarV = if (asciiOnly) "#" else "║"
-      val doubleTopLeft = if (asciiOnly) "#" else "╔"
-      val doubleTopRight = if (asciiOnly) "#" else "╗"
-      val doubleBottomLeft = if (asciiOnly) "#" else "╚"
-      val doubleBottomRight = if (asciiOnly) "#" else "╝"
-
-      val leftConnect = if (asciiOnly) "#" else "╡"
-      val rightConnect = if (asciiOnly) "#" else "╞"
-      val doubleRightConnect = if (asciiOnly) "#" else "╟"
-      val doubleLeftConnect = if (asciiOnly) "#" else "╢"
+      val doubleBarH = if (asciiOnly) "" else "═"
+      val doubleBarV = if (asciiOnly) "" else "║"
+      val doubleTopLeft = if (asciiOnly) "" else "╔"
+      val doubleTopRight = if (asciiOnly) "" else "╗"
+      val doubleBottomLeft = if (asciiOnly) "" else "╚"
+      val doubleBottomRight = if (asciiOnly) "" else "╝"
+
+      val leftConnect = if (asciiOnly) "" else "╡"
+      val rightConnect = if (asciiOnly) "" else "╞"
+      val doubleRightConnect = if (asciiOnly) "" else "╟"
+      val doubleLeftConnect = if (asciiOnly) "" else "╢"
 
       sb append s"  $topLeft$barH" + (barH * titleWidth) + s"$barH$topRight\n"
       sb append s"$doubleTopLeft$doubleBarH$leftConnect " + title + s" $rightConnect" + (doubleBarH * padWidth) + s"$doubleTopRight\n"
@@ -99,7 +99,7 @@ object ASCIIHelpers {
           sb append doubleRightConnect + (dots * fullWidth) + s"$doubleLeftConnect\n"
 
         case Row(cells) =>
-          sb append s"$doubleBarV "
+          if (!asciiOnly) sb append s"$doubleBarV "
           var i = 0
           for (c <- cells) {
             if (i > 0) {