Вывести ограничения SMTLib на стандартный вывод в PySMT

Question

У меня проблема с кодированием с использованием API-интерфейсов PySMT. На странице PySMT на GitHub показан пример использования любого SMTLib-совместимого решателя с PySMT. В нем говорится, что PySMT передаст проблему для решения в stdin. Но я не могу найти простой способ распечатать это на стандартный вывод или в файл.

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)