summaryrefslogtreecommitdiff
path: root/src/theory/rewriter/ir.py
blob: c9c9fa9c310493a5840827b43871e2fb442e557d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
from node import collect_vars

class IRNode:
    def __init__(self):
        pass


class Assign(IRNode):
    def __init__(self, name, expr):
        super(IRNode, self).__init__()
        self.name = name
        self.expr = expr


class Assert(IRNode):
    def __init__(self, expr):
        super(IRNode, self).__init__()
        self.expr = expr


def optimize_ir(out_var, instrs):
    used_vars = set([out_var])
    for instr in instrs:
        if isinstance(instr, Assert):
            used_vars |= collect_vars(instr.expr)
        elif isinstance(instr, Assign):
            used_vars |= collect_vars(instr.expr)

    opt_instrs = []
    for instr in instrs:
        if not(isinstance(instr, Assign)) or instr.name in used_vars:
            opt_instrs.append(instr)
    return opt_instrs
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback