From b4506cf79392359380bbcfd0522e153544b43d87 Mon Sep 17 00:00:00 2001 From: Theo Date: Thu, 19 Dec 2013 16:56:55 +0000 Subject: [PATCH] CoInductive tabling --- C/stdpreds.c | 9 +++ H/iatoms.h | 1 + H/ratoms.h | 1 + H/tatoms.h | 2 + OPTYap/tab.insts.i | 136 +++++++++++++++++++++++++++++++------------- OPTYap/tab.macros.h | 3 + misc/ATOMS | 1 + 7 files changed, 114 insertions(+), 39 deletions(-) diff --git a/C/stdpreds.c b/C/stdpreds.c index c5f6ca20d..da5ad3d9e 100644 --- a/C/stdpreds.c +++ b/C/stdpreds.c @@ -1676,6 +1676,8 @@ p_access_yap_flags( USES_REGS1 ) tout = MkPairTerm(MkAtomTerm(AtomLocal), tout); else if (IsMode_Batched(yap_flags[flag])) tout = MkPairTerm(MkAtomTerm(AtomBatched), tout); + else if (IsMode_CoInductive(yap_flags[flag])) + tout = MkPairTerm(MkAtomTerm(AtomCoInductive), tout); #else tout = MkAtomTerm(AtomFalse); #endif /* TABLING */ @@ -1818,6 +1820,13 @@ p_set_yap_flags( USES_REGS1 ) tab_ent = TabEnt_next(tab_ent); } 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; #endif /* TABLING */ diff --git a/H/iatoms.h b/H/iatoms.h index 4d0dc419c..6102b7d8a 100644 --- a/H/iatoms.h +++ b/H/iatoms.h @@ -54,6 +54,7 @@ AtomColomn = Yap_LookupAtom(":"); AtomCodeSpace = Yap_LookupAtom("code_space"); AtomCodes = Yap_LookupAtom("codes"); + AtomCoInductive = Yap_LookupAtom("coinductive"); AtomComma = Yap_LookupAtom(","); AtomCommentHook = Yap_LookupAtom("comment_hook"); AtomCompound = Yap_LookupAtom("compound"); diff --git a/H/ratoms.h b/H/ratoms.h index 412d2532b..216126cc0 100644 --- a/H/ratoms.h +++ b/H/ratoms.h @@ -54,6 +54,7 @@ AtomColomn = AtomAdjust(AtomColomn); AtomCodeSpace = AtomAdjust(AtomCodeSpace); AtomCodes = AtomAdjust(AtomCodes); + AtomCoInductive = AtomAdjust(AtomCoInductive); AtomComma = AtomAdjust(AtomComma); AtomCommentHook = AtomAdjust(AtomCommentHook); AtomCompound = AtomAdjust(AtomCompound); diff --git a/H/tatoms.h b/H/tatoms.h index bdbce87ba..2c400fffd 100644 --- a/H/tatoms.h +++ b/H/tatoms.h @@ -106,6 +106,8 @@ #define AtomCodeSpace Yap_heap_regs->AtomCodeSpace_ Atom AtomCodes_; #define AtomCodes Yap_heap_regs->AtomCodes_ + Atom AtomCoInductive_; +#define AtomCoInductive Yap_heap_regs->AtomCoInductive_ Atom AtomComma_; #define AtomComma Yap_heap_regs->AtomComma_ Atom AtomCommentHook_; diff --git a/OPTYap/tab.insts.i b/OPTYap/tab.insts.i index 67820772c..2ff59446c 100644 --- a/OPTYap/tab.insts.i +++ b/OPTYap/tab.insts.i @@ -513,27 +513,64 @@ GONext(); #ifdef INCOMPLETE_TABLING } else if (SgFr_state(sg_fr) == incomplete) { - /* subgoal incomplete --> start by loading the answers already found */ - ans_node_ptr ans_node = SgFr_first_answer(sg_fr); - CELL *subs_ptr = YENV; - init_subgoal_frame(sg_fr); - UNLOCK_SG_FR(sg_fr); - SgFr_try_answer(sg_fr) = ans_node; - store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER); - PREG = (yamop *) CPREG; - PREFETCH_OP(PREG); - load_answer(ans_node, subs_ptr); - YENV = ENV; - GONext(); +printf("Yoho1\n"); + + /* subgoal incomplete --> start by loading the answers already found */ + ans_node_ptr ans_node = SgFr_first_answer(sg_fr); + CELL *subs_ptr = YENV; + init_subgoal_frame(sg_fr); + UNLOCK_SG_FR(sg_fr); + SgFr_try_answer(sg_fr) = ans_node; + store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER); + PREG = (yamop *) CPREG; + PREFETCH_OP(PREG); + load_answer(ans_node, subs_ptr); + YENV = ENV; + GONext(); + + + #endif /* INCOMPLETE_TABLING */ } else if (SgFr_state(sg_fr) == evaluating) { - /* subgoal in evaluation */ - choiceptr leader_cp; - int leader_dep_on_stack; - find_dependency_node(sg_fr, leader_cp, leader_dep_on_stack); + if (IsMode_CoInductive(TabEnt_mode(tab_ent))) { + printf("Hi!\n"); + } else { + 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); - find_leader_node(leader_cp, leader_dep_on_stack); - store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack); + PREG = (yamop *) CPREG; + 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 if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) { choiceptr aux_cp; @@ -653,27 +690,31 @@ GONext(); #ifdef INCOMPLETE_TABLING } else if (SgFr_state(sg_fr) == incomplete) { - /* subgoal incomplete --> start by loading the answers already found */ - ans_node_ptr ans_node = SgFr_first_answer(sg_fr); - CELL *subs_ptr = YENV; - init_subgoal_frame(sg_fr); - UNLOCK_SG_FR(sg_fr); - SgFr_try_answer(sg_fr) = ans_node; - store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER); - PREG = (yamop *) CPREG; - PREFETCH_OP(PREG); - load_answer(ans_node, subs_ptr); - YENV = ENV; - GONext(); +printf("Yoho3\n"); + /* subgoal incomplete --> start by loading the answers already found */ + ans_node_ptr ans_node = SgFr_first_answer(sg_fr); + CELL *subs_ptr = YENV; + init_subgoal_frame(sg_fr); + UNLOCK_SG_FR(sg_fr); + SgFr_try_answer(sg_fr) = ans_node; + store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, TRY_ANSWER); + PREG = (yamop *) CPREG; + PREFETCH_OP(PREG); + load_answer(ans_node, subs_ptr); + YENV = ENV; + GONext(); #endif /* INCOMPLETE_TABLING */ } else if (SgFr_state(sg_fr) == evaluating) { - /* 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); +printf("Yoho4\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 if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) { choiceptr aux_cp; @@ -793,6 +834,7 @@ GONext(); #ifdef INCOMPLETE_TABLING } else if (SgFr_state(sg_fr) == incomplete) { +printf("Yoho5\n"); /* subgoal incomplete --> start by loading the answers already found */ ans_node_ptr ans_node = SgFr_first_answer(sg_fr); CELL *subs_ptr = YENV; @@ -807,13 +849,29 @@ GONext(); #endif /* INCOMPLETE_TABLING */ } 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 */ - choiceptr leader_cp; +/* 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); + store_consumer_node(tab_ent, sg_fr, leader_cp, leader_dep_on_stack);*/ #ifdef DEBUG_OPTYAP if (GLOBAL_parallel_mode == PARALLEL_MODE_RUNNING) { choiceptr aux_cp; diff --git a/OPTYap/tab.macros.h b/OPTYap/tab.macros.h index 8cee55523..d74372c64 100644 --- a/OPTYap/tab.macros.h +++ b/OPTYap/tab.macros.h @@ -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_GlobalTrie 0x200 #define Flags_TrieMode (Flag_LocalTrie | Flag_GlobalTrie) +#define Flag_CoInductive 0x008 #define SetMode_Batched(X) (X) = ((X) & ~Flags_SchedulingMode) | Flag_Batched #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_LocalTrie(X) (X) = ((X) & ~Flags_TrieMode) | Flag_LocalTrie #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_Local(X) ((X) & Flag_Local) #define IsMode_ExecAnswers(X) ((X) & Flag_ExecAnswers) #define IsMode_LoadAnswers(X) ((X) & Flag_LoadAnswers) #define IsMode_LocalTrie(X) ((X) & Flag_LocalTrie) #define IsMode_GlobalTrie(X) ((X) & Flag_GlobalTrie) +#define IsMode_CoInductive(X) ((X) & Flag_CoInductive) diff --git a/misc/ATOMS b/misc/ATOMS index 64e6e4d25..98feea28c 100644 --- a/misc/ATOMS +++ b/misc/ATOMS @@ -59,6 +59,7 @@ A CleanCall F "$clean_call" A Colomn N ":" A CodeSpace N "code_space" A Codes N "codes" +A CoInductive N "coinductive" A Comma N "," A CommentHook N "comment_hook" A Compound N "compound"