search

potassco / fclingo

Solver for ASP plus conditional linear constraints with founded variables
MIT License
2 stars 0 forks source link

unexpected behaviour with undefined conditions #9

Open wanko opened 1 year ago

wanko commented 1 year ago

Example program test.lp:

&fsum{y:p} = 5.

Expected result:

fclingo version 0.1
Reading from test.lp
Solving...
Answer: 1
p val(y,5)
SATISFIABLE

Actual result:

fclingo version 0.1
Reading from test.lp
-:1:9-10: info: atom does not occur in any rule head:
  p

Solving...
UNSATISFIABLE

Workaround:

#external p.
&fsum{y:p} = 5.
rkaminsk commented 1 year ago

We defined head aggregates in clingo as shortcuts for choices + body aggregates. You can have a look at the AG paper.. There is an explicit literal that goes into the choice. For theory atoms, there is no such literal. There is just a condition meant to derive the set of elements of the theory atom.