spyro/output_parser.py at master · ebmoon/spyro · GitHub

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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
from util import *

def replace_last_argument(text, var):
    start = text.rfind(',')
    end = text.rfind(')')

    return text[:start] + ', out' + text[end:]

class OutputParser:
    def __init__(self, text):
        self.__text = text.decode('utf-8')

    def __get_function_code_lines(self, function_name):
        lines = self.__text.splitlines()

        target = 'void ' + function_name + ' ('
        start = find_linenum_starts_with(lines, target)
        end = find_linenum_starts_with(lines, '}', start)

        return lines[start+2:end]

    def get_lam_functions(self):
        lines = self.__text.splitlines()

        lam_functions = {}
        for n, line in enumerate(lines):
            if ('void' in line) and ('lam' in line):
                end = find_linenum_starts_with(lines, '}', n)
                lam_code = "\n".join(lines[n:end+1])
                fun_name = line[6:line.find("(")]
                lam_functions[fun_name] = lam_code

        return lam_functions

    def parse_positive_example(self):
        soundness_code_lines = self.__get_function_code_lines('soundness')
        soundness_code_lines = [line for line in soundness_code_lines if 'copy' not in line]
        soundness_code_lines = [line for line in soundness_code_lines if 'minimize' not in line]
        soundness_code_lines = ['\t' + line.strip() for line in soundness_code_lines]

        property_call = soundness_code_lines[-2].replace('obtained_property', 'property')

        positive_example_code = '\n'.join(soundness_code_lines[:-3])

        if property_call.find('(') >= 0:
            property_call = replace_last_argument(property_call, 'out')

            positive_example_code += '\n\tboolean out;'
            positive_example_code += '\n' + property_call
            positive_example_code += '\n\tassert out;'
        else:
            positive_example_code += '\n' + property_call
            positive_example_code += '\n\tassert out;'

        positive_example_code = positive_example_code.replace("//{}", "")

        return positive_example_code

    def parse_negative_example_precision(self):
        precision_code_lines = self.__get_function_code_lines('precision')
        precision_code_lines = [line for line in precision_code_lines if 'copy' not in line]
        precision_code_lines = [line for line in precision_code_lines if 'minimize' not in line]
        precision_code_lines = ['\t' + line.strip() for line in precision_code_lines]

        negative_example_code = '\n'.join(precision_code_lines[:-9])

        if precision_code_lines[-2].find("(") >= 0:
            property_call = replace_last_argument(precision_code_lines[-2], 'out')

            negative_example_code += '\n\tboolean out;'
            negative_example_code += '\n' + property_call
            negative_example_code += '\n\tassert !out;'
        else:
            negative_example_code += '\n' + precision_code_lines[-2].replace('out_3', 'out')
            negative_example_code += '\n\tassert !out;'

        negative_example_code = negative_example_code.replace("//{}", "")

        return negative_example_code

    def parse_improves_predicate(self):
        precision_code_lines = self.__get_function_code_lines('improves_predicate')
        precision_code_lines = ['\t' + line.strip() for line in precision_code_lines]

        property_call = replace_last_argument(precision_code_lines[-2], 'out')

        negative_example_code = '\n'.join(precision_code_lines[:-6])
        negative_example_code += '\n\tboolean out;'
        negative_example_code += '\n' + property_call.replace("obtained_property", "property")
        negative_example_code += '\n\tassert !out;'

        negative_example_code = negative_example_code.replace("//{}", "")

        return negative_example_code

    def parse_maxsat(self, neg_examples):
        maxsat_code_lines = self.__get_function_code_lines('maxsat')
        maxsat_code = '\n'.join(maxsat_code_lines)

        used_neg_examples = []
        discarded_examples = []
        for i, e in enumerate(neg_examples):
            if 'negative_example_{}'.format(i) in maxsat_code:
                used_neg_examples.append(e)
            else:
                discarded_examples.append(e)

        return used_neg_examples, discarded_examples

    def parse_property(self):
        property_code_lines = self.__get_function_code_lines('property')
        property_code_lines = ['\t' + line.strip() for line in property_code_lines]

        property_code = '\n'.join(property_code_lines)
        property_code = property_code.replace("//{}", "")

        return property_code.strip()