在 PySMT 中将 SMTLib 约束打印到标准输出

问题描述

我在使用 pysmt API 编码时遇到了一些问题。 pysmt 的 GitHub 页面显示了一个关于将任何 SMTLib 兼容求解器与 pysmt 结合使用的示例。它说 pysmt 会将问题交给 stdin 中的求解器。但我找不到任何直接的方法将其打印到标准输出或文件。

解决方法

我从 PySMTsolver.py 读取了一些代码后设法解决了这个问题。因此，当 PySMT 为求解器设置选项时，它期望“成功”作为返回值，当它说“（check-sat）”时，它期望“sat”或“unsat”。所以我写了这个小脚本，它将适当地提供对 PySMT 的响应并将所有约束记录到一个文件中。希望它可以帮助某人。打印后立即刷新字符串很重要，否则求解器将无法获取它们。我最终浪费了一些时间来调试它。

#!/usr/bin/python3
from sys import stdin
import os

os.system('rm out1.smt2')
for line in stdin:
    data = line
    with open('out1.smt2','a') as f:
        f.write(data)
    if 'check-sat' in data:
        print('unsat',flush=True)
    elif 'get-model' in data:
        print('()',flush=True)
    else:
        print('success',flush=True)

pysmt smt smt-lib