Making some arithmetic ops n-ary

Author: mario-bucev

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

@@ -51,6 +51,7 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
 
   {
+    import theories.Core.Equals
     import theories.Ints._
     val theoryString = "Theory of Ints"
     var counter = 0
@@ -84,9 +85,22 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
     val f8 = LessEquals(Sub(NumeralLit(5), NumeralLit(3)), NumeralLit(1))
     mkTest(f8, UnsatStatus, uniqueName())
+
+    val f9 = Equals(Add(NumeralLit(1), NumeralLit(2), NumeralLit(3), NumeralLit(4)), NumeralLit(10))
+    mkTest(f9, SatStatus, uniqueName())
+
+    val f10 = Equals(Sub(NumeralLit(1), NumeralLit(2), NumeralLit(3), NumeralLit(4)), NumeralLit(-8))
+    mkTest(f10, SatStatus, uniqueName())
+
+    val f11 = Equals(Mul(NumeralLit(1), NumeralLit(2), NumeralLit(3), NumeralLit(4)), NumeralLit(24))
+    mkTest(f11, SatStatus, uniqueName())
+
+    val f12 = Equals(Div(NumeralLit(80), NumeralLit(4), NumeralLit(2)), NumeralLit(10))
+    mkTest(f12, SatStatus, uniqueName())
   }
 
   {
+    import theories.Core.Equals
     import theories.Reals._
     val theoryString = "Theory of Reals"
     var counter = 0
@@ -116,6 +130,18 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
     val f8 = LessEquals(Sub(NumeralLit(5), NumeralLit(3)), NumeralLit(1))
     mkTest(f8, UnsatStatus, uniqueName())
+
+    val f9 = Equals(Add(NumeralLit(1), NumeralLit(2), NumeralLit(3), NumeralLit(4)), NumeralLit(10))
+    mkTest(f9, SatStatus, uniqueName())
+
+    val f10 = Equals(Sub(NumeralLit(1), NumeralLit(2), NumeralLit(3), NumeralLit(4)), NumeralLit(-8))
+    mkTest(f10, SatStatus, uniqueName())
+
+    val f11 = Equals(Mul(NumeralLit(1), NumeralLit(2), NumeralLit(3), NumeralLit(4)), NumeralLit(24))
+    mkTest(f11, SatStatus, uniqueName())
+
+    val f12 = Equals(Div(NumeralLit(80), NumeralLit(4), NumeralLit(2)), NumeralLit(10))
+    mkTest(f12, SatStatus, uniqueName())
   }
 
   {
@@ -181,5 +207,11 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
     // Int2BV does not care about the sign
     val f17 = Equals(Int2BV(8, NumeralLit(-214)), BitVectorConstant(42, 8))
     mkTest(f17, SatStatus, uniqueName())
+
+    val f18 = Equals(Add(BitVectorConstant(1, 32), BitVectorConstant(2, 32), BitVectorConstant(3, 32), BitVectorConstant(4, 32)), BitVectorConstant(10, 32))
+    mkTest(f18, SatStatus, uniqueName())
+
+    val f20 = Equals(Mul(BitVectorConstant(1, 32), BitVectorConstant(2, 32), BitVectorConstant(3, 32), BitVectorConstant(4, 32)), BitVectorConstant(24, 32))
+    mkTest(f20, SatStatus, uniqueName())
   }
 }

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

@@ -56,7 +56,7 @@ object FixedSizeBitVectors {
   }
 
 
-  object Concat extends Operation2 { override val name = "concat" }
+  object Concat extends OperationN1 { override val name = "concat" }
 
   object Not extends Operation1 { override val name = "bvnot" }
   object Neg extends Operation1 { override val name = "bvneg" }
@@ -68,9 +68,9 @@ object FixedSizeBitVectors {
   object XNOr extends Operation2 { override val name = "bvxnor" }
 
   object Comp extends Operation2 { override val name = "bvcomp" }
-  object Add extends Operation2 { override val name = "bvadd" }
+  object Add extends OperationN1 { override val name = "bvadd" }
   object Sub extends Operation2 { override val name = "bvsub" }
-  object Mul extends Operation2 { override val name = "bvmul" }
+  object Mul extends OperationN1 { override val name = "bvmul" }
   object UDiv extends Operation2 { override val name = "bvudiv" }
   object SDiv extends Operation2 { override val name = "bvsdiv" }
   object URem extends Operation2 { override val name = "bvurem" }

src/main/scala/smtlib/theories/Ints.scala

@@ -42,10 +42,10 @@ object Ints {
   }
 
   object Neg extends Operation1 { override val name = "-" }
-  object Add extends Operation2 { override val name = "+" }
-  object Sub extends Operation2 { override val name = "-" }
-  object Mul extends Operation2 { override val name = "*" }
-  object Div extends Operation2 { override val name = "div" }
+  object Add extends OperationN1 { override val name = "+" }
+  object Sub extends OperationN1 { override val name = "-" }
+  object Mul extends OperationN1 { override val name = "*" }
+  object Div extends OperationN1 { override val name = "div" }
   object Mod extends Operation2 { override val name = "mod" }
   object Abs extends Operation1 { override val name = "abs" }
 

src/main/scala/smtlib/theories/Reals.scala

@@ -28,7 +28,7 @@ object Reals {
       case _ => None
     }
   }
-  
+
   object DecimalLit {
     def apply(value: BigDecimal): Term = SDecimal(value)
     def unapply(term: Term): Option[BigDecimal] = term match {
@@ -38,10 +38,10 @@ object Reals {
   }
 
   object Neg extends Operation1 { override val name = "-" }
-  object Add extends Operation2 { override val name = "+" }
-  object Sub extends Operation2 { override val name = "-" }
-  object Mul extends Operation2 { override val name = "*" }
-  object Div extends Operation2 { override val name = "/" }
+  object Add extends OperationN1 { override val name = "+" }
+  object Sub extends OperationN1 { override val name = "-" }
+  object Mul extends OperationN1 { override val name = "*" }
+  object Div extends OperationN1 { override val name = "/" }
 
   object LessThan extends Operation2 { override val name = "<" }
   object LessEquals extends Operation2 { override val name = "<=" }