It’s hard to express this, but do you think X should be constrained to one in the following example (query check, foo(X))? SWISH -- SWI-Prolog for SHaring
Sorry for previous response, I should have looked more closely. You appear to have figured this out already but
foo(X).
one(X) :- X #= 1.
check(X) :- foo(X), one(X).
/** <examples>
?- check, foo(X).
*/
The X variable in the predicate check is not the same variable as the X in the query. Prolog variable names are local to the clause. So you would have to define:
check(X) :- foo(X), one(X).
Then I believe ?- check(X), foo(X). or, even just ? - check(X). will generate the result you expect.
Indeed the essence of your issue - logic variables in Prolog are not global. And this is not a CLP issue; it’s a Prolog issue.
Doesn’t the query have the variable if it’s required to be in the “answer”? Alternatively, the query contains a variable which is unified with a term containing such a variable? And there’s nothing special about a query - it’s just a conjunction of goals - this applies at any level inside the Prolog program.
clp(r) has the same behavior: SWISH -- SWI-Prolog for SHaring So I assume this is just the way that clp is designed.
I think my personal hangup is that clp constrains unified Prolog variables (duh), which have a scope. I am more used to SMT constraints, where variables are globally declared, and any constraint can refer back to them. In clp, since the constraints are on free variables, which are transient, this is more difficult. It appears there has to be a unification path back from the constraint all the way to the query.
This is awkward for my problem, but maybe with foreach/2 could work okay. I’ll do a little more experimenting.
I appreciate all the discussion.
At the heart of this the question is, given a model, what are the questions you want answered (or what do you want to prove). Your simple example didn’t go into any detail on that. Resolving this should help you decide whether foreach/2 or something else is applicable.
I don’t see the difference between a value being constrained to 1 and being 1. If constraints are implemented using attributed variables, when the value becomes 1, that allows unfreezing other goals and propagation of values. Of course, more sophisticated propagation methods are possible but the attributed variables technique is relatively straightforward.
You’re absolutely right; my response suggesting otherwise was premature and wrong.
I think my confusion was that constraints are on variables, but I really want to talk about constraints on variables that are associated with terms (such as constructor(m1)). I really want a get_var_for_term/2 predicate so that
:- use_module(library(clpb)).
add_constraint :- get_var_for_term(foo, Var), sat(Var =:= 1).
check :- add_constraint, get_var_for_term(foo, Var), (Var == 1 -> writeln('good')).
querying check would succeed and print “good”.
The good news is that the following implementation works for that program:
get_var_for_term(Term, Out) :-
nb_current(Term, Out), !.
get_var_for_term(Term, Out) :-
var(Out),
b_setval(Term, Out), !.
But the bad news is that it doesn’t work for compound terms, and the following implementation does not work for reasons I don’t understand:
get_var_for_term(Term, Out) :-
term_to_var(Term, Var), !,
Var = Out,
true.
get_var_for_term(Term, Out) :-
fresh(Newvar),
assert(term_to_var(Term, Newvar)),
format('Asserting Newvar = ~w~n', NewVar),
Out = Newvar.
But these are not actually problems with the constraint system.
Far be it from me to critique somebody else’s programming style, but heavily using side effects (b_setval, assert) isn’t really logic programming IMO. Rather it’s using Prolog to implement an imperative style program. You can certainly do that but, to some degree, you’re swimming against the current. I might be able to offer some suggestions but, as I said before, I don’t really understand what you’re trying to do.
I had the chance to play around with this some more, and here’s a small demo of what I was trying to do:
:- 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).
% 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))).
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,
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.
Here are the results of my small tests:
?- test.
Can m1 and m2 both be constructors?
Yes
Can m1 be a constructor and m2 be a destructor?
No
Iterating over the possible satisfying labels
[constructor(m1),constructor(m2),constructor(m3),constructor(m4),constructor(m5),destructor(m1),destructor(m2),destructor(m3),destructor(m4),destructor(m5)]
[0,0,0,0,0,0,0,0,0,0]
true ;
[0,0,0,0,0,0,0,1,0,0]
true ;
[0,0,0,0,0,0,1,0,0,0]
true ;
[0,0,0,0,0,0,1,1,0,0]
true ;
[1,1,0,0,0,0,0,0,0,0]
true ;
[1,1,0,0,0,0,0,1,0,0]
true.