20 lines
322 B
20 lines
322 B
# coding: utf-8
|
|
from z3 import *
|
|
|
|
# Create an instance of a z3 solver
|
|
|
|
solver = None
|
|
|
|
# Declare needed z3 variables
|
|
|
|
# Add the needed constraints to check equivalence of the two formulae.
|
|
|
|
# solver.add(...)
|
|
|
|
|
|
# Check and print the result.
|
|
|
|
result = solver.check()
|
|
print(result)
|
|
if result == sat:
|
|
print(solver.model())
|