Обход Z3Context с помощью API z3.scala.dsl

Я использую инструмент scala^Z3 для небольшой библиотеки, которая (среди прочего) печатает ограничения Z3Context в латексном формате. Хотя можно пройтись по Z3AST и преобразовать выражения в латекс путем сравнения строк, было бы гораздо удобнее использовать объектную структуру пакета z3.scala.dsl. Есть ли способ получить z3.scala.dsl.Tree из Z3AST?


scala latex z3
person Byron Hawkins    schedule 10.06.2012    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Это правда, что DSL в настоящее время «только для записи», в том смысле, что вы можете использовать его для создания деревьев и отправки их в Z3, но не для их обратного чтения.

Стандартный способ чтения деревьев Z3 — использовать getASTKind и getDeclKind от Z3Context. Классы, представляющие результаты: Z3ASTKind< /a> и Z3DeclKind соответственно. (Поскольку большинство деревьев являются приложениями, в последнем содержится большая часть информации).

person Philippe    schedule 11.06.2012
comment
Ах, это намного лучше, чем то, что я пытался сделать :-) Поэтому для гибкости я разрабатываю два латексных преобразования: одно печатает исходное дерево DSL, другое печатает из Z3Context, используя getASTKind и getDeclKind. - person Byron Hawkins; 11.06.2012

arrow_upward
0
arrow_downward

Похоже, способ сделать это — создать исходные ограничения с помощью z3.scala.dsl, а затем добавить каждое ограничение с помощью Z3Context.assertCnstr (tree: Tree[BoolSort]). Таким образом, у меня есть целое дерево DSL для легкого преобразования в латекс. По какой-то причине примеры на сайте scala^Z3 собирают AST вообще без использования DSL, так что этот вариант не был очевиден.

person Byron Hawkins    schedule 11.06.2012