The following code is supposed to work just like clingo but print each answer in a sorted manner.
from clingo.application import Application, clingo_main
class ClingoApp(Application):
def print_model(self, model, printer) -> None:
print(" ".join(sorted(str(s) for s in model.symbols(shown=True))))
def main(self, ctl, files):
for f in files:
ctl.load(f)
if not files:
ctl.load("-")
ctl.ground([("base", [])])
ctl.solve()
clingo_main(ClingoApp())
If run in the terminal, that is exactly what it happen. For instance
$echo "a. b." | python sortedclingo_printer.py
clingo version 5.6.2
Reading from stdin
Solving...
Answer: 1
a b
SATISFIABLE
Models : 1+
Calls : 1
Time : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.001s
but if the output is redirected we may get
$echo "a. b." | python sortedclingo_printer.py | cat
clingo version 5.6.2
Reading from stdin
Solving...
Answer: 1
SATISFIABLE
Models : 1+
Calls : 1
Time : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.001s
a b
with the output printed at the last line instead after Answer: 1
I think this is because python and C++ code use different buffers and when they are flushed is non-deterministic. In fact, if sys.stdout.flush() is added at the end of the print_model() function, then it works as intended.
I think this is quite prone to difficult to debug errors and it would be nice if it worked as intended without explicitly flushing the output. Specially, because the print() function flushed with each new line when run in a terminal but in block when the output goes to a file or a pipe.
The following code is supposed to work just like clingo but print each answer in a sorted manner.
If run in the terminal, that is exactly what it happen. For instance
but if the output is redirected we may get
with the output printed at the last line instead after
Answer: 1
I think this is because python and C++ code use different buffers and when they are flushed is non-deterministic. In fact, if
sys.stdout.flush()
is added at the end of theprint_model()
function, then it works as intended.I think this is quite prone to difficult to debug errors and it would be nice if it worked as intended without explicitly flushing the output. Specially, because the
print()
function flushed with each new line when run in a terminal but in block when the output goes to a file or a pipe.