search

potassco / ngo

Non Ground Optimizer for logic programs.
MIT License
4 stars 0 forks source link

math trait wrong translation of negated disjunction #106

Closed MaxOstrowski closed 8 months ago

MaxOstrowski commented 8 months ago 
{foo(1..10)}.
:- not #inf <= #sum {Y : foo(Y) } 15.

Currently ngo math trait removes the second rule, but the correct meaning would be #inf > #sum {Y : foo(Y) } OR #sum {Y : foo(Y) } > 15

example provided by @henryotunuya

MaxOstrowski commented 8 months ago

Its more complicated than this:

{foo(1..10)}.
:- #inf <= #sum {Y : foo(Y) } 15.

is also removed, as inf is translated with infinity, and math with infinity is always fun and not weird at all.

Solution:

  1. ignore negated 2 sided aggregates
  2. ignore comparisons including #inf or #sup
  3. remove trivial #inf and #sup in preprocessing
MaxOstrowski commented 8 months ago

Definition of funny: Temporary helping formulas of the form -infinity = auxvar become -infinity - auxvar = 0 become -inifinity = 0 ;)