Получение символических значений с использованием Z3

Пожалуйста, обратите внимание на следующие утверждения.Получение символических значений с использованием Z3

у: = 10

г: = х + у

После того, как эти два утверждения выполняются "г" имеет значение "Х + 10", где "х" представляет символическое стоимость; такие символические значения важны при проверке программы - например, для вычисления характеристик пути с использованием самого слабого метода предсказания Дейкстра.

Теперь рассмотрим следующий код для Z3.

(declare-const x Int) 
(declare-const y Int) 
(declare-const z Int) 

(assert (= y 10)) 
(assert (= z (+ x y))) 

(check-sat) 
(get-value (z))

Он производит следующий вывод, поскольку он рассмотрит интерпретацию, где «у» имеет 10 и «х» имеет значение 0.

sat 

((z 10))

Есть ли какой-нибудь способ, которым я могу сделать Z3 производить выход «x + 10»? то есть, я заинтересован в получении символических значений в терминах переменных, которые не были созданы с какими-либо конкретными значениями.

источник

2014-04-16 LKB

«в терминах переменных, которые не были экземпляры с какими-либо конкретными значениями»: Вы имеете в виду без ограничений переменных или переменных, которые являются постоянными? Если вы просто хотите обрабатывать константу, это можно сделать простой заменой. – Tushar

Поскольку вычисление слабого предварительного условия связано в основном с заменой - я думаю, что замена должна выполнять эту работу. Но, как сказал Хуан Оспина, нет ли альтернативы в Z3-SMT-LIB, соответствующей его коду в Z3Py? – LKB

Я не уверен в этом. Однако я считаю, что C++ API имеет более гибкие возможности, чем Z3-SMT-LIB. – Tushar

Я не эксперт, но я думаю, что использовать Z3-SMT-LIB невозможно. Но можно использовать Z3Py.

x = Int('x') 
y = 10 
z = x + y 
print z

и выход

x + 10

источник

2014-04-16 11:01:42

Это просто замена. Нет никакого вызова фактическому решателю. Если я даю z3py, следующий код: {x = Int ('x') y = Int ('y') z = Int ('z') доказать (и (z == x + y, y == 10))}, я получаю вывод {counterexample [y = 10, z = 1, x = -10]}, который не является тем, что ищет LKB. Доказательный вызов фактически вызывает решателя SMT. – Tushar

Привет, Тушар, ты прав. Дело в том, что когда решатель называется выходом, это числовое значение, это не символическое выражение. Вы согласны? –

Да, согласен. Я знаю, что в C++ API есть функция eval, в которой выражение z3 может быть оценено на другое выражение z3, просматривая модель z3. Если модель z3 является неполной (т. Е. Не имеет оценок для неограниченных переменных), то она должна быть способна дать мне выражение Z3, которое является символическим выражением, а не численным значением. Тем не менее, последний раз, когда я проверил, он сообщает об ошибке и ожидает, что клиент установит завершение модели в true, и в этом случае z3 eval даст числовое значение. – Tushar

Получение символических значений с использованием Z3

ответ

Смежные вопросы