时间戳

首页 > 解决方案 > z3py 中函数“from_file()”的问题

z3 - z3py 中函数“from_file()”的问题

问题描述

假设我们有以下文件：

    (declare-datatypes (T) ((AVL leafA (nodeA (val T) (alt Int) (izq AVL) (der AVL)))))

     (declare-const t (AVL  Int))

以及以下代码：

    from z3 import *

    s = Solver()

    s.from_file("func.smt")
    s.from_file("espec.smt")

当指令 "s.from_file("espec.smt")" 被执行时，z3 抛出下一个异常：

z3.z3types.Z3Exception: b'(error "line 1 column 18: unknown sort \'AVL\'")\n'

似乎求解器“s”不保存数据类型（以及函数）的信息。这就是他抛出异常的原因（我猜）。

以下代码是解决它的一种方法：

    s = Solver()

    file = open("func.smt", "r")
    func = file.read()
    file.close()

    file = open("espec.smt", "r")
    espec = file.read()
    file.close()

    s.from_string(func + espec)

但是这种方式效率不高。

是否有另一种更有效的方法来解决这个问题并使 z3 为将来的断言和声明保存数据类型和函数？

编辑：

例如，在我的真实案例中，文件“func.smt”在函数和数据类型之间总共有 54 个声明（有些相当复杂）。“spec.smt”文件几乎没有声明和断言。最后我有一个文件，其中有许多断言，我必须一点一点地阅读并生成一个模型。

也就是说，假设我有 600 行断言，我从 10 到 10 读取，所以每 10 行我生成一个模型。也就是说，如果我们假设我已经读取的那些断言存储在一个名为“aux”的变量中，那么每次我想要获得一个新模型时，我都必须执行“s.from_string (func + spec + aux)”总共 60 次，我不知道这是否可以提高效率。

标签： z3solverz3py

解决方案

正如您发现的那样，单独读取文件并加载到求解器是您最好的选择。

除非效率是最重要的，否则我不会担心进一步优化它。对于任何合理的问题，您的求解器时间将支配从几个（或几千个！）文件加载断言所花费的任何时间。您是否有一个真正需要这部分显着加快的用例？

推荐阅读