A toy encoding of OO rules using CLPB

f.pl

:- use_module(library(clpb)).

term_to_atom(T, Atom) :-
    term_hash(T, Hash),
    term_string(Hash, S),
    atom_string(Atom, S).

get_var_for_term(Term, Out) :-
    term_to_atom(Term, Atom),
    nb_current(Atom, Out), !.

get_var_for_term(Term, Out) :-
	var(Out),
    term_to_atom(Term, Atom),
    b_setval(Atom, Out), !.

% Add constraint that M is definitely a constructor
isConstructor(M) :- get_var_for_term(constructor(M), V), V = 1.
isNOTConstructor(M) :- get_var_for_term(constructor(M), V), V = 0.

isDestructor(M) :- get_var_for_term(destructor(M), V), V = 1.
isNOTDestructor(M) :- get_var_for_term(destructor(M), V), V = 0.

% These are the input facts...

method(m1).
method(m2).
method(m3).
method(m4).
method(m5).

possibleConstructor(m1).
possibleConstructor(m2).

possibleDestructor(m2).
possibleDestructor(m3).

certainConstructorOrDestructor(m2).

% m1 is a constructor iff m2 is.
connected_constructors(m1, m2).

% End facts

% A method cannot be both a constructor and a destructor
check1(M) :-
    get_var_for_term(constructor(M), CV),
    get_var_for_term(destructor(M), DV),
    sat(~(CV * DV)).


check(M) :-
    check1(M).

check :- foreach(method(M), check(M)).

ruleNOTConstructor(M) :-
    not(possibleConstructor(M)) -> isNOTConstructor(M).

ruleNOTConstructor :-
    foreach(method(M), ignore(ruleNOTConstructor(M))).

ruleNOTDestructor(M) :-
    not(possibleDestructor(M)) -> isNOTDestructor(M).

ruleNOTDestructor :-
    foreach(method(M), ignore(ruleNOTDestructor(M))).

ruleCertainCtorOrDtor(M) :- certainConstructorOrDestructor(M) -> get_var_for_term(constructor(M), C), get_var_for_term(destructor(M), D), sat(C # D).

ruleCertainCtorOrDtor :- foreach(method(M), ignore(ruleCertainCtorOrDtor(M))).

ruleConnectedConstructors(M1, M2) :- get_var_for_term(constructor(M1), C1), get_var_for_term(constructor(M2), C2), C1 = C2.

ruleConnectedConstructors :-
    foreach(connected_constructors(M1, M2),
            ruleConnectedConstructors(M1, M2)).

rules :-
    check,
    ruleNOTConstructor,
    ruleNOTDestructor,
    ruleCertainCtorOrDtor,
    ruleConnectedConstructors.

test1 :-
    writeln('Can m1 and m2 both be constructors?'),
    (rules, isConstructor(m1), isConstructor(m2) -> writeln('Yes'); writeln('No')).

test2 :-
    % Can m1 be a constructor and m2 be a constructor? (No)
    writeln('Can m1 be a constructor and m2 be a destructor?'),
    (rules, isConstructor(m1), isDestructor(m2) -> writeln('Yes'); writeln('No')).

test3 :-
    writeln('Iterating over the possible satisfying labels'),
    rules,
    setof(F, FactType^Method^(member(FactType, [constructor, destructor]), method(Method), F =.. [FactType, Method]), TermSet),
    writeln(TermSet),
    maplist(get_var_for_term, TermSet, Out),
    term_variables(Out, Vars),
    labeling(Vars),
    writeln(Out).

test :- ignore((test1, fail)), ignore((test2, fail)), test3.