add "or false" to a definition breaks it.

[Pierre Carbonnelle]

The following theory admits the solution that jerry shaves himself.

!x y: Shaves(x, y) <- (x=jerry & y=jerry).

If I add " | false " at the end of the definition, jerry does not shave himself anymore !?

Yet, a | false is always the same as a (even in ternary logic).

[Pierre Carbonnelle]

A related, and more significant issue, is that this theory is equivalent to this one (which uses a "or" in the definition, but they yield different results : the first one has no solution (OK), but the second one has one (not OK).

[Ingmar Dasseville]

probably duplicate of Issue #953 which was incorrectly marked resolved

[Ingmar Dasseville]

@Pierre: it is probably safer to use a subtype of string instead of constructed types while there is no new release. The theory would then look like this: http://dtai.cs.kuleuven.be/krr/idp-ide/?src=be4c034584ba1b75e3dec044602f66fe

[Pierre Carbonnelle]

Thanks for the quick reply. I'll try the work-around in my real problem.

[Bart Bogaerts]

If you build IDP yourself, you can also try the fixed version (commit 53b93a0b9b351f2363103de8835d1ee1f01d2309 )

[Bart Bogaerts]

I can confirm that all your examples work well in the fixed version.

[Pierre Carbonnelle]

Good to know. Unfortunately, I don't have access to the source code of idp.

[Bart Bogaerts]

Now you should be able to access it.

[Pierre Carbonnelle]

Indeed. Thanks.

Before I try to compile idp on a Windows machine (not sure if it is easy), could you tell me if you can solve this theory with it ? The previous version could not find a solution, even after 10 hours of trying...

[Pierre Carbonnelle]

And if you can solve it, could you send me the result ?

[Bart Bogaerts]

Hi Pierre,

Some remarks:

• The bug you had should not be present on Windows version of IDP, only on unix versions (as XSB does not work under windows). So, there's no need to resort to the fix if you run on a windows machine.

• If you wish to compile IDP on windows, you should ask @ingdas

• The last theory you sent me does not contain definitions, hence has nothing to do with the current bug

• The problem with your last theory is that you ask all models and there just are a lot of them. On my machine, if I just ask 10.000 models, I can find (and print) them in 6 seconds. To get some models, see http://dtai.cs.kuleuven.be/krr/idp-ide/?src=d90a32f2cae7d62036bab7b6d5091842

[Bart Bogaerts]

edit: The estimated number of models of your theory is someting like 2^4 * 2^4 * 2^4 * 2^4 = 65536 (interpretations for

 authorizesT(Person, Person)
    blocksT(Person, Person)

    authorizesF(Person, Person)
    blocksF(Person, Person)

Checked this, and there are 44464 of them.

[Pierre Carbonnelle]

OK. Thanks.

[Bart Bogaerts]

Merged in graphbug (pull request #414)

Fixed XSB graphing bug. Fixes #953 Fixes #954

→ <<cset 2e889d256f0c>>

[Bart Bogaerts]

The latest release of IDP contains these fixes. https://dtai.cs.kuleuven.be/krr/files/releases/idp/idp-linux-latest.tar.gz