учитывая выражение x'=x+1, я хочу переименовать x' в y. Как сделать с помощью z3?
Как переименовать переменную с помощью Z3?
Ответы (1)
Существует ряд функций API, которые позволяют изменять термины и заменять старые подтермины новыми. Они описаны в разделе «Модификаторы», который содержит модификаторы Z3_update_term, z3_substitute и Z3_substitute_vars (есть также Z3_translate для переноса терминов между двумя контекстами). Ссылка здесь:
http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa7497c70a827db2d61ba98889fe657b5
Вы также можете напрямую просматривать термины и писать утилиты для изменения терминов. В примере display_ast показаны основные случаи рекурсивного обхода терминов:
http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi__ex.html#ga807b5fe0e26acdec09e52a77318208d0
person
Nikolaj Bjorner
schedule
02.09.2012
Спасибо, однако, есть ли какие-либо API-функции С#, которые я могу использовать для изменения терминов, замены старых подтерминов новыми?
- person ; 03.09.2012
Да, соответствующая функция в C# называется Substitute и находится в классе Expr. Также есть Expr.Update и Expr.Translate и т.д.
- person Christoph Wintersteiger; 03.09.2012
Вы, наверное, спасли 5 дней моей жизни, спасибо. Проблема с C++ API заключается в том, что в нем нет исчерпывающего руководства, за исключением файла `example.cpp' в исходном коде, а просмотр документации очень громоздкий. Вы знаете хороший источник, чтобы узнать это?
- person Giacomo Tagliabue; 17.04.2013
Как вы рекомендуете заменить функциональный символ на другой? Например, я хотел бы заменить все вхождения функции f на функцию g. Для формулы f(a) › f(b) это даст g(a) › g(b).
- person rsinha; 21.07.2014
