Преобразование Z3 формулы CNF в представление списка списков с использованием Z3Py

Question

Учитывая формулу Z3 в CNF, можно ли преобразовать ее в представление списка списков с помощью Z3Py? Я хотел бы сделать это для облегчения доступа и манипулирования литералами. Если Python был функциональный язык, я мог бы сделать что-то вроде

def cnf2list(fm) : 
    match fm with 
    | And(P,Q) -> cnf2list(P) + cnf2list(Q) 
    | P -> clause2list(P) 

def clause2list(fm) : 
    match fm with 
    | Or(P,Q) -> clause2list(P) + clause2list(Q) 
    | P -> [P] 

Но я не уверен, что я могу сделать это в Python. Возможно ли выполнить сопоставление с образцом, как указано выше (или использовать какой-то совсем другой метод), чтобы получить представление списка рецептов формулы Z3 CNF?

Answer 1

Там нет сравнения с шаблоном, но z3py позволяет контролировать Z3 выражения:

def clause2list(expr): 
    if z3.is_const(expr): 
     return [str(expr)] 
    elif z3.is_or(expr): 
     return [atom for disjunct in expr.children() 
        for atom in clause2list(disjunct)] 
    else: 
     assert False, ('not supported', expr) 

x, y, z = z3.Bools('x y z') 
print(clause2list(z3.Or(x, y, z))) 
# ['x', 'y', 'z'] 

Поддержка отрицаний, союзами, и истинные и ложные литералов в качестве упражнения :) См z3.py, Ctrl-F "def is_".

Обратите внимание, что моя реализация возвращает списки имен переменных вместо самих переменных Z3. Это из-за предупреждения Christoph Wintersteiger's. Если вы намерены выполнять какую-либо обработку в этих списках, символическое значение __eq__ скорее всего не то, что вы хотите.

---

Я не знаю, что проблема, которую вы пытаетесь решить, но если вы создаете У себя, рассмотреть их производство в списках списка-в-форма с самого начала. Легче преобразовать список списков в выражение Z3, чем наоборот.

Answer 2

Я не эксперт Python любых средств, а просто положить скобки [...] вокруг выражений, а затем с помощью оператора + для конкатенации делает построить несколько списков, например, вот так:

from z3 import * 

x = Int('x') 
y = Int('y') 
z = Int('z') 

print(x) 
print(y) 
print(z) 
lst = [x] + [y] 
print(lst) 
s = sum(lst) 
print(s) 
lst.reverse() 
print(lst) 
print(x in lst) 

Однако, элемент comparsions, кажется, дают неожиданные результаты, например, эти:

print(z in lst) 
print(lst.count(x)) 

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