Conversion de la formule CNF Z3 en représentation de liste de listes à l'aide de Z3Py

Question

Étant donné une formule Z3 dans CNF, est-il possible de la convertir en une liste de listes avec Z3Py? Je voudrais le faire pour faciliter l'accès et la manipulation des littéraux. Si Python était un langage fonctionnel, je pourrais faire quelque chose comme

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] 

Mais je ne suis pas sûr que je peux le faire en Python. Est-il possible d'effectuer un appariement de modèles comme ci-dessus (ou d'utiliser une méthode entièrement différente) pour obtenir une représentation par liste de listes d'une formule CNF Z3?

Answer 1

Il n'y a pas de correspondance de motif, mais z3py permet d'inspecter les expressions 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'] 

Soutien aux négations, conjonctions et littéraux vrai et le faux est laissé comme un exercice :) Voir z3.py, ctrl-f "def is_".

Notez que mon implémentation renvoie des listes de noms de variables au lieu des variables Z3 elles-mêmes. C'est à cause de l'avertissement Christoph Wintersteiger's. Si vous avez l'intention de faire un traitement sur ces listes, le symbole __eq__ n'est probablement pas ce que vous voulez.

---

Je ne sais pas quel est le problème que vous essayez de résoudre, mais si vous générez CNF vous, pensez à les produire dans la liste-de-listes forment dès le début. Il est plus facile de convertir une liste de listes en une expression Z3 que l'inverse.

Answer 2

Je ne suis pas un expert en Python par tout moyen, mais simplement mettre entre parenthèses [...] autour des expressions puis en utilisant l'opérateur + pour la concaténation ne construit certaines listes, par exemple, comme ceci:

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) 

Cependant, les comparsions d'éléments semblent donner des résultats inattendus, par exemple ceux-ci:

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

à ce stade, je ne suis pas sûr que j'utilise des listes Python de façon inattendue ou si c'est un Z3 Python Problème d'API