z3 - z3py中的函数“ from_file（）”出现问题(Problem with function “from_file()” at z3py)

Question

Let's assume that we have the following files:

(假设我们有以下文件：)

• func.smt

  (func.smt)

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

• espec.smt

  (espec.smt)

     (declare-const t (AVL  Int))

And the following code:

(和以下代码：)

    from z3 import *

    s = Solver()

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

When instruction "s.from_file("espec.smt")" is executed, z3 throws the next exception:

(执行指令“ s.from_file（“ espec.smt”）“时，z3引发下一个异常：)

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

It seems that the Solver "s" doesn't save the information of datatypes (and functions too).

(似乎规划求解“ s”没有保存数据类型的信息（以及函数）。)

That is why he throws the exception (I guess).

(这就是为什么他抛出异常（我想）。)

The following code is a way to solve it:

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

    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)

But this way it's not efficient.

(但是这种方式效率不高。)

Is there another more efficient way to solve this and make z3 save datatypes and functions for future asserts and declarations?

(还有另一种更有效的方法来解决此问题，并使z3保存数据类型和函数以用于将来的断言和声明吗？)

Edit:

(编辑：)

In my real case for example, the file "func.smt" has a total of 54 declarations between functions and datatypes (some quite complex).

(以我的实际情况为例，文件“ func.smt”在函数和数据类型之间（总共相当复杂）总共有54个声明。)

The "spec.smt" file has few declarations and asserts.

(“ spec.smt”文件具有很少的声明和断言。)

And finally I have a file in which there are many asserts which I have to read little by little and generate a model.

(最后，我有一个文件，其中包含许多断言，我必须一点一点地阅读它们并生成一个模型。)

That is, imagine that I have 600 lines of asserts, and I read from 10 to 10, so every 10 lines I generate a model.

(也就是说，假设我有600条断言，并且我从10到10进行读取，所以每10行就会生成一个模型。)

That is, if we assume that those asserts that I have read are stored in a variable called "aux", every time I want to get a new model, I will have to do "s.from_string (func + spec + aux)" 60 times in total, and I don't know if that could be made more efficient.

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

  ask by alecille translate from so

Answer 1

Separately reading the files and loading to solver is your best bet, as you found out.

(如您所知，单独读取文件并将其加载到求解器是您最好的选择。)

Unless efficiency is of paramount importance, I would not worry about trying to optimize this any further.

(除非效率是最重要的，否则我不会担心尝试进一步优化它。)

For any reasonable problem, your solver time will dominate any time spent in loading the assertions from a few (or a few thousand!) files.

(对于任何合理的问题，您的求解器时间将占据从几个（或几千个！）文件中加载断言所花费的时间。)

Do you have a use case that really requires this part to be significantly faster?

(您是否有一个用例，确实需要该部分要快得多？)