diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

CoInductive tabling

Browse Source
This commit is contained in:
Theo 2013-12-19 16:56:55 +00:00
parent 1f0f9968df
commit b4506cf793
7 changed files with 114 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
C/stdpreds.c
View File

@ -1676,6 +1676,8 @@ p_access_yap_flags( USES_REGS1 )
tout = MkPairTerm(MkAtomTerm(AtomLocal), tout); tout = MkPairTerm(MkAtomTerm(AtomLocal), tout);
else if (IsMode_Batched(yap_flags[flag])) else if (IsMode_Batched(yap_flags[flag]))
tout = MkPairTerm(MkAtomTerm(AtomBatched), tout); tout = MkPairTerm(MkAtomTerm(AtomBatched), tout);
else if (IsMode_CoInductive(yap_flags[flag]))
tout = MkPairTerm(MkAtomTerm(AtomCoInductive), tout);
#else #else
tout = MkAtomTerm(AtomFalse); tout = MkAtomTerm(AtomFalse);
#endif /* TABLING */ #endif /* TABLING */
@ -1818,6 +1820,13 @@ p_set_yap_flags( USES_REGS1 )
tab_ent = TabEnt_next(tab_ent); tab_ent = TabEnt_next(tab_ent);
} }
SetMode_GlobalTrie(yap_flags[TABLING_MODE_FLAG]); SetMode_GlobalTrie(yap_flags[TABLING_MODE_FLAG]);
} else if (value == 7) { /* CoInductive */
tab_ent_ptr tab_ent = GLOBAL_root_tab_ent;
while(tab_ent) {
SetMode_CoInductive(TabEnt_mode(tab_ent));
tab_ent = TabEnt_next(tab_ent);
}
SetMode_CoInductive(yap_flags[TABLING_MODE_FLAG]);
} }
break; break;
#endif /* TABLING */ #endif /* TABLING */

1
H/iatoms.h
View File

@ -54,6 +54,7 @@
AtomColomn = Yap_LookupAtom(":"); AtomColomn = Yap_LookupAtom(":");
AtomCodeSpace = Yap_LookupAtom("code_space"); AtomCodeSpace = Yap_LookupAtom("code_space");
AtomCodes = Yap_LookupAtom("codes"); AtomCodes = Yap_LookupAtom("codes");
AtomCoInductive = Yap_LookupAtom("coinductive");
AtomComma = Yap_LookupAtom(","); AtomComma = Yap_LookupAtom(",");
AtomCommentHook = Yap_LookupAtom("comment_hook"); AtomCommentHook = Yap_LookupAtom("comment_hook");
AtomCompound = Yap_LookupAtom("compound"); AtomCompound = Yap_LookupAtom("compound");

1
H/ratoms.h
View File

@ -54,6 +54,7 @@
AtomColomn = AtomAdjust(AtomColomn); AtomColomn = AtomAdjust(AtomColomn);
AtomCodeSpace = AtomAdjust(AtomCodeSpace); AtomCodeSpace = AtomAdjust(AtomCodeSpace);
AtomCodes = AtomAdjust(AtomCodes); AtomCodes = AtomAdjust(AtomCodes);
AtomCoInductive = AtomAdjust(AtomCoInductive);
AtomComma = AtomAdjust(AtomComma); AtomComma = AtomAdjust(AtomComma);
AtomCommentHook = AtomAdjust(AtomCommentHook); AtomCommentHook = AtomAdjust(AtomCommentHook);
AtomCompound = AtomAdjust(AtomCompound); AtomCompound = AtomAdjust(AtomCompound);

2
H/tatoms.h
View File

@ -106,6 +106,8 @@
#define AtomCodeSpace Yap_heap_regs->AtomCodeSpace_ #define AtomCodeSpace Yap_heap_regs->AtomCodeSpace_
Atom AtomCodes_; Atom AtomCodes_;
#define AtomCodes Yap_heap_regs->AtomCodes_ #define AtomCodes Yap_heap_regs->AtomCodes_
Atom AtomCoInductive_;
#define AtomCoInductive Yap_heap_regs->AtomCoInductive_
Atom AtomComma_; Atom AtomComma_;
#define AtomComma Yap_heap_regs->AtomComma_ #define AtomComma Yap_heap_regs->AtomComma_
Atom AtomCommentHook_; Atom AtomCommentHook_;

