Print SMTLib constraints to stdout in PySMT

Question

I have some problem encoded using PySMT APIs. PySMT's GitHub page shows an example about using any SMTLib compliant solver with PySMT. It says that PySMT will give the problem to solver in stdin. But I can't find any straightforward way of printing this to stdout or to a file.

Answer 1

I manged to solve the issue after reading some code from PySMT solver.py. So when PySMT sets an option for the solver, it expectes "success" as the return value and when it says "(check-sat)" it expects "sat" or "unsat". So I wrote this small script which will provide responses to PySMT appropriately and log all constraints to a file. Hope it helps someone. It is important to flush the strings immediately after printing or the solver will not get them. I ended up wasting some time trying to debug that.

#!/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)