Source code for utils.Z3Converter

import re
from typing import List

from pyparsing import Suppress, Forward, Word, Group, ZeroOrMore, alphanums, oneOf, Literal
from z3 import Or, And, Xor, If, Not, Bool, is_app_of, Z3_OP_XOR, Z3_OP_UNINTERPRETED, is_const, is_not, AstRef, is_and, \
    is_or, ExprRef, set_option


[docs] class AstRefKey: def __init__(self, n): self.n = n def __hash__(self): return self.n.hash() def __eq__(self, other): return self.n.eq(other.n) def __repr__(self): return str(self.n)
[docs] class Z3Converter:
[docs] @staticmethod def simple_paths_to_z3(one_paths: List[List[str]]) -> Bool: """ Returns a formula in Verilog to a formula compatible with Z3. :param one_paths: :return: """ products = [] for one_path in one_paths: product = [] for raw_literal in one_path: literal = str(raw_literal).replace('\\+', '~') if literal.startswith('~'): product.append(Not(Bool(literal.replace('~', '')))) else: if literal == "True": product.append(True) else: product.append(Bool(literal)) products.append(And(product)) formula = Or(products) return formula
@staticmethod def _converted_formula_tree(lst): """ Returns a formula in Verilog to a formula compatible with Z3. :param lst: :return: """ if not lst: return Or() if isinstance(lst, str): if lst[0] == '~': return Not(Bool(lst[1:])) return Bool(lst) if len(lst) == 1: return Z3Converter._converted_formula_tree(lst[0]) elif len(lst) >= 3 and lst[1] == '^': expressions = [lst[i] for i in range(0, len(lst), 2)] z3_expressions = list(map(lambda e: Z3Converter._converted_formula_tree(e), expressions)) return Xor(*z3_expressions) elif len(lst) >= 3 and lst[1] == '&': expressions = [lst[i] for i in range(0, len(lst), 2)] z3_expressions = list(map(lambda e: Z3Converter._converted_formula_tree(e), expressions)) return And(*z3_expressions) elif len(lst) >= 3 and lst[1] == '|': expressions = [lst[i] for i in range(0, len(lst), 2)] z3_expressions = list(map(lambda e: Z3Converter._converted_formula_tree(e), expressions)) return Or(*z3_expressions) elif len(lst) >= 5 and lst[1] == '?': cond = lst[0] true_stmt = lst[2] false_stmt = lst[4] return If(Z3Converter._converted_formula_tree(cond), Z3Converter._converted_formula_tree(true_stmt), Z3Converter._converted_formula_tree(false_stmt), ctx=None) return
[docs] @staticmethod def verilog_to_tree(verilog_formula: str): # Begin Source # URL: https://stackoverflow.com/questions/37925803/parserelement-enablepackrat-doesnt-make-infixnotation-faster # Author: PaulMcG # Published on: June 20, 2016 # Accessed on: July 15, 2020 # Begin Source (2): https://stackoverflow.com/questions/23879784/parse-mathematical-expressions-with-pyparsing # Author: PaulMcG # Published on: May 20, 2014 # Visited on: July 15, 2020 LPAR, RPAR = map(Suppress, '()') expr = Forward() variable = Word(alphanums + '_~' '[' ']') nested = variable | Group(LPAR + expr + RPAR) binary_op = nested + ZeroOrMore(oneOf('^ | &') + nested) ternary_op = nested + Literal('?') + nested + Literal(':') + nested formula_expr = ternary_op | binary_op expr <<= formula_expr verilog_tree = [expr.parseString(verilog_formula).asList()] # End Source return verilog_tree
[docs] @staticmethod def verilog_to_z3(verilog_formula: str): if verilog_formula == "1\'b0": return False elif verilog_formula == "1\'b1": return True else: verilog_tree = Z3Converter.verilog_to_tree(verilog_formula) z3_formula = Z3Converter._converted_formula_tree(verilog_tree) return z3_formula
@staticmethod def _is_xor(a): return is_app_of(a, Z3_OP_XOR) @staticmethod def _askey(n): assert isinstance(n, AstRef) return AstRefKey(n) @staticmethod def _collect(f: Bool) -> str: if f is None: return "" if is_const(f): if f.decl().kind() == Z3_OP_UNINTERPRETED: return str(Z3Converter._askey(f)) else: return str(f) elif is_not(f): s = "~" for c in f.children(): s += Z3Converter._collect(c) return s elif is_and(f): return "(" + " & ".join([str(Z3Converter._collect(c)) for c in f.children()]) + ")" elif is_or(f): return "(" + " | ".join([str(Z3Converter._collect(c)) for c in f.children()]) + ")" elif Z3Converter._is_xor(f): return "(" + " ^ ".join([str(Z3Converter._collect(c)) for c in f.children()]) + ")" elif isinstance(f, ExprRef): # IF statement children = list(map(lambda e: Z3Converter._collect(e), f.children())) return "(({}) ? ({}) : ({}))".format(children[0], children[1], children[2]) else: raise Exception("Unexpected operator.")
[docs] @staticmethod def z3_to_str(z3_formula: Bool) -> str: set_option(max_args=1000000000000, max_lines=100000000000, max_depth=1000000000000, max_visited=100000000000) return str(z3_formula)