Is there a way to use z3 to convert a formula to CNF (using Tseitsin-style encoding)? I am looking for something like the simplify command, but guaranteeing that the returned formula is CNF.
You can use the apply command for doing it. We can provide arbitrary tactics/strategies to this command. For more information about tactics and strategies in Z3 4.0, check the tutorial http://rise4fun.com/Z3/tutorial/strategies
The command (help-tactic) can be used to display all available tactics in Z3 4.0 and their parameters. The programmatic is more convenient to use and flexible. Here is a tutorial based on the new Python API: http://rise4fun.com/Z3Py/tutorial/strategies.
The same capabilities are available in the .Net and C/C++ APIs.
The following script demonstrates how to convert a formula into CNF using this framework: