SMT公式处理与求解的解算器不可知库
PySMT的Python项目详细描述
Pysmt使可满足性模理论的工作变得简单。
其中，您可以：
- 以独立于解算器的方式定义公式 迭代法，
- 编写即席简化器和运算符，
- 将问题以smt lib格式转储，
- 使用本机解算器之一解算它们，或通过包装任何 SMT LIB投诉解决程序。
支持的理论和求解器
Pysmt提供了在线性实数运算（LRA）中定义公式的方法， 实差逻辑（RDL）、它们的组合（LIRA） 等式和非意外函数（EUF）、位向量（BV）和数组（A）。 通过本机API支持以下解算器：
- 数学卫星（http://mathsat.fbk.eu/）
- z3（https://github.com/Z3Prover/z3/）
- cvc4（http://cvc4.cs.nyu.edu/web/）
- 易斯2（http://yices.csl.sri.com/）
- cudd（http://vlsi.colorado.edu/~fabio/CUDD/）
- 微微卫星（http://fmv.jku.at/picosat/）
- boolector（http://fmv.jku.at/boolector/）
此外，您可以使用任何符合SMT-LIB 2的解算器。
pysmt假设安装了smt解算器的python绑定，并且 从你的Python身上。
pysmt对python 3和python 2都有效。
想知道更多吗？
欢迎加入QQ群-->： 979659372
