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

Question

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

Answer 1

在阅读了 PySMT solver.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)