potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
603 stars 80 forks source link

clingo prints unexpected `ANSWER` when called with `--outf=1` #355

Closed teiesti closed 2 years ago

teiesti commented 2 years ago

When clingo is called with --outf=1, it prints ANSWER making it impossible to use the output directly as a logic program. The problem becomes even more obvious when used with --out-ifs="\n".

Steps to reproduce:

$ echo "a. b. c." | clingo --outf=1 --out-ifs="\n" 0
% clingo version 5.5.1
% Reading from stdin
% Solving...
% Answer: 1
ANSWER
a.
ANSWER
b.
ANSWER
c.
%
% Models         : 1
% Calls          : 1
% Time           : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
% CPU Time       : 0.000s
teiesti commented 2 years ago

cc @MaxOstrowski

rkaminsk commented 2 years ago

The ANSWER line is part of the of the competition format. It is a perfect anchor to use a tool like sed to get the following line.

@BenKaufmann The behavior of the --out-ifs="\n" line is indeed strange. Should this be fixed?

PS: This gives the facts in one line. A robust version splitting this into multiple lines would be more effort. Rather use the json format + a little scripting then.

echo "a. b. c." | clingo --outf=1 | sed -n '/^ANSWER$/{n;p}'

PPS: While somewhat ugly, you can still squeeze the JSON version in one line:

echo "a. b. c." | clingo --outf=2 | python -c 'import json, sys; sys.stdout.write("".join(f"{a}.\n" for a in json.load(sys.stdin)["Call"][0]["Witnesses"][0]["Value"]))'
BenKaufmann commented 2 years ago

The behavior of the --out-ifs="\n" line is indeed strange. Should this be fixed?

It certainly looks strange for the aspcomp 2013 format (and is probably also not correct) but this behavior is actually needed for sat/pb output (v ...) - and that's the reason why it's currently implemented like this.

@teiesti @rkaminsk There is also the option --out-atomf, which you could (mis-)use here. E.g.

$ echo "a. b. c." | clingo  --out-atomf='%0.' --out-ifs='\n' -V0 | head -n -1
a.
b.
c.

or alternatively:

$ echo "a. b. c." | clingo  --out-atomf='__atom(%0).' --out-ifs='\n' | sed -n 's/__atom(\(.*\))\./\1./p'
a.
b.
c. 
rkaminsk commented 2 years ago

Then I am inclined to just close this issue. While the implementation has its quirks, it is doing what it is supposed to. For processing answer sets, the structured JSON format is imo the best way.

PS: It is quite difficult to write a regular expression that correctly matches all atoms. It would have to consider string literals; between quotes anything is possible. That's why I was advocating the JSON output.

BenKaufmann commented 2 years ago

Then I am inclined to just close this issue. While the implementation has its quirks, it is doing what it is supposed to.

I decided to change the logic so that the ANSWER line is no longer repeated. There was also quirk when printing comment/summary lines; I now dropped the use of the specified ifs in these kind of lines.

Of course, if you disagree with these changes or find a problem, I can also revert them.

rkaminsk commented 2 years ago

I hardly ever use the output options. As soon as it gets serious, I use the API or structured output. Getting the quirks out is a good idea, though. So, fine with me.

rkaminsk commented 2 years ago

I update the wip branch and build development binaries. This had to wait a bit to settle some other problems first. Closing now.