Hi,
I’m trying to compute constraints on a list of boolean pairs.
Essentially, I want this, but yielding clp(BNR) constraints instead of enumerating solutions:
core_([],0,0).
core_([K-V|T],Tp,Fp):-
[K,V]::boolean,
{(K and V),Tp==Tpn+1},
core_(T,Tpn,Fp).
core_([K-V|T],Tp,Fp):-
[K,V]::boolean,
{(K > V),Fp==Fpn+1},
core_(T,Tp,Fpn).
core(P,Tp,Fp):-
length(P,L),
[Tp,Fp]::integer(0,L),
core_(P,Tp,Fp).
?- P=[1-1,1-_],core(P,Tp,Fp),{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-1],
Tp = 2,
Fp = 0,
Ppv = 1 ;
P = [1-1, 1-0],
Tp = Fp, Fp = 1,
Ppv = 1r2 ;
false.
I tried rewriting as below:
core([],0,0).
core([K-V|T],Tp,Fp):-
[K,V]::boolean,
{
Btp==(K,V),Tp==Tp1+Btp,
Bfp==(K > V),Fp==Fp1+Bfp
},
core(T,Tp1,Fp1).
The conditions on K and V are mutually exclusive, so I would expect: Ppv::real(1r2, 1)
… but in fact, this happens: Ppv::real(0.3333333333333333, 2)
?- P=[1-1,1-_],core(P,Tp,Fp),{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-_A],
Tp::real(1, 2),
Fp::real(0, 1),
_A::boolean,
Ppv::real(0.3333333333333333, 2).
While giving Ppv as input yields expected results in cases :
?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=1r3,{Ppv==Tp/(Tp+Fp)}.
false.
?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=1r2,{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-0],
Tp = Fp, Fp = 1,
Ppv = 1r2.
?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=2,{Ppv==Tp/(Tp+Fp)}.
false.
.. but misses that _A should be 1 in :
?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=1,{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-_A],
Ppv = 1,
Tp::real(1, 2),
Fp::real(0, 1),
_A::boolean.
Why are Ppv bounds 1r3->2 instead of 1r2->1 ?
Thanks !