Let's assume that we have the following files:
(declare-datatypes (T) ((AVL leafA (nodeA (val T) (alt Int) (izq AVL) (der AVL)))))
(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:
z3.z3types.Z3Exception: b'(error "line 1 column 18: unknown sort \'AVL\'")\n'
It seems that the Solver "s" doesn't save the information of datatypes (and functions too). 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?
Edit:
In my real case for example, the file "func.smt" has a total of 54 declarations between functions and datatypes (some quite complex). The "spec.smt" file has few declarations and asserts. 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. 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.
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?