Insts

src/btoropt/parser.py

@@ -187,13 +187,18 @@ def parse_inst(line: str, p: list[Instruction]) -> Instruction:
         case "output":
             # Sanity check: verify that instruction is well formed
             assert len(inst) >= 3,\
-                "input instruction must be of the form: <lid> output <opid>. Found: " + line
+                "output instruction must be of the form: <lid> output <opid> [name]. Found: " + line
 
             # Find the op associated to this instruction
             out = find_inst(p, int(inst[2]))
 
+            if len(inst) >= 4:
+                name = inst[3].strip()
+            else:
+                name = f"output_{inst[0]}"
+
             # Construct instruction
-            op = Output(lid, out)
+            op = Output(lid, out, name)
 
         case "bad":
             # Sanity check: verify that instruction is well formed
@@ -461,6 +466,33 @@ def parse_inst(line: str, p: list[Instruction]) -> Instruction:
             # Construct instruction
             op = Smod(lid, sort, op1, op2)
 
+        case "srem":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> srem <sid> <op1> <op2>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            op1 = find_inst(p, int(inst[3]))
+            op2 = find_inst(p, int(inst[4]))
+
+            # Construct instruction
+            op = Srem(lid, sort, op1, op2)
+
+        case "urem":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> urem <sid> <op1> <op2>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            op1 = find_inst(p, int(inst[3]))
+            op2 = find_inst(p, int(inst[4]))
+
+            # Construct instruction
+            op = Urem(lid, sort, op1, op2)
+
+
         case "sll":
             # Sanity check: verify that instruction is well formed
             assert len(inst) >= 5,\

src/btoropt/program.py

@@ -22,8 +22,9 @@
 tags = ["sort","input", "output", "bad", "constraint", "zero",
         "one", "ones", "constd", "consth", "const", "state",
         "init", "next", "slice", "ite", "implies", "iff",
-        "add", "sub", "mul", "sdiv", "udiv", "smod", "sll",
-        "srl", "sra", "and", "or", "xor", "concat", 
+        "add", "sub", "mul", "sdiv", "udiv", "smod", 
+        "srem", "urem", "sll", "srl", "sra", "and", 
+        "or", "xor", "concat", 
         # Unary operations
         "not", "inc", "dec", "neg", "redor", "redxor", "redand",
         "eq", "neq", "ugt", "sgt", "ugte", "sgte", "ult",
@@ -119,8 +120,9 @@ def serialize(self) -> str:
 
 
 class Output(Instruction):
-    def __init__(self, lid: int, out: Instruction):
+    def __init__(self, lid: int, out: Instruction, name: str):
         super().__init__(lid, "output", [out])
+        self.name = name
 
 ## Unary Instructions ##
 
@@ -285,6 +287,14 @@ class Smod(Instruction):
     def __init__(self, lid: int, sort: Sort, op1: Instruction, op2: Instruction):
         super().__init__(lid, "smod", [sort, op1, op2])
 
+class Srem(Instruction):
+    def __init__(self, lid: int, sort: Sort, op1: Instruction, op2: Instruction):
+        super().__init__(lid, "srem", [sort, op1, op2])
+
+class Urem(Instruction):
+    def __init__(self, lid: int, sort: Sort, op1: Instruction, op2: Instruction):
+        super().__init__(lid, "urem", [sort, op1, op2])
+
 class Sll(Instruction):
     def __init__(self, lid: int, sort: Sort, op1: Instruction, op2: Instruction):
         super().__init__(lid, "sll", [sort, op1, op2])