potassco / clingo

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

gringo output syntac #432

Closed hharryyf closed 1 year ago

hharryyf commented 1 year ago

Hi, I'm trying to establish a dependency graph of an answer set program at the ground atom level. Basically, when we have a rule a :- b, I want to draw an edge b -> a. This is just my entire goal. However, in some cases, the "gringo --text" can give me a ground program not just containing normal logic program. It can contain things like #delayed(1) <=> 1<=#count{0,f(1):f(1)}<=1 I know #delay is normally because of recursive program or choice rules. My main problem is I don't know how to identify f(1) is a ground atom. So, I'm wondering, is there a syntax manual for possible gringo output? Thanks.

rkaminsk commented 1 year ago

The gringo output syntax is mostly a subset of its input language sans a few corner cases. Have a look at #331 for some more info. I want to really make it a subset at some point but did not find the time yet.

mingodad commented 1 year ago

I showed how to get a railroad diagram for the grammar here https://github.com/potassco/clingo/issues/429 and I think that it can help.

hharryyf commented 1 year ago

Hi, thanks for your reply. I realized I don't need to parse the gringo output to do my task, I just need the smodels output. I have an additional question: in the smodels output format, suppose I have only have normal rules, cardinality rules and choice rules, can I expect that in clingo --output=smodels, all the rules (in numerical format) are of "implication" form. In other words, in smodels output, there's nothing like "#delay(1) <=> count{...}"? All of the "if and only if" are rewritten to "implication" form as well?

rkaminsk commented 1 year ago

We switched to the aspif format a long time ago. The smodels format does not support all the systems features. Note that there is also an API to intercept the output. Check the following:

hharryyf commented 1 year ago

Thanks for your reply. I'm a bit confused is there a documentation on what systems features does "smodels" support? I think some of the tools I'm using still need the smodels format. And I only need to use a very small subset of the ASP language. Normal logic rule, choice rules like 1 {choices} 1 :- body of literals, and cardinality rules with integrity constraints, :- a {choices} b. Also, when you say smodels format does not support, will it output an error if the non-support features are present?

rkaminsk commented 1 year ago

Thanks for your reply. I'm a bit confused is there a documentation on what systems features does "smodels" support? I think some of the tools I'm using still need the smodels format. And I only need to use a very small subset of the ASP language. Normal logic rule, choice rules like 1 {choices} 1 :- body of literals, and cardinality rules with integrity constraints, :- a {choices} b. Also, when you say smodels format does not support, will it output an error if the non-support features are present?

Both formats are equally easy to parse. You can compare the two formats having a look at the appendices of:

Both formats cover the language fragments you are mentioning. Note however that the rules you are mentioning are rewritten. The formats support only choice rules (without bounds) and cardinality/weight rules with lower bounds.

hharryyf commented 1 year ago

Thanks for your reply. Let me confirm my understanding is correct. Both aspif and smodels format support the language features I mentioned, however, in smodels, the output program is logically "equivalent" but does not look exactly the same as the input program (that's why it's not line-oriented). Because some choice rules, and cardinality rules need to be rewritten to the format you described (e.g. choice rules without bounds).

rkaminsk commented 1 year ago

Thanks for your reply. Let me confirm my understanding is correct. Both aspif and smodels format support the language features I mentioned, however, in smodels, the output program is logically "equivalent" but does not look exactly the same as the input program (that's why it's not line-oriented). Because some choice rules, and cardinality rules need to be rewritten to the format you described (e.g. choice rules without bounds).

This applies to both formats. There is no one to one mapping. The clingo (via clasp) ships the lpconvert tool. You can use it to convert between formats and also get a textual representation via the --text format to see what happens.

hharryyf commented 1 year ago

Hi, thanks a lot for your reply. I have another question related to ground programs. If my original ungrounded program has no negative dependency cycles (i.e. it is stratified), can the program output by smodels or aspif contain negative cycles?

rkaminsk commented 1 year ago

A locally stratified program will have a stratified grounding. And then there are also some more programs that will have stratified groundings. Clingo will not introduce negative cycles.