diff --git a/OPTYap/opt.config.h b/OPTYap/opt.config.h index cc0664925..ec437aea7 100644 --- a/OPTYap/opt.config.h +++ b/OPTYap/opt.config.h @@ -13,109 +13,45 @@ -/************************************************************************ -** General Configuration Parameters ** -************************************************************************/ - -/****************************************************************************************** -** use shared pages memory alloc scheme for OPTYap data structures? (optional) ** -******************************************************************************************/ -#ifdef THREADS -#define USE_PAGES_MALLOC 1 -#endif - - - -/************************************************************************ -** Tabling Configuration Parameters ** -************************************************************************/ - -/**************************** -** default sizes ** -****************************/ -#define MAX_TABLE_VARS 1000 - -/********************************************************** -** trail freeze scheme (mandatory, define one) ** -**********************************************************/ -#define BFZ_TRAIL_SCHEME 1 -/* #define BBREG_TRAIL_SCHEME 1 */ - -/********************************************************* -** support mode directed tabling ? (optional) ** -*********************************************************/ -#define MODE_DIRECTED_TABLING 1 - -/**************************************************** -** support early completion ? (optional) ** -****************************************************/ -#define TABLING_EARLY_COMPLETION 1 - -/****************************************************** -** support trie compact pairs ? (optional) ** -******************************************************/ -#define TRIE_COMPACT_PAIRS 1 - -/************************************************************ -** support global trie for subterms ? (optional) ** -************************************************************/ -/* #define GLOBAL_TRIE_FOR_SUBTERMS 1 */ - -/****************************************************** -** support incomplete tabling ? (optional) ** -******************************************************/ -/* #define INCOMPLETE_TABLING 1 */ - -/****************************************************** -** limit the table space size ? (optional) ** -******************************************************/ -/* #define LIMIT_TABLING 1 */ - -/********************************************************* -** support deterministic tabling ? (optional) ** -*********************************************************/ -/* #define DETERMINISTIC_TABLING 1 */ - -/************************************************* -** enable error checking ? (optional) ** -*************************************************/ -/* #define DEBUG_TABLING 1 */ - - - -/************************************************************************ -** YapOr Configuration Parameters ** -************************************************************************/ +/**************************************************************** +** Configuration Parameters ** +****************************************************************/ /**************************** ** default sizes ** ****************************/ +#define MAX_TABLE_VARS 1000 +#define TRIE_LOCK_BUCKETS 512 +#define THREADS_FIRST_LEVEL_BUCKETS 16 +#define THREADS_SECOND_LEVEL_BUCKETS (MAX_THREADS / THREADS_FIRST_LEVEL_BUCKETS) /* 64 (1024/16) */ +#define TG_ANSWER_SLOTS 20 #define MAX_LENGTH_ANSWER 1000 #define MAX_BRANCH_DEPTH 1000 -#define MAX_BEST_TIMES 21 -/************************************************************ -** memory mapping scheme (mandatory, define one) ** -************************************************************/ +/********************************************************************** +** memory mapping scheme for YapOr (mandatory, define one) ** +**********************************************************************/ #define MMAP_MEMORY_MAPPING_SCHEME 1 /* #define SHM_MEMORY_MAPPING_SCHEME 1 */ -/************************************************* -** enable error checking ? (optional) ** -*************************************************/ -/* #define DEBUG_YAPOR 1 */ - +/**************************************************************** +** use shared pages memory alloc scheme ? (optional) ** +****************************************************************/ +/* #define USE_PAGES_MALLOC 1 */ +/********************************************************************** +** trail freeze scheme for tabling (mandatory, define one) ** +**********************************************************************/ +#define BFZ_TRAIL_SCHEME 1 +/* #define BBREG_TRAIL_SCHEME 1 */ /************************************************************************ -** OPTYap Configuration Parameters ** +** multithreading design for tabling (mandatory, define one) ** ************************************************************************/ - -/**************************** -** default sizes ** -****************************/ -#define TG_ANSWER_SLOTS 20 -#define TRIE_LOCK_BUCKETS 512 +#define THREADS_NO_SHARING 1 +/* #define THREADS_SUBGOAL_SHARING 1 */ +/* #define THREADS_FULL_SHARING 1 */ +/* #define THREADS_CONSUMER_SHARING 1 */ /************************************************************************* ** tries locking scheme (mandatory, define one per trie type) ** @@ -156,26 +92,86 @@ #define TRIE_LOCK_USING_NODE_FIELD 1 /* #define TRIE_LOCK_USING_GLOBAL_ARRAY 1 */ +/********************************************************* +** support mode directed tabling ? (optional) ** +*********************************************************/ +#define MODE_DIRECTED_TABLING 1 + +/**************************************************************** +** support early completion for tabling ? (optional) ** +*****************************************************************/ +#define TABLING_EARLY_COMPLETION 1 + /****************************************************** -** support tabling inner cuts ? (optional) ** +** support trie compact pairs ? (optional) ** ******************************************************/ -#define TABLING_INNER_CUTS 1 +#define TRIE_COMPACT_PAIRS 1 + +/************************************************************ +** support global trie for subterms ? (optional) ** +************************************************************/ +/* #define GLOBAL_TRIE_FOR_SUBTERMS 1 */ + +/****************************************************** +** support incomplete tabling ? (optional) ** +******************************************************/ +/* #define INCOMPLETE_TABLING 1 */ + +/****************************************************** +** limit the table space size ? (optional) ** +******************************************************/ +/* #define LIMIT_TABLING 1 */ /********************************************************* -** use timestamps for suspension ? (optional) ** +** support deterministic tabling ? (optional) ** *********************************************************/ +/* #define DETERMINISTIC_TABLING 1 */ + +/****************************************************************** +** support tabling inner cuts with OPTYap ? (optional) ** +******************************************************************/ +#define TABLING_INNER_CUTS 1 + +/********************************************************************* +** use timestamps for suspension with OPTYap ? (optional) ** +*********************************************************************/ #define TIMESTAMP_CHECK 1 +/************************************************* +** enable error checking ? (optional) ** +*************************************************/ +/* #define DEBUG_TABLING 1 */ +/* #define DEBUG_YAPOR 1 */ + +/************************************************** +** enable output checking ? (optional) ** +**************************************************/ +/* #define OUTPUT_THREADS_TABLING 1 */ + + + /************************************************************************ ** Parameter Checks ** ************************************************************************/ -#ifndef USE_PAGES_MALLOC -#undef LIMIT_TABLING -#endif /* ! USE_PAGES_MALLOC */ - +#ifdef YAPOR +#ifdef i386 /* For i386 machines we use shared memory segments */ +#undef MMAP_MEMORY_MAPPING_SCHEME +#define SHM_MEMORY_MAPPING_SCHEME +#endif +#if !defined(MMAP_MEMORY_MAPPING_SCHEME) && !defined(SHM_MEMORY_MAPPING_SCHEME) +#error Define a memory mapping scheme +#endif +#if defined(MMAP_MEMORY_MAPPING_SCHEME) && defined(SHM_MEMORY_MAPPING_SCHEME) +#error Do not define multiple memory mapping schemes +#endif +#else /* ! YAPOR */ +#undef MMAP_MEMORY_MAPPING_SCHEME +#undef SHM_MEMORY_MAPPING_SCHEME +#undef DEBUG_YAPOR +#endif /* YAPOR */ #ifdef TABLING #if !defined(BFZ_TRAIL_SCHEME) && !defined(BBREG_TRAIL_SCHEME) @@ -197,27 +193,7 @@ #undef DEBUG_TABLING #endif /* TABLING */ - -#ifdef YAPOR -#ifdef i386 /* For i386 machines we use shared memory segments */ -#undef MMAP_MEMORY_MAPPING_SCHEME -#define SHM_MEMORY_MAPPING_SCHEME -#endif -#if !defined(MMAP_MEMORY_MAPPING_SCHEME) && !defined(SHM_MEMORY_MAPPING_SCHEME) -#error Define a memory mapping scheme -#endif -#if defined(MMAP_MEMORY_MAPPING_SCHEME) && defined(SHM_MEMORY_MAPPING_SCHEME) -#error Do not define multiple memory mapping schemes -#endif -#undef LIMIT_TABLING -#else /* ! YAPOR */ -#undef MMAP_MEMORY_MAPPING_SCHEME -#undef SHM_MEMORY_MAPPING_SCHEME -#undef DEBUG_YAPOR -#endif /* YAPOR */ - - -#if defined(YAPOR) && defined(TABLING) +#if defined(TABLING) && (defined(YAPOR) || defined(THREADS)) /* SUBGOAL_TRIE_LOCK_LEVEL */ #if !defined(SUBGOAL_TRIE_LOCK_AT_ENTRY_LEVEL) && !defined(SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL) && !defined(SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL) #error Define a subgoal trie lock scheme @@ -260,13 +236,70 @@ #ifndef GLOBAL_TRIE_LOCK_AT_WRITE_LEVEL #undef GLOBAL_TRIE_ALLOC_BEFORE_CHECK #endif -/* TRIE_LOCK_USING_NODE_FIELD / TRIE_LOCK_USING_GLOBAL_ARRAY */ +/* TRIE_LOCK_USING */ #if !defined(TRIE_LOCK_USING_NODE_FIELD) && !defined(TRIE_LOCK_USING_GLOBAL_ARRAY) #error Define a trie lock data structure #endif #if defined(TRIE_LOCK_USING_NODE_FIELD) && defined(TRIE_LOCK_USING_GLOBAL_ARRAY) #error Do not define multiple trie lock data structures #endif +#else /* ! TABLING || (! YAPOR && ! THREADS) */ +#undef SUBGOAL_TRIE_LOCK_AT_ENTRY_LEVEL +#undef SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL +#undef SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL +#undef SUBGOAL_TRIE_ALLOC_BEFORE_CHECK +#undef ANSWER_TRIE_LOCK_AT_ENTRY_LEVEL +#undef ANSWER_TRIE_LOCK_AT_NODE_LEVEL +#undef ANSWER_TRIE_LOCK_AT_WRITE_LEVEL +#undef ANSWER_TRIE_ALLOC_BEFORE_CHECK +#undef GLOBAL_TRIE_LOCK_AT_NODE_LEVEL +#undef GLOBAL_TRIE_LOCK_AT_WRITE_LEVEL +#undef GLOBAL_TRIE_ALLOC_BEFORE_CHECK +#undef TRIE_LOCK_USING_NODE_FIELD +#undef TRIE_LOCK_USING_GLOBAL_ARRAY +#endif /* TABLING && (YAPOR || THREADS) */ + +#if defined(TABLING) && defined(THREADS) +#if !defined(THREADS_NO_SHARING) && !defined(THREADS_SUBGOAL_SHARING) && !defined(THREADS_FULL_SHARING) && !defined(THREADS_CONSUMER_SHARING) +#error Define a multithreading table design +#endif +#if defined(THREADS_NO_SHARING) && defined(THREADS_SUBGOAL_SHARING) +#error Do not define multiple multithreading table designs +#endif +#if defined(THREADS_NO_SHARING) && defined(THREADS_FULL_SHARING) +#error Do not define multiple multithreading table designs +#endif +#if defined(THREADS_NO_SHARING) && defined(THREADS_CONSUMER_SHARING) +#error Do not define multiple multithreading table designs +#endif +#if defined(THREADS_SUBGOAL_SHARING) && defined(THREADS_FULL_SHARING) +#error Do not define multiple multithreading table designs +#endif +#if defined(THREADS_SUBGOAL_SHARING) && defined(THREADS_CONSUMER_SHARING) +#error Do not define multiple multithreading table designs +#endif +#if defined(THREADS_FULL_SHARING) && defined(THREADS_CONSUMER_SHARING) +#error Do not define multiple multithreading table designs +#endif +#ifdef THREADS_NO_SHARING +#undef SUBGOAL_TRIE_LOCK_AT_ENTRY_LEVEL +#undef SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL +#undef SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL +#undef SUBGOAL_TRIE_ALLOC_BEFORE_CHECK +#endif +#if defined(THREADS_NO_SHARING) || defined(THREADS_SUBGOAL_SHARING) +#undef ANSWER_TRIE_LOCK_AT_ENTRY_LEVEL +#undef ANSWER_TRIE_LOCK_AT_NODE_LEVEL +#undef ANSWER_TRIE_LOCK_AT_WRITE_LEVEL +#undef ANSWER_TRIE_ALLOC_BEFORE_CHECK +#endif +#else /* ! TABLING || ! THREADS */ +#undef THREADS_NO_SHARING +#undef THREADS_SUBGOAL_SHARING +#undef THREADS_FULL_SHARING +#undef THREADS_CONSUMER_SHARING +#endif /* TABLING && THREADS */ + #ifdef TRIE_LOCK_USING_NODE_FIELD #if defined(SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL) || defined(SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL) #define SUBGOAL_TRIE_LOCK_USING_NODE_FIELD 1 @@ -288,25 +321,34 @@ #define GLOBAL_TRIE_LOCK_USING_GLOBAL_ARRAY 1 #endif #endif -#else /* ! TABLING || ! YAPOR */ -#undef SUBGOAL_TRIE_LOCK_AT_ENTRY_LEVEL -#undef SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL -#undef SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL -#undef SUBGOAL_TRIE_ALLOC_BEFORE_CHECK -#undef ANSWER_TRIE_LOCK_AT_ENTRY_LEVEL -#undef ANSWER_TRIE_LOCK_AT_NODE_LEVEL -#undef ANSWER_TRIE_LOCK_AT_WRITE_LEVEL -#undef ANSWER_TRIE_ALLOC_BEFORE_CHECK -#undef GLOBAL_TRIE_LOCK_AT_NODE_LEVEL -#undef GLOBAL_TRIE_LOCK_AT_WRITE_LEVEL -#undef GLOBAL_TRIE_ALLOC_BEFORE_CHECK -#undef TRIE_LOCK_USING_NODE_FIELD -#undef TRIE_LOCK_USING_GLOBAL_ARRAY + +#if !defined(TABLING) || !defined(YAPOR) #undef TABLING_INNER_CUTS #undef TIMESTAMP_CHECK -#endif /* YAPOR && TABLING */ +#endif +#if defined(TABLING) && defined(THREADS) +#if THREADS_FIRST_LEVEL_BUCKETS > THREADS_SECOND_LEVEL_BUCKETS +#error THREADS_FIRST_LEVEL_BUCKETS cannot exceed THREADS_SECOND_LEVEL_BUCKETS +#endif +#else +#undef OUTPUT_THREADS_TABLING +#endif #if defined(DEBUG_YAPOR) && defined(DEBUG_TABLING) #define DEBUG_OPTYAP -#endif /* DEBUG_YAPOR && DEBUG_TABLING */ +#endif + +#if defined(LIMIT_TABLING) && !defined(USE_PAGES_MALLOC) +#error LIMIT_TABLING requires USE_PAGES_MALLOC +#endif + +#if defined(YAPOR) || defined(THREADS) +#undef MODE_DIRECTED_TABLING +#undef TABLING_EARLY_COMPLETION +#undef INCOMPLETE_TABLING +#undef LIMIT_TABLING +#undef DETERMINISTIC_TABLING +#endif + + diff --git a/OPTYap/opt.init.c b/OPTYap/opt.init.c index e7b982e0c..65eceea8d 100644 --- a/OPTYap/opt.init.c +++ b/OPTYap/opt.init.c @@ -219,7 +219,7 @@ void Yap_init_root_frames(void) { #ifdef TABLING /* root dependency frame */ #ifdef YAPOR - DepFr_cons_cp(GLOBAL_root_dep_fr) = B; + DepFr_cons_cp(GLOBAL_root_dep_fr) = B; /* with YAPOR, at that point, LOCAL_top_dep_fr shouldn't be the same as GLOBAL_root_dep_fr ? */ #else DepFr_cons_cp(LOCAL_top_dep_fr) = B; #endif /* YAPOR */ diff --git a/OPTYap/opt.structs.h b/OPTYap/opt.structs.h index 471f067ab..00afdfc1f 100644 --- a/OPTYap/opt.structs.h +++ b/OPTYap/opt.structs.h @@ -78,10 +78,10 @@ typedef struct page_header { ***************************/ struct pages { -#ifdef USE_PAGES_MALLOC #if defined(YAPOR) || defined(THREADS) lockvar lock; -#endif /* YAPOR */ +#endif /* YAPOR || THREADS */ +#ifdef USE_PAGES_MALLOC int structs_per_page; struct page_header *first_free_page; volatile long pages_allocated; @@ -127,6 +127,12 @@ struct global_pages { struct pages answer_trie_hash_pages; struct pages global_trie_hash_pages; #endif /* TABLING */ +#if defined(THREADS_FULL_SHARING) || defined(THREADS_CONSUMER_SHARING) + struct pages subgoal_entry_pages; +#endif /* THREADS_FULL_SHARING || THREADS_CONSUMER_SHARING */ +#ifdef THREADS_FULL_SHARING + struct pages answer_ref_node_pages; +#endif /* THREADS_FULL_SHARING */ #if defined(YAPOR) && defined(TABLING) struct pages suspension_frame_pages; #endif /* YAPOR && TABLING */ @@ -158,6 +164,30 @@ struct global_optyap_locks { +/*************************************** +** threads_dependency_frame ** +***************************************/ + +#ifdef THREADS_CONSUMER_SHARING +struct threads_dependency_frame { + lockvar lock; + enum { + working, + idle, + completing + } state; + int terminator; + int next; +}; +#endif /* THREADS_CONSUMER_SHARING */ + +#define ThDepFr_lock(X) ((X).lock) +#define ThDepFr_state(X) ((X).state) +#define ThDepFr_terminator(X) ((X).terminator) +#define ThDepFr_next(X) ((X).next) + + + /********************************* * Struct global_optyap_data ** *********************************/ @@ -212,6 +242,9 @@ struct global_optyap_data { #ifdef YAPOR struct dependency_frame *root_dependency_frame; #endif /* YAPOR */ +#ifdef THREADS_CONSUMER_SHARING + struct threads_dependency_frame threads_dependency_frame[MAX_THREADS]; +#endif /*THREADS_CONSUMER_SHARING*/ CELL table_var_enumerator[MAX_TABLE_VARS]; #ifdef TRIE_LOCK_USING_GLOBAL_ARRAY lockvar trie_locks[TRIE_LOCK_BUCKETS]; @@ -238,6 +271,8 @@ struct global_optyap_data { #define GLOBAL_pages_sg_hash (GLOBAL_optyap_data.pages.subgoal_trie_hash_pages) #define GLOBAL_pages_ans_hash (GLOBAL_optyap_data.pages.answer_trie_hash_pages) #define GLOBAL_pages_gt_hash (GLOBAL_optyap_data.pages.global_trie_hash_pages) +#define GLOBAL_pages_sg_ent (GLOBAL_optyap_data.pages.subgoal_entry_pages) +#define GLOBAL_pages_ans_ref (GLOBAL_optyap_data.pages.answer_ref_node_pages) #define GLOBAL_pages_susp_fr (GLOBAL_optyap_data.pages.suspension_frame_pages) #define GLOBAL_scheduler_loop (GLOBAL_optyap_data.scheduler_loop) #define GLOBAL_delayed_release_load (GLOBAL_optyap_data.delayed_release_load) @@ -280,6 +315,7 @@ struct global_optyap_data { #define GLOBAL_last_sg_fr (GLOBAL_optyap_data.last_subgoal_frame) #define GLOBAL_check_sg_fr (GLOBAL_optyap_data.check_subgoal_frame) #define GLOBAL_root_dep_fr (GLOBAL_optyap_data.root_dependency_frame) +#define GLOBAL_th_dep_fr(wid) (GLOBAL_optyap_data.threads_dependency_frame[wid]) #define GLOBAL_table_var_enumerator(index) (GLOBAL_optyap_data.table_var_enumerator[index]) #define GLOBAL_table_var_enumerator_addr(index) (GLOBAL_optyap_data.table_var_enumerator + (index)) #define GLOBAL_trie_locks(index) (GLOBAL_optyap_data.trie_locks[index]) diff --git a/OPTYap/tab.macros.h b/OPTYap/tab.macros.h index bba941a71..bd4b14fcc 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); ** Tabling defines ** ******************************/ +/* traverse macros */ #define SHOW_MODE_STRUCTURE 0 #define SHOW_MODE_STATISTICS 1 #define TRAVERSE_MODE_NORMAL 0 @@ -135,6 +136,24 @@ static inline tg_sol_fr_ptr CUT_prune_tg_solution_frames(tg_sol_fr_ptr, int); #define CompactPairEndList AbsPair((Term *) (2*(LowTagBits + 1))) #endif /* TRIE_COMPACT_PAIRS */ +/* threads */ +#if (_trie_retry_gterm - _trie_do_var + 1) + 1 <= 64 /* 60 (trie instructions) + 1 (ANSWER_TRIE_HASH_MARK) <= 64 */ +#define ANSWER_LEAF_NODE_INSTR_BITS 6 /* 2^6 = 64 */ +#define ANSWER_LEAF_NODE_INSTR_MASK 0x3F +#endif +#if SIZEOF_INT_P == 4 +#define ANSWER_LEAF_NODE_MAX_THREADS (32 - ANSWER_LEAF_NODE_INSTR_BITS) +#elif SIZEOF_INT_P == 8 +#define ANSWER_LEAF_NODE_MAX_THREADS (64 - ANSWER_LEAF_NODE_INSTR_BITS) +#else +#define ANSWER_LEAF_NODE_MAX_THREADS OOOOPPS!!! Unknown Pointer Sizeof +#endif /* SIZEOF_INT_P */ +#define ANSWER_LEAF_NODE_INSTR_RELATIVE(NODE) TrNode_instr(NODE) = TrNode_instr(NODE) - _trie_do_var + 1 +#define ANSWER_LEAF_NODE_INSTR_ABSOLUTE(NODE) TrNode_instr(NODE) = (TrNode_instr(NODE) & ANSWER_LEAF_NODE_INSTR_MASK) + _trie_do_var - 1 +#define ANSWER_LEAF_NODE_SET_WID(NODE,WID) BITMAP_insert(TrNode_instr(NODE), WID + ANSWER_LEAF_NODE_INSTR_BITS) +#define ANSWER_LEAF_NODE_DEL_WID(NODE,WID) BITMAP_delete(TrNode_instr(NODE), WID + ANSWER_LEAF_NODE_INSTR_BITS) +#define ANSWER_LEAF_NODE_CHECK_WID(NODE,WID) BITMAP_member(TrNode_instr(NODE), WID + ANSWER_LEAF_NODE_INSTR_BITS) + /* choice points */ #define NORM_CP(CP) ((choiceptr)(CP)) #define GEN_CP(CP) ((struct generator_choicept *)(CP)) diff --git a/OPTYap/tab.structs.h b/OPTYap/tab.structs.h index 1cf140b73..cc8ceab2f 100644 --- a/OPTYap/tab.structs.h +++ b/OPTYap/tab.structs.h @@ -31,21 +31,30 @@ typedef struct table_entry { #ifdef MODE_DIRECTED_TABLING int* mode_directed_array; #endif /*MODE_DIRECTED_TABLING*/ +#ifdef THREADS_NO_SHARING + struct subgoal_trie_node *subgoal_trie[THREADS_FIRST_LEVEL_BUCKETS]; +#else struct subgoal_trie_node *subgoal_trie; +#endif /*THREADS_NO_SHARING */ struct subgoal_trie_hash *hash_chain; struct table_entry *next; } *tab_ent_ptr; -#define TabEnt_lock(X) ((X)->lock) -#define TabEnt_pe(X) ((X)->pred_entry) -#define TabEnt_atom(X) ((X)->pred_atom) -#define TabEnt_arity(X) ((X)->pred_arity) -#define TabEnt_flags(X) ((X)->pred_flags) -#define TabEnt_mode(X) ((X)->execution_mode) -#define TabEnt_mode_directed(X) ((X)->mode_directed_array) -#define TabEnt_subgoal_trie(X) ((X)->subgoal_trie) -#define TabEnt_hash_chain(X) ((X)->hash_chain) -#define TabEnt_next(X) ((X)->next) +#define TabEnt_lock(X) ((X)->lock) +#define TabEnt_pe(X) ((X)->pred_entry) +#define TabEnt_atom(X) ((X)->pred_atom) +#define TabEnt_arity(X) ((X)->pred_arity) +#define TabEnt_flags(X) ((X)->pred_flags) +#define TabEnt_mode(X) ((X)->execution_mode) +#define TabEnt_mode_directed(X) ((X)->mode_directed_array) +#ifdef THREADS_NO_SHARING +#define TabEnt_subgoal_trie(X) ((X)->subgoal_trie[worker_id]) +#define TabEnt_subgoal_trie(X,I) ((X)->subgoal_trie[I]) +#else +#define TabEnt_subgoal_trie(X) ((X)->subgoal_trie) +#endif /*THREADS_NO_SHARING */ +#define TabEnt_hash_chain(X) ((X)->hash_chain) +#define TabEnt_next(X) ((X)->next) @@ -148,6 +157,24 @@ typedef struct global_trie_hash { +/****************************** +** answer_ref_node ** +******************************/ + +#ifdef THREADS_FULL_SHARING +typedef struct answer_ref_node { + struct answer_trie_node *ans_node; + struct answer_ref_node *next; + struct answer_ref_node *previous; +} *ans_ref_ptr; +#endif /* THREADS_FULL_SHARING */ + +#define RefNode_answer(X) ((X)->ans_node) +#define RefNode_next(X) ((X)->next) +#define RefNode_previous(X) ((X)->previous) + + + /************************************************************************ ** Execution Data Structures ** ************************************************************************/ @@ -193,29 +220,32 @@ struct loader_choicept { +/********************************* +** subgoal_state_flag ** +*********************************/ + +typedef enum { /* do not change order !!! */ + incomplete = 0, /* INCOMPLETE_TABLING */ + ready_external = 1, /* THREADS_CONSUMER_SHARING */ + ready = 2, + evaluating = 3, + complete = 4, + complete_in_use = 5, /* LIMIT_TABLING */ + compiled = 6, + compiled_in_use = 7 /* LIMIT_TABLING */ +} subgoal_state_flag; + + + /**************************** -** subgoal_frame ** +** subgoal_entry ** ****************************/ -typedef struct subgoal_frame { -#if defined(YAPOR) || defined(THREADS) +typedef struct subgoal_entry { +#if defined(YAPOR) || defined(THREADS_FULL_SHARING) || defined(THREADS_CONSUMER_SHARING) lockvar lock; -#endif /* YAPOR || THREADS */ -#ifdef YAPOR - int generator_worker; - struct or_frame *top_or_frame_on_generator_branch; -#endif /* YAPOR */ +#endif /* YAPOR || THREADS_FULL_SHARING || THREADS_CONSUMER_SHARING */ yamop *code_of_subgoal; - enum { /* do not change order !!! */ - incomplete = 0, /* INCOMPLETE_TABLING */ - ready = 1, - evaluating = 2, - complete = 3, - complete_in_use = 4, /* LIMIT_TABLING */ - compiled = 5, - compiled_in_use = 6 /* LIMIT_TABLING */ - } state_flag; - choiceptr generator_choice_point; struct answer_trie_hash *hash_chain; struct answer_trie_node *answer_trie; struct answer_trie_node *first_answer; @@ -223,61 +253,130 @@ typedef struct subgoal_frame { #ifdef MODE_DIRECTED_TABLING int* mode_directed_array; struct answer_trie_node *invalid_chain; -#endif /*MODE_DIRECTED_TABLING*/ +#endif /* MODE_DIRECTED_TABLING */ #ifdef INCOMPLETE_TABLING struct answer_trie_node *try_answer; #endif /* INCOMPLETE_TABLING */ #ifdef LIMIT_TABLING struct subgoal_frame *previous; #endif /* LIMIT_TABLING */ +#ifdef YAPOR + struct or_frame *top_or_frame_on_generator_branch; +#endif /* YAPOR */ +#if defined(YAPOR) || defined(THREADS_CONSUMER_SHARING) + int generator_worker; +#endif /* YAPOR || THREADS_CONSUMER_SHARING */ +#if defined(THREADS_FULL_SHARING) || defined(THREADS_CONSUMER_SHARING) + subgoal_state_flag state_flag; + int active_workers; + struct subgoal_frame *subgoal_frame[THREADS_FIRST_LEVEL_BUCKETS]; +#endif /* THREADS_FULL_SHARING || THREADS_CONSUMER_SHARING */ +}* sg_ent_ptr; + +#define SgEnt_lock(X) ((X)->lock) +#define SgEnt_code(X) ((X)->code_of_subgoal) +#define SgEnt_tab_ent(X) (((X)->code_of_subgoal)->u.Otapl.te) +#define SgEnt_arity(X) (((X)->code_of_subgoal)->u.Otapl.s) +#define SgEnt_hash_chain(X) ((X)->hash_chain) +#define SgEnt_answer_trie(X) ((X)->answer_trie) +#define SgEnt_first_answer(X) ((X)->first_answer) +#define SgEnt_last_answer(X) ((X)->last_answer) +#define SgEnt_mode_directed(X) ((X)->mode_directed_array) +#define SgEnt_invalid_chain(X) ((X)->invalid_chain) +#define SgEnt_try_answer(X) ((X)->try_answer) +#define SgEnt_previous(X) ((X)->previous) +#define SgEnt_gen_top_or_fr(X) ((X)->top_or_frame_on_generator_branch) +#define SgEnt_gen_worker(X) ((X)->generator_worker) +#define SgEnt_sg_ent_state(X) ((X)->state_flag) +#define SgEnt_active_workers(X) ((X)->active_workers) +#define SgEnt_sg_fr(X,I) ((X)->subgoal_frame[I]) + + + +/**************************** +** subgoal_frame ** +****************************/ + +typedef struct subgoal_frame { +#ifdef THREADS +#if defined(THREADS_FULL_SHARING) || defined(THREADS_CONSUMER_SHARING) + struct subgoal_entry *subgoal_entry; +#endif /* THREADS_FULL_SHARING || THREADS_CONSUMER_SHARING */ +#ifdef THREADS_FULL_SHARING + struct answer_trie_node *batched_last_answer; + struct answer_ref_node *batched_cached_answers; +#endif /* THREADS_FULL_SHARING */ +#else + struct subgoal_entry subgoal_entry; +#endif /* THREADS */ + subgoal_state_flag state_flag; + choiceptr generator_choice_point; struct subgoal_frame *next; } *sg_fr_ptr; -#define SgFr_lock(X) ((X)->lock) -#define SgFr_gen_worker(X) ((X)->generator_worker) -#define SgFr_gen_top_or_fr(X) ((X)->top_or_frame_on_generator_branch) -#define SgFr_code(X) ((X)->code_of_subgoal) -#define SgFr_tab_ent(X) (((X)->code_of_subgoal)->u.Otapl.te) -#define SgFr_arity(X) (((X)->code_of_subgoal)->u.Otapl.s) -#define SgFr_state(X) ((X)->state_flag) -#define SgFr_gen_cp(X) ((X)->generator_choice_point) -#define SgFr_hash_chain(X) ((X)->hash_chain) -#define SgFr_answer_trie(X) ((X)->answer_trie) -#define SgFr_first_answer(X) ((X)->first_answer) -#define SgFr_last_answer(X) ((X)->last_answer) -#define SgFr_mode_directed(X) ((X)->mode_directed_array) -#define SgFr_invalid_chain(X) ((X)->invalid_chain) -#define SgFr_try_answer(X) ((X)->try_answer) -#define SgFr_previous(X) ((X)->previous) -#define SgFr_next(X) ((X)->next) +/* subgoal_entry fields */ +#ifdef THREADS +#define SUBGOAL_ENTRY(X) SgFr_subgoal_entry(X)-> +#else +#define SUBGOAL_ENTRY(X) (X)->subgoal_entry. +#endif /* THREADS */ +#define SgFr_lock(X) (SUBGOAL_ENTRY(X) lock) +#define SgFr_code(X) (SUBGOAL_ENTRY(X) code_of_subgoal) +#define SgFr_tab_ent(X) ((SUBGOAL_ENTRY(X) code_of_subgoal)->u.Otapl.te) +#define SgFr_arity(X) ((SUBGOAL_ENTRY(X) code_of_subgoal)->u.Otapl.s) +#define SgFr_hash_chain(X) (SUBGOAL_ENTRY(X) hash_chain) +#define SgFr_answer_trie(X) (SUBGOAL_ENTRY(X) answer_trie) +#define SgFr_first_answer(X) (SUBGOAL_ENTRY(X) first_answer) +#define SgFr_last_answer(X) (SUBGOAL_ENTRY(X) last_answer) +#define SgFr_mode_directed(X) (SUBGOAL_ENTRY(X) mode_directed_array) +#define SgFr_invalid_chain(X) (SUBGOAL_ENTRY(X) invalid_chain) +#define SgFr_try_answer(X) (SUBGOAL_ENTRY(X) try_answer) +#define SgFr_previous(X) (SUBGOAL_ENTRY(X) previous) +#define SgFr_gen_top_or_fr(X) (SUBGOAL_ENTRY(X) top_or_frame_on_generator_branch) +#define SgFr_gen_worker(X) (SUBGOAL_ENTRY(X) generator_worker) +#define SgFr_sg_ent_state(X) (SUBGOAL_ENTRY(X) state_flag) +#define SgFr_active_workers(X) (SUBGOAL_ENTRY(X) active_workers) +/* subgoal_frame fields */ +#define SgFr_subgoal_entry(X) ((X)->subgoal_entry) +#define SgFr_batched_last_answer(X) ((X)->batched_last_answer) +#define SgFr_batched_cached_answers(X) ((X)->batched_cached_answers) +#define SgFr_state(X) ((X)->state_flag) +#define SgFr_gen_cp(X) ((X)->generator_choice_point) +#define SgFr_next(X) ((X)->next) -/************************************************************************************************** +/********************************************************************************************************** - SgFr_lock: spin-lock to modify the frame fields. - SgFr_gen_worker: the id of the worker that had allocated the frame. - SgFr_gen_top_or_fr: a pointer to the top or-frame in the generator choice point branch. - When the generator choice point is shared the pointer is updated - to its or-frame. It is used to find the direct dependency node for - consumer nodes in other workers branches. - SgFr_code initial instruction of the subgoal's compiled code. - SgFr_tab_ent a pointer to the correspondent table entry. - SgFr_arity the arity of the subgoal. - SgFr_state: a flag that indicates the subgoal state. - SgFr_gen_cp: a pointer to the correspondent generator choice point. - SgFr_hash_chain: a pointer to the first answer_trie_hash struct for the subgoal in hand. - SgFr_answer_trie: a pointer to the top answer trie node. - It is used to check for/insert new answers. - SgFr_first_answer: a pointer to the bottom answer trie node of the first available answer. - SgFr_last_answer: a pointer to the bottom answer trie node of the last available answer. - SgFr_mode_directed: a pointer to the mode directed array. - SgFr_invalid_chain: a pointer to the first invalid leaf node when using mode directed tabling. - SgFr_try_answer: a pointer to the bottom answer trie node of the last tried answer. - It is used when a subgoal was not completed during the previous evaluation. - Not completed subgoals start by trying the answers already found. - SgFr_previous: a pointer to the previous subgoal frame on the chain. - SgFr_next: a pointer to the next subgoal frame on the chain. + SgFr_lock: spin-lock to modify the frame fields. + SgFr_code initial instruction of the subgoal's compiled code. + SgFr_tab_ent a pointer to the corresponding table entry. + SgFr_arity the arity of the subgoal. + SgFr_hash_chain: a pointer to the first answer_trie_hash struct. + SgFr_answer_trie: a pointer to the top answer trie node. + SgFr_first_answer: a pointer to the leaf answer trie node of the first answer. + SgFr_last_answer: a pointer to the leaf answer trie node of the last answer. + SgFr_mode_directed: a pointer to the mode directed array. + SgFr_invalid_chain: a pointer to the first invalid leaf node when using mode directed tabling. + SgFr_try_answer: a pointer to the leaf answer trie node of the last tried answer. + It is used when a subgoal was not completed during the previous evaluation. + Not completed subgoals start by trying the answers already found. + SgFr_previous: a pointer to the previous subgoal frame on the chain. + SgFr_gen_top_or_fr: a pointer to the top or-frame in the generator choice point branch. + When the generator choice point is shared the pointer is updated + to its or-frame. It is used to find the direct dependency node for + consumer nodes in other workers branches. + SgFr_gen_worker: the id of the worker that had allocated the frame. + SgFr_sg_ent_state: a flag that indicates the subgoal entry state. + SgFr_active_workers: the number of workers evaluating the subgoal. + SgFr_subgoal_entry: a pointer to the corresponding subgoal entry. + SgFr_batched_last_answer: a pointer to the leaf answer trie node of the last checked answer + when using batched scheduling. + SgFr_batched_cached_answers: a pointer to the chain of answers already inserted in the trie, but not + yet found when using batched scheduling. + SgFr_state: a flag that indicates the subgoal frame state. + SgFr_gen_cp: a pointer to the correspondent generator choice point. + SgFr_next: a pointer to the next subgoal frame on the chain. -**************************************************************************************************/ +**********************************************************************************************************/ @@ -286,9 +385,9 @@ typedef struct subgoal_frame { *******************************/ typedef struct dependency_frame { -#if defined(YAPOR) || defined(THREADS) +#ifdef YAPOR lockvar lock; -#endif /* YAPOR || THREADS */ +#endif /* YAPOR */ #ifdef YAPOR int leader_dependency_is_on_stack; struct or_frame *top_or_frame; @@ -300,6 +399,9 @@ typedef struct dependency_frame { choiceptr leader_choice_point; choiceptr consumer_choice_point; struct answer_trie_node *last_consumed_answer; +#ifdef THREADS_CONSUMER_SHARING + int generator_is_external; +#endif /* THREADS_CONSUMER_SHARING */ struct dependency_frame *next; } *dep_fr_ptr; @@ -311,9 +413,10 @@ typedef struct dependency_frame { #define DepFr_leader_cp(X) ((X)->leader_choice_point) #define DepFr_cons_cp(X) ((X)->consumer_choice_point) #define DepFr_last_answer(X) ((X)->last_consumed_answer) +#define DepFr_external(X) ((X)->generator_is_external) #define DepFr_next(X) ((X)->next) -/******************************************************************************************************* +/********************************************************************************************************* DepFr_lock: lock variable to modify the frame fields. DepFr_leader_dep_is_on_stack: the generator choice point for the correspondent consumer choice point @@ -330,9 +433,10 @@ typedef struct dependency_frame { DepFr_leader_cp: a pointer to the leader choice point. DepFr_cons_cp: a pointer to the correspondent consumer choice point. DepFr_last_answer: a pointer to the last consumed answer. + DepFr_external: the generator choice point is external to the current thread (FALSE/TRUE). DepFr_next: a pointer to the next dependency frame on the chain. -*******************************************************************************************************/ +*********************************************************************************************************/ diff --git a/packages/ProbLog/problog.yap b/packages/ProbLog/problog.yap index 218403d28..ae3d06297 100644 --- a/packages/ProbLog/problog.yap +++ b/packages/ProbLog/problog.yap @@ -2099,6 +2099,398 @@ problog_low(_, _, LP, Status) :- (problog_flag(retain_tables, true) -> retain_tabling; true), clear_tabling. +:- ensure_loaded(library(tries)). +:- ensure_loaded(library(rbtrees)). +:- ensure_loaded(library(readutil)). +:- ensure_loaded(library(lineutils)). +problog_cnf(Goal, _) :- + init_problog_low(0.0), + problog_control(off, up), + timer_start(sld_time), + problog_call(Goal), + add_solution, + fail. +problog_cnf(_,Prob) :- + timer_stop(sld_time,SLD_Time), + problog_var_set(sld_time, SLD_Time), + nb_getval(problog_completed_proofs, Trie_Completed_Proofs), + trie_to_cnf(Trie_Completed_Proofs, CNF, RB), +% randomize_cnf_varids(CNF, RandomVNameCNF), +% invert_cnf_varids(CNF, RandomVNameCNF), + CNF = RandomVNameCNF, + cnf_to_dimacs(RandomVNameCNF, _File), + % should generate a tmp file. + unix(system('./c2d_linux -in dimacs')), + nnf_to_probability(_NNFFile, RB, CompProb), + Prob is 1-CompProb, + delete_ptree(Trie_Completed_Proofs), + (problog_flag(retain_tables, true) -> retain_tabling; true), + clear_tabling. + +problog_wcnf(Goal, _) :- + init_problog_low(0.0), + problog_control(off, up), + timer_start(sld_time), + problog_call(Goal), + add_solution, + fail. +problog_wcnf(_,Prob) :- + timer_stop(sld_time,SLD_Time), + problog_var_set(sld_time, SLD_Time), + nb_getval(problog_completed_proofs, Trie_Completed_Proofs), + trie_to_cnf(Trie_Completed_Proofs, CNF, RB), +% randomize_cnf_varids(CNF, RandomVNameCNF), +% invert_cnf_varids(CNF, RandomVNameCNF), + CNF = RandomVNameCNF, + cnf_to_wdimacs(RandomVNameCNF, RB, _File), + % should generate a tmp file. + unix(system('./c2d_linux -in dimacs')), + nnf_to_probability(_NNFFile, RB, CompProb), + Prob is 1-CompProb, + delete_ptree(Trie_Completed_Proofs), + (problog_flag(retain_tables, true) -> retain_tabling; true), + clear_tabling. + +trie_to_cnf(Trie, CNF, RB) :- + trie_traverse_first(Trie, RefFirst), + rb_new(RB0), + nb_setval(cnf_nodes, 0), + trie_to_list_of_numbers(Trie, RB0, RefFirst, CNF, RB). + +trie_to_list_of_numbers(Trie, RB0, CurrentRef, Proof.Proofs, RB) :- + trie_get_entry(CurrentRef, Entry), + convert_trie_entry_to_numbers(Entry, RB0, Proof, RBI), + continue_processing_trie(Trie, RBI, CurrentRef, Proofs, RB). + +continue_processing_trie(Trie, RB0, CurrentRef, Proofs, RB) :- + trie_traverse_next(CurrentRef, NextRef), !, + trie_to_list_of_numbers(Trie, RB0, NextRef, Proofs, RB). +continue_processing_trie(_, RB, _CurrentRef, [], RB). + +convert_trie_entry_to_numbers([], RB, [], RB). +convert_trie_entry_to_numbers(not(Val).Entry, RB0, Numb.Proof, RB) :- !, + convert_goal_to_number(Val, RB0, Numb, RBI), + convert_trie_entry_to_numbers(Entry, RBI, Proof, RB). +convert_trie_entry_to_numbers(Val.Entry, RB0, NegNumb.Proof, RB) :- !, + convert_goal_to_number(Val, RB0, Numb, RBI), + NegNumb is -Numb, + convert_trie_entry_to_numbers(Entry, RBI, Proof, RB). + +convert_goal_to_number(Val, RB0, Numb, RBI) :- + rb_lookup(Val, Numb, RB0), !, + RB0 = RBI. +convert_goal_to_number(Val, RB0, I, RBI) :- + nb_getval(cnf_nodes, I0), + I is I0+1, + nb_setval(cnf_nodes, I), + rb_insert(RB0, Val, I, RBI). + +invert_cnf_varids(CNF, InvVNameCNF) :- + nb_getval(cnf_nodes,Nodes), + invert_cnf_varids(CNF, Nodes, InvVNameCNF, []). + +invert_cnf_varids([], _) --> []. +invert_cnf_varids(C.CNF, Nodes) --> [NC], + { invert_c_varids(C, Nodes, NC, []) }, + invert_cnf_varids(CNF, Nodes). + +invert_c_varids([], _Nodes) --> []. +invert_c_varids(N.CNF, Nodes) --> + [NN], + { inv_node(N,Nodes,NN) }, + invert_c_varids(CNF, Nodes). + +inv_node(N,Nodes,NN) :- + ( N > 0 -> NN is (Nodes-N)+1 ; NN is -(Nodes+N+1) ). + +randomize_cnf_varids(CNF, RandomVNameCNF) :- + nb_getval(cnf_nodes,Nodes), + generate_numbers(Nodes, Numbers), + randomize_list(Numbers, RandomNumbers). + +cnf_to_wdimacs(CNF, RB, File) :- + File = dimacs, + open(dimacs,write,Stream), + length(CNF,M), + nb_getval(cnf_nodes,N), + format(Stream,'p cnf ~d ~d~n',[N,M]), + output_probs(Stream, RB), + cnf_lines_to_dimacs(CNF, Stream), + close(Stream). + +output_probs(Stream, RB) :- + rb_in(K, V, RB), + dump_weight(Stream, K, V), + fail. +output_probs(_Stream, _RB). + +dump_weight(Stream, K, V) :- + get_fact_probability(K,ProbFact), + format(Stream,'w ~d ~f~n',[V,ProbFact]). + +cnf_to_dimacs(CNF, File) :- + File = dimacs, + open(dimacs,write,Stream), + length(CNF,M), + nb_getval(cnf_nodes,N), + format(Stream,'p cnf ~d ~d~n',[N,M]), + cnf_lines_to_dimacs(CNF, Stream), + close(Stream). + +cnf_lines_to_dimacs([], _Stream). +cnf_lines_to_dimacs([Line|CNF], Stream) :- + cnf_line_to_dimacs(Line,Stream), + cnf_lines_to_dimacs(CNF, Stream). + +cnf_line_to_dimacs([],Stream) :- + format(Stream,'0~n',[]). +cnf_line_to_dimacs([L|Line],Stream) :- + format(Stream,'~w ',[L]), + cnf_line_to_dimacs(Line,Stream). + +nnf_to_probability(File, RBTree, Result) :- + File = 'dimacs.nnf', + open(File, read, Stream), + process_nnf(Stream, RBTree, Result), + close(Stream). + +process_nnf(Stream, RevRBTree, Result) :- + rb_visit(RevRBTree, ListOfPairs), + swap_key_values(ListOfPairs, SwappedList), + list_to_rbtree(SwappedList, RBTree), + read_line_to_codes(Stream, Header), + split(Header, ["nnf",VS,_ES,_NS]), + number_codes(V, VS), + %trace, + call(functor(TempResults, nnf, V)), + process_nnf_lines(Stream, RBTree, 1, TempResults), + arg(V, TempResults, Result). + +swap_key_values([], []). +swap_key_values((K-V).ListOfPairs, (V-K).SwappedList) :- + swap_key_values(ListOfPairs, SwappedList). + + +process_nnf_lines(Stream, RBTree, LineNumber, TempResults) :- + read_line_to_codes(Stream, Codes), + ( Codes = end_of_file -> true ; +% (LineNumber > 1 -> N is LineNumber-1, arg(N,TempResults,P), format("~w ",[P]);true), +% format("~s~n",[Codes]), + process_nnf_line(RBTree, LineNumber, TempResults, Codes, []), + NewLine is LineNumber+1, + process_nnf_lines(Stream, RBTree, NewLine, TempResults) + ). + +process_nnf_line(RBTree, Line, TempResults) --> "L ", + nnf_leaf(RBTree, Line, TempResults). +process_nnf_line(_RBTree, Line, TempResults) --> "A ", + nnf_and_node(Line, TempResults). +process_nnf_line(_RBTree, Line, TempResults) --> "O ", + nnf_or_node(Line, TempResults). + +nnf_leaf(RBTree, LineNumber, TempResults, Codes, []) :- + number_codes(Number, Codes), + Abs is abs(Number), + rb_lookup(Abs, Node, RBTree), +% get_fact_probability(Node, ProbFact), +% (Number < 0 -> Prob is 1-ProbFact ; Prob = ProbFact), + (get_fact_probability(Node,ProbFact) -> (Number < 0 -> Prob is 1-ProbFact ; Prob = ProbFact) ; Prob = special), + arg(LineNumber, TempResults, Prob). + +nnf_and_node(LineNumber, TempResults, Codes, []) :- + split(Codes, [_|NumberAsStrings]), + multiply_nodes(NumberAsStrings, 1.0, TempResults, Product), + arg(LineNumber, TempResults, Product). + +multiply_nodes([], Product, _, Product). +multiply_nodes(NumberAsString.NumberAsStrings, Product0, TempResults, Product) :- + number_codes(Pos, NumberAsString), + Pos1 is Pos+1, + arg(Pos1, TempResults, P), + ( P == special -> ProductI=Product0; ProductI is P*Product0 ), + multiply_nodes(NumberAsStrings, ProductI, TempResults, Product). + +nnf_or_node(LineNumber, TempResults, Codes, []) :- + split(Codes, [_,_|NumberAsStrings]), + add_nodes(NumberAsStrings, 0.0, TempResults, Product), + arg(LineNumber, TempResults, Product). + +add_nodes([], Product, _, Product). +add_nodes(NumberAsString.NumberAsStrings, Product0, TempResults, Product) :- + number_codes(Pos, NumberAsString), + Pos1 is Pos+1, + arg(Pos1, TempResults, P), + ( P == special -> ProductI=Product0; ProductI is P+Product0 ), + add_nodes(NumberAsStrings, ProductI, TempResults, Product). + +problog_cnf_positive(Goal, _) :- + init_problog_low(0.0), + problog_control(off, up), + timer_start(sld_time), + problog_call(Goal), + add_solution, + fail. +problog_cnf_positive(_,Prob) :- + timer_stop(sld_time,SLD_Time), + problog_var_set(sld_time, SLD_Time), + nb_getval(problog_completed_proofs, Trie_Completed_Proofs), +% trie_to_cnf(Trie_Completed_Proofs, CNF, RB), +% cnf_to_dimacs(CNF, _File), + trie_to_dimacs(Trie_Completed_Proofs, RB, _File), + unix(system('./c2d_linux -in dimacs')), + % execute c2d at this point, but we're lazy + nnf_to_probability(_NNFFile, RB, Prob), + delete_ptree(Trie_Completed_Proofs), + (problog_flag(retain_tables, true) -> retain_tabling; true), + clear_tabling. + +trie_to_dimacs(Trie_Completed_Proofs, RB, File) :- + problog_flag(db_trie_opt_lvl, OptimizationLevel), + trie_to_depth_breadth_trie(Trie_Completed_Proofs, DBTrie, LL, OptimizationLevel), + dbtrie_to_cnf(DBTrie, LL, RB, CNF), + File = dimacs, + open(dimacs,write,Stream), + length(CNF,M), + nb_getval(cnf_nodes,N), + format(Stream,'p cnf ~d ~d~n',[N,M]), + cnf_lines_to_dimacs(CNF, Stream), + close(Stream). + + +dbtrie_to_cnf(DBTrie, LL, RB, CNF) :- + % tricky way to find the number of intermediate nodes. + (atomic_concat('L', _InterStep, LL) -> + % cleanup + retractall(deref(_,_)), + (problog_flag(deref_terms, true) -> + asserta(deref(LL,no)), + mark_for_deref(DBTrie), + V = 3 + ; + V = 1 + ), + % do the real work + bdd_defs_to_cnf(DBTrie, CNF, LL, RB) + ; + % cases true, false, single literal + ( LL == true -> CNF = [[1,-1]] + ; + LL == false -> CNF = [[1],[-1]] + ; + convert_goal_to_number(LL, RB, NN, _RBI), + CNF = [[NN]] + ) + ). + +bdd_defs_to_cnf(DBTrie, [[NN]|CNF], LL, RB) :- fail, + findall(Node, in_trie(DBTrie, Node), Nodes0), +% reverse(Nodes0, Nodes), +% depth_first(Nodes0, LL, Nodes), + Nodes0 = Nodes, + rb_new(RB0), + nb_setval(cnf_nodes, 0), + convert_goal_to_number(LL, RB0, NN, RB1), + xnodes_to_cnf(Nodes, RB1, RB, CNF, []). +bdd_defs_to_cnf(Trie, [[NN]|CNF], LL, RB) :- + trie_traverse_first(Trie, RefFirst), + rb_new(RB0), + nb_setval(cnf_nodes, 0), + convert_goal_to_number(LL, RB0, NN, RB1), + bdd_defs_to_list_of_numbers(Trie, RB1, RefFirst, [], CNF, RB). + + +depth_first(Nodes0, LL, Nodes) :- + rb_new(RB0), + insert_all(Nodes0, RB0, RB), + pick_nodes(LL, RB, _, Nodes, []). + +insert_all([], RB, RB). +insert_all(Node.Nodes0, RB0, RB) :- + arg(2, Node, Key), + rb_insert(RB0, Key, Node, RBI), + insert_all(Nodes0, RBI, RB). + +pick_nodes(Key, RB0, RBF) --> + { rb_delete(RB0, Key, Node, RBI) }, + !, + [Node], + { arg(1, Node, Children) }, + pick_recursively(Children, RBI, RBF). +pick_nodes(_, RB, RB) --> []. + +pick_recursively([], RB, RB) --> []. +pick_recursively(Key.Keys, RB0, RBF) --> + pick_nodes(Key, RB0, RBI), + pick_recursively(Keys, RBI, RBF). + +in_trie(Trie, Entry) :- + trie_traverse(Trie, Ref), + trie_get_entry(Ref, Entry). + +xnodes_to_cnf([], RB, RB) --> []. +xnodes_to_cnf(Node.Nodes, RB0, RB) --> + xnode_to_cnf(Node, RB0, RBI), + xnodes_to_cnf(Nodes, RBI, RB). + +xnode_to_cnf(Node, RB0, RBI, CNF, PartialCNF) :- + convert_dbtrie_entry_to_numbers(Node, RB0, PartialCNF, CNF, RBI). + +bdd_defs_to_list_of_numbers(Trie, RB0, CurrentRef, PartialCNF, FinalCNF, RB) :- + trie_get_entry(CurrentRef, Entry), +writeln(Entry), + convert_dbtrie_entry_to_numbers(Entry, RB0, PartialCNF, NextCNF, RBI), + continue_processing_dbtrie(Trie, RBI, CurrentRef, NextCNF, FinalCNF, RB). + +continue_processing_dbtrie(Trie, RB0, CurrentRef, PartialCNF, FinalCNF, RB) :- + trie_traverse_next(CurrentRef, NextRef), !, + bdd_defs_to_list_of_numbers(Trie, RB0, NextRef, PartialCNF, FinalCNF, RB). +continue_processing_dbtrie(_, RB, _CurrentRef, CNF, CNF, RB). + +convert_dbtrie_entry_to_numbers(depth(List,Name), RB0, PartialCNF, CNF, RBI) :- + convert_trie_entry_to_numbers_positive(List, RB0, NumList, NextRB), + convert_goal_to_number(Name, NextRB, NumName, RBI), + add_conjunction_to_cnf(NumList, NumName, PartialCNF, CNF).%,format(user_error,'conj ~q gives ~q~n',[NumList-NumName, CNF]). +convert_dbtrie_entry_to_numbers(breadth(List,Name), RB0, PartialCNF, CNF, RBI) :- + convert_trie_entry_to_numbers_positive(List, RB0, NumList, NextRB), + convert_goal_to_number(Name, NextRB, NumName, RBI), + add_disjunction_to_cnf(NumList, NumName, PartialCNF, CNF).%,format(user_error,'disj ~q gives ~q~n',[NumList-NumName, CNF]). + +convert_trie_entry_to_numbers_positive([], RB, [], RB). +convert_trie_entry_to_numbers_positive(not(Val).Entry, RB0, (-Numb).Proof, RB) :- !, + convert_goal_to_number(Val, RB0, Numb, RBI), + convert_trie_entry_to_numbers_positive(Entry, RBI, Proof, RB). +convert_trie_entry_to_numbers_positive(Val.Entry, RB0, Numb.Proof, RB) :- !, + convert_goal_to_number(Val, RB0, Numb, RBI), + convert_trie_entry_to_numbers_positive(Entry, RBI, Proof, RB). + +add_conjunction_to_cnf(NumList, NumName, PartialCNF, CNF) :- + neg_numbers(NumList,NegList), + add_conj_to_cnf(NumList, NumName, [[NumName|NegList]|PartialCNF], CNF). + +add_conj_to_cnf([],_,CNF,CNF). +add_conj_to_cnf([Num|List],NumName,CNF0,CNF) :- + NegNumName is -NumName, + add_conj_to_cnf(List,NumName,[[NegNumName,Num]|CNF0],CNF). + +add_disjunction_to_cnf(NumList, NumName, PartialCNF, CNF) :- + NegNumName is -NumName, + add_disj_to_cnf(NumList, NumName, [[NegNumName|NumList]|PartialCNF], CNF). + +add_disj_to_cnf([],_,CNF,CNF). +add_disj_to_cnf([Num|List],NumName,CNF0,CNF) :- + neg_num(Num,NegNum), + add_disj_to_cnf(List,NumName,[[NumName,NegNum]|CNF0],CNF). + +neg_num(Y,X) :- X is -Y. + +neg_numbers([],[]). +neg_numbers([Y|List],[X|ListN]) :- + neg_num(Y,X), + neg_numbers(List,ListN). + + +%%%% + init_problog_low(Threshold) :- init_ptree(Trie_Completed_Proofs), nb_setval(problog_completed_proofs, Trie_Completed_Proofs), diff --git a/packages/ProbLog/problog_lfi.yap b/packages/ProbLog/problog_lfi.yap index c9f74dadc..b4c24c7dd 100644 --- a/packages/ProbLog/problog_lfi.yap +++ b/packages/ProbLog/problog_lfi.yap @@ -239,6 +239,8 @@ :- dynamic(query_all_scripts/2). :- dynamic(last_llh/1). +:- dynamic(user:myclause/2). + :- discontiguous(user:myclause/1). :- discontiguous(user:myclause/2). :- discontiguous(user:known/3).