Update BitVectorExpressions.kt

tudo-aqua · Mar 31, 2024 · 68aca00 · 68aca00
1 parent f4dd11f
commit 68aca00
Showing 1 changed file with 19 additions and 0 deletions.
diff --git a/src/main/kotlin/tools/aqua/konstraints/theories/BitVectorExpressions.kt b/src/main/kotlin/tools/aqua/konstraints/theories/BitVectorExpressions.kt
@@ -555,3 +555,22 @@ object BVUltDecl :
       bindings: Bindings
   ): Expression<BoolSort> = BVUlt(param1, param2)
 }
+
+fun BVNAnd(lhs: Expression<BVSort>, rhs: Expression<BVSort>) : Expression<BVSort> = BVNot(BVAnd(lhs, rhs))
+
+object BVNAndDecl :
+        FunctionDecl2<BVSort, BVSort, BVSort>(
+            "bvnand".symbol(),
+            emptySet(),
+            BVSort.fromSymbol("m"),
+            BVSort.fromSymbol("m"),
+            emptySet(),
+            setOf(SymbolIndex("m")),
+            BVSort.fromSymbol("m")
+        ) {
+    override fun buildExpression(
+        param1: Expression<BVSort>,
+        param2: Expression<BVSort>,
+        bindings: Bindings
+    ): Expression<BVSort> = BVNAnd(param1, param2)
+}