将公式转换为 CNF [英] Convert formula to CNF
问题描述
有没有办法使用 z3 将公式转换为 CNF(使用 Tseitsin 样式编码)?我正在寻找类似 simplify
命令的东西,但要保证返回的公式是 CNF.
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.
推荐答案
您可以使用 apply
命令来执行此操作.我们可以为这个命令提供任意的战术/策略.有关 Z3 4.0 中战术和策略的更多信息,请查看教程 http://rise4fun.com/Z3/tutorial/策略
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
命令(help-tactic)
可用于显示Z3 4.0中所有可用的策略及其参数.程序化使用更方便、灵活.以下是基于新 Python API 的教程:http://rise4fun.com/Z3Py/tutorial/strategies..Net 和 C/C++ API 中提供了相同的功能.
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.
以下脚本演示了如何使用此框架将公式转换为 CNF:
The following script demonstrates how to convert a formula into CNF using this framework:
这篇关于将公式转换为 CNF的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!