#71 Subsumptive tabl. doesn't recognize fully instantiated goal

[Henrik Pilegaard]

When I run the program below, which is an analysis of a
discretionary ambient program, I encounter a problem.

The program is correct and computes well in another
solver.

When I run it in XSB (with demo.) I get the following
error msg:
****************************************************************
Answer Return ERROR: Failed to unify answer
ret(s_1_1,r,overlineopen(p,r))
with Answer Template:
ret(\"s_1_1\",\"r\",overlineopen(\"s_1_1\",\"r\"))
(* Note: this template may be partially instantiated *)
++Error[XSB]: [Runtime/C] Unequal Constants
! Aborting...
Removing incomplete tables...
*****************************************************************
To me this implies that XSB fails to recognize the
answer template
as a fully instantiated answer, which is sort of
orthogonal to the
subsumption unification bug corrected in version 2.4.
Notice that
the relevant predicates are also tabled subsumptively.

:- import length/2 from basics.

pRG(t, *, amb(p)).
pRG(*, p, in(s_1_1)).
pRG(*, p, overlinein(r, p)).
pRG(*, p, open(r)).
pRG(t, *, amb(s_1_1)).
pRG(*, s_1_1, overlinein(p, s_1_1)).
pRG(*, s_1_1, overlineout(p, s_1_1)).
pRG(*, s_1_1, amb(r)).
pRG(s_1_1, r, in(p)).
pRG(s_1_1, r, overlineopen(p, r)).
pRG(s_1_1, r, out(s_1_1)).
pRG(s_1_1, r, in(s_2_1)).
pRG(*, s_1_1, amb(r)).
pRG(s_1_1, r, in(p)).
pRG(s_1_1, r, overlineopen(p, r)).
pRG(s_1_1, r, out(s_1_1)).
pRG(s_1_1, r, in(s_1_2)).
pRG(t, *, amb(s_1_2)).
pRG(*, s_1_2, overlinein(p, s_1_2)).
pRG(*, s_1_2, overlineout(p, s_1_2)).
pRG(*, s_1_2, amb(r)).
pRG(s_1_2, r, in(p)).
pRG(s_1_2, r, overlineopen(p, r)).
pRG(s_1_2, r, out(s_1_2)).
pRG(s_1_2, r, in(s_2_2)).
pRG(t, *, amb(s_2_1)).
pRG(*, s_2_1, overlinein(p, s_2_1)).
pRG(*, s_2_1, overlineout(p, s_2_1)).
pRG(*, s_2_1, amb(r)).
pRG(s_2_1, r, in(p)).
pRG(s_2_1, r, overlineopen(p, r)).
pRG(s_2_1, r, out(s_2_1)).
pRG(s_2_1, r, in(s_2_2)).
pRG(t, *, amb(s_2_2)).
pRG(*, s_2_2, overlinein(p, s_2_2)).
calI(Top, Star, Mu) :- amb(Mu) = T_1, pRG(Top, Star, T_1).
calI(Top_1, Star_2, T_1_4) :- in(Mu_3) = T_1_4,
pRG(Top_1, tar_2,
T_1_4).
calI(Mup, Mu_3, Mua) :- in(Mu_3) = T_1_4, pRG(Top_1,
Star_2, T_1_4),
overlinein(Mua, Mu_3) = T_2, calI(Mup, Mu_3, T_2),
calI(Muq, Mup, Mu_3),
calI(Mup, Mua, T_1_4), calI(Muq, Mup, Mua).
calI(Mu_3, Mua, U_1) :- in(Mu_3) = T_1_4, pRG(Top_1,
Star_2, T_1_4),
overlinein(Mua, Mu_3) = T_2, calI(Mup, Mu_3, T_2),
calI(Muq, Mup, Mu_3),
calI(Mup, Mua, T_1_4), calI(Muq, Mup, Mua), calI(Mup,
Mua, U_1).
calI(Top_5, Star_6, T_1_8) :- out(Mu_7) = T_1_8,
pRG(Top_5, Star_6,
T_1_8).
calI(Muq_10, Mug, Mua_9) :- out(Mu_7) = T_1_8,
pRG(Top_5, Star_6,
T_1_8), overlineout(Mua_9, Mu_7) = T_2_11, calI(Mug,
Mu_7, T_2_11),
calI(Muq_10, Mug, Mu_7), calI(Mu_7, Mua_9, T_1_8),
calI(Mug, Mu_7,
Mua_9).
calI(Mug, Mua_9, U_1_12) :- out(Mu_7) = T_1_8,
pRG(Top_5, Star_6,
T_1_8), overlineout(Mua_9, Mu_7) = T_2_11, calI(Mug,
Mu_7, T_2_11),
calI(Muq_10, Mug, Mu_7), calI(Mu_7, Mua_9, T_1_8),
calI(Mug, Mu_7,
Mua_9), calI(Mu_7, Mua_9, U_1_12).
calI(Top_13, Star_14, T_1_16) :- open(Mu_15) = T_1_16,
pRG(Top_13,
Star_14, T_1_16).
calI(Muq_18, Mup_17, U_1_20) :- open(Mu_15) = T_1_16,
pRG(Top_13,
Star_14, T_1_16), overlineopen(Mup_17, Mu_15) =
T_2_19, calI(Mup_17,
Mu_15, T_2_19), calI(Muq_18, Mup_17, Mu_15),
calI(Muq_18, Mup_17,
T_1_16), calI(Mup_17, Mu_15, U_1_20).
calI(Top_21, Star_22, T_1_24) :- overlinein(Mu_23,
MuPr) = T_1_24,
pRG(Top_21, Star_22, T_1_24).
calI(Top_25, Star_26, T_1_29) :- overlineout(Mu_27,
MuPr_28) = T_1_29,
pRG(Top_25, Star_26, T_1_29).
calI(Top_30, Star_31, overlineopen(Mu, Mu1)) :-
pRG(Top_30, Star_31,
overlineopen(Mu, Mu1)).
:- table pRG/3.
:- use_subsumptive_tabling(pRG/3).
:- table calI/3.
:- use_subsumptive_tabling(calI/3).
demo :- shell(\'rm -f tablexsb2.P.al\'),
tell(\'tablexsb2.P.al\'),
cputime(A0),
write(\'calI/3 = \'),
setof((X1,Y1,Z1),calI(X1,Y1,Z1),Q1), write(Q1),
nl,length(Q1, L1), write(L1),nl,nl,
cputime(A1), told, Time is A1 - A0,
open(\'tablexsb.dat\', \'append\',
File), write(File, 2),write(File, \' \'),
write(File, 6), write(File,
\' \'),write(File, L1), write(File, \'
\'),write(File, Time), write(File, \'
\'), close(File)

[Theresa Swift]

Logged In: YES
user_id=13011

Fixed this a while ago -- 11/05 I think. The program is now in table_tests in
the test suite.