оценка выражений массива

Question

Я использую c-api для Z3-3.2 (для linux) для решения проблем QF_AUFBV.

Если формула является выполнимой, я хотел бы прочитать значение переменных свободного массива из модели.

Я пытался что-то вдоль линий следующего кода, и я хотел бы знать, если общая идея о том, как сделать это правильно:

void evaluate(Z3_context context, Z3_model model, Z3_ast array) 
{ 
    Z3_ast value; 
    Z3_bool success = Z3_eval(context, model, array, &value); 
    if (success) { 
    unsigned num_entries; 
    if (Z3_is_array_value(context, model, value, &num_entries)) { 
     Z3_ast indices[num_entries]; 
     Z3_ast values[num_entries]; 
     Z3_ast def; 
     Z3_get_array_value(context, model, array, num_entries, indices, values, &def); 

     // do something with indices, values, and def 
    } 
    } 
} 

Входной Z3_ast массив, безусловно, свободное выражение массив , Z3_eval возвращает true, поэтому мы, похоже, успешно оценили это выражение, но тогда Z3_is_array_value возвращает false. Я бы ожидал, что результат успешного Z3_eval в выражении массива будет значением массива, так почему же это не так?

Кстати: Нам удалось получить нужную информацию, итерации по всем файлам model_func_decls и поиск подходящего для этого массива путем сравнения их get_symbol_string. Таким образом, информация, по-видимому, доступна где-то в Z3, но это вряд ли считается хорошим решением.

Спасибо за любую помощь по этому вопросу.

С наилучшими пожеланиями, Флориан

Answer 1

оценщик является немного более мощным, чем API для доступа к значениям массива. Функция is_array_value выполняется только тогда, когда представленный массив имеет вид (магазин (магазин (магазин (... (const v) ...) ..) ..)) или формы as-array [f ], где f - конечная унарная функция.

is_array_value и get_array_value функция может быть реализована с использованием существующего API и подвергается для удобства (как вы описываете, за исключение того, мы можем не использовать сравнение строк и вместо того, чтобы использовать сравнения на объявление функций, которые перечисление сорта). Похоже, мы сможем поддерживать больше в вашем случае, и мне любопытно, как выглядит модель . Вы могли бы предоставить дополнительную информацию о примере, который не проходит? (распечатать?)

Thanks