Учитывая сортировку Z3 и строку s, я пытаюсь создать константу Z3 такого рода с именем s.
Например, учитывая IntSort() и имя "x", я хотел бы получить целочисленную константу с именем "x".
Я знаю, что могу заставить его вызывать Int('x'), но поскольку я создаю эти переменные динамически, я не могу предсказать, какой вид будет иметь данная переменная. Что мне нужно сделать, так это создать переменную того же типа, что и предоставленная системой, но с новым именем (которое я должен указать во время выполнения).
Чтобы быть более конкретным,
1. I get a model for a user defined formula calling the Z3 Solver on it,
2. I save it in a database (recording for each assignment in such a model the variable name, the value to be assigned to it and the sort of that variable)
3. I retrieve that assignment after a while from the database and I try it o a new formula having the same variables of the original one.
Для этого я превращаю каждое задание в предложение вида var == value, добавляю их в решатель вместе с целевой формулой и проверяю на выполнимость.
До сих пор я работал только с целочисленной сортировкой, поэтому я жестко запрограммировал преобразование строки в константу с помощью функции Int. Теперь я пытаюсь обобщить подход к разным логикам и разным типам данных, поэтому мне нужно что-то для создания правильной константы из того, что я сохранил в своей базе данных.
По вашему мнению, такой подход разумен? Как вы думаете, есть ли какой-нибудь трюк, чтобы сделать это лучше?
