Unsatcore vs modelexpand

[Ingmar Dasseville]

unsatcore says there are models

modelexpand says there aren't

=> bug

http://dtai.cs.kuleuven.be/krr/idp-ide/?src=e0531052bf0ce8062761

[Bart Bogaerts]

Misschien iets te maken met Warning: Currently, no support for definitions that have recursive agg regates

[Bart Bogaerts]

Smaller bug

http://dtai.cs.kuleuven.be/krr/idp-ide/?src=7a493515042d7792e03f

[Bart Bogaerts]

Reverse bug!!!!

http://dtai.cs.kuleuven.be/krr/idp-ide/?src=e74ad8cedaf5f21dbbfa

[Bart Bogaerts]

Something weird is going on here!

The reverse bug is because of XSB http://dtai.cs.kuleuven.be/krr/idp-ide/?src=390a0afb872f13ecc579

[Ruben Lapauw]

Voor de reverse bug: merk op dat de definitie zelf inconsistent is.

Deze definieert geen functie. Blijkbaar controleert de grounder niet genoeg of iets een functie is.

[Ruben Lapauw]

Het is misschien een verkeerde theorietransformatie: Deze regel werkt wel:

RA(a,b) = x <- (x = EA(a,b)) | (! y : x ~=y => y ~= EA(a,b) & x = RA1(a,b)) & ?z : z = RA1(a,b).

http://dtai.cs.kuleuven.be/krr/idp-ide/?src=4e00685e5b2714cf0a38

[Bart Bogaerts]

Inderdaad, Er lijkt in XSB een controle te weinig te zitten of iets wel degelijk een (partiele) functie is. De UNSAT core is zeer goed bij de reverse bug. Ik splits deze issue af., zie #881