Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Spurious answers sets if there are theory atoms with trivially false bodies #71

Closed
rkaminsk opened this issue Sep 15, 2021 · 1 comment

Comments

@rkaminsk
Copy link
Member

If a program contains a theory atom with a trivially false body, then there are too many answer sets. I suspect that clasp treats it like a theory atom in a rule body in this case:

#theory bug {
  t {}; 
  &x/0: t,head       
}.                            
                                     
{c}.
:- c.    
&x { c } :- c.

Hiding the false body a bit produces the right results:

```prolog
#theory bug {
  t {}; 
  &x/0: t,head       
}.                            
                                     
{c,d}.
:- c, d.    
:- c, not d.    
:- not c, d.    
&x { c } :- c.

The aspif of the problematic version is:

asp 1 0 0
1 1 1 1 0 0
1 0 1 2 0 1 1
1 0 0 0 1 1
9 1 0 1 x
9 1 1 1 c
9 4 0 1 1 0
9 5 2 0 1 0
4 1 c 1 1
0

And the output of clasp is:

clasp version 3.3.6
Reading from stdin
Solving...
Answer: 1

Answer: 2

SATISFIABLE

Models       : 2
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s
BenKaufmann added a commit that referenced this issue Sep 18, 2021
* Ensure that theory atoms occurring in the head of a rule are always
  treated as such even if the rule body is known to be false.
@BenKaufmann
Copy link
Contributor

@rkaminsk
Pushed a fix to dev.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants