How to get every clauses of a CNF formula in Z3

user_14483825 0
Viewed 127

like in the code below, Is there any function in Z3 to get all the clauses of a formula(as a CNF)?

x = Boolean('x')
y = Boolean('y')

f = And(x, Or(x,y),And(x,Not(x,y))
# can I get all the clauses of formula f stored in a list
z3 boolean-logic
1 Answers

You can do something like the following:

from z3 import *

x = Bool('x')    #  Note: Bool() rather than Boolean()
y = Bool('y')
z = Bool('z')

f = And(x, Or(x,y), And(x, z == Not(y)))

#  from https://stackoverflow.com/a/18003288/1911064

g = Goal()
g.add(f)
    
# use describe_tactics() to get to know the tactics available

t = Tactic('tseitin-cnf')
clauses = t(g)

for clause in clauses[0]:
    print(clause)

Output is a list of disjunctive clauses:

x
Or(x, y)
Or(y, z)
Or(Not(y), Not(z))

Your original expression is not satisfiable.

What is Not(x, y) supposed to do?

As simpler way to convert (nested) Boolean expressions to CNF is provided by bc2cnf.

user_19110640
Related