136
OPTYap/tab.insts.i
View File

@ -513,27 +513,64 @@
GONext(); GONext();
#ifdef INCOMPLETE_TABLING #ifdef INCOMPLETE_TABLING
} else if (SgFr_state(sg_fr) == incomplete) { } else if (SgFr_state(sg_fr) == incomplete) {
/* subgoal incomplete --> start by loading the answers already found */ printf("Yoho1\n");
ans_node_ptr ans_node = SgFr_first_answer(sg_fr);
CELL *subs_ptr = YENV; /* subgoal incomplete --> start by loading the answers already found */
init_subgoal_frame(sg_fr); ans_node_ptr ans_node = SgFr_first_answer(sg_fr);
UNLOCK_SG_FR(sg_fr); CELL *subs_ptr = YENV;
SgFr_try_answer(sg_fr) = ans_node; init_subgoal_frame(sg_fr);
store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER); UNLOCK_SG_FR(sg_fr);
PREG = (yamop *) CPREG; SgFr_try_answer(sg_fr) = ans_node;
PREFETCH_OP(PREG); store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER);
load_answer(ans_node, subs_ptr); PREG = (yamop *) CPREG;
YENV = ENV; PREFETCH_OP(PREG);
GONext(); load_answer(ans_node, subs_ptr);
YENV = ENV;
GONext();
#endif /* INCOMPLETE_TABLING */ #endif /* INCOMPLETE_TABLING */
} else if (SgFr_state(sg_fr) == evaluating) { } else if (SgFr_state(sg_fr) == evaluating) {
/* subgoal in evaluation */ if (IsMode_CoInductive(TabEnt_mode(tab_ent))) {
choiceptr leader_cp; printf("Hi!\n");
int leader_dep_on_stack; } else {
find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack); printf("Ok\n");
}
printf("Yoho2\n");
/* Used for coinductive tabling strategy */
CELL *subs_ptr;
subs_ptr = (CELL *) (GEN_CP(SgFr_gen_cp(sg_fr)) + 1);
subs_ptr += SgFr_arity(sg_fr); // Points at the Parent goal Variables
int i;
for (i = 0; i < subs_ptr[0]; i++)
Yap_unify(subs_ptr[i+1], YENV[i+1]);
/* yes answer --> procceed */
UNLOCK_SG_FR(sg_fr); UNLOCK_SG_FR(sg_fr);
find_leader_node(leader_cp, leader_dep_on_stack); PREG = (yamop *) CPREG;
store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack); PREFETCH_OP(PREG);
YENV = ENV; // Consume the variables
GONext(); // Succeed the goal :-D
// printf("I'm here\n Arity: %i Count: %i\n", subs_ptr[0], sg_fr->TempVariables.Count);
// printf("YENV: %i, ENV: %i, YENV+1: %i, ENV+1: %i\n", YENV[0], ENV[0], YENV[1], ENV[1]);
/* for (i = 0; i < sg_fr->TempVariables.Count; i++) {
Yap_unify(sg_fr->TempVariables.OriginalVariables[i], sg_fr->TempVariables.CycleVariables[i]);
printf("Variable: %i is O: %i C: %i H: %i E: %i\n", i, sg_fr->TempVariables.OriginalVariables[i], sg_fr->TempVariables.CycleVariables[i], subs_ptr[i+1], YENV[i+1]);
}
printf("I'm out of here\n");*/
/* subgoal in evaluation */
/* choiceptr leader_cp;
int leader_dep_on_stack;
find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack);
UNLOCK_SG_FR(sg_fr);
find_leader_node(leader_cp, leader_dep_on_stack);
store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack);
*/
#ifdef DEBUG_OPTYAP #ifdef DEBUG_OPTYAP
if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) { if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) {
choiceptr aux_cp; choiceptr aux_cp;
@ -653,27 +690,31 @@
GONext(); GONext();
#ifdef INCOMPLETE_TABLING #ifdef INCOMPLETE_TABLING
} else if (SgFr_state(sg_fr) == incomplete) { } else if (SgFr_state(sg_fr) == incomplete) {
/* subgoal incomplete --> start by loading the answers already found */ printf("Yoho3\n");
ans_node_ptr ans_node = SgFr_first_answer(sg_fr); /* subgoal incomplete --> start by loading the answers already found */
CELL *subs_ptr = YENV; ans_node_ptr ans_node = SgFr_first_answer(sg_fr);
init_subgoal_frame(sg_fr); CELL *subs_ptr = YENV;
UNLOCK_SG_FR(sg_fr); init_subgoal_frame(sg_fr);
SgFr_try_answer(sg_fr) = ans_node; UNLOCK_SG_FR(sg_fr);
store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER); SgFr_try_answer(sg_fr) = ans_node;
PREG = (yamop *) CPREG; store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER);
PREFETCH_OP(PREG); PREG = (yamop *) CPREG;
load_answer(ans_node, subs_ptr); PREFETCH_OP(PREG);
YENV = ENV; load_answer(ans_node, subs_ptr);
GONext(); YENV = ENV;
GONext();
#endif /* INCOMPLETE_TABLING */ #endif /* INCOMPLETE_TABLING */
} else if (SgFr_state(sg_fr) == evaluating) { } else if (SgFr_state(sg_fr) == evaluating) {
/* subgoal in evaluation */ printf("Yoho4\n");
choiceptr leader_cp;
int leader_dep_on_stack;
find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack); /* subgoal in evaluation */
UNLOCK_SG_FR(sg_fr); choiceptr leader_cp;
find_leader_node(leader_cp, leader_dep_on_stack); int leader_dep_on_stack;
store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack); find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack);
UNLOCK_SG_FR(sg_fr);
find_leader_node(leader_cp, leader_dep_on_stack);
store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack);
#ifdef DEBUG_OPTYAP #ifdef DEBUG_OPTYAP
if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) { if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) {
choiceptr aux_cp; choiceptr aux_cp;
@ -793,6 +834,7 @@
GONext(); GONext();
#ifdef INCOMPLETE_TABLING #ifdef INCOMPLETE_TABLING
} else if (SgFr_state(sg_fr) == incomplete) { } else if (SgFr_state(sg_fr) == incomplete) {
printf("Yoho5\n");
/* subgoal incomplete --> start by loading the answers already found */ /* subgoal incomplete --> start by loading the answers already found */
ans_node_ptr ans_node = SgFr_first_answer(sg_fr); ans_node_ptr ans_node = SgFr_first_answer(sg_fr);
CELL *subs_ptr = YENV; CELL *subs_ptr = YENV;
@ -807,13 +849,29 @@
GONext(); GONext();
#endif /* INCOMPLETE_TABLING */ #endif /* INCOMPLETE_TABLING */
} else if (SgFr_state(sg_fr) == evaluating) { } else if (SgFr_state(sg_fr) == evaluating) {
printf("Yoho6\n");
/* Used for coinductive tabling strategy */
CELL *subs_ptr;
subs_ptr = (CELL *) (GEN_CP(SgFr_gen_cp(sg_fr)) + 1);
subs_ptr += SgFr_arity(sg_fr); // Points at the Parent goal Variables
int i;
for (i = 0; i < subs_ptr[0]; i++)
Yap_unify(subs_ptr[i+1], YENV[i+1]);
/* yes answer --> procceed */
UNLOCK_SG_FR(sg_fr);
PREG = (yamop *) CPREG;
PREFETCH_OP(PREG);
YENV = ENV; // Consume the variables
GONext(); // Succeed the goal :-D
/* subgoal in evaluation */ /* subgoal in evaluation */
choiceptr leader_cp; /* choiceptr leader_cp;
int leader_dep_on_stack; int leader_dep_on_stack;
find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack); find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack);
UNLOCK_SG_FR(sg_fr); UNLOCK_SG_FR(sg_fr);
find_leader_node(leader_cp, leader_dep_on_stack); find_leader_node(leader_cp, leader_dep_on_stack);
store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack); store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack);*/
#ifdef DEBUG_OPTYAP #ifdef DEBUG_OPTYAP
if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) { if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) {
choiceptr aux_cp; choiceptr aux_cp;

3
OPTYap/tab.macros.h
View File

@ -88,6 +88,7 @@ static inline tg_sol_fr_ptr CUT_prune_tg_solution_frames(tg_sol_fr_ptr, int);
#define Flag_LocalTrie 0x100 #define Flag_LocalTrie 0x100
#define Flag_GlobalTrie 0x200 #define Flag_GlobalTrie 0x200
#define Flags_TrieMode (Flag_LocalTrie | Flag_GlobalTrie) #define Flags_TrieMode (Flag_LocalTrie | Flag_GlobalTrie)
#define Flag_CoInductive 0x008
#define SetMode_Batched(X) (X) = ((X) & ~Flags_SchedulingMode) | Flag_Batched #define SetMode_Batched(X) (X) = ((X) & ~Flags_SchedulingMode) | Flag_Batched
#define SetMode_Local(X) (X) = ((X) & ~Flags_SchedulingMode) | Flag_Local #define SetMode_Local(X) (X) = ((X) & ~Flags_SchedulingMode) | Flag_Local
@ -95,12 +96,14 @@ static inline tg_sol_fr_ptr CUT_prune_tg_solution_frames(tg_sol_fr_ptr, int);
#define SetMode_LoadAnswers(X) (X) = ((X) & ~Flags_AnswersMode) | Flag_LoadAnswers #define SetMode_LoadAnswers(X) (X) = ((X) & ~Flags_AnswersMode) | Flag_LoadAnswers
#define SetMode_LocalTrie(X) (X) = ((X) & ~Flags_TrieMode) | Flag_LocalTrie #define SetMode_LocalTrie(X) (X) = ((X) & ~Flags_TrieMode) | Flag_LocalTrie
#define SetMode_GlobalTrie(X) (X) = ((X) & ~Flags_TrieMode) | Flag_GlobalTrie #define SetMode_GlobalTrie(X) (X) = ((X) & ~Flags_TrieMode) | Flag_GlobalTrie
#define SetMode_CoInductive(X) (X) = (X) | Flag_CoInductive
#define IsMode_Batched(X) ((X) & Flag_Batched) #define IsMode_Batched(X) ((X) & Flag_Batched)
#define IsMode_Local(X) ((X) & Flag_Local) #define IsMode_Local(X) ((X) & Flag_Local)
#define IsMode_ExecAnswers(X) ((X) & Flag_ExecAnswers) #define IsMode_ExecAnswers(X) ((X) & Flag_ExecAnswers)
#define IsMode_LoadAnswers(X) ((X) & Flag_LoadAnswers) #define IsMode_LoadAnswers(X) ((X) & Flag_LoadAnswers)
#define IsMode_LocalTrie(X) ((X) & Flag_LocalTrie) #define IsMode_LocalTrie(X) ((X) & Flag_LocalTrie)
#define IsMode_GlobalTrie(X) ((X) & Flag_GlobalTrie) #define IsMode_GlobalTrie(X) ((X) & Flag_GlobalTrie)
#define IsMode_CoInductive(X) ((X) & Flag_CoInductive)

1
misc/ATOMS
View File

@ -59,6 +59,7 @@ A CleanCall F "$clean_call"
A Colomn N ":" A Colomn N ":"
A CodeSpace N "code_space" A CodeSpace N "code_space"
A Codes N "codes" A Codes N "codes"
A CoInductive N "coinductive"
A Comma N "," A Comma N ","
A CommentHook N "comment_hook" A CommentHook N "comment_hook"
A Compound N "compound" A Compound N "compound"