Reputation: 1
when using the #external-directive in combination with reification in clingo, I noticed a discrepancy that I cannot explain. Here is a minimal working example.
Take as a program test.lp
p:- not p.
p:- p.
q:- q.
p:- not r.
#external p.
#external q.
#external r.
When I run clingo --output=reify test.lp
, I get the following:
external(1,false).
external(2,false).
external(3,false).
atom_tuple(0).
atom_tuple(0,3).
literal_tuple(0).
literal_tuple(0,-1).
rule(disjunction(0),normal(0)).
atom_tuple(1).
atom_tuple(1,2).
literal_tuple(1).
literal_tuple(1,2).
rule(disjunction(1),normal(1)).
literal_tuple(2).
literal_tuple(2,-3).
rule(disjunction(0),normal(2)).
literal_tuple(3).
literal_tuple(3,3).
rule(disjunction(0),normal(3)).
output(p,3).
output(q,1).
literal_tuple(4).
literal_tuple(4,1).
output(r,4).
atom_tuple(1,2), literal_tuple(1,2) and rule(disjunction(1),normal(1)) correspond to the rule q:-q.
However, what I don't understand is why we have output(q,1). I would have expected output(q,2) here. What am I missing here?
Thanks
Upvotes: 0
Views: 18