Repository: dobios/btor2-opt (language: python)

Issue:
Add support for modularity
In order to simplify the benchmarking of the recently introduced [contract system in CIRCT](https://circt.llvm.org/docs/Dialects/Verif/#contracts), we should artificially introduce the concept of modularity to btor2. Let's illustrate what I mean with an example, where we will take the [reg_en example](https://github.com/dobios/btor2-opt/blob/main/tests/btor/reg_en.btor) and update it to encode the following hoare triple `{A.d=0} reg_en {A.q>0}`:
```btor
module A {
    1 sort bitvec 32
    2 input 1 A.d 
    3 sort bitvec 1
    4 input 3 A.en 
    5 input 3 A.rst 
    6 input 1 B.d 
    7 input 3 B.en 
    8 input 3 B.rst 
    9 input 3 clk
    10 state 1 A.q
    11 output 10 qA 
    12 state 1 B.q
    13 output 12 qB 
    14 uext 3 9 0 A.clk 
    15 uext 3 9 0 B.clk 
    16 ite 1 4 2 10
    17 const 1 00000000000000000000000000000000
    18 ite 1 5 17 16
    19 next 1 10 18
    20 ite 1 7 6 12
    21 ite 1 8 17 20
    22 next 1 12 21
}
contract A {
    1 sort bitvec 1
    2 ref A 1
    3 const 2 0
    4 ref A 2
    5 eq 1 4 2
    6 prec 3
    7 ref A 10
    8 gt 1 7 2
    9 post 5  
}
module C {
    1 sort bitvec 32
    2 input 1 C.i
    3 inst A ; will either inline A or replace it with its contract
    4 ref A 1
    5 set 3 4 2 
    6 sort bitvec 1
    7 const 1 0
    8 ref A 10
    9 eq 1 7 6
    10 bad 7 
}
```  
The new constructs introduced here are:  
- `module <name> {...}` : Wraps a series of operations into a block that can be referred to by name.  
- `contract <existing_name>`: Associates a contract (preconditions and post conditions) to an existing module.
- `inst <existing_name>`: Create an instance of a module.
- `ref` <existing_name> <line>: Create a local reference to a line in another named block.
- `set <instance_id> <ref_id> <driver_id>`: Sets an instance's input to an operation result. This will require that the "driver" operation meet the preconditions set in the module's contract.

Using this structure, when enabled, the preconditions will be asserted in the module that instantiates the contract, and the postconditions will be assumed (turned into btor2 constraints). This will allow for the quick benchmarking of various modularization and solver parallelization methods. Btor-opt should take this as input and yield valid standard btor2: one file per module, where verifying a contract requires:
- *Module*: Assume preconditions, check module, assert postconditions  
- *Instance*: Assert preconditions on set inputs, assume postconditions  



Discussion / hints:

Fix patch:
diff --git a/src/btoropt/__main__.py b/src/btoropt/__main__.py
index 6698a89..7f490f1 100644
--- a/src/btoropt/__main__.py
+++ b/src/btoropt/__main__.py
@@ -21,22 +21,42 @@
 from .parser import *
 import sys
 
+options = ["modular"]
+
 def main():
     # Retrieve flags
     if len(sys.argv) < 3:
-        print("Usage: btoropt <file.btor2> <pass_names_in_order> ...")
+        print("Usage: btoropt [optional](--modular) <file.btor2> <pass_names_in_order> ...")
         exit(1)
 
+    # Check options
+    base = 1
+    modular = False
+    if "--" in sys.argv[1].strip():
+        option = sys.argv[1].strip().strip("--")
+        if option not in options:
+            print(f"Invalid option given: {option}")
+            exit(1)
+        modular = True
+        base += 1
+        
+
     # Retrieve design
     btor2str: list[str] = []
-    with open(sys.argv[1], "r") as f:
+    with open(sys.argv[base], "r") as f:
         btor2str = f.readlines()
 
     # Parse the design
-    btor2: list[Instruction] = parse(btor2str)
+    btor2 = None
+    if modular:
+        btor2 = parse_file(btor2str)
+    else:
+        btor2 = parse(btor2str)
+    
+    assert btor2 is not None
 
     # Check that the given pass names are valid
-    for name in sys.argv[1:]:
+    for name in sys.argv[base:]:
         if find_pass(all_passes, name) is None:
             print(f"Invalid pass given as argument: {name}")
             exit(1)
@@ -46,10 +66,16 @@ def main():
 
     # Run all passes in the pipeline
     for p in pipeline:
-        btor2 = p.run(btor2)
+        if modular: 
+            btor2 = p.runOnProgram(btor2)
+        else:
+            btor2 = p.run(btor2)
 
     # Show the result to the user
-    print(serialize_p(btor2))
+    if(modular):
+        print(serialize_p(btor2))
+    else:
+        print("Success")
 
 if __name__ == "__main__":
     main()
diff --git a/src/btoropt/parser.py b/src/btoropt/parser.py
index ad2d27a..5e7dd70 100644
--- a/src/btoropt/parser.py
+++ b/src/btoropt/parser.py
@@ -18,576 +18,734 @@
 
 from .program import *
 
+# Retrieves an instruction with the given ID from the given standard program
+# This is a safe wrapper around `get_inst` and enforces that the given 
+# ID must be correct.
 def find_inst(p: list[Instruction], id: int) -> Instruction:
     inst = get_inst(p, id)
     assert inst is not None, f"Undeclared instruction used with id: {id}"
     return inst
 
-def parse(inp: list[str]) -> list[Instruction]:
-    # Split the string into instructions and read them 1 by 1
+# Checks thaa a given module name has been defined
+def check_name(name: str, modules: list[Module]) -> bool:
+    return name in [m.name for m in modules]
+
+# Retrives a module by name from a list of parsed modules
+def get_module(name: str, modules: list[Module]) -> Module:
+    return [m for m in modules if m.name == name][0]
+
+# Extracts a body from an arbitrary code sequence
+# Returns the line idx at which the scanning ended
+def scan_body(inp: list[str], i: int) -> tuple[list[str], int]:
+    res = []
+    l = inp[i].split(" ")
+    ## Check that the declaration line ends with an '{'
+    assert str(l[len(l)-1].strip()) == '{', f"invalid body start: {l[len(l)-1]}"
+
+    i += 1
+    while inp[i].strip() != "}":
+        # Check that there are no nested structures
+        lid = inp[i].strip().split(" ")[0]
+        assert lid.isnumeric(), f"All body lines must be instructions! Found: {lid}"
+        res.append(inp[i].strip())
+        i += 1
+    return (res, i)
+
+# Parses a ref instruction (only custom inst that is allowed in both modules and contracts)
+# @param inst: the pre-split ref instruction to be parsed 
+# @param modules: the list of already parsed modules that can be referenced
+def parse_ref(inst: list[str], modules: list[Module]) -> Ref:
+    ## Sanity check: Must be a ref instruction
+    assert inst[1] == "ref", f"`parse_ref` can only handle ref instructions, not {inst[1]}!"
+    ref_mod = inst[2]
+
+    ## Sanity check: check that the name exists
+    assert check_name(ref_mod, modules), f"Named module {ref_mod} is undefined!"
+
+    module = get_module(ref_mod, modules)
+    val = find_inst(module.body, int(inst[3]))
+    return Ref(int(inst[0]), ref_mod, val)
+
+# Parse a module's pre-scanned body
+# @param body: the list of instructions contained within the body
+# @param modules: the list of already parsed modules that can be referenced
+def parse_module_body(body: list[str], modules: list[Module]) -> list[Instruction]:
     p = []
-    for line in inp:
+    for line in body:
         inst = line.split(" ")
-        # BTOR comment
-        if inst[0] == ";":
+        if inst[0] == ";": # handle comments
             continue
         lid = int(inst[0])
         tag = inst[1]
+        match tag:
+            # Handle special instructions
+            case "inst":
+                instd_mod = inst[2]
+                ## Sanity check: check that the name exists
+                assert check_name(instd_mod, modules), f"Named module {instd_mod} is undefined!"
+                p.append(Instance(lid, instd_mod))
+
+            case "ref":
+                p.append(parse_ref(inst, modules))
+
+            case "set":
+                instance = find_inst(p, int(inst[2]))
+                ref = find_inst(p, int(inst[3]))
+                assert ref.name == instance.name, "`set` can only set a reference to an instance input!"
+                alias = find_inst(p, int(inst[4]))
+                p.append(Set(lid, instance, ref, alias))
+
+            # Handle standard instructions
+            case _:
+                op = parse_inst(line, p)
+                if op is not None:
+                    p.append(op)
 
-        # Check if tag is valid
-        assert tag in tags, f"Unsupported operation type: {tag} in {line}"
-
-        # Create the instruction associated to the tag
-        op = None
+    return p
 
+# Parse a contract's pre-scanned body
+# @param name: the name given to the module
+# @param body: the list of instructions contained within the body
+# @param modules: the list of already parsed modules that can be referenced
+def parse_contract_body(body: list[str], modules: list[Module]) -> list[Instruction]:
+    p = []
+    for line in body:
+        inst = line.split(" ")
+        if inst[0] == ";": # handle comments
+            continue
+        lid = int(inst[0])
+        tag = inst[1]
         match tag:
-            case "sort":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "sort instruction must be of the form: <lid> sort \{bitvector|array\} <width>. Found: " + line
-                assert inst[2] in sort_tags,\
-                    f"sort must be of type bitvector or array! Found: {inst[2]}"
+            # Handle special instructions
+            case "prec":
+                # Find the op associated to this instruction
+                cond = find_inst(p, int(inst[2]))
+                p.append(Prec(lid, cond))
+
+            case "post":
+                # Find the op associated to this instruction
+                cond = find_inst(p, int(inst[2]))
+                p.append(Post(lid, cond))
 
-                # Construct instruction
-                op = Sort(lid, inst[2], int(inst[3]))
+            case "ref":
+                p.append(parse_ref(inst, modules))
 
+            # Handle standard instructions
+            case _:
+                op = parse_inst(line, p)
+                if op is not None:
+                    p.append(op)
 
-            case "input":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "input instruction must be of the form: <lid> input <sid> <name>. Found: " + line
+    return p
 
-                # Find the sort associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                assert isinstance(sort, Sort), f"Input sort must be a Sort. Found: " + line
+# Parses a single instruction
+# @param line: the current instruction that needs to be parsed
+# @param p: the current parsed state of the program
+def parse_inst(line: str, p: list[Instruction]) -> Instruction:
+    inst = line.split(" ")
+    # BTOR comment
+    if inst[0] == ";":
+        return None
+    lid = int(inst[0])
+    tag = inst[1]
 
-                # Construct instruction
-                op = Input(lid, sort, inst[3])
+    # Check if tag is valid
+    assert tag in tags, f"Unsupported operation type: {tag} in {line}"
 
-            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
+    # Create the instruction associated to the tag
+    op = None
 
-                # Find the op associated to this instruction
-                out = find_inst(p, int(inst[2]))
+    match tag:
+        case "sort":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "sort instruction must be of the form: <lid> sort \{bitvector|array\} <width>. Found: " + line
+            assert inst[2] in sort_tags,\
+                f"sort must be of type bitvector or array! Found: {inst[2]}"
 
-                # Construct instruction
-                op = Output(lid, out)
+            # Construct instruction
+            op = Sort(lid, inst[2], int(inst[3]))
 
-            case "bad":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 3,\
-                    "sort instruction must be of the form: <lid> bad <opid>. Found: " + line
 
-                # Find the op associated to this instruction
-                cond = find_inst(p, int(inst[2]))
+        case "input":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "input instruction must be of the form: <lid> input <sid> <name>. Found: " + line
 
-                # Construct instruction
-                op = Bad(lid, cond)
+            # Find the sort associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            assert isinstance(sort, Sort), f"Input sort must be a Sort. Found: " + line
 
-            case "constraint":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 3,\
-                    "sort instruction must be of the form: <lid> constraint <opid>. Found: " + line
+            # Construct instruction
+            op = Input(lid, sort, inst[3])
 
-                # Find the op associated to this instruction
-                cond = find_inst(p, int(inst[2]))
+        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
 
-                # Construct instruction
-                op = Constraint(lid, cond)
+            # Find the op associated to this instruction
+            out = find_inst(p, int(inst[2]))
 
-            case "zero":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 3,\
-                    "sort instruction must be of the form: <lid> zero <sid>. Found: " + line
+            # Construct instruction
+            op = Output(lid, out)
 
-                # Find the sort associated to this instruction
-                sort = find_inst(p, int(inst[2]))
+        case "bad":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 3,\
+                "sort instruction must be of the form: <lid> bad <opid>. Found: " + line
 
-                # Construct instruction
-                op = Zero(lid, sort)
+            # Find the op associated to this instruction
+            cond = find_inst(p, int(inst[2]))
 
-            case "one":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 3,\
-                    "sort instruction must be of the form: <lid> one <sid>. Found: " + line
+            # Construct instruction
+            op = Bad(lid, cond)
 
-                # Find the sort associated to this instruction
-                sort = find_inst(p, int(inst[2]))
+        case "constraint":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 3,\
+                "sort instruction must be of the form: <lid> constraint <opid>. Found: " + line
 
-                # Construct instruction
-                op = One(lid, sort)
+            # Find the op associated to this instruction
+            cond = find_inst(p, int(inst[2]))
 
-            case "ones":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 3,\
-                    "sort instruction must be of the form: <lid> ones <sid>. Found: " + line
+            # Construct instruction
+            op = Constraint(lid, cond)
 
-                # Find the sort associated to this instruction
-                sort = find_inst(p, int(inst[2]))
+        case "zero":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 3,\
+                "sort instruction must be of the form: <lid> zero <sid>. Found: " + line
+
+            # Find the sort associated to this instruction
+            sort = find_inst(p, int(inst[2]))
 
-                # Construct instruction
-                op = Ones(lid, sort)
-
-            case "constd":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "sort instruction must be of the form: <lid> constd <sid> <value>. Found: " + line
+            # Construct instruction
+            op = Zero(lid, sort)
 
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                value = int(inst[3])
+        case "one":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 3,\
+                "sort instruction must be of the form: <lid> one <sid>. Found: " + line
 
-                # Construct instruction
-                op = Constd(lid, sort, value)
-
-            case "consth":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "sort instruction must be of the form: <lid> consth <sid> <value>. Found: " + line
+            # Find the sort associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+
+            # Construct instruction
+            op = One(lid, sort)
+
+        case "ones":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 3,\
+                "sort instruction must be of the form: <lid> ones <sid>. Found: " + line
+
+            # Find the sort associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+
+            # Construct instruction
+            op = Ones(lid, sort)
+
+        case "constd":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "sort instruction must be of the form: <lid> constd <sid> <value>. Found: " + line
 
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                value = int(inst[3])
-
-                # Construct instruction
-                op = Consth(lid, sort, value)
-
-            case "const":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "sort instruction must be of the form: <lid> const <sid> <value>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                # Default base is 2
-                value = int(inst[3], 2)
-
-                # Construct instruction
-                op = Const(lid, sort, value)
-
-            case "state":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "state instruction must be of the form: <lid> state <sid> <name>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                assert isinstance(sort, Sort), f"State sort must be a Sort. Found: " + line
-                name = inst[3].strip()
-
-                # Construct instruction
-                op = State(lid, sort, name)
-
-            case "init":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> init <sid> <stateid> <valueid>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                state = find_inst(p, int(inst[3]))
-                val = find_inst(p, int(inst[4]))
-
-                # Construct instruction
-                op = Init(lid, sort, state, val)
-
-            case "next":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> next <sid> <stateid> <nextid>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                state = find_inst(p, int(inst[3]))
-                next = find_inst(p, int(inst[4]))
-
-                # Construct instruction
-                op = Next(lid, sort, state, next)
-
-            case "slice":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 6,\
-                    "sort instruction must be of the form: <lid> slice <sid> <opid> <width> <lowbit>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                operand = find_inst(p, int(inst[3]))
-                width = int(inst[4])
-                lowbit = int(inst[5])
-
-                # Construct instruction
-                op = Slice(lid, sort, operand, width, lowbit)
-
-            case "ite":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 6,\
-                    "sort instruction must be of the form: <lid> ite <sid> <condid> <tid> <fid>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                cond = find_inst(p, int(inst[3]))
-                t = find_inst(p, int(inst[4]))
-                f = find_inst(p, int(inst[5]))
-
-                # Construct instruction
-                op = Ite(lid, sort, cond, t, f)
-
-            case "implies":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> implies <sid> <lhsid> <rhsid>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                lhs = find_inst(p, int(inst[3]))
-                rhs = find_inst(p, int(inst[4]))
-
-                # Construct instruction
-                op = Implies(lid, sort, lhs, rhs)
-
-            case "iff":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> iff <sid> <lhsid> <rhsid>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                lhs = find_inst(p, int(inst[3]))
-                rhs = find_inst(p, int(inst[4]))
-
-                # Construct instruction
-                op = Iff(lid, sort, lhs, rhs)
-
-            case "add":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> add <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 = Add(lid, sort, op1, op2)
-
-            case "sub":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> sub <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 = Sub(lid, sort, op1, op2)
-
-            case "mul":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> mul <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 = Mul(lid, sort, op1, op2)
-
-            case "sdiv":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> sdiv <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 = Sdiv(lid, sort, op1, op2)
-
-            case "udiv":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> udiv <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 = Udiv(lid, sort, op1, op2)
-
-            case "smod":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> smod <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(int(inst[4]))
-
-                # Construct instruction
-                op = Smod(lid, sort, op1, op2)
-
-            case "sll":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> sll <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 = Sll(lid, sort, op1, op2)
-
-            case "srl":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> srl <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 = Srl(lid, sort, op1, op2)
-
-            case "sra":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> sra <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 = Sra(lid, sort, op1, op2)
-
-            case "and":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> and <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 = And(lid, sort, op1, op2)
-
-            case "or":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> or <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 = Or(lid, sort, op1, op2)
-
-            case "xor":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> xor <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 = Xor(lid, sort, op1, op2)
-
-            case "concat":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> concat <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 = Concat(lid, sort, op1, op2)
-
-            case "not":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 4,\
-                    "sort instruction must be of the form: <lid> not <sid> <cond>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                cond = find_inst(p, int(inst[3]))
-
-                # Construct instruction
-                op = Not(lid, sort, cond)
-
-            case "eq":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> eq <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 = Eq(lid, sort, op1, op2)
-
-            case "neq":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> neq <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 = Neq(lid, sort, op1, op2)
-
-            case "ugt":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> ugt <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 = Ugt(lid, sort, op1, op2)
-
-            case "sgt":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> sgt <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 = Sgt(lid, sort, op1, op2)
-
-            case "ugte":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> ugte <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 = Ugte(lid, sort, op1, op2)
-
-            case "sgte":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> sgte <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 = Sgte(lid, sort, op1, op2)
-
-            case "ult":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> ult <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 = Ult(lid, sort, op1, op2)
-
-            case "slt":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> slt <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 = Slt(lid, sort, op1, op2)
-
-            case "ulte":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> ulte <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 = Ulte(lid, sort, op1, op2)
-
-            case "slte":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 5,\
-                    "sort instruction must be of the form: <lid> slte <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 = Slte(lid, sort, op1, op2)
-
-            case "uext":
-                # Sanity check: verify that instruction is well formed
-                assert len(inst) >= 6,\
-                    "sort instruction must be of the form: <lid> uext <sid> <opid> <width> <name>. Found: " + line
-
-                # Find the operands associated to this instruction
-                sort = find_inst(p, int(inst[2]))
-                operand = find_inst(p, int(inst[3]))
-                width = int(inst[4])
-
-                # Construct instruction
-                op = Uext(lid, sort, operand, width, inst[5])
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            value = int(inst[3])
+
+            # Construct instruction
+            op = Constd(lid, sort, value)
+
+        case "consth":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "sort instruction must be of the form: <lid> consth <sid> <value>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            value = int(inst[3])
+
+            # Construct instruction
+            op = Consth(lid, sort, value)
+
+        case "const":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "sort instruction must be of the form: <lid> const <sid> <value>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            # Default base is 2
+            value = int(inst[3], 2)
+
+            # Construct instruction
+            op = Const(lid, sort, value)
+
+        case "state":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "state instruction must be of the form: <lid> state <sid> <name>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            assert isinstance(sort, Sort), f"State sort must be a Sort. Found: " + line
+            name = inst[3].strip()
+
+            # Construct instruction
+            op = State(lid, sort, name)
+
+        case "init":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> init <sid> <stateid> <valueid>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            state = find_inst(p, int(inst[3]))
+            val = find_inst(p, int(inst[4]))
+
+            # Construct instruction
+            op = Init(lid, sort, state, val)
+
+        case "next":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> next <sid> <stateid> <nextid>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            state = find_inst(p, int(inst[3]))
+            next = find_inst(p, int(inst[4]))
+
+            # Construct instruction
+            op = Next(lid, sort, state, next)
+
+        case "slice":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 6,\
+                "sort instruction must be of the form: <lid> slice <sid> <opid> <width> <lowbit>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            operand = find_inst(p, int(inst[3]))
+            width = int(inst[4])
+            lowbit = int(inst[5])
+
+            # Construct instruction
+            op = Slice(lid, sort, operand, width, lowbit)
+
+        case "ite":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 6,\
+                "sort instruction must be of the form: <lid> ite <sid> <condid> <tid> <fid>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            cond = find_inst(p, int(inst[3]))
+            t = find_inst(p, int(inst[4]))
+            f = find_inst(p, int(inst[5]))
+
+            # Construct instruction
+            op = Ite(lid, sort, cond, t, f)
+
+        case "implies":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> implies <sid> <lhsid> <rhsid>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            lhs = find_inst(p, int(inst[3]))
+            rhs = find_inst(p, int(inst[4]))
+
+            # Construct instruction
+            op = Implies(lid, sort, lhs, rhs)
+
+        case "iff":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> iff <sid> <lhsid> <rhsid>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            lhs = find_inst(p, int(inst[3]))
+            rhs = find_inst(p, int(inst[4]))
+
+            # Construct instruction
+            op = Iff(lid, sort, lhs, rhs)
+
+        case "add":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> add <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 = Add(lid, sort, op1, op2)
+
+        case "sub":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> sub <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 = Sub(lid, sort, op1, op2)
+
+        case "mul":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> mul <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 = Mul(lid, sort, op1, op2)
+
+        case "sdiv":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> sdiv <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 = Sdiv(lid, sort, op1, op2)
+
+        case "udiv":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> udiv <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 = Udiv(lid, sort, op1, op2)
+
+        case "smod":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> smod <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(int(inst[4]))
+
+            # Construct instruction
+            op = Smod(lid, sort, op1, op2)
+
+        case "sll":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> sll <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 = Sll(lid, sort, op1, op2)
+
+        case "srl":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> srl <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 = Srl(lid, sort, op1, op2)
+
+        case "sra":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> sra <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 = Sra(lid, sort, op1, op2)
+
+        case "and":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> and <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 = And(lid, sort, op1, op2)
+
+        case "or":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> or <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 = Or(lid, sort, op1, op2)
+
+        case "xor":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> xor <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 = Xor(lid, sort, op1, op2)
+
+        case "concat":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> concat <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 = Concat(lid, sort, op1, op2)
+
+        case "not":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 4,\
+                "sort instruction must be of the form: <lid> not <sid> <cond>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            cond = find_inst(p, int(inst[3]))
+
+            # Construct instruction
+            op = Not(lid, sort, cond)
+
+        case "eq":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> eq <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 = Eq(lid, sort, op1, op2)
+
+        case "neq":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> neq <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 = Neq(lid, sort, op1, op2)
+
+        case "ugt":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> ugt <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 = Ugt(lid, sort, op1, op2)
+
+        case "sgt":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> sgt <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 = Sgt(lid, sort, op1, op2)
+
+        case "ugte":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> ugte <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 = Ugte(lid, sort, op1, op2)
+
+        case "sgte":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> sgte <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 = Sgte(lid, sort, op1, op2)
+
+        case "ult":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> ult <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 = Ult(lid, sort, op1, op2)
+
+        case "slt":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> slt <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 = Slt(lid, sort, op1, op2)
+
+        case "ulte":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> ulte <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 = Ulte(lid, sort, op1, op2)
+
+        case "slte":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 5,\
+                "sort instruction must be of the form: <lid> slte <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 = Slte(lid, sort, op1, op2)
+
+        case "uext":
+            # Sanity check: verify that instruction is well formed
+            assert len(inst) >= 6,\
+                "sort instruction must be of the form: <lid> uext <sid> <opid> <width> <name>. Found: " + line
+
+            # Find the operands associated to this instruction
+            sort = find_inst(p, int(inst[2]))
+            operand = find_inst(p, int(inst[3]))
+            width = int(inst[4])
+
+            # Construct instruction
+            op = Uext(lid, sort, operand, width, inst[5])
+
+        case _:
+            print(f"Unsupported operation type: {tag} in {line}")
+            exit(1)
+    return op
+
+# Parse an entire file that can contain contracts and modules
+def parse_file(inp: list[str]) -> Program:
+    m: list[Module] = []
+    c: list[Contract] = []
+    i = 0
+    while i < len(inp):
+        symbols = inp[i].strip().split(" ")
+        # Check whether it's a module or a contract
+        tag = symbols[0]
+        match tag:
+            case "module":
+                name = symbols[1]
+                # Scan and parse the body
+                (body, i) = scan_body(inp, i)
+                b = parse_module_body(body, m)
+                # Create and store the module
+                m.append(Module(name, b))
+                            
+            case "contract":
+                name = symbols[1]
+                assert check_name(name, m), f"Contract name {name} is not defined!"
+                (body, i) = scan_body(inp, i)
+                body = parse_contract_body(body, m)
+                # Create and store the module
+                c.append(Contract(name, body))
+
+            case "}":
+                i+=1
+                continue
 
             case _:
-                print(f"Unsupported operation type: {tag} in {line}")
+                print(f"Unsupported structure: {tag} is not module | contract")
                 exit(1)
+            
+    return Program(m, c)
 
+# Parse a standard btor2 file, does not handle custom instructions
+def parse(inp: list[str]) -> list[Instruction]:
+    # Split the string into instructions and read them 1 by 1
+    p = []
+    for line in inp:
+        op = parse_inst(line, p)
         if op is not None:
             p.append(op)
     return p
diff --git a/src/btoropt/passes/genericpass.py b/src/btoropt/passes/genericpass.py
index 56223f3..6180cdf 100644
--- a/src/btoropt/passes/genericpass.py
+++ b/src/btoropt/passes/genericpass.py
@@ -18,7 +18,8 @@
 
 # Abstract class for a compiler pass
 
-from ..program import Instruction
+from ..program import Instruction, Program, Module
+import multiprocessing
 
 # Base clas for compiler pass
 # @param id: the unique name of this pass
@@ -26,5 +27,13 @@ class Pass:
     def __init__(self, id: str):
         self.id = id
 
-    def run(p: list[Instruction]) -> list[Instruction]:
+    def run(self, p: list[Instruction]) -> list[Instruction]:
         return p
+    
+    # By default runs the standard pass in parallel on all modules
+    def runOnProgram(self, p: Program) -> Program:
+        pool = multiprocessing.Pool()
+        f = lambda m : Module(m.name, self.run(m.body))
+        p.modules = pool.map(f, p.modules)
+        return p
+
diff --git a/src/btoropt/program.py b/src/btoropt/program.py
index 0dd7224..62f58fa 100644
--- a/src/btoropt/program.py
+++ b/src/btoropt/program.py
@@ -30,16 +30,24 @@
 # All legal sort types
 sort_tags = ["bitvector", "bitvec", "array"]
 
+# All custom tags
+custom_tags = ["inst", "set", "ref", "prec", "post"]
+structure_tags = ["module", "contract"]
+
 # Base class for an instruction
 # @param lid: the line identifier of the instruction
 # @param inst: the string litteral keyword for the instruction
 # @param operands: the list of operands given to this instruction,
 # these must also be instructions
+# @param is_standard: whether or not the instruction is part of the btor2
+#   True: instruction is part of the btor2 spec
+#   False: instruction is a custom extension for btor-opt
 class Instruction:
-    def __init__(self, lid: int, inst: str, operands = []):
+    def __init__(self, lid: int, inst: str, operands = [], is_standard=True):
         self.lid = lid
         self.inst = inst
         self.operands = operands
+        self.is_standard = is_standard
 
     def move_up(self, amount: int):
         self.lid += amount
@@ -69,10 +77,11 @@ def serialize(self) -> str:
 def serialize_p(p: list[Instruction]) -> str:
     return reduce(lambda acc, s: acc + s.serialize() + "\n", p, "")
 
+# Extracts an instruction from a given program
 def get_inst(p: list[Instruction], lid: int) -> Instruction:
-    for op in p:
-        if op.lid == lid:
-            return op
+    ops = [op for op in p if op.lid == lid]
+    if len(ops) > 0:
+        return ops[0]
     return None
 
 # Sort declaration instruction
@@ -106,12 +115,13 @@ def eq(self, inst) -> bool:
     def serialize(self) -> str:
         return super().serialize() + self.name
 
-## Unary Instructions ##
 
 class Output(Instruction):
     def __init__(self, lid: int, out: Instruction):
         super().__init__(lid, "output", [out])
 
+## Unary Instructions ##
+
 class Bad(Instruction):
     def __init__(self, lid: int, cond: Instruction):
         super().__init__(lid, "bad", [cond])
@@ -330,3 +340,120 @@ class Sext(Instruction):
     def __init__(self, lid: int, sort: Sort, op: Instruction, width: int, name: str):
         super().__init__(lid, "sext", [sort, op, width, name])
         self.width: int = width
+
+
+############ NON-STANDARD: Custom extensions for btor-opt ############
+
+# Precondition instruction
+# This becomes a "x not cond; bad x" when verifying an instance
+#      becomes a "constraint cond" when verifying a module
+class Prec(Instruction):
+    def __init__(self, lid: int, cond: Instruction):
+        super().__init__(lid, "prec", [cond], False)
+
+# Postcondition instruction
+# This becomes a "constraint cond" when verifying an instance
+#      becomes a "x not cond; bad x" when verifying a module
+class Post(Instruction):
+    def __init__(self, lid: int, cond: Instruction):
+        super().__init__(lid, "post", [cond], False)
+
+# Instance Instruction
+# Creates an instance of a named module
+# @param name: the name of the module to instantiate
+class Instance(Instruction):
+    def __init__(self, lid: int, name: str):
+        super().__init__(lid, "inst", [], False)
+        self.name = name
+
+# Reference to an instruction in a different named region
+# Has a weird infix notation `<mod_name>:<lid>`
+# Not really an instruction, more of a reference to an instruction
+class Ref(Instruction):
+    def __init__(self, lid: int, name: str, val: Instruction):
+        super().__init__(lid, ":", [val], False)
+        self.name = name
+        self.val = val
+
+# Set Instruction
+# Similarly to an alias, this sets the inputs of an instance to a specific operation
+# @param instance: the instance this is setting inputs for
+# @param ref: a reference to the module's input we want to set, e.g. A:2
+# @param alias: the instruction we want to set the input to
+class Set(Instruction):
+    def __init__(self, lid: int, instance: Instance, ref: Ref, alias: Instruction):
+        super().__init__(lid, "set", [instance, ref, alias], False)
+
+
+# Structural extensions
+class ModuleLike():
+    def __init__(self, name: str, body: list[Instruction]) -> None:
+        self.name = name
+        self.body = body
+
+    def get_inst(self, i: int) -> Instruction:
+        return self.body[i]
+
+# Module instruction 
+# Declares a named region of standard instructions
+# Can be referred to by name and associated with a contract
+class Module(ModuleLike):
+    def __init__(self, name: str, body: list[Instruction]) -> None:
+        super().__init__(name, body)
+   
+# Contract instruction 
+# Declares a named region of custom instructions
+# Only preconditions and postconditions are allowed
+# Name must be an existing module name 
+class Contract(ModuleLike):
+    def __init__(self, name: str, body: list[Instruction]) -> None:
+        super().__init__(name, body)
+        self.preconditions = [i for i in body if isinstance(i, Prec)]
+        self.postconditions = [i for i in body if isinstance(i, Post)]
+        assert len(self.preconditions) > 0 or len(self.postconditions) > 0, \
+            "Contracts must contain either a precondition or a post-condition!"
+        
+
+# Base class for a custom btor2 file (standard is simply a list of instructions)
+class Program():
+    def __init__(self, modules: list[Module], contracts: list[Contract]) -> None:
+        self.modules = modules
+        # Ignore all contracts that don't have an existing name
+        self.contracts = contracts
+        ## Sanity check: We should have as many modules as there are contracts
+        assert len(modules) >= len(contracts), \
+            "There should be at least as many modules as there are contracts!"
+        ## Sanity check: Each module should have at most one contract
+        for m in modules:
+            cs = [c for c in contracts if c.name == m.name]
+            assert len(cs) <= 1, f"Module {m.name} has more than one contract!"
+        ## Sanity check: Each contract should name a module exactly once
+        for c in contracts:
+            ms = [m for m in modules if c.name == m.name]
+            assert len(ms) == 1, f"Contract {c.name} references {str(len(ms))} modules instead of 1!"
+    
+    # Retrieves a module by its given name
+    # @param name: the name of the module we want to retrive
+    def get_module(self, name: str) -> Module:
+        res = [x for x in self.modules if x.name == name]
+        ## Check if the given name is defined
+        assert len(res) > 0 , f"name: {name} is not defined!"
+        return res[0]
+    
+    # Retrieves a contract by its given name
+    # @param name: the name of the contract we want to retrive
+    def get_contract(self, name: str) -> Contract:
+        res = [x for x in self.contracts if x.name == name]
+        ## Check if the given name is defined, otherwise return None
+        if len(res) == 0:
+            return None
+        return res[0]
+    
+    # Retrieves the contract associated to a module if it exists
+    # If it does not exist then simply return None
+    def get_module_contract(self, module: Module) -> Contract:
+        c = self.get_contract(module.name)
+        ## Check that a contract was found
+        return c
+
+########################################################################


Test patch:
diff --git a/tests/btor/modular.btor b/tests/btor/modular.btor
new file mode 100644
index 0000000..f7b61e1
--- /dev/null
+++ b/tests/btor/modular.btor
@@ -0,0 +1,47 @@
+module A {
+    1 sort bitvec 32
+    2 input 1 A.d 
+    3 sort bitvec 1
+    4 input 3 A.en 
+    5 input 3 A.rst 
+    6 input 1 B.d 
+    7 input 3 B.en 
+    8 input 3 B.rst 
+    9 input 3 clk
+    10 state 1 A.q
+    11 output 10 qA 
+    12 state 1 B.q
+    13 output 12 qB 
+    14 uext 3 9 0 A.clk 
+    15 uext 3 9 0 B.clk 
+    16 ite 1 4 2 10
+    17 const 1 00000000000000000000000000000000
+    18 ite 1 5 17 16
+    19 next 1 10 18
+    20 ite 1 7 6 12
+    21 ite 1 8 17 20
+    22 next 1 12 21
+}
+contract A {
+    1 sort bitvec 1
+    2 ref A 1
+    3 const 2 0
+    4 ref A 2
+    5 eq 1 4 2
+    6 prec 3
+    7 ref A 10
+    8 ugt 1 7 2
+    9 post 5  
+}
+module C {
+    1 sort bitvec 32
+    2 input 1 C.i
+    3 inst A
+    4 ref A 1
+    5 set 3 4 2 
+    6 sort bitvec 1
+    7 const 1 0
+    8 ref A 10
+    9 eq 1 7 6
+    10 bad 7 
+}
diff --git a/tests/test.py b/tests/test.py
index 42b405d..60c0b55 100644
--- a/tests/test.py
+++ b/tests/test.py
@@ -27,10 +27,10 @@ def parsewrapper (filepath):
         btor2str = f.readlines()
     return btor2str
 
-class BTORTest(unittest.TestCase):
+class BTORTestParser(unittest.TestCase):
     """Check whether BTOR interface is working properly"""
 
-    def test_btor1(self):
+    def test_standard(self):
         prgm = parse(parsewrapper("tests/btor/reg_en.btor"))
 
         self.assertEqual(prgm[0].inst, "sort")
@@ -39,6 +39,19 @@ def test_btor1(self):
 
         print("test passed")
 
+    def test_modular(self):
+            p: Program = parse_file(parsewrapper("tests/btor/modular.btor"))
+            self.assertIsNotNone(p)
+
+            self.assertEqual(len(p.modules), 2)
+            self.assertEqual(len(p.contracts), 1)
+            ma = p.get_module("A")
+            ca = p.get_contract("A")
+            self.assertIsNotNone(ca)
+            c = p.get_module_contract(ma)
+            self.assertIsNotNone(c)
+            self.assertEqual(c, ca)
+            self.assertEqual(c.name, "A")
 
 if __name__ == '__main__':
     unittest.main()