Символьные переменные в z3

Есть ли способ заставить решатель z3 выдавать «символические» решения? Например, для уравнения:

1+x=c

решение x=c-1, но z3 всегда выдает определенную модель, например [c = 0, x = -1]. Как «определить» c как символическую переменную?


solver z3 smt
person user1367401    schedule 27.06.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

К сожалению, Z3 не предоставляет такой функциональности. Хотя мы используем решатели внутри компании, они не отображаются в API. В будущих версиях мы хотим раскрыть внутренние компоненты, такие как: решатель, процедуры баз Гробнера и т. д. В текущей версии у нас есть тактика под названием solve-eqs (см. http://rise4fun.com/Z3Py/tutorial/strategies). Он устраняет переменные, используя обобщение исключения Гаусса. Однако это этап предварительной обработки, и вы не можете контролировать, какие переменные исключаются.

person Leonardo de Moura    schedule 27.06.2012
comment
Любое обновление для этого? Есть ли API для получения символьных решений в версии 4.5 Z3? - person Torgny; 21.03.2017