Merge branch 'master' of ssh://yap.git.sourceforge.net/gitroot/yap/yap-6.3
Conflicts: OPTYap/opt.config.h OPTYap/opt.structs.h
This commit is contained in:
Vítor Santos Costa
commit
79d1bf5eec
@ -13,109 +13,45 @@
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
/************************************************************************
|
/****************************************************************
|
||||||
** General Configuration Parameters **
|
** 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 **
|
|
||||||
************************************************************************/
|
|
||||||
|
|
||||||
/****************************
|
/****************************
|
||||||
** default sizes **
|
** 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_LENGTH_ANSWER 1000
|
||||||
#define MAX_BRANCH_DEPTH 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 MMAP_MEMORY_MAPPING_SCHEME 1
|
||||||
/* #define SHM_MEMORY_MAPPING_SCHEME 1 */
|
/* #define SHM_MEMORY_MAPPING_SCHEME 1 */
|
||||||
|
|
||||||
/*************************************************
|
/****************************************************************
|
||||||
** enable error checking ? (optional) **
|
** use shared pages memory alloc scheme ? (optional) **
|
||||||
*************************************************/
|
****************************************************************/
|
||||||
/* #define DEBUG_YAPOR 1 */
|
/* #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) **
|
||||||
************************************************************************/
|
************************************************************************/
|
||||||
|
#define THREADS_NO_SHARING 1
|
||||||
/****************************
|
/* #define THREADS_SUBGOAL_SHARING 1 */
|
||||||
** default sizes **
|
/* #define THREADS_FULL_SHARING 1 */
|
||||||
****************************/
|
/* #define THREADS_CONSUMER_SHARING 1 */
|
||||||
#define TG_ANSWER_SLOTS 20
|
|
||||||
#define TRIE_LOCK_BUCKETS 512
|
|
||||||
|
|
||||||
/*************************************************************************
|
/*************************************************************************
|
||||||
** tries locking scheme (mandatory, define one per trie type) **
|
** tries locking scheme (mandatory, define one per trie type) **
|
||||||
@ -156,26 +92,86 @@
|
|||||||
#define TRIE_LOCK_USING_NODE_FIELD 1
|
#define TRIE_LOCK_USING_NODE_FIELD 1
|
||||||
/* #define TRIE_LOCK_USING_GLOBAL_ARRAY 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
|
#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 **
|
** Parameter Checks **
|
||||||
************************************************************************/
|
************************************************************************/
|
||||||
|
|
||||||
#ifndef USE_PAGES_MALLOC
|
#ifdef YAPOR
|
||||||
#undef LIMIT_TABLING
|
#ifdef i386 /* For i386 machines we use shared memory segments */
|
||||||
#endif /* ! USE_PAGES_MALLOC */
|
#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
|
#ifdef TABLING
|
||||||
#if !defined(BFZ_TRAIL_SCHEME) && !defined(BBREG_TRAIL_SCHEME)
|
#if !defined(BFZ_TRAIL_SCHEME) && !defined(BBREG_TRAIL_SCHEME)
|
||||||
@ -197,27 +193,7 @@
|
|||||||
#undef DEBUG_TABLING
|
#undef DEBUG_TABLING
|
||||||
#endif /* TABLING */
|
#endif /* TABLING */
|
||||||
|
|
||||||
|
#if defined(TABLING) && (defined(YAPOR) || defined(THREADS))
|
||||||
#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)
|
|
||||||
/* SUBGOAL_TRIE_LOCK_LEVEL */
|
/* 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)
|
#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
|
#error Define a subgoal trie lock scheme
|
||||||
@ -260,13 +236,70 @@
|
|||||||
#ifndef GLOBAL_TRIE_LOCK_AT_WRITE_LEVEL
|
#ifndef GLOBAL_TRIE_LOCK_AT_WRITE_LEVEL
|
||||||
#undef GLOBAL_TRIE_ALLOC_BEFORE_CHECK
|
#undef GLOBAL_TRIE_ALLOC_BEFORE_CHECK
|
||||||
#endif
|
#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)
|
#if !defined(TRIE_LOCK_USING_NODE_FIELD) && !defined(TRIE_LOCK_USING_GLOBAL_ARRAY)
|
||||||
#error Define a trie lock data structure
|
#error Define a trie lock data structure
|
||||||
#endif
|
#endif
|
||||||
#if defined(TRIE_LOCK_USING_NODE_FIELD) && defined(TRIE_LOCK_USING_GLOBAL_ARRAY)
|
#if defined(TRIE_LOCK_USING_NODE_FIELD) && defined(TRIE_LOCK_USING_GLOBAL_ARRAY)
|
||||||
#error Do not define multiple trie lock data structures
|
#error Do not define multiple trie lock data structures
|
||||||
#endif
|
#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
|
#ifdef TRIE_LOCK_USING_NODE_FIELD
|
||||||
#if defined(SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL) || defined(SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL)
|
#if defined(SUBGOAL_TRIE_LOCK_AT_NODE_LEVEL) || defined(SUBGOAL_TRIE_LOCK_AT_WRITE_LEVEL)
|
||||||
#define SUBGOAL_TRIE_LOCK_USING_NODE_FIELD 1
|
#define SUBGOAL_TRIE_LOCK_USING_NODE_FIELD 1
|
||||||
@ -288,25 +321,34 @@
|
|||||||
#define GLOBAL_TRIE_LOCK_USING_GLOBAL_ARRAY 1
|
#define GLOBAL_TRIE_LOCK_USING_GLOBAL_ARRAY 1
|
||||||
#endif
|
#endif
|
||||||
#endif
|
#endif
|
||||||
#else /* ! TABLING || ! YAPOR */
|
|
||||||
#undef SUBGOAL_TRIE_LOCK_AT_ENTRY_LEVEL
|
#if !defined(TABLING) || !defined(YAPOR)
|
||||||
#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
|
|
||||||
#undef TABLING_INNER_CUTS
|
#undef TABLING_INNER_CUTS
|
||||||
#undef TIMESTAMP_CHECK
|
#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)
|
#if defined(DEBUG_YAPOR) && defined(DEBUG_TABLING)
|
||||||
#define DEBUG_OPTYAP
|
#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
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
@ -219,7 +219,7 @@ void Yap_init_root_frames(void) {
|
|||||||
#ifdef TABLING
|
#ifdef TABLING
|
||||||
/* root dependency frame */
|
/* root dependency frame */
|
||||||
#ifdef YAPOR
|
#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
|
#else
|
||||||
DepFr_cons_cp(LOCAL_top_dep_fr) = B;
|
DepFr_cons_cp(LOCAL_top_dep_fr) = B;
|
||||||
#endif /* YAPOR */
|
#endif /* YAPOR */
|
||||||
|
|||||||
@ -78,10 +78,10 @@ typedef struct page_header {
|
|||||||
***************************/
|
***************************/
|
||||||
|
|
||||||
struct pages {
|
struct pages {
|
||||||
#ifdef USE_PAGES_MALLOC
|
|
||||||
#if defined(YAPOR) || defined(THREADS)
|
#if defined(YAPOR) || defined(THREADS)
|
||||||
lockvar lock;
|
lockvar lock;
|
||||||
#endif /* YAPOR */
|
#endif /* YAPOR || THREADS */
|
||||||
|
#ifdef USE_PAGES_MALLOC
|
||||||
int structs_per_page;
|
int structs_per_page;
|
||||||
struct page_header *first_free_page;
|
struct page_header *first_free_page;
|
||||||
volatile long pages_allocated;
|
volatile long pages_allocated;
|
||||||
@ -127,6 +127,12 @@ struct global_pages {
|
|||||||
struct pages answer_trie_hash_pages;
|
struct pages answer_trie_hash_pages;
|
||||||
struct pages global_trie_hash_pages;
|
struct pages global_trie_hash_pages;
|
||||||
#endif /* TABLING */
|
#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)
|
#if defined(YAPOR) && defined(TABLING)
|
||||||
struct pages suspension_frame_pages;
|
struct pages suspension_frame_pages;
|
||||||
#endif /* YAPOR && TABLING */
|
#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 **
|
* Struct global_optyap_data **
|
||||||
*********************************/
|
*********************************/
|
||||||
@ -212,6 +242,9 @@ struct global_optyap_data {
|
|||||||
#ifdef YAPOR
|
#ifdef YAPOR
|
||||||
struct dependency_frame *root_dependency_frame;
|
struct dependency_frame *root_dependency_frame;
|
||||||
#endif /* YAPOR */
|
#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];
|
CELL table_var_enumerator[MAX_TABLE_VARS];
|
||||||
#ifdef TRIE_LOCK_USING_GLOBAL_ARRAY
|
#ifdef TRIE_LOCK_USING_GLOBAL_ARRAY
|
||||||
lockvar trie_locks[TRIE_LOCK_BUCKETS];
|
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_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_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_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_pages_susp_fr (GLOBAL_optyap_data.pages.suspension_frame_pages)
|
||||||
#define GLOBAL_scheduler_loop (GLOBAL_optyap_data.scheduler_loop)
|
#define GLOBAL_scheduler_loop (GLOBAL_optyap_data.scheduler_loop)
|
||||||
#define GLOBAL_delayed_release_load (GLOBAL_optyap_data.delayed_release_load)
|
#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_last_sg_fr (GLOBAL_optyap_data.last_subgoal_frame)
|
||||||
#define GLOBAL_check_sg_fr (GLOBAL_optyap_data.check_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_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(index) (GLOBAL_optyap_data.table_var_enumerator[index])
|
||||||
#define GLOBAL_table_var_enumerator_addr(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])
|
#define GLOBAL_trie_locks(index) (GLOBAL_optyap_data.trie_locks[index])
|
||||||
|
|||||||
@ -88,6 +88,7 @@ static inline tg_sol_fr_ptr CUT_prune_tg_solution_frames(tg_sol_fr_ptr, int);
|
|||||||
** Tabling defines **
|
** Tabling defines **
|
||||||
******************************/
|
******************************/
|
||||||
|
|
||||||
|
/* traverse macros */
|
||||||
#define SHOW_MODE_STRUCTURE 0
|
#define SHOW_MODE_STRUCTURE 0
|
||||||
#define SHOW_MODE_STATISTICS 1
|
#define SHOW_MODE_STATISTICS 1
|
||||||
#define TRAVERSE_MODE_NORMAL 0
|
#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)))
|
#define CompactPairEndList AbsPair((Term *) (2*(LowTagBits + 1)))
|
||||||
#endif /* TRIE_COMPACT_PAIRS */
|
#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 */
|
/* choice points */
|
||||||
#define NORM_CP(CP) ((choiceptr)(CP))
|
#define NORM_CP(CP) ((choiceptr)(CP))
|
||||||
#define GEN_CP(CP) ((struct generator_choicept *)(CP))
|
#define GEN_CP(CP) ((struct generator_choicept *)(CP))
|
||||||
|
|||||||
@ -31,21 +31,30 @@ typedef struct table_entry {
|
|||||||
#ifdef MODE_DIRECTED_TABLING
|
#ifdef MODE_DIRECTED_TABLING
|
||||||
int* mode_directed_array;
|
int* mode_directed_array;
|
||||||
#endif /*MODE_DIRECTED_TABLING*/
|
#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;
|
struct subgoal_trie_node *subgoal_trie;
|
||||||
|
#endif /*THREADS_NO_SHARING */
|
||||||
struct subgoal_trie_hash *hash_chain;
|
struct subgoal_trie_hash *hash_chain;
|
||||||
struct table_entry *next;
|
struct table_entry *next;
|
||||||
} *tab_ent_ptr;
|
} *tab_ent_ptr;
|
||||||
|
|
||||||
#define TabEnt_lock(X) ((X)->lock)
|
#define TabEnt_lock(X) ((X)->lock)
|
||||||
#define TabEnt_pe(X) ((X)->pred_entry)
|
#define TabEnt_pe(X) ((X)->pred_entry)
|
||||||
#define TabEnt_atom(X) ((X)->pred_atom)
|
#define TabEnt_atom(X) ((X)->pred_atom)
|
||||||
#define TabEnt_arity(X) ((X)->pred_arity)
|
#define TabEnt_arity(X) ((X)->pred_arity)
|
||||||
#define TabEnt_flags(X) ((X)->pred_flags)
|
#define TabEnt_flags(X) ((X)->pred_flags)
|
||||||
#define TabEnt_mode(X) ((X)->execution_mode)
|
#define TabEnt_mode(X) ((X)->execution_mode)
|
||||||
#define TabEnt_mode_directed(X) ((X)->mode_directed_array)
|
#define TabEnt_mode_directed(X) ((X)->mode_directed_array)
|
||||||
#define TabEnt_subgoal_trie(X) ((X)->subgoal_trie)
|
#ifdef THREADS_NO_SHARING
|
||||||
#define TabEnt_hash_chain(X) ((X)->hash_chain)
|
#define TabEnt_subgoal_trie(X) ((X)->subgoal_trie[worker_id])
|
||||||
#define TabEnt_next(X) ((X)->next)
|
#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 **
|
** 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 {
|
typedef struct subgoal_entry {
|
||||||
#if defined(YAPOR) || defined(THREADS)
|
#if defined(YAPOR) || defined(THREADS_FULL_SHARING) || defined(THREADS_CONSUMER_SHARING)
|
||||||
lockvar lock;
|
lockvar lock;
|
||||||
#endif /* YAPOR || THREADS */
|
#endif /* YAPOR || THREADS_FULL_SHARING || THREADS_CONSUMER_SHARING */
|
||||||
#ifdef YAPOR
|
|
||||||
int generator_worker;
|
|
||||||
struct or_frame *top_or_frame_on_generator_branch;
|
|
||||||
#endif /* YAPOR */
|
|
||||||
yamop *code_of_subgoal;
|
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_hash *hash_chain;
|
||||||
struct answer_trie_node *answer_trie;
|
struct answer_trie_node *answer_trie;
|
||||||
struct answer_trie_node *first_answer;
|
struct answer_trie_node *first_answer;
|
||||||
@ -223,61 +253,130 @@ typedef struct subgoal_frame {
|
|||||||
#ifdef MODE_DIRECTED_TABLING
|
#ifdef MODE_DIRECTED_TABLING
|
||||||
int* mode_directed_array;
|
int* mode_directed_array;
|
||||||
struct answer_trie_node *invalid_chain;
|
struct answer_trie_node *invalid_chain;
|
||||||
#endif /*MODE_DIRECTED_TABLING*/
|
#endif /* MODE_DIRECTED_TABLING */
|
||||||
#ifdef INCOMPLETE_TABLING
|
#ifdef INCOMPLETE_TABLING
|
||||||
struct answer_trie_node *try_answer;
|
struct answer_trie_node *try_answer;
|
||||||
#endif /* INCOMPLETE_TABLING */
|
#endif /* INCOMPLETE_TABLING */
|
||||||
#ifdef LIMIT_TABLING
|
#ifdef LIMIT_TABLING
|
||||||
struct subgoal_frame *previous;
|
struct subgoal_frame *previous;
|
||||||
#endif /* LIMIT_TABLING */
|
#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;
|
struct subgoal_frame *next;
|
||||||
} *sg_fr_ptr;
|
} *sg_fr_ptr;
|
||||||
|
|
||||||
#define SgFr_lock(X) ((X)->lock)
|
/* subgoal_entry fields */
|
||||||
#define SgFr_gen_worker(X) ((X)->generator_worker)
|
#ifdef THREADS
|
||||||
#define SgFr_gen_top_or_fr(X) ((X)->top_or_frame_on_generator_branch)
|
#define SUBGOAL_ENTRY(X) SgFr_subgoal_entry(X)->
|
||||||
#define SgFr_code(X) ((X)->code_of_subgoal)
|
#else
|
||||||
#define SgFr_tab_ent(X) (((X)->code_of_subgoal)->u.Otapl.te)
|
#define SUBGOAL_ENTRY(X) (X)->subgoal_entry.
|
||||||
#define SgFr_arity(X) (((X)->code_of_subgoal)->u.Otapl.s)
|
#endif /* THREADS */
|
||||||
#define SgFr_state(X) ((X)->state_flag)
|
#define SgFr_lock(X) (SUBGOAL_ENTRY(X) lock)
|
||||||
#define SgFr_gen_cp(X) ((X)->generator_choice_point)
|
#define SgFr_code(X) (SUBGOAL_ENTRY(X) code_of_subgoal)
|
||||||
#define SgFr_hash_chain(X) ((X)->hash_chain)
|
#define SgFr_tab_ent(X) ((SUBGOAL_ENTRY(X) code_of_subgoal)->u.Otapl.te)
|
||||||
#define SgFr_answer_trie(X) ((X)->answer_trie)
|
#define SgFr_arity(X) ((SUBGOAL_ENTRY(X) code_of_subgoal)->u.Otapl.s)
|
||||||
#define SgFr_first_answer(X) ((X)->first_answer)
|
#define SgFr_hash_chain(X) (SUBGOAL_ENTRY(X) hash_chain)
|
||||||
#define SgFr_last_answer(X) ((X)->last_answer)
|
#define SgFr_answer_trie(X) (SUBGOAL_ENTRY(X) answer_trie)
|
||||||
#define SgFr_mode_directed(X) ((X)->mode_directed_array)
|
#define SgFr_first_answer(X) (SUBGOAL_ENTRY(X) first_answer)
|
||||||
#define SgFr_invalid_chain(X) ((X)->invalid_chain)
|
#define SgFr_last_answer(X) (SUBGOAL_ENTRY(X) last_answer)
|
||||||
#define SgFr_try_answer(X) ((X)->try_answer)
|
#define SgFr_mode_directed(X) (SUBGOAL_ENTRY(X) mode_directed_array)
|
||||||
#define SgFr_previous(X) ((X)->previous)
|
#define SgFr_invalid_chain(X) (SUBGOAL_ENTRY(X) invalid_chain)
|
||||||
#define SgFr_next(X) ((X)->next)
|
#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_lock: spin-lock to modify the frame fields.
|
||||||
SgFr_gen_worker: the id of the worker that had allocated the frame.
|
SgFr_code initial instruction of the subgoal's compiled code.
|
||||||
SgFr_gen_top_or_fr: a pointer to the top or-frame in the generator choice point branch.
|
SgFr_tab_ent a pointer to the corresponding table entry.
|
||||||
When the generator choice point is shared the pointer is updated
|
SgFr_arity the arity of the subgoal.
|
||||||
to its or-frame. It is used to find the direct dependency node for
|
SgFr_hash_chain: a pointer to the first answer_trie_hash struct.
|
||||||
consumer nodes in other workers branches.
|
SgFr_answer_trie: a pointer to the top answer trie node.
|
||||||
SgFr_code initial instruction of the subgoal's compiled code.
|
SgFr_first_answer: a pointer to the leaf answer trie node of the first answer.
|
||||||
SgFr_tab_ent a pointer to the correspondent table entry.
|
SgFr_last_answer: a pointer to the leaf answer trie node of the last answer.
|
||||||
SgFr_arity the arity of the subgoal.
|
SgFr_mode_directed: a pointer to the mode directed array.
|
||||||
SgFr_state: a flag that indicates the subgoal state.
|
SgFr_invalid_chain: a pointer to the first invalid leaf node when using mode directed tabling.
|
||||||
SgFr_gen_cp: a pointer to the correspondent generator choice point.
|
SgFr_try_answer: a pointer to the leaf answer trie node of the last tried answer.
|
||||||
SgFr_hash_chain: a pointer to the first answer_trie_hash struct for the subgoal in hand.
|
It is used when a subgoal was not completed during the previous evaluation.
|
||||||
SgFr_answer_trie: a pointer to the top answer trie node.
|
Not completed subgoals start by trying the answers already found.
|
||||||
It is used to check for/insert new answers.
|
SgFr_previous: a pointer to the previous subgoal frame on the chain.
|
||||||
SgFr_first_answer: a pointer to the bottom answer trie node of the first available answer.
|
SgFr_gen_top_or_fr: a pointer to the top or-frame in the generator choice point branch.
|
||||||
SgFr_last_answer: a pointer to the bottom answer trie node of the last available answer.
|
When the generator choice point is shared the pointer is updated
|
||||||
SgFr_mode_directed: a pointer to the mode directed array.
|
to its or-frame. It is used to find the direct dependency node for
|
||||||
SgFr_invalid_chain: a pointer to the first invalid leaf node when using mode directed tabling.
|
consumer nodes in other workers branches.
|
||||||
SgFr_try_answer: a pointer to the bottom answer trie node of the last tried answer.
|
SgFr_gen_worker: the id of the worker that had allocated the frame.
|
||||||
It is used when a subgoal was not completed during the previous evaluation.
|
SgFr_sg_ent_state: a flag that indicates the subgoal entry state.
|
||||||
Not completed subgoals start by trying the answers already found.
|
SgFr_active_workers: the number of workers evaluating the subgoal.
|
||||||
SgFr_previous: a pointer to the previous subgoal frame on the chain.
|
SgFr_subgoal_entry: a pointer to the corresponding subgoal entry.
|
||||||
SgFr_next: a pointer to the next subgoal frame on the chain.
|
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 {
|
typedef struct dependency_frame {
|
||||||
#if defined(YAPOR) || defined(THREADS)
|
#ifdef YAPOR
|
||||||
lockvar lock;
|
lockvar lock;
|
||||||
#endif /* YAPOR || THREADS */
|
#endif /* YAPOR */
|
||||||
#ifdef YAPOR
|
#ifdef YAPOR
|
||||||
int leader_dependency_is_on_stack;
|
int leader_dependency_is_on_stack;
|
||||||
struct or_frame *top_or_frame;
|
struct or_frame *top_or_frame;
|
||||||
@ -300,6 +399,9 @@ typedef struct dependency_frame {
|
|||||||
choiceptr leader_choice_point;
|
choiceptr leader_choice_point;
|
||||||
choiceptr consumer_choice_point;
|
choiceptr consumer_choice_point;
|
||||||
struct answer_trie_node *last_consumed_answer;
|
struct answer_trie_node *last_consumed_answer;
|
||||||
|
#ifdef THREADS_CONSUMER_SHARING
|
||||||
|
int generator_is_external;
|
||||||
|
#endif /* THREADS_CONSUMER_SHARING */
|
||||||
struct dependency_frame *next;
|
struct dependency_frame *next;
|
||||||
} *dep_fr_ptr;
|
} *dep_fr_ptr;
|
||||||
|
|
||||||
@ -311,9 +413,10 @@ typedef struct dependency_frame {
|
|||||||
#define DepFr_leader_cp(X) ((X)->leader_choice_point)
|
#define DepFr_leader_cp(X) ((X)->leader_choice_point)
|
||||||
#define DepFr_cons_cp(X) ((X)->consumer_choice_point)
|
#define DepFr_cons_cp(X) ((X)->consumer_choice_point)
|
||||||
#define DepFr_last_answer(X) ((X)->last_consumed_answer)
|
#define DepFr_last_answer(X) ((X)->last_consumed_answer)
|
||||||
|
#define DepFr_external(X) ((X)->generator_is_external)
|
||||||
#define DepFr_next(X) ((X)->next)
|
#define DepFr_next(X) ((X)->next)
|
||||||
|
|
||||||
/*******************************************************************************************************
|
/*********************************************************************************************************
|
||||||
|
|
||||||
DepFr_lock: lock variable to modify the frame fields.
|
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
|
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_leader_cp: a pointer to the leader choice point.
|
||||||
DepFr_cons_cp: a pointer to the correspondent consumer choice point.
|
DepFr_cons_cp: a pointer to the correspondent consumer choice point.
|
||||||
DepFr_last_answer: a pointer to the last consumed answer.
|
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.
|
DepFr_next: a pointer to the next dependency frame on the chain.
|
||||||
|
|
||||||
*******************************************************************************************************/
|
*********************************************************************************************************/
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
@ -2099,6 +2099,398 @@ problog_low(_, _, LP, Status) :-
|
|||||||
(problog_flag(retain_tables, true) -> retain_tabling; true),
|
(problog_flag(retain_tables, true) -> retain_tabling; true),
|
||||||
clear_tabling.
|
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_problog_low(Threshold) :-
|
||||||
init_ptree(Trie_Completed_Proofs),
|
init_ptree(Trie_Completed_Proofs),
|
||||||
nb_setval(problog_completed_proofs, Trie_Completed_Proofs),
|
nb_setval(problog_completed_proofs, Trie_Completed_Proofs),
|
||||||
|
|||||||
@ -239,6 +239,8 @@
|
|||||||
:- dynamic(query_all_scripts/2).
|
:- dynamic(query_all_scripts/2).
|
||||||
:- dynamic(last_llh/1).
|
:- dynamic(last_llh/1).
|
||||||
|
|
||||||
|
:- dynamic(user:myclause/2).
|
||||||
|
|
||||||
:- discontiguous(user:myclause/1).
|
:- discontiguous(user:myclause/1).
|
||||||
:- discontiguous(user:myclause/2).
|
:- discontiguous(user:myclause/2).
|
||||||
:- discontiguous(user:known/3).
|
:- discontiguous(user:known/3).
|
||||||
|
|||||||
Reference in New Issue
Block a user