Tabling with coinductive mode for predicate

This commit is contained in:
Theo 2013-12-20 14:56:13 +00:00
parent ffa0823e57
commit e105130a8b
3 changed files with 50 additions and 44 deletions

View File

@ -404,6 +404,8 @@ static Int p_tabling_mode( USES_REGS1 ) {
t = MkPairTerm(MkAtomTerm(AtomBatched), t); t = MkPairTerm(MkAtomTerm(AtomBatched), t);
else if (IsMode_Local(TabEnt_flags(tab_ent))) else if (IsMode_Local(TabEnt_flags(tab_ent)))
t = MkPairTerm(MkAtomTerm(AtomLocal), t); t = MkPairTerm(MkAtomTerm(AtomLocal), t);
if (IsMode_CoInductive(TabEnt_flags(tab_ent)))
t = MkPairTerm(MkAtomTerm(AtomCoInductive), t);
t = MkPairTerm(MkAtomTerm(AtomDefault), t); t = MkPairTerm(MkAtomTerm(AtomDefault), t);
t = MkPairTerm(t, TermNil); t = MkPairTerm(t, TermNil);
if (IsMode_LocalTrie(TabEnt_mode(tab_ent))) if (IsMode_LocalTrie(TabEnt_mode(tab_ent)))
@ -458,6 +460,9 @@ static Int p_tabling_mode( USES_REGS1 ) {
SetMode_GlobalTrie(TabEnt_mode(tab_ent)); SetMode_GlobalTrie(TabEnt_mode(tab_ent));
return(TRUE); return(TRUE);
} }
} else if (value == 7) { /* coinductive */ //only affect the predicate flag. Also it cant be unset
SetMode_CoInductive(TabEnt_flags(tab_ent));
return(TRUE);
} }
} }
return (FALSE); return (FALSE);

View File

@ -513,7 +513,7 @@
GONext(); GONext();
#ifdef INCOMPLETE_TABLING #ifdef INCOMPLETE_TABLING
} else if (SgFr_state(sg_fr) == incomplete) { } else if (SgFr_state(sg_fr) == incomplete) {
if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { if (IsMode_CoInductive(TabEnt_flags(tab_ent))) {
printf("Currently Unsupported\n"); printf("Currently Unsupported\n");
} else { } else {
/* subgoal incomplete --> start by loading the answers already found */ /* subgoal incomplete --> start by loading the answers already found */
@ -531,7 +531,7 @@
} }
#endif /* INCOMPLETE_TABLING */ #endif /* INCOMPLETE_TABLING */
} else if (SgFr_state(sg_fr) == evaluating) { } else if (SgFr_state(sg_fr) == evaluating) {
if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { if (IsMode_CoInductive(TabEnt_flags(tab_ent))) {
/* Used for coinductive tabling strategy */ /* Used for coinductive tabling strategy */
CELL *subs_ptr; CELL *subs_ptr;
subs_ptr = (CELL *) (GEN_CP(SgFr_gen_cp(sg_fr)) + 1); subs_ptr = (CELL *) (GEN_CP(SgFr_gen_cp(sg_fr)) + 1);
@ -673,7 +673,7 @@
GONext(); GONext();
#ifdef INCOMPLETE_TABLING #ifdef INCOMPLETE_TABLING
} else if (SgFr_state(sg_fr) == incomplete) { } else if (SgFr_state(sg_fr) == incomplete) {
if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { if (IsMode_CoInductive(TabEnt_flags(tab_ent))) {
printf("Currently Unsupported\n"); printf("Currently Unsupported\n");
} else { } else {
/* subgoal incomplete --> start by loading the answers already found */ /* subgoal incomplete --> start by loading the answers already found */
@ -691,7 +691,7 @@
} }
#endif /* INCOMPLETE_TABLING */ #endif /* INCOMPLETE_TABLING */
} else if (SgFr_state(sg_fr) == evaluating) { } else if (SgFr_state(sg_fr) == evaluating) {
if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { if (IsMode_CoInductive(TabEnt_flags(tab_ent))) {
printf("Currently Unsupported\n"); printf("Currently Unsupported\n");
} else { } else {
/* subgoal in evaluation */ /* subgoal in evaluation */
@ -821,7 +821,7 @@
GONext(); GONext();
#ifdef INCOMPLETE_TABLING #ifdef INCOMPLETE_TABLING
} else if (SgFr_state(sg_fr) == incomplete) { } else if (SgFr_state(sg_fr) == incomplete) {
if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { if (IsMode_CoInductive(TabEnt_flags(tab_ent))) {
printf("Currently Unsupported\n"); printf("Currently Unsupported\n");
} else { } else {
/* subgoal incomplete --> start by loading the answers already found */ /* subgoal incomplete --> start by loading the answers already found */
@ -839,7 +839,7 @@
} }
#endif /* INCOMPLETE_TABLING */ #endif /* INCOMPLETE_TABLING */
} else if (SgFr_state(sg_fr) == evaluating) { } else if (SgFr_state(sg_fr) == evaluating) {
if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { if (IsMode_CoInductive(TabEnt_flags(tab_ent))) {
/* Used for coinductive tabling strategy */ /* Used for coinductive tabling strategy */
CELL *subs_ptr; CELL *subs_ptr;
subs_ptr = (CELL *) (GEN_CP(SgFr_gen_cp(sg_fr)) + 1); subs_ptr = (CELL *) (GEN_CP(SgFr_gen_cp(sg_fr)) + 1);

View File

@ -250,6 +250,7 @@ tabling_mode(Pred,Options) :-
'$transl_to_pred_flag_tabling_mode'(4,load_answers). '$transl_to_pred_flag_tabling_mode'(4,load_answers).
'$transl_to_pred_flag_tabling_mode'(5,local_trie). '$transl_to_pred_flag_tabling_mode'(5,local_trie).
'$transl_to_pred_flag_tabling_mode'(6,global_trie). '$transl_to_pred_flag_tabling_mode'(6,global_trie).
'$transl_to_pred_flag_tabling_mode'(7,coinductive).