Adding int2bv and bv2nat

Author: mario-bucev

src/it/scala/smtlib/it/TheoriesBuilderTests.scala

@@ -59,7 +59,7 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
       "%d - %s".format(counter, theoryString)
     }
 
-    
+
     val f1 = GreaterEquals(NumeralLit(42), NumeralLit(12))
     mkTest(f1, SatStatus, uniqueName())
 
@@ -95,7 +95,7 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
       "%d - %s".format(counter, theoryString)
     }
 
-    
+
     val f1 = GreaterEquals(NumeralLit(42), NumeralLit(12))
     mkTest(f1, SatStatus, uniqueName())
 
@@ -119,6 +119,8 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
   }
 
   {
+    import theories.Core.Equals
+    import theories.Ints.NumeralLit
     import theories.FixedSizeBitVectors._
     val theoryString = "Theory of Bit Vectors"
     var counter = 0
@@ -127,7 +129,6 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
       "%d - %s".format(counter, theoryString)
     }
 
-    
     val f1 = SGreaterEquals(BitVectorConstant(42, 32), BitVectorConstant(12, 32))
     mkTest(f1, SatStatus, uniqueName())
 
@@ -160,5 +161,25 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
     val f11 = UGreaterEquals(BitVectorLit(List(true, false)), BitVectorLit(List(true, false)))
     mkTest(f11, SatStatus, uniqueName())
+
+    val f12 = Equals(Int2BV(8, NumeralLit(42)), BitVectorConstant(42, 8))
+    mkTest(f12, SatStatus, uniqueName())
+
+    val f13 = Equals(BV2Nat(BitVectorConstant(42, 8)), NumeralLit(42))
+    mkTest(f13, SatStatus, uniqueName())
+
+    val f14 = Equals(Int2BV(8, NumeralLit(24)), BitVectorConstant(123, 8))
+    mkTest(f14, UnsatStatus, uniqueName())
+
+    val f15 = Equals(BV2Nat(BitVectorConstant(42, 8)), NumeralLit(123))
+    mkTest(f15, UnsatStatus, uniqueName())
+
+    // Testing that Int2BV wraps around for integer exceeding the BV size
+    val f16 = Equals(Int2BV(8, NumeralLit(42 + 256*3)), BitVectorConstant(42, 8))
+    mkTest(f16, SatStatus, uniqueName())
+
+    // Int2BV does not care about the sign
+    val f17 = Equals(Int2BV(8, NumeralLit(-214)), BitVectorConstant(42, 8))
+    mkTest(f17, SatStatus, uniqueName())
   }
 }

src/main/scala/smtlib/printer/PrintingContext.scala

@@ -170,7 +170,9 @@ class PrintingContext(writer: Writer) {
         print(id)
     }
 
-    case SNumeral(value) => print(value.toString)
+    case SNumeral(value) =>
+      if (value >= 0) print(value.toString)
+      else print(s"(- ${-value})")
     case SHexadecimal(value) => print(value.toString)
     case SBinary(value) => print("#b" + value.map(if(_) "1" else "0").mkString)
     case SDecimal(value) => print(value.toString)
@@ -341,7 +343,7 @@ class PrintingContext(writer: Writer) {
   }
 
   protected def printCommandResponse(response: CommandResponse): Unit = response match {
-    case Success => 
+    case Success =>
       print("success\n")
 
     case Unsupported =>

src/main/scala/smtlib/theories/FixedSizeBitVectors.scala

@@ -90,13 +90,17 @@ object FixedSizeBitVectors {
   object LShiftRight extends Operation2 { override val name = "bvlshr" }
   object AShiftRight extends Operation2 { override val name = "bvashr" }
 
+  object BV2Nat extends Operation1 { override val name = "bv2nat" }
 
   object Extract {
-    def apply(i: BigInt, j: BigInt, t: Term): Term =
+    def apply(i: BigInt, j: BigInt, t: Term): Term = {
+      require(i >= j)
       FunctionApplication(
         QualifiedIdentifier(Identifier(SSymbol("extract"), Seq(SNumeral(i), SNumeral(j)))),
         Seq(t)
       )
+    }
+
     def unapply(term: Term): Option[(BigInt, BigInt, Term)] = term match {
       case FunctionApplication(
         QualifiedIdentifier(
@@ -197,4 +201,20 @@ object FixedSizeBitVectors {
     }
   }
 
+  object Int2BV {
+    def apply(m: BigInt, t: Term): Term =
+      FunctionApplication(
+        QualifiedIdentifier(Identifier(SSymbol("int2bv"), Seq(SNumeral(m)))),
+        Seq(t)
+      )
+    def unapply(term: Term): Option[(BigInt, Term)] = term match {
+      case FunctionApplication(
+        QualifiedIdentifier(
+          Identifier(SSymbol("int2bv"), Seq(SNumeral(m))),
+          None
+        ), Seq(t)) => Some((m, t))
+      case _ => None
+    }
+  }
+
 }