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

Question

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

Answer 1

在阅读了PySMT solver.py的一些代码后，我设法解决了这个问题。因此，当PySMT为求解器设置一个选项时，它期望返回值为"success“，当它说"(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)