add support for $mul, $div, $divfloor, $mod, $modfloor, $pow in functional backend

This commit is contained in:
Emily Schmidt
2024-08-21 11:02:31 +01:00
parent 50f487e08c
commit 1b2986f7fb
5 changed files with 177 additions and 11 deletions
+6
View File
@@ -119,6 +119,12 @@ template <class NodeNames> struct SmtPrintVisitor {
std::string sub(Node, Node a, Node b, int) { return format("(bvsub %0 %1)", np(a), np(b)); }
std::string mul(Node, Node a, Node b, int) { return format("(bvmul %0 %1)", np(a), np(b)); }
std::string unsigned_div(Node, Node a, Node b, int) { return format("(bvudiv %0 %1)", np(a), np(b)); }
std::string unsigned_mod(Node, Node a, Node b, int) { return format("(bvurem %0 %1)", np(a), np(b)); }
std::string bitwise_and(Node, Node a, Node b, int) { return format("(bvand %0 %1)", np(a), np(b)); }
std::string bitwise_or(Node, Node a, Node b, int) { return format("(bvor %0 %1)", np(a), np(b)); }