diff options
-rw-r--r-- | src/theory/rewriter/backend_lfsc.py | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/src/theory/rewriter/backend_lfsc.py b/src/theory/rewriter/backend_lfsc.py new file mode 100644 index 000000000..24f19ece6 --- /dev/null +++ b/src/theory/rewriter/backend_lfsc.py @@ -0,0 +1,44 @@ +from node import * + +class ProofRule: + def __init__(name, params, arguments, subproofs): + self.name = name + self.params = params + self.arguments = arguments + self.subproofs = subproofs + +def collect_node_sort_params(node): + params = set() + + if isinstance(node, BVConst): + v = Var('bv{}_{}'.format(node.val, node.bw)) + v.sort = Sort(BaseSort.BitVec, [node.bw]) + params.add(v) + + if isinstance(node, Fn): + if node.op in [Op.ZERO_EXTEND]: + v = Var('zebv') + v.sort = Sort(BaseSort.Int, []) + params.add(v) + + v = Var('zeamount') + v.sort = Sort(BaseSort.Int, []) + params.add(v) + + for child in node.children: + params |= collect_node_sort_params(child) + + if isinstance(node, Var) and node.sort.base == BaseSort.Int: + params.add(node) + + return params + +def collect_params(rule): + params = set() + for name, sort in rule.rvars.items(): + if sort.base == BaseSort.BitVec and isinstance(sort.children[0], Var): + sort.children[0].sort = Sort(BaseSort.Int, []) + params.add(sort.children[0]) + + params |= collect_node_sort_params(rule.lhs) + return params |