LLM4Ind/cvc5_parser.py at main · fengwz17/LLM4Ind · 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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
import os
import re
import shutil

def process_files_in_folder(input_folder, output_folder):
    # 遍历输入文件夹中的所有文件
    for filename in os.listdir(input_folder):
        if filename.endswith(".smt2"):
            input_file_path = os.path.join(input_folder, filename)
            output_subfolder = os.path.join(output_folder, filename.replace(".smt2", ""))

            # 创建输出子文件夹
            if not os.path.exists(output_subfolder):
                os.makedirs(output_subfolder)

            # 复制原始文件到输出子文件夹
            shutil.copy(input_file_path, os.path.join(output_subfolder, "origin.smt2"))

            # 处理文件并生成template和goals文件
            process_smt2_file(input_file_path, output_subfolder)

def process_smt2_file(input_file_path, output_subfolder):
    template_lines = []
    goals = []
    datatypes = []
    conjectures = []
    decfuns = []

    # 正则表达式匹配 (assert (not ...)) 形式的行
    assert_not_pattern = re.compile(r'\(assert \(not .*\)\)')
    assert_pattern = re.compile(r'\(assert \(.*\)\)')
    datatype_pattern = re.compile(r'\(declare-datatypes \(.*\)\)')
    decfun_pattern = re.compile(r'\(declare-fun .*\)')
    deffun_pattern = re.compile(r'\(define-fun .*\)')

    with open(input_file_path, 'r') as infile:
        for line in infile:
            # 如果匹配到 (assert (not ...)) 形式的行，将其添加到goals列表中
            if assert_not_pattern.search(line):
                goals.append(line.strip())

            if assert_pattern.search(line):
                if not assert_not_pattern.search(line):
                    conjectures.append(line.strip())

            if datatype_pattern.search(line):
                datatypes.append(line.strip())

            if decfun_pattern.search(line) or deffun_pattern.search(line):
                decfuns.append(line.strip())

            elif "(check-sat)" not in line and "(exit)" not in line:
                template_lines.append(line)

    # 如果没有识别到goals，打印反馈
    if not goals:
        print(f"No goals found in file: {input_file_path}")

    generated_lemms_path = os.path.join(output_subfolder, "generated_lemmas.smt2")
    with open(generated_lemms_path, 'w') as generated_lemms:
        generated_lemms.write(";-------------- generated lemmas ---------------\n")

    # 生成template文件
    template_file_path = os.path.join(output_subfolder, "template.smt2")
    with open(template_file_path, 'w') as template_file:
        template_file.write(";-------------- datatypes ---------------\n")
        # for line in template_lines:
        #     template_file.write(line)
        # 在 (check-sat) 之前插入 {invalid_lemmas}, {new_lemmas}, {goals} 占位符
        for datatype in datatypes:
            template_file.write(datatype + '\n')
        template_file.write(";-------------- End of datatypes ---------------\n")
        template_file.write("\n")

        template_file.write(";-------------- conjectures ---------------\n")
        for conjecture in conjectures:
            template_file.write(conjecture + '\n')
        template_file.write(";-------------- End of conjectures ---------------\n")

        template_file.write("\n")
        template_file.write(";------------------------ Goals to prove -----------------------\n")
        for goal in goals:
            template_file.write(goal + '\n')
        template_file.write(";------------------------- End of goals ------------------------\n")

        template_file.write(";-------------- Invalid lemmas generated by LLMs ---------------\n")
        template_file.write("{invalid_lemmas}\n")
        template_file.write(";-------------------- End of invalid lemmas --------------------\n")

        template_file.write(";...... new conjectures ......\n")
        template_file.write("{new_lemmas}\n")
        template_file.write(";---------------------- End of new conjectures ----------------------\n")

    # generate defination files for cvc5 api
    definitions_file_path = os.path.join(output_subfolder, "definitions.smt2")
    with open(definitions_file_path, 'w') as definitions_file:
        for datatype in datatypes:
            definitions_file.write(datatype + '\n')
        for decfun in decfuns:
            definitions_file.write(decfun + '\n')

    # # 生成goals文件
    # goals_file_path = os.path.join(output_subfolder, "goals")
    # with open(goals_file_path, 'w') as goals_file:
    #     for goal in goals:
    #         goals_file.write(goal + "\n")

    # # 生成new_lemmas文件（目前为空）
    # new_lemmas_file_path = os.path.join(output_subfolder, "new_lemmas")
    # with open(new_lemmas_file_path, 'w') as new_lemmas_file:
    #     new_lemmas_file.write("")

    # # 生成invalid_lemmas文件（目前为空）
    # invalid_lemmas_file_path = os.path.join(output_subfolder, "invalid_lemmas")
    # with open(invalid_lemmas_file_path, 'w') as invalid_lemmas_file:
    #     invalid_lemmas_file.write("")

def synthesize_smt2_file(template_path, invalid_lemmas_path, new_lemmas_path, goals_path, output_path):
    """
    根据模板文件、new_lemmas文件和goals文件合成一个新的smt2文件。
    """
    with open(template_path, 'r') as template_file:
        template_content = template_file.read()

    with open(invalid_lemmas_path, 'r') as invalid_lemmas_file:
        invalid_lemmas_content = invalid_lemmas_file.read()

    with open(new_lemmas_path, 'r') as new_lemmas_file:
        new_lemmas_content = new_lemmas_file.read()

    with open(goals_path, 'r') as goals_file:
        goals_content = goals_file.read()

    # 替换模板中的占位符
    synthesized_content = template_content.replace("{new_lemmas}", new_lemmas_content)
    synthesized_content = synthesized_content.replace("{invalid_lemmas}", invalid_lemmas_content)
    synthesized_content = synthesized_content.replace("{goals}", goals_content)

    # 写入合成后的内容到输出文件
    with open(output_path, 'w') as output_file:
        output_file.write(synthesized_content)

if __name__ == "__main__":
    input_folder = "testcases/nosg"  # 输入文件夹路径
    output_folder = "fwzProcessed"  # 输出文件夹路径

    if not os.path.exists(output_folder):
        os.makedirs(output_folder)

    process_files_in_folder(input_folder, output_folder)

    # # 示例：如何使用模板文件合成一个新的smt2文件
    # example_subfolder = os.path.join(output_folder, "nichomachus-goal2")
    # if os.path.exists(example_subfolder):
    #     template_path = os.path.join(example_subfolder, "template")
    #     new_lemmas_path = os.path.join(example_subfolder, "new_lemmas")
    #     invalid_lemmas_path = os.path.join(example_subfolder, "invalid_lemmas")
    #     goals_path = os.path.join(example_subfolder, "goals")
    #     synthesized_smt2_path = os.path.join(example_subfolder, "synthesized.smt2")

    #     synthesize_smt2_file(template_path, invalid_lemmas_path, new_lemmas_path, goals_path, synthesized_smt2_path)
    #     print(f"Synthesized SMT2 file created at: {synthesized_smt2_path}")