Negation in chr program

I’m working on adding chr to a program for abductive reasoning. I use this to ask what conditions are necessary for a predicate to be true.
Up to now the program made use of negation as failure to consider unproven facts as false, but with chr it doesn’t work.

A simple example:

:- use_module(library(chr)).					

:- chr_constraint professor/1, rich/1, has_student/2.
professor(X), rich(X) ==> fail.

happy(X):- rich(X).
happy(X):- professor(X), has_good_students(X).

    \+ has_student(X, bad_student).

In my mind this should have answered with two possibilities to the query happy(bob):

  • rich(bob)
  • professor(bob), not has_student(X, bad_student).

The second option is missing. I must be missing something.
It’s the first time I reason with chr.

CHR constraints do not behave as normal predicates. If you run listing(has_student), you’ll not see facts you stated, eg. has_student('bob', 'peter'). Instead there’s a pretty cryptic chunk of code that wires the constrained variables with frozen goals that later apply the constraint rules. So \+ has_student(X, bad_student) does not check if there is a bad student, it states that there should be one within a negation, which fails because there’s nothing to disprove it.

You can achieve what you want by doing this instead:

has_good_students(X), has_student(X, bad_student) ==> false.

So that running has_good_students(X) will constrain X so that later running has_student(X, bad-student) will fail.

Is it possible to have something like not has_student(X, bad_student) in the solutions?
If I run happy(X) I get the following:

rich(mario) ;

I would like to have it say:

rich(mario) ;
+ has_student(mario, bad_student).

I don’t think there’s a generic way to do this. I don’t see any form of negation supported by CHR system provided by SWI Prolog and from what I understand CHR rules are isolated per-module, so there’s probably no way to implement a generic operator.

Closest you could get is write a negated constraint has_not_student/2 yourself:

has_not_student(X, S), has_student(X, S) <=> false.
has_good_students(X) <=> has_not_student(X, bad_student).

Thanks @AmbientTea . This seems to be close to what I intended.
Just one more thing…
The code is now:

:- use_module(library(chr)).					

:- dynamic has_student/2.

:- chr_constraint professor/1, rich/1, has_student/2, has_good_students/1, has_student/1, not_has_student/2.
professor(X), rich(X) ==> fail.

% Exception in CHR.
not_has_student(X, S), has_student(X, S) ==> false.
has_good_students(X) <=> not_has_student(X, bad_student).

happy(X):- rich(X).
happy(X):- professor(X), has_good_students(X).

If I load this file and run assert(has_student(bob, bad_student) and query happy(bob) I still get has_good_students(bob) as a possible solution.
But it should not be true.

If you intend to assert has_student as a fact then it should not be a CHR constraint. Constraints are put on variables to limit how these variables can be instantiated in the future and they’re not asserted, they’re called like normal predicates.