Merge branch 'master' of ssh://git.dcc.fc.up.pt/yap-6.3
This commit is contained in:
commit
524edecdd3
12
C/absmi.c
12
C/absmi.c
@ -2252,7 +2252,7 @@ Yap_absmi(int inp)
|
||||
PREG = NEXTOP(NEXTOP(NEXTOP(PREG, s),Osbpp),l);
|
||||
/* assume cut is always in stack */
|
||||
saveregs();
|
||||
prune((choiceptr)YREG[E_CB]);
|
||||
prune((choiceptr)YREG[E_CB] PASS_REGS);
|
||||
setregs();
|
||||
GONext();
|
||||
ENDOp();
|
||||
@ -2271,7 +2271,7 @@ Yap_absmi(int inp)
|
||||
SET_ASP(YREG, PREG->u.s.s);
|
||||
/* assume cut is always in stack */
|
||||
saveregs();
|
||||
prune((choiceptr)YREG[E_CB]);
|
||||
prune((choiceptr)YREG[E_CB] PASS_REGS);
|
||||
setregs();
|
||||
PREG = NEXTOP(NEXTOP(NEXTOP(PREG, s),Osbpp),l);
|
||||
GONext();
|
||||
@ -2290,7 +2290,7 @@ Yap_absmi(int inp)
|
||||
SET_ASP(YREG, PREG->u.s.s);
|
||||
PREG = NEXTOP(NEXTOP(NEXTOP(PREG, s),Osbpp),l);
|
||||
saveregs();
|
||||
prune((choiceptr)SREG[E_CB]);
|
||||
prune((choiceptr)SREG[E_CB] PASS_REGS);
|
||||
setregs();
|
||||
GONext();
|
||||
ENDOp();
|
||||
@ -2343,7 +2343,7 @@ Yap_absmi(int inp)
|
||||
pt0 = (choiceptr)(LCL0-IntegerOfTerm(d0));
|
||||
#endif /* YAPOR_SBA && FROZEN_STACKS */
|
||||
saveregs();
|
||||
prune(pt0);
|
||||
prune(pt0 PASS_REGS);
|
||||
setregs();
|
||||
}
|
||||
GONext();
|
||||
@ -2379,7 +2379,7 @@ Yap_absmi(int inp)
|
||||
pt0 = (choiceptr)(LCL0-IntegerOfTerm(d0));
|
||||
#endif
|
||||
saveregs();
|
||||
prune(pt0);
|
||||
prune(pt0 PASS_REGS);
|
||||
setregs();
|
||||
}
|
||||
GONext();
|
||||
@ -13080,7 +13080,7 @@ Yap_absmi(int inp)
|
||||
if (pen->FunctorOfPred == (Functor)AtomCut) {
|
||||
if (b_ptr != B) {
|
||||
saveregs();
|
||||
prune(b_ptr);
|
||||
prune(b_ptr PASS_REGS);
|
||||
setregs();
|
||||
}
|
||||
}
|
||||
|
52
C/alloc.c
52
C/alloc.c
@ -245,23 +245,24 @@ Yap_FreeAtomSpace(char *p)
|
||||
/* If you need to dinamically allocate space from the heap, this is
|
||||
* the macro you should use */
|
||||
ADDR
|
||||
Yap_InitPreAllocCodeSpace(void)
|
||||
Yap_InitPreAllocCodeSpace(int wid)
|
||||
{
|
||||
CACHE_REGS
|
||||
char *ptr;
|
||||
UInt sz = LOCAL_ScratchPad.msz;
|
||||
if (LOCAL_ScratchPad.ptr == NULL) {
|
||||
UInt sz = REMOTE_ScratchPad(wid).msz;
|
||||
|
||||
if (REMOTE_ScratchPad(wid).ptr == NULL) {
|
||||
#if USE_DL_MALLOC
|
||||
LOCK(DLMallocLock);
|
||||
#endif
|
||||
LOCAL_PrologMode |= MallocMode;
|
||||
REMOTE_PrologMode(wid) |= MallocMode;
|
||||
#if INSTRUMENT_MALLOC
|
||||
mallocs++;
|
||||
tmalloc += sz;
|
||||
sz += sizeof(CELL);
|
||||
#endif
|
||||
while (!(ptr = my_malloc(sz))) {
|
||||
LOCAL_PrologMode &= ~MallocMode;
|
||||
REMOTE_PrologMode(wid) &= ~MallocMode;
|
||||
#if USE_DL_MALLOC
|
||||
UNLOCK(DLMallocLock);
|
||||
#endif
|
||||
@ -277,18 +278,18 @@ Yap_InitPreAllocCodeSpace(void)
|
||||
#if USE_DL_MALLOC
|
||||
LOCK(DLMallocLock);
|
||||
#endif
|
||||
LOCAL_PrologMode |= MallocMode;
|
||||
REMOTE_PrologMode(wid) |= MallocMode;
|
||||
}
|
||||
LOCAL_PrologMode &= ~MallocMode;
|
||||
REMOTE_PrologMode(wid) &= ~MallocMode;
|
||||
#if USE_DL_MALLOC
|
||||
UNLOCK(DLMallocLock);
|
||||
#endif
|
||||
LOCAL_ScratchPad.ptr = ptr;
|
||||
REMOTE_ScratchPad(wid).ptr = ptr;
|
||||
} else {
|
||||
ptr = LOCAL_ScratchPad.ptr;
|
||||
ptr = REMOTE_ScratchPad(wid).ptr;
|
||||
}
|
||||
AuxBase = (ADDR)(ptr);
|
||||
AuxSp = (CELL *)(AuxTop = AuxBase+LOCAL_ScratchPad.sz);
|
||||
AuxSp = (CELL *)(AuxTop = AuxBase+REMOTE_ScratchPad(wid).sz);
|
||||
return ptr;
|
||||
}
|
||||
|
||||
@ -352,7 +353,7 @@ Yap_InitHeap(void *heap_addr)
|
||||
}
|
||||
|
||||
static void
|
||||
InitExStacks(int Trail, int Stack)
|
||||
InitExStacks(int wid, int Trail, int Stack)
|
||||
{
|
||||
CACHE_REGS
|
||||
UInt pm, sa;
|
||||
@ -367,23 +368,24 @@ InitExStacks(int Trail, int Stack)
|
||||
sa = Stack*K; /* stack area size */
|
||||
|
||||
#ifdef THREADS
|
||||
if (worker_id)
|
||||
LOCAL_GlobalBase = (ADDR)LOCAL_ThreadHandle.stack_address;
|
||||
if (wid)
|
||||
REMOTE_GlobalBase(wid) = (ADDR)REMOTE_ThreadHandle(wid).stack_address;
|
||||
else
|
||||
AuxSp = NULL;
|
||||
#endif
|
||||
LOCAL_TrailTop = LOCAL_GlobalBase + pm;
|
||||
LOCAL_LocalBase = LOCAL_GlobalBase + sa;
|
||||
LOCAL_TrailBase = LOCAL_LocalBase + sizeof(CELL);
|
||||
REMOTE_TrailTop(wid) = REMOTE_GlobalBase(wid) + pm;
|
||||
REMOTE_LocalBase(wid) = REMOTE_GlobalBase(wid) + sa;
|
||||
REMOTE_TrailBase(wid) = REMOTE_LocalBase(wid) + sizeof(CELL);
|
||||
|
||||
LOCAL_ScratchPad.ptr = NULL;
|
||||
LOCAL_ScratchPad.sz = LOCAL_ScratchPad.msz = SCRATCH_START_SIZE;
|
||||
AuxSp = NULL;
|
||||
REMOTE_ScratchPad(wid).ptr = NULL;
|
||||
REMOTE_ScratchPad(wid).sz = REMOTE_ScratchPad(wid).msz = SCRATCH_START_SIZE;
|
||||
|
||||
#ifdef DEBUG
|
||||
if (Yap_output_msg) {
|
||||
UInt ta;
|
||||
|
||||
fprintf(stderr, "HeapBase = %p GlobalBase = %p\n LocalBase = %p TrailTop = %p\n",
|
||||
Yap_HeapBase, LOCAL_GlobalBase, LOCAL_LocalBase, LOCAL_TrailTop);
|
||||
Yap_HeapBase, REMOTE_GlobalBase(wid), REMOTE_LocalBase(wid), REMOTE_TrailTop(wid));
|
||||
|
||||
ta = Trail*K; /* trail area size */
|
||||
fprintf(stderr, "Heap+Aux: %lu\tLocal+Global: %lu\tTrail: %lu\n",
|
||||
@ -393,9 +395,9 @@ InitExStacks(int Trail, int Stack)
|
||||
}
|
||||
|
||||
void
|
||||
Yap_InitExStacks(int Trail, int Stack)
|
||||
Yap_InitExStacks(int wid, int Trail, int Stack)
|
||||
{
|
||||
InitExStacks(Trail, Stack);
|
||||
InitExStacks(wid, Trail, Stack);
|
||||
}
|
||||
|
||||
#if defined(THREADS)
|
||||
@ -1557,11 +1559,11 @@ Yap_InitMemory(UInt Trail, UInt Heap, UInt Stack)
|
||||
}
|
||||
|
||||
void
|
||||
Yap_InitExStacks(int Trail, int Stack)
|
||||
Yap_InitExStacks(int wid, int Trail, int Stack)
|
||||
{
|
||||
#if USE_DL_MALLOC
|
||||
LOCAL_ScratchPad.ptr = NULL;
|
||||
LOCAL_ScratchPad.sz = LOCAL_ScratchPad.msz = SCRATCH_START_SIZE;
|
||||
REMOTE_ScratchPad(wid).ptr = NULL;
|
||||
REMOTE_ScratchPad(wid).sz = REMOTE_ScratchPad(wid).msz = SCRATCH_START_SIZE;
|
||||
AuxSp = NULL;
|
||||
#endif
|
||||
}
|
||||
|
@ -2699,12 +2699,12 @@ X_API void
|
||||
YAP_ClearExceptions(void)
|
||||
{
|
||||
CACHE_REGS
|
||||
Yap_ResetExceptionTerm();
|
||||
|
||||
if (EX) {
|
||||
LOCAL_BallTerm = EX;
|
||||
}
|
||||
EX = NULL;
|
||||
Yap_ResetExceptionTerm();
|
||||
Yap_ResetExceptionTerm( 0 );
|
||||
LOCAL_UncaughtThrow = FALSE;
|
||||
}
|
||||
|
||||
@ -3065,13 +3065,13 @@ YAP_Init(YAP_init_args *yap_init)
|
||||
GLOBAL_AllowGlobalExpansion = TRUE;
|
||||
GLOBAL_AllowLocalExpansion = TRUE;
|
||||
GLOBAL_AllowTrailExpansion = TRUE;
|
||||
Yap_InitExStacks (Trail, Stack);
|
||||
Yap_InitExStacks (0, Trail, Stack);
|
||||
if (yap_init->QuietMode) {
|
||||
yap_flags[QUIET_MODE_FLAG] = TRUE;
|
||||
}
|
||||
|
||||
{ BACKUP_MACHINE_REGS();
|
||||
Yap_InitYaamRegs( 0);
|
||||
Yap_InitYaamRegs( 0 );
|
||||
|
||||
#if HAVE_MPE
|
||||
Yap_InitMPE ();
|
||||
@ -3111,10 +3111,10 @@ YAP_Init(YAP_init_args *yap_init)
|
||||
In the SBA we cannot just happily inherit registers
|
||||
from the other workers
|
||||
*/
|
||||
Yap_InitYaamRegs( 0);
|
||||
Yap_InitYaamRegs( 0 );
|
||||
#endif /* YAPOR_COPY || YAPOR_SBA */
|
||||
#ifndef YAPOR_THREADS
|
||||
Yap_InitPreAllocCodeSpace();
|
||||
Yap_InitPreAllocCodeSpace( 0 );
|
||||
#endif /* YAPOR_THREADS */
|
||||
/* slaves, waiting for work */
|
||||
CurrentModule = USER_MODULE;
|
||||
|
@ -4,9 +4,9 @@
|
||||
#include "cut_c.h"
|
||||
#include <stdio.h>
|
||||
|
||||
void cut_c_initialize(void){
|
||||
void cut_c_initialize(int wid){
|
||||
CACHE_REGS
|
||||
Yap_REGS.CUT_C_TOP=(cut_c_str_ptr)LOCAL_LocalBase;
|
||||
Yap_REGS.CUT_C_TOP=(cut_c_str_ptr)REMOTE_LocalBase(wid);
|
||||
}
|
||||
|
||||
/*Removes a choice_point from the stack*/
|
||||
|
63
C/exec.c
63
C/exec.c
@ -1723,25 +1723,22 @@ Yap_InitYaamRegs( int myworker_id )
|
||||
machine registers */
|
||||
#ifdef THREADS
|
||||
CACHE_REGS
|
||||
int wid = worker_id;
|
||||
if (wid != myworker_id) {
|
||||
if (myworker_id) {
|
||||
pthread_setspecific(Yap_yaamregs_key, (const void *)REMOTE_ThreadHandle(myworker_id).default_yaam_regs);
|
||||
REFRESH_CACHE_REGS
|
||||
REMOTE_ThreadHandle(myworker_id).current_yaam_regs = REMOTE_ThreadHandle(myworker_id).default_yaam_regs;
|
||||
worker_id = myworker_id;
|
||||
REFRESH_CACHE_REGS
|
||||
}
|
||||
/* may be run by worker_id on behalf on myworker_id */
|
||||
#else
|
||||
Yap_regp = &Yap_standard_regs;
|
||||
#endif
|
||||
#endif /* PUSH_REGS */
|
||||
Yap_ResetExceptionTerm ();
|
||||
Yap_ResetExceptionTerm ( myworker_id );
|
||||
Yap_PutValue (AtomBreak, MkIntTerm (0));
|
||||
TR = (tr_fr_ptr)LOCAL_TrailBase;
|
||||
H = H0 = ((CELL *) REMOTE_GlobalBase(wid));
|
||||
RESET_VARIABLE(H0-1);
|
||||
LCL0 = ASP = (CELL *) REMOTE_LocalBase(wid);
|
||||
CurrentTrailTop = (tr_fr_ptr)(REMOTE_TrailTop(wid)-MinTrailGap);
|
||||
TR = (tr_fr_ptr)REMOTE_TrailBase(myworker_id);
|
||||
H = H0 = ((CELL *) REMOTE_GlobalBase(myworker_id));
|
||||
LCL0 = ASP = (CELL *) REMOTE_LocalBase(myworker_id);
|
||||
CurrentTrailTop = (tr_fr_ptr)(REMOTE_TrailTop(myworker_id)-MinTrailGap);
|
||||
/* notice that an initial choice-point and environment
|
||||
*must* be created since for the garbage collector to work */
|
||||
B = NULL;
|
||||
@ -1756,49 +1753,46 @@ Yap_InitYaamRegs( int myworker_id )
|
||||
#ifdef YAPOR_SBA
|
||||
BSEG =
|
||||
#endif /* YAPOR_SBA */
|
||||
BBREG = B_FZ = (choiceptr) REMOTE_LocalBase(wid);
|
||||
TR = TR_FZ = (tr_fr_ptr) REMOTE_TrailBase(wid);
|
||||
BBREG = B_FZ = (choiceptr) REMOTE_LocalBase(myworker_id);
|
||||
TR = TR_FZ = (tr_fr_ptr) REMOTE_TrailBase(myworker_id);
|
||||
#endif /* FROZEN_STACKS */
|
||||
LOCK(REMOTE_SignalLock(wid));
|
||||
LOCK(REMOTE_SignalLock(myworker_id));
|
||||
CreepFlag = CalculateStackGap();
|
||||
UNLOCK(REMOTE_SignalLock(wid));
|
||||
UNLOCK(REMOTE_SignalLock(myworker_id));
|
||||
EX = NULL;
|
||||
init_stack(0, NULL, TRUE, NULL PASS_REGS);
|
||||
/* the first real choice-point will also have AP=FAIL */
|
||||
/* always have an empty slots for people to use */
|
||||
CurSlot = 0;
|
||||
Yap_StartSlots( PASS_REGS1 );
|
||||
REMOTE_GlobalArena(wid) = TermNil;
|
||||
REMOTE_GlobalArena(myworker_id) = TermNil;
|
||||
h0var = MkVarTerm();
|
||||
#ifdef THREADS
|
||||
LOCAL = REMOTE(myworker_id);
|
||||
#endif /* THREADS */
|
||||
#if COROUTINING
|
||||
REMOTE_WokenGoals(wid) = Yap_NewTimedVar(TermNil);
|
||||
REMOTE_AttsMutableList(wid) = Yap_NewTimedVar(h0var);
|
||||
REMOTE_WokenGoals(myworker_id) = Yap_NewTimedVar(TermNil);
|
||||
REMOTE_AttsMutableList(myworker_id) = Yap_NewTimedVar(h0var);
|
||||
#endif
|
||||
REMOTE_GcGeneration(wid) = Yap_NewTimedVar(h0var);
|
||||
REMOTE_GcCurrentPhase(wid) = 0L;
|
||||
REMOTE_GcPhase(wid) = Yap_NewTimedVar(MkIntTerm(REMOTE_GcCurrentPhase(wid)));
|
||||
REMOTE_GcGeneration(myworker_id) = Yap_NewTimedVar(h0var);
|
||||
REMOTE_GcCurrentPhase(myworker_id) = 0L;
|
||||
REMOTE_GcPhase(myworker_id) = Yap_NewTimedVar(MkIntTerm(REMOTE_GcCurrentPhase(myworker_id)));
|
||||
#if defined(YAPOR) || defined(THREADS)
|
||||
PP = NULL;
|
||||
PREG_ADDR = NULL;
|
||||
#endif
|
||||
Yap_AllocateDefaultArena(128*1024, 2);
|
||||
Yap_InitPreAllocCodeSpace();
|
||||
Yap_AllocateDefaultArena(128*1024, 2, myworker_id);
|
||||
Yap_InitPreAllocCodeSpace( myworker_id );
|
||||
#ifdef CUT_C
|
||||
cut_c_initialize();
|
||||
cut_c_initialize( myworker_id );
|
||||
#endif
|
||||
#if defined MYDDAS_MYSQL || defined MYDDAS_ODBC
|
||||
Yap_REGS.MYDDAS_GLOBAL_POINTER = NULL;
|
||||
#endif
|
||||
#ifdef TABLING
|
||||
/* ensure that LOCAL_top_dep_fr is always valid */
|
||||
if (REMOTE_top_dep_fr(wid))
|
||||
DepFr_cons_cp(REMOTE_top_dep_fr(wid)) = NORM_CP(B);
|
||||
#endif
|
||||
#ifdef THREADS
|
||||
worker_id = wid;
|
||||
if (myworker_id != worker_id) {
|
||||
pthread_setspecific(Yap_yaamregs_key, (const void *)REMOTE_ThreadHandle(worker_id).default_yaam_regs);
|
||||
}
|
||||
if (REMOTE_top_dep_fr(myworker_id))
|
||||
DepFr_cons_cp(REMOTE_top_dep_fr(myworker_id)) = NORM_CP(B);
|
||||
#endif
|
||||
}
|
||||
|
||||
@ -1886,11 +1880,10 @@ p_reset_exception( USES_REGS1 )
|
||||
}
|
||||
|
||||
void
|
||||
Yap_ResetExceptionTerm(void)
|
||||
Yap_ResetExceptionTerm(int wid)
|
||||
{
|
||||
CACHE_REGS
|
||||
Yap_ReleaseTermFromDB(LOCAL_BallTerm);
|
||||
LOCAL_BallTerm = NULL;
|
||||
Yap_ReleaseTermFromDB(REMOTE_BallTerm(wid));
|
||||
REMOTE_BallTerm(wid) = NULL;
|
||||
}
|
||||
|
||||
static Int
|
||||
|
@ -151,10 +151,10 @@ p_default_arena_size( USES_REGS1 )
|
||||
|
||||
|
||||
void
|
||||
Yap_AllocateDefaultArena(Int gsize, Int attsize)
|
||||
Yap_AllocateDefaultArena(Int gsize, Int attsize, int wid)
|
||||
{
|
||||
CACHE_REGS
|
||||
LOCAL_GlobalArena = NewArena(gsize, 2, NULL PASS_REGS);
|
||||
REMOTE_GlobalArena(wid) = NewArena(gsize, 2, NULL PASS_REGS);
|
||||
}
|
||||
|
||||
static void
|
||||
|
2
C/save.c
2
C/save.c
@ -1794,7 +1794,7 @@ Restore(char *s, char *lib_dir USES_REGS)
|
||||
Yap_InitSysPath();
|
||||
#if USE_DL_MALLOC || USE_SYSTEM_MALLOC
|
||||
if (!AuxSp) {
|
||||
Yap_InitPreAllocCodeSpace();
|
||||
Yap_InitPreAllocCodeSpace( 0 );
|
||||
}
|
||||
#endif
|
||||
CloseRestore();
|
||||
|
31
C/threads.c
31
C/threads.c
@ -230,15 +230,11 @@ setup_engine(int myworker_id, int init_thread)
|
||||
regcache = standard_regs;
|
||||
/* create the YAAM descriptor */
|
||||
REMOTE_ThreadHandle(myworker_id).default_yaam_regs = standard_regs;
|
||||
if (init_thread) {
|
||||
pthread_setspecific(Yap_yaamregs_key, (void *)REMOTE_ThreadHandle(myworker_id).default_yaam_regs);
|
||||
}
|
||||
worker_id = myworker_id;
|
||||
LOCAL = REMOTE(worker_id);
|
||||
Yap_InitExStacks(REMOTE_ThreadHandle(myworker_id).tsize, REMOTE_ThreadHandle(myworker_id).ssize);
|
||||
Yap_InitExStacks(myworker_id, REMOTE_ThreadHandle(myworker_id).tsize, REMOTE_ThreadHandle(myworker_id).ssize);
|
||||
CurrentModule = REMOTE_ThreadHandle(myworker_id).cmod;
|
||||
Yap_InitTime( myworker_id );
|
||||
Yap_InitYaamRegs( myworker_id );
|
||||
REFRESH_CACHE_REGS
|
||||
Yap_ReleasePreAllocCodeSpace(Yap_PreAllocCodeSpace());
|
||||
/* I exist */
|
||||
GLOBAL_NOfThreadsCreated++;
|
||||
@ -254,7 +250,11 @@ setup_engine(int myworker_id, int init_thread)
|
||||
static void
|
||||
start_thread(int myworker_id)
|
||||
{
|
||||
setup_engine(myworker_id, TRUE);
|
||||
CACHE_REGS
|
||||
pthread_setspecific(Yap_yaamregs_key, (void *)REMOTE_ThreadHandle(myworker_id).default_yaam_regs);
|
||||
REFRESH_CACHE_REGS;
|
||||
worker_id = myworker_id;
|
||||
LOCAL = REMOTE(myworker_id);
|
||||
}
|
||||
|
||||
static void *
|
||||
@ -267,13 +267,14 @@ thread_run(void *widp)
|
||||
#ifdef OUTPUT_THREADS_TABLING
|
||||
char thread_name[25];
|
||||
char filename[YAP_FILENAME_MAX];
|
||||
|
||||
sprintf(thread_name, "/thread_output_%d", myworker_id);
|
||||
strcpy(filename, YAP_BINDIR);
|
||||
strncat(filename, thread_name, 25);
|
||||
LOCAL_thread_output = fopen(filename, "w");
|
||||
REMOTE_thread_output(myworker_id) = fopen(filename, "w");
|
||||
#endif /* OUTPUT_THREADS_TABLING */
|
||||
start_thread(myworker_id);
|
||||
regcache = ((REGSTORE *)pthread_getspecific(Yap_yaamregs_key));
|
||||
REFRESH_CACHE_REGS;
|
||||
do {
|
||||
t = tgs[0] = Yap_PopTermFromDB(LOCAL_ThreadHandle.tgoal);
|
||||
if (t == 0) {
|
||||
@ -328,7 +329,8 @@ p_create_thread( USES_REGS1 )
|
||||
Term x2 = Deref(ARG2);
|
||||
Term x3 = Deref(ARG3);
|
||||
Term x4 = Deref(ARG4);
|
||||
int new_worker_id = IntegerOfTerm(Deref(ARG7));
|
||||
int new_worker_id = IntegerOfTerm(Deref(ARG7)),
|
||||
owid = worker_id;
|
||||
|
||||
// fprintf(stderr," %d --> %d\n", worker_id, new_worker_id);
|
||||
if (IsBigIntTerm(x2))
|
||||
@ -349,10 +351,13 @@ p_create_thread( USES_REGS1 )
|
||||
//REMOTE_ThreadHandle(new_worker_id).pthread_handle = 0L;
|
||||
REMOTE_ThreadHandle(new_worker_id).id = new_worker_id;
|
||||
REMOTE_ThreadHandle(new_worker_id).ref_count = 1;
|
||||
setup_engine(new_worker_id, FALSE);
|
||||
if ((REMOTE_ThreadHandle(new_worker_id).ret = pthread_create(&REMOTE_ThreadHandle(new_worker_id).pthread_handle, NULL, thread_run, (void *)(&(REMOTE_ThreadHandle(new_worker_id).id)))) == 0) {
|
||||
pthread_setspecific(Yap_yaamregs_key, (const void *)REMOTE_ThreadHandle(owid).current_yaam_regs);
|
||||
/* wait until the client is initialised */
|
||||
return TRUE;
|
||||
}
|
||||
pthread_setspecific(Yap_yaamregs_key, (const void *)REMOTE_ThreadHandle(owid).current_yaam_regs);
|
||||
return FALSE;
|
||||
}
|
||||
|
||||
@ -493,6 +498,7 @@ Yap_thread_create_engine(thread_attr *ops)
|
||||
Int
|
||||
Yap_thread_attach_engine(int wid)
|
||||
{
|
||||
CACHE_REGS
|
||||
/*
|
||||
already locked
|
||||
pthread_mutex_lock(&(REMOTE_ThreadHandle(wid).tlock));
|
||||
@ -506,9 +512,8 @@ Yap_thread_attach_engine(int wid)
|
||||
}
|
||||
REMOTE_ThreadHandle(wid).pthread_handle = pthread_self();
|
||||
REMOTE_ThreadHandle(wid).ref_count++;
|
||||
pthread_setspecific(Yap_yaamregs_key, (const void *)REMOTE_ThreadHandle(wid).default_yaam_regs);
|
||||
CACHE_REGS
|
||||
worker_id = wid; /* ricroc: for what I understand, this shouldn't be necessary */
|
||||
pthread_setspecific(Yap_yaamregs_key, (const void *)REMOTE_ThreadHandle(wid).current_yaam_regs);
|
||||
REFRESH_CACHE_REGS;
|
||||
DEBUG_TLOCK_ACCESS(9, wid);
|
||||
pthread_mutex_unlock(&(REMOTE_ThreadHandle(wid).tlock));
|
||||
return TRUE;
|
||||
|
@ -4694,7 +4694,7 @@ static Int numbervars_in_complex_term(register CELL *pt0, register CELL *pt0_end
|
||||
goto loop;
|
||||
}
|
||||
|
||||
prune(B);
|
||||
prune(B PASS_REGS);
|
||||
Yap_ReleasePreAllocCodeSpace((ADDR)to_visit0);
|
||||
return numbv;
|
||||
|
||||
|
@ -220,7 +220,7 @@ UInt STD_PROTO(Yap_givemallinfo, (void));
|
||||
|
||||
ADDR STD_PROTO(Yap_ExpandPreAllocCodeSpace, (UInt, void *, int));
|
||||
#define Yap_ReleasePreAllocCodeSpace(x)
|
||||
ADDR STD_PROTO(Yap_InitPreAllocCodeSpace, (void));
|
||||
ADDR STD_PROTO(Yap_InitPreAllocCodeSpace, (int));
|
||||
|
||||
#include "inline-only.h"
|
||||
INLINE_ONLY EXTERN inline ADDR
|
||||
|
@ -91,7 +91,7 @@ int STD_PROTO(Yap_ExtendWorkSpace,(Int));
|
||||
void STD_PROTO(Yap_FreeAtomSpace,(char *));
|
||||
int STD_PROTO(Yap_FreeWorkSpace, (void));
|
||||
void STD_PROTO(Yap_InitMemory,(UInt,UInt,UInt));
|
||||
void STD_PROTO(Yap_InitExStacks,(int,int));
|
||||
void STD_PROTO(Yap_InitExStacks,(int,int,int));
|
||||
|
||||
/* amasm.c */
|
||||
OPCODE STD_PROTO(Yap_opcode,(op_numbers));
|
||||
@ -177,7 +177,7 @@ Term STD_PROTO(Yap_ExecuteCallMetaCall,(Term));
|
||||
void STD_PROTO(Yap_InitExecFs,(void));
|
||||
Int STD_PROTO(Yap_JumpToEnv,(Term));
|
||||
Term STD_PROTO(Yap_RunTopGoal,(Term));
|
||||
void STD_PROTO(Yap_ResetExceptionTerm,(void));
|
||||
void STD_PROTO(Yap_ResetExceptionTerm,(int));
|
||||
Int STD_PROTO(Yap_execute_goal,(Term, int, Term));
|
||||
Int STD_PROTO(Yap_exec_absmi,(int));
|
||||
void STD_PROTO(Yap_trust_last,(void));
|
||||
@ -200,7 +200,7 @@ void STD_PROTO(Yap_InitGlobals,(void));
|
||||
Term STD_PROTO(Yap_SaveTerm, (Term));
|
||||
Term STD_PROTO(Yap_SetGlobalVal, (Atom, Term));
|
||||
Int STD_PROTO(Yap_DeleteGlobal, (Atom));
|
||||
void STD_PROTO(Yap_AllocateDefaultArena, (Int, Int));
|
||||
void STD_PROTO(Yap_AllocateDefaultArena, (Int, Int, int));
|
||||
|
||||
/* grow.c */
|
||||
Int STD_PROTO(Yap_total_stack_shift_time,(void));
|
||||
|
@ -1546,9 +1546,8 @@ Yap_regtoregno(wamreg reg)
|
||||
#endif
|
||||
|
||||
static inline void
|
||||
prune(choiceptr cp)
|
||||
prune(choiceptr cp USES_REGS)
|
||||
{
|
||||
CACHE_REGS
|
||||
#ifdef YAPOR
|
||||
CUT_prune_to(cp);
|
||||
#endif /* YAPOR */
|
||||
|
@ -46,7 +46,7 @@ struct cut_c_str{
|
||||
|
||||
|
||||
/*Initializes CUT_C_TOP*/
|
||||
void cut_c_initialize(void);
|
||||
void cut_c_initialize(int wid );
|
||||
|
||||
/*Removes a choice_point from the stack*/
|
||||
void cut_c_pop(void);
|
||||
|
@ -78,7 +78,7 @@ CLPBN_SCHOOL_EXAMPLES= \
|
||||
$(CLPBN_EXDIR)/School/README \
|
||||
$(CLPBN_EXDIR)/School/evidence_128.yap \
|
||||
$(CLPBN_EXDIR)/School/schema.yap \
|
||||
$(CLPBN_EXDIR)/School/parschema.yap \
|
||||
$(CLPBN_EXDIR)/School/parschema.pfl \
|
||||
$(CLPBN_EXDIR)/School/school_128.yap \
|
||||
$(CLPBN_EXDIR)/School/school_32.yap \
|
||||
$(CLPBN_EXDIR)/School/sch32.yap \
|
||||
@ -96,8 +96,9 @@ CLPBN_HMMER_EXAMPLES= \
|
||||
$(CLPBN_EXDIR)/HMMer/score.yap
|
||||
|
||||
CLPBN_LEARNING_EXAMPLES= \
|
||||
$(CLPBN_EXDIR)/learning/debug_school.yap \
|
||||
$(CLPBN_EXDIR)/learning/prof_params.pfl \
|
||||
$(CLPBN_EXDIR)/learning/school_params.pfl \
|
||||
$(CLPBN_EXDIR)/learning/school_params.yap \
|
||||
$(CLPBN_EXDIR)/learning/sprinkler_params.yap \
|
||||
$(CLPBN_EXDIR)/learning/train.yap
|
||||
|
||||
@ -106,13 +107,12 @@ CLPBN_EXAMPLES= \
|
||||
$(CLPBN_EXDIR)/burglary-alarm.pfl \
|
||||
$(CLPBN_EXDIR)/burglary-alarm.uai \
|
||||
$(CLPBN_EXDIR)/cg.yap \
|
||||
$(CLPBN_EXDIR)/city.yap \
|
||||
$(CLPBN_EXDIR)/comp_workshops.yap \
|
||||
$(CLPBN_EXDIR)/social_domain1.yap \
|
||||
$(CLPBN_EXDIR)/social_domain2.yap \
|
||||
$(CLPBN_EXDIR)/city.pfl \
|
||||
$(CLPBN_EXDIR)/comp_workshops.pfl \
|
||||
$(CLPBN_EXDIR)/social_domain1.pfl \
|
||||
$(CLPBN_EXDIR)/social_domain2.pfl \
|
||||
$(CLPBN_EXDIR)/sprinkler.pfl \
|
||||
$(CLPBN_EXDIR)/sprinkler.yap \
|
||||
$(CLPBN_EXDIR)/workshop_attrs.yap
|
||||
$(CLPBN_EXDIR)/workshop_attrs.pfl
|
||||
|
||||
|
||||
install: $(CLBN_TOP) $(CLBN_PROGRAMS) $(CLPBN_PROGRAMS)
|
||||
|
@ -109,7 +109,7 @@ collect(Keys, Factors) :-
|
||||
queue_in(K) :-
|
||||
queue(K), !.
|
||||
queue_in(K) :-
|
||||
%writeln(+K),
|
||||
% writeln(q+K),
|
||||
assert(queue(K)),
|
||||
fail.
|
||||
queue_in(_).
|
||||
@ -139,7 +139,7 @@ do_propagate(_K) :-
|
||||
propagate.
|
||||
|
||||
add_factor(factor(Type, Id, Ks, _, _Phi, Constraints), NKs) :-
|
||||
%writeln(+Ks),
|
||||
% writeln(+Ks),
|
||||
( Ks = [K,Els], var(Els)
|
||||
->
|
||||
% aggregate factor
|
||||
@ -147,7 +147,7 @@ add_factor(factor(Type, Id, Ks, _, _Phi, Constraints), NKs) :-
|
||||
avg_factors(K, Els, 0.0, NewKeys, NewId),
|
||||
NKs = [K|NewKeys]
|
||||
;
|
||||
once(run(Constraints)),
|
||||
run(Constraints),
|
||||
NKs = Ks,
|
||||
Id = NewId
|
||||
),
|
||||
|
@ -31,24 +31,16 @@
|
||||
get_dist_params/2
|
||||
]).
|
||||
|
||||
:- use_module(library('clpbn/ground_factors'),
|
||||
[generate_network/5
|
||||
]).
|
||||
|
||||
:- use_module(library('clpbn/display'),
|
||||
[clpbn_bind_vals/3]).
|
||||
|
||||
:- use_module(library('clpbn/aggregates'),
|
||||
[check_for_agg_vars/2]).
|
||||
|
||||
:- use_module(library(clpbn/numbers)).
|
||||
|
||||
:- use_module(library(charsio),
|
||||
[term_to_atom/2]).
|
||||
|
||||
:- use_module(library(pfl),
|
||||
[skolem/2
|
||||
]).
|
||||
[skolem/2]).
|
||||
|
||||
:- use_module(library(maplist)).
|
||||
|
||||
@ -60,32 +52,38 @@
|
||||
|
||||
|
||||
call_horus_ground_solver(QueryVars, QueryKeys, AllKeys, Factors, Evidence, Output) :-
|
||||
call_horus_ground_solver_for_probabilities([QueryKeys], AllKeys, Factors, Evidence, Solutions),
|
||||
clpbn_bind_vals([QueryVars], Solutions, Output).
|
||||
|
||||
call_horus_ground_solver_for_probabilities(QueryKeys, AllKeys, Factors, Evidence, Solutions) :-
|
||||
get_factors_type(Factors, Type),
|
||||
keys_to_numbers(AllKeys, Factors, Evidence, Hash4, Id4, FactorIds, EvidenceIds),
|
||||
%writeln(evidence:Evidence), writeln(''),
|
||||
%writeln(evidenceIds:EvidenceIds), writeln(''),
|
||||
%writeln(factorIds:FactorIds), writeln(''),
|
||||
cpp_create_ground_network(Type, FactorIds, EvidenceIds, Network),
|
||||
maplist(get_var_information, AllKeys, StatesNames),
|
||||
maplist(term_to_atom, AllKeys, KeysAtoms),
|
||||
%writeln(s1:KeysAtoms:KeysAtoms:StatesNames),
|
||||
cpp_set_vars_information(KeysAtoms, StatesNames),
|
||||
%writeln(network:(Type, FactorIds, EvidenceIds, Network)), writeln(''),
|
||||
run_solver(ground(Network,Hash4,Id4), QueryKeys, Solutions),
|
||||
cpp_free_ground_network(Network).
|
||||
init_horus_ground_solver(QueryKeys, AllKeys, Factors, Evidence, State),
|
||||
run_solver(State, [QueryKeys], Solutions),
|
||||
clpbn_bind_vals([QueryVars], Solutions, Output),
|
||||
finalize_horus_ground_solver(State).
|
||||
|
||||
|
||||
run_solver(ground(Network,Hash,Id), QueryKeys, Solutions) :-
|
||||
%get_dists_parameters(DistIds, DistsParams),
|
||||
%cpp_set_factors_params(Network, DistsParams),
|
||||
lists_of_keys_to_ids(QueryKeys, QueryIds, Hash, _, Id, _),
|
||||
%writeln(queryKeys:QueryKeys), writeln(''),
|
||||
% writeln(queryIds:QueryIds), writeln(''),
|
||||
cpp_run_ground_solver(Network, QueryIds, Solutions).
|
||||
init_horus_ground_solver(QueryKeys, AllKeys, Factors, Evidence, state(Network,Hash4,Id4)) :-
|
||||
get_factors_type(Factors, Type),
|
||||
keys_to_numbers(AllKeys, Factors, Evidence, Hash4, Id4, FactorIds, EvidenceIds),
|
||||
cpp_create_ground_network(Type, FactorIds, EvidenceIds, Network),
|
||||
%writeln(network:(Type, FactorIds, EvidenceIds, Network)), writeln(''),
|
||||
maplist(get_var_information, AllKeys, StatesNames),
|
||||
maplist(term_to_atom, AllKeys, KeysAtoms),
|
||||
cpp_set_vars_information(KeysAtoms, StatesNames).
|
||||
|
||||
|
||||
run_horus_ground_solver(_QueryVars, Solutions, horus(GKeys, Keys, Factors, Evidence), Solver) :-
|
||||
set_solver(Solver),
|
||||
call_horus_ground_solver_for_probabilities(GKeys, Keys, Factors, Evidence, Solutions).
|
||||
|
||||
|
||||
% TODO this is not beeing called!
|
||||
finalize_horus_ground_solver(state(Network,_Hash,_Id)) :-
|
||||
cpp_free_ground_network(Network).
|
||||
|
||||
|
||||
run_solver(state(Network,Hash,Id), QueryKeys, Solutions) :-
|
||||
%get_dists_parameters(DistIds, DistsParams),
|
||||
%cpp_set_factors_params(Network, DistsParams),
|
||||
lists_of_keys_to_ids(QueryKeys, QueryIds, Hash, _, Id, _),
|
||||
cpp_run_ground_solver(Network, QueryIds, Solutions).
|
||||
|
||||
|
||||
get_factors_type([f(bayes, _, _)|_], bayes) :- ! .
|
||||
get_factors_type([f(markov, _, _)|_], markov) :- ! .
|
||||
@ -97,47 +95,8 @@ get_var_information(Key, Domain) :-
|
||||
skolem(Key, Domain).
|
||||
|
||||
|
||||
finalize_horus_ground_solver(bp(Network, _)) :-
|
||||
cpp_free_ground_network(Network).
|
||||
finalize_horus_ground_solver(horus(_, _, _, _)).
|
||||
|
||||
%
|
||||
% QVars: all query variables?
|
||||
%
|
||||
%
|
||||
init_horus_ground_solver(QueryKeys, AllKeys, Factors, Evidence, horus(QueryKeys, AllKeys, Factors, Evidence)).
|
||||
|
||||
%
|
||||
% just call horus solver.
|
||||
%
|
||||
run_horus_ground_solver(_QueryVars, Solutions, horus(GKeys, Keys, Factors, Evidence) , Solver) :-
|
||||
set_solver(Solver),
|
||||
call_horus_ground_solver_for_probabilities(GKeys, Keys, Factors, Evidence, Solutions).
|
||||
|
||||
%bp([[]],_,_) :- !.
|
||||
%bp([QueryVars], AllVars, Output) :-
|
||||
% init_horus_ground_solver(_, AllVars, _, Network),
|
||||
% run_horus_ground_solver([QueryVars], LPs, Network),
|
||||
% finalize_horus_ground_solver(Network),
|
||||
% clpbn_bind_vals([QueryVars], LPs, Output).
|
||||
%
|
||||
%init_horus_ground_solver(_, AllVars0, _, bp(BayesNet, DistIds)) :-
|
||||
% %check_for_agg_vars(AllVars0, AllVars),
|
||||
% get_vars_info(AllVars0, VarsInfo, DistIds0),
|
||||
% sort(DistIds0, DistIds),
|
||||
% cpp_create_ground_network(VarsInfo, BayesNet),
|
||||
% true.
|
||||
%
|
||||
%
|
||||
%run_horus_ground_solver(QueryVars, Solutions, bp(Network, DistIds)) :-
|
||||
% get_dists_parameters(DistIds, DistsParams),
|
||||
% cpp_set_factors_params(Network, DistsParams),
|
||||
% vars_to_ids(QueryVars, QueryVarsIds),
|
||||
% cpp_run_ground_solver(Network, QueryVarsIds, Solutions).
|
||||
|
||||
|
||||
get_dists_parameters([],[]).
|
||||
get_dists_parameters([Id|Ids], [dist(Id, Params)|DistsInfo]) :-
|
||||
get_dist_params(Id, Params),
|
||||
get_dists_parameters(Ids, DistsInfo).
|
||||
%get_dists_parameters([],[]).
|
||||
%get_dists_parameters([Id|Ids], [dist(Id, Params)|DistsInfo]) :-
|
||||
% get_dist_params(Id, Params),
|
||||
% get_dists_parameters(Ids, DistsInfo).
|
||||
|
||||
|
@ -1,8 +1,10 @@
|
||||
/*******************************************************
|
||||
|
||||
Interface to Horus Lifted Solvers. Used by:
|
||||
- Lifted Variable Elimination
|
||||
- Generalized Counting First-Order Variable Elimination (GC-FOVE)
|
||||
- Lifted First-Order Belief Propagation
|
||||
- Lifted First-Order Knowledge Compilation
|
||||
|
||||
********************************************************/
|
||||
|
||||
:- module(clpbn_horus_lifted,
|
||||
@ -33,22 +35,33 @@
|
||||
]).
|
||||
|
||||
|
||||
call_horus_lifted_solver([[]], _, _) :- !.
|
||||
call_horus_lifted_solver([QueryVars], AllVars, Output) :-
|
||||
init_horus_lifted_solver(_, AllVars, _, ParfactorList),
|
||||
run_horus_lifted_solver([QueryVars], LPs, ParfactorList),
|
||||
finalize_horus_lifted_solver(ParfactorList),
|
||||
clpbn_bind_vals([QueryVars], LPs, Output).
|
||||
call_horus_lifted_solver(QueryVars, AllVars, Output) :-
|
||||
init_horus_lifted_solver(_, AllVars, _, State),
|
||||
run_horus_lifted_solver(QueryVars, Solutions, State),
|
||||
clpbn_bind_vals(QueryVars, Solutions, Output),
|
||||
finalize_horus_lifted_solver(State).
|
||||
|
||||
|
||||
init_horus_lifted_solver(_, AllAttVars, _, fove(ParfactorList, DistIds)) :-
|
||||
init_horus_lifted_solver(_, AllVars, _, state(ParfactorList, DistIds)) :-
|
||||
get_parfactors(Parfactors),
|
||||
get_dist_ids(Parfactors, DistIds0),
|
||||
sort(DistIds0, DistIds),
|
||||
get_observed_vars(AllAttVars, ObservedVars),
|
||||
get_observed_vars(AllVars, ObservedVars),
|
||||
%writeln(parfactors:Parfactors:'\n'),
|
||||
%writeln(evidence:ObservedVars:'\n'),
|
||||
cpp_create_lifted_network(Parfactors,ObservedVars,ParfactorList).
|
||||
cpp_create_lifted_network(Parfactors, ObservedVars, ParfactorList).
|
||||
|
||||
|
||||
run_horus_lifted_solver(QueryVars, Solutions, state(ParfactorList, DistIds)) :-
|
||||
get_query_keys(QueryVars, QueryKeys),
|
||||
get_dists_parameters(DistIds, DistsParams),
|
||||
%writeln(dists:DistsParams), writeln(''),
|
||||
cpp_set_parfactors_params(ParfactorList, DistsParams),
|
||||
cpp_run_lifted_solver(ParfactorList, QueryKeys, Solutions).
|
||||
|
||||
|
||||
finalize_horus_lifted_solver(state(ParfactorList, _)) :-
|
||||
cpp_free_lifted_network(ParfactorList).
|
||||
|
||||
|
||||
:- table get_parfactors/1.
|
||||
@ -76,7 +89,7 @@ is_factor(pf(Id, Ks, Rs, Phi, Tuples)) :-
|
||||
|
||||
|
||||
get_ranges([],[]).
|
||||
get_ranges(K.Ks, Range.Rs) :- !,
|
||||
get_ranges(K.Ks, Range.Rs) :- !,
|
||||
skolem(K,Domain),
|
||||
length(Domain,Range),
|
||||
get_ranges(Ks, Rs).
|
||||
@ -116,16 +129,16 @@ get_observed_vars(V.AllAttVars, ObservedVars) :-
|
||||
get_observed_vars(AllAttVars, ObservedVars).
|
||||
|
||||
|
||||
get_query_vars([], []).
|
||||
get_query_vars(E1.L1, E2.L2) :-
|
||||
get_query_vars_2(E1,E2),
|
||||
get_query_vars(L1, L2).
|
||||
get_query_keys([], []).
|
||||
get_query_keys(E1.L1, E2.L2) :-
|
||||
get_query_keys_2(E1,E2),
|
||||
get_query_keys(L1, L2).
|
||||
|
||||
|
||||
get_query_vars_2([], []).
|
||||
get_query_vars_2(V.AttVars, [RV|RVs]) :-
|
||||
get_query_keys_2([], []).
|
||||
get_query_keys_2(V.AttVars, [RV|RVs]) :-
|
||||
clpbn:get_atts(V,[key(RV)]), !,
|
||||
get_query_vars_2(AttVars, RVs).
|
||||
get_query_keys_2(AttVars, RVs).
|
||||
|
||||
|
||||
get_dists_parameters([], []).
|
||||
@ -133,16 +146,3 @@ get_dists_parameters([Id|Ids], [dist(Id, Params)|DistsInfo]) :-
|
||||
get_pfl_parameters(Id, Params),
|
||||
get_dists_parameters(Ids, DistsInfo).
|
||||
|
||||
|
||||
run_horus_lifted_solver(QueryVarsAtts, Solutions, fove(ParfactorList, DistIds)) :-
|
||||
get_query_vars(QueryVarsAtts, QueryVars),
|
||||
%writeln(queryVars:QueryVars), writeln(''),
|
||||
get_dists_parameters(DistIds, DistsParams),
|
||||
%writeln(dists:DistsParams), writeln(''),
|
||||
cpp_set_parfactors_params(ParfactorList, DistsParams),
|
||||
cpp_run_lifted_solver(ParfactorList, QueryVars, Solutions).
|
||||
|
||||
|
||||
finalize_horus_lifted_solver(fove(ParfactorList, _)) :-
|
||||
cpp_free_lifted_network(ParfactorList).
|
||||
|
||||
|
@ -5,13 +5,13 @@ There are four main files:
|
||||
|
||||
school_128.yap: a school with 128 professors, 256 courses and 4096 students.
|
||||
school_64.yap: medium size school
|
||||
school_32.yap: small school (pfl)
|
||||
school_32.yap: small school (CLP(BN))
|
||||
|
||||
sch32.yap: small school (clp(bn))
|
||||
sch32.yap: small school (PFL)
|
||||
|
||||
parschema.yap: the CLP(BN) schema
|
||||
parschema.pfl: the PFL schema
|
||||
|
||||
schema.yap: the PFL schema
|
||||
schema.yap: the CLP(BN) schema
|
||||
|
||||
tables: CPTs
|
||||
|
||||
@ -53,4 +53,3 @@ rank(s0,X).
|
||||
|
||||
rank(s0,X), student_intelligence(s0,h).
|
||||
|
||||
|
||||
|
82
packages/CLPBN/examples/School/parschema.pfl
Normal file
82
packages/CLPBN/examples/School/parschema.pfl
Normal file
@ -0,0 +1,82 @@
|
||||
/* Base file for school database. Supposed to be called from school_*.yap */
|
||||
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
bayes abi(K)::[h,m,l] ; abi_table ; [professor(K)].
|
||||
|
||||
bayes pop(K)::[h,m,l], abi(K) ; pop_table ; [professor(K)].
|
||||
|
||||
bayes diff(C)::[h,m,l] ; diff_table ; [course(C,_)].
|
||||
|
||||
bayes int(S)::[h,m,l] ; int_table ; [student(S)].
|
||||
|
||||
bayes grade(C,S)::[a,b,c,d], int(S), diff(C) ;
|
||||
grade_table ;
|
||||
[registration(_,C,S)].
|
||||
|
||||
bayes satisfaction(C,S)::[h,m,l], abi(P), grade(C,S) ;
|
||||
sat_table ;
|
||||
[reg_satisfaction(C,S,P)].
|
||||
|
||||
bayes rat(C)::[h,m,l], Sats ; avg ; [course_rat(C, Sats)].
|
||||
|
||||
bayes rank(S)::[a,b,c,d], Grades ; avg ; [student_ranking(S,Grades)].
|
||||
|
||||
|
||||
grade(Key, Grade) :-
|
||||
registration(Key, CKey, SKey),
|
||||
grade(CKey, SKey, Grade).
|
||||
|
||||
reg_satisfaction(CKey, SKey, PKey) :-
|
||||
registration(_Key, CKey, SKey),
|
||||
course(CKey, PKey).
|
||||
|
||||
course_rat(CKey, Sats) :-
|
||||
course(CKey, _),
|
||||
setof(satisfaction(CKey,SKey),
|
||||
PKey^reg_satisfaction(CKey, SKey, PKey),
|
||||
Sats).
|
||||
|
||||
student_ranking(SKey, Grades) :-
|
||||
student(SKey),
|
||||
setof(grade(CKey,SKey),
|
||||
RKey^registration(RKey,CKey,SKey),
|
||||
Grades).
|
||||
|
||||
:- ensure_loaded(tables).
|
||||
|
||||
%
|
||||
% Convert to longer names
|
||||
%
|
||||
professor_ability(P,A) :- abi(P,A).
|
||||
|
||||
professor_popularity(P,A) :- pop(P,A).
|
||||
|
||||
course_difficulty(P,A) :- diff(P,A).
|
||||
|
||||
student_intelligence(P,A) :- int(P,A).
|
||||
|
||||
course_rating(C,X) :- rat(C,X).
|
||||
|
||||
registration_grade(R,A) :-
|
||||
registration(R,C,S),
|
||||
grade(C,S,A).
|
||||
|
||||
registration_satisfaction(R,A) :-
|
||||
registration(R,C,S),
|
||||
satisfaction(C,S,A).
|
||||
|
||||
registration_course(R,C) :- registration(R,C,_).
|
||||
|
||||
registration_student(R,S) :- registration(R,_,S).
|
||||
|
||||
%
|
||||
% Evidence
|
||||
%
|
||||
%abi(p0, h).
|
||||
%pop(p1, m).
|
||||
%pop(p2, h).
|
||||
|
||||
% Query
|
||||
% ?- abi(p0, X).
|
||||
|
@ -1,93 +0,0 @@
|
||||
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
/* base file for school database. Supposed to be called from school_*.yap */
|
||||
|
||||
%
|
||||
% bayes is a parfactor for a bayesian network,
|
||||
% first argument is target of other arguments pop(K) <- abi(K)
|
||||
% second argument is the name of a predicate to call for \phi (CPT)
|
||||
% last argument is a list of goals defining the constraints over the elements
|
||||
% of the
|
||||
%
|
||||
|
||||
%
|
||||
% these states that skolem variables abi(K) are in a parametric factor with
|
||||
% with \phi defined by abi_table(X) and whose domain and constraints
|
||||
% is obtained from professor/1.
|
||||
%
|
||||
|
||||
bayes abi(K)::[h,m,l] ; abi_table ; [professor(K)].
|
||||
|
||||
bayes pop(K)::[h,m,l], abi(K) ; pop_table ; [professor(K)].
|
||||
|
||||
bayes diff(C) :: [h,m,l] ; diff_table ; [course(C,_)].
|
||||
|
||||
bayes int(S) :: [h,m,l] ; int_table ; [student(S)].
|
||||
|
||||
bayes grade(C,S)::[a,b,c,d], int(S), diff(C) ; grade_table ; [registration(_,C,S)].
|
||||
|
||||
bayes satisfaction(C,S)::[h,m,l], abi(P), grade(C,S) ; sat_table ; [reg_satisfaction(C,S,P)].
|
||||
|
||||
bayes rat(C) :: [h,m,l], Sats ; avg ; [course_rat(C, Sats)].
|
||||
|
||||
bayes rank(S) :: [a,b,c,d], Grades ; avg ; [student_ranking(S,Grades)].
|
||||
|
||||
|
||||
grade(Key, Grade) :-
|
||||
registration(Key, CKey, SKey),
|
||||
grade(CKey, SKey, Grade).
|
||||
|
||||
reg_satisfaction(CKey, SKey, PKey) :-
|
||||
registration(_Key, CKey, SKey),
|
||||
course(CKey, PKey).
|
||||
|
||||
course_rat(CKey, Sats) :-
|
||||
course(CKey, _),
|
||||
setof(satisfaction(CKey,SKey),
|
||||
PKey^reg_satisfaction(CKey, SKey, PKey),
|
||||
Sats).
|
||||
|
||||
student_ranking(SKey, Grades) :-
|
||||
student(SKey),
|
||||
setof(grade(CKey,SKey), RKey^registration(RKey,CKey,SKey), Grades).
|
||||
|
||||
:- ensure_loaded(tables).
|
||||
|
||||
% convert to longer names
|
||||
professor_ability(P,A) :- abi(P, A).
|
||||
|
||||
professor_popularity(P,A) :- pop(P, A).
|
||||
|
||||
registration_grade(R,A) :-
|
||||
registration(R,C,S),
|
||||
grade(C,S,A).
|
||||
|
||||
registration_satisfaction(R,A) :-
|
||||
registration(R,C,S),
|
||||
satisfaction(C,S,A).
|
||||
|
||||
student_intelligence(P,A) :- int(P, A).
|
||||
|
||||
course_difficulty(P,A) :- diff(P, A).
|
||||
|
||||
|
||||
registration_course(R,C) :-
|
||||
registration(R, C, _).
|
||||
|
||||
registration_student(R,S) :-
|
||||
registration(R, _, S).
|
||||
|
||||
course_rating(C,X) :- rat(C,X).
|
||||
|
||||
%
|
||||
% evidence
|
||||
%
|
||||
%abi(p0, h).
|
||||
|
||||
%pop(p1, m).
|
||||
%pop(p2, h).
|
||||
|
||||
% Query
|
||||
% ?- abi(p0, X).
|
||||
|
@ -17,9 +17,9 @@ total_students(256).
|
||||
|
||||
:- yap_flag(write_strings,on).
|
||||
|
||||
:- ensure_loaded(parschema).
|
||||
:- ensure_loaded('parschema.pfl').
|
||||
|
||||
:- ensure_loaded(school32_data).
|
||||
|
||||
:- set_clpbn_flag(solver, bdd).
|
||||
:- set_solver(hve).
|
||||
|
||||
|
@ -1,5 +1,4 @@
|
||||
|
||||
/* base file for school database. Supposed to be called from school_*.yap */
|
||||
/* Base file for school database. Supposed to be called from school_*.yap */
|
||||
|
||||
professor_key(Key) :-
|
||||
professor(Key).
|
||||
@ -67,5 +66,3 @@ student_ranking(Key, Rank) :-
|
||||
|
||||
:- ensure_loaded(tables).
|
||||
|
||||
|
||||
|
||||
|
@ -1,5 +1,3 @@
|
||||
|
||||
|
||||
/*
|
||||
total_professors(32).
|
||||
|
||||
@ -13,17 +11,13 @@ total_students(256).
|
||||
|
||||
:- style_check(all).
|
||||
|
||||
:- yap_flag(unknown,error).
|
||||
|
||||
:- yap_flag(write_strings,on).
|
||||
|
||||
:- ensure_loaded(parschema).
|
||||
:- use_module(library(clpbn)).
|
||||
|
||||
:- yap_flag(unknown,error).
|
||||
%:- clpbn_horus:set_solver(lve).
|
||||
%:- clpbn_horus:set_solver(hve).
|
||||
:- clpbn_horus:set_solver(bp).
|
||||
%:- clpbn_horus:set_solver(bdd).
|
||||
:- clpbn_horus:set_solver(ve).
|
||||
%:- clpbn_horus:set_solver(cbp).
|
||||
:- [-schema].
|
||||
|
||||
:- ensure_loaded(school32_data).
|
||||
|
||||
|
@ -4702,5 +4702,3 @@ registration(r3457,c5,s1023).
|
||||
registration(r3458,c37,s1023).
|
||||
registration(r3459,c57,s1023).
|
||||
|
||||
|
||||
|
||||
|
@ -1,30 +1,49 @@
|
||||
|
||||
int_table(_,T ,[h, m, l]) :- int_table(T).
|
||||
abi_table(
|
||||
/* h */ [ 0.50,
|
||||
/* m */ 0.40,
|
||||
/* l */ 0.10 ]).
|
||||
|
||||
int_table([0.5,
|
||||
0.4,
|
||||
0.1]).
|
||||
abi_table(_, T) :- abi_table(T).
|
||||
|
||||
/* h h h m h l m h m m m l l h l m l l */
|
||||
grade_table([
|
||||
0.2, 0.7, 0.85, 0.1, 0.2, 0.5, 0.01, 0.05,0.1 ,
|
||||
0.6, 0.25, 0.12, 0.3, 0.6,0.35,0.04, 0.15, 0.4 ,
|
||||
0.15,0.04, 0.02, 0.4,0.15,0.12, 0.5, 0.6, 0.4,
|
||||
0.05,0.01, 0.01, 0.2,0.05,0.03, 0.45, 0.2, 0.1 ]).
|
||||
pop_table(
|
||||
/* h m l */
|
||||
/* h */ [ 0.9, 0.2, 0.01,
|
||||
/* m */ 0.09, 0.6, 0.09,
|
||||
/* l */ 0.01, 0.2, 0.9 ]).
|
||||
|
||||
pop_table(_, T) :- pop_table(T).
|
||||
|
||||
diff_table(
|
||||
/* h */ [ 0.25,
|
||||
/* m */ 0.50,
|
||||
/* l */ 0.25 ]).
|
||||
|
||||
dif_table(_, T) :- diff_table(T).
|
||||
|
||||
int_table(
|
||||
/* h */ [ 0.5,
|
||||
/* m */ 0.4,
|
||||
/* l */ 0.1 ]).
|
||||
|
||||
int_table(_,T ,[h,m,l]) :- int_table(T).
|
||||
|
||||
grade_table(
|
||||
/* h h h m h l m h m m m l l h l m l l */
|
||||
/* a */ [ 0.2, 0.7, 0.85, 0.1, 0.2, 0.5, 0.01, 0.05, 0.1,
|
||||
/* b */ 0.6, 0.25, 0.12, 0.3, 0.6, 0.35, 0.04, 0.15, 0.4,
|
||||
/* c */ 0.15, 0.04, 0.02, 0.4, 0.15, 0.12, 0.5, 0.6, 0.4,
|
||||
/* d */ 0.05, 0.01, 0.01, 0.2, 0.05, 0.03, 0.45, 0.2, 0.1 ]).
|
||||
|
||||
grade_table(I, D,
|
||||
/* h h h m h l m h m m m l l h l m l l */
|
||||
p([a,b,c,d], T, [I,D])) :- grade_table(T).
|
||||
p([a,b,c,d], T, [I,D])) :- grade_table(T).
|
||||
|
||||
sat_table(
|
||||
/* h a h b h c h d m a m b m c m d l a l b l c l d */
|
||||
/*h*/ [0.98, 0.9, 0.8 , 0.6, 0.9, 0.4, 0.2, 0.01, 0.5, 0.2, 0.01, 0.01,
|
||||
/*m*/ 0.01, 0.09,0.15, 0.3, 0.05, 0.4, 0.3, 0.04, 0.35, 0.3, 0.09, 0.01 ,
|
||||
/*l*/ 0.01, 0.01,0.05, 0.1, 0.05, 0.2, 0.5, 0.95, 0.15, 0.5, 0.9, 0.98]).
|
||||
/*
|
||||
A: professor's ability;
|
||||
B: student's grade (for course registration).
|
||||
*/
|
||||
/* h a h b h c h d m a m b m c m d l a l b l c l d */
|
||||
/* h */ [ 0.98, 0.9, 0.8 , 0.6, 0.9, 0.4, 0.2, 0.01, 0.5, 0.2, 0.01, 0.01,
|
||||
/* m */ 0.01, 0.09, 0.15, 0.3, 0.05, 0.4, 0.3, 0.04, 0.35, 0.3, 0.09, 0.01,
|
||||
/* l */ 0.01, 0.01, 0.05, 0.1, 0.05, 0.2, 0.5, 0.95, 0.15, 0.5, 0.9, 0.98 ]).
|
||||
|
||||
satisfaction_table(A, G, p([h,m,l], T, [A,G])) :- sat_table(T).
|
||||
|
||||
|
||||
@ -35,22 +54,8 @@ satisfaction_table(A, G, p([h,m,l], T, [A,G])) :- sat_table(T).
|
||||
%
|
||||
% add all and divide on the number of elements on the table!
|
||||
%
|
||||
rating_prob_table([0.9,0.05,0.01,
|
||||
0.09,0.9,0.09,
|
||||
0.01,0.05,0.9]).
|
||||
|
||||
abi_table( [0.50, 0.40, 0.10]).
|
||||
|
||||
abi_table( _, T) :- abi_table(T).
|
||||
|
||||
|
||||
pop_table( [0.9, 0.2, 0.01,
|
||||
0.09, 0.6, 0.09,
|
||||
0.01, 0.2, 0.9]).
|
||||
|
||||
pop_table(_, T) :- pop_table(T).
|
||||
|
||||
diff_table([0.25, 0.50, 0.25]).
|
||||
|
||||
dif_table(_, T) :- diff_table(T).
|
||||
rating_prob_table(
|
||||
[ 0.9, 0.05, 0.01,
|
||||
0.09, 0.9, 0.09,
|
||||
0.01, 0.05, 0.9 ]).
|
||||
|
||||
|
@ -1,23 +1,45 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bdd).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
:- yap_flag(write_strings, off).
|
||||
bayes burglary ; burglary_table ; [].
|
||||
|
||||
bayes burglary::[t,f] ; [0.001, 0.999] ; [].
|
||||
bayes earthquake ; earthquake_table ; [].
|
||||
|
||||
bayes earthquake::[t,f] ; [0.002, 0.998]; [].
|
||||
bayes alarm, burglary, earthquake ; alarm_table ; [].
|
||||
|
||||
bayes alarm::[t,f], burglary, earthquake ;
|
||||
[0.95, 0.94, 0.29, 0.001, 0.05, 0.06, 0.71, 0.999] ;
|
||||
[].
|
||||
bayes john_calls, alarm ; john_calls_table ; [].
|
||||
|
||||
bayes john_calls::[t,f], alarm ; [0.9, 0.05, 0.1, 0.95] ; [].
|
||||
bayes mary_calls, alarm ; mary_calls_table ; [].
|
||||
|
||||
bayes mary_calls::[t,f], alarm ; [0.7, 0.01, 0.3, 0.99] ; [].
|
||||
burglary_table(
|
||||
[ 0.001,
|
||||
0.999 ]).
|
||||
|
||||
earthquake_table(
|
||||
[ 0.002,
|
||||
0.998 ]).
|
||||
|
||||
alarm_table(
|
||||
[ 0.95, 0.94, 0.29, 0.001,
|
||||
0.05, 0.06, 0.71, 0.999 ]).
|
||||
|
||||
john_calls_table(
|
||||
[ 0.9, 0.05,
|
||||
0.1, 0.95 ]).
|
||||
|
||||
mary_calls_table(
|
||||
[ 0.7, 0.01,
|
||||
0.3, 0.99 ]).
|
||||
|
||||
% ?- john_calls(J), mary_calls(t).
|
||||
|
||||
|
134
packages/CLPBN/examples/city.pfl
Normal file
134
packages/CLPBN/examples/city.pfl
Normal file
@ -0,0 +1,134 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bdd).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
:- multifile people/2.
|
||||
:- multifile ev/1.
|
||||
|
||||
people(joe,nyc).
|
||||
people(p2, nyc).
|
||||
people(p3, nyc).
|
||||
people(p4, nyc).
|
||||
people(p5, nyc).
|
||||
|
||||
ev(descn(p2, fits)).
|
||||
ev(descn(p3, fits)).
|
||||
ev(descn(p4, fits)).
|
||||
ev(descn(p5, fits)).
|
||||
|
||||
bayes city_conservativeness(C)::[high,low] ;
|
||||
cons_table(C) ;
|
||||
[people(_,C)].
|
||||
|
||||
bayes gender(P)::[male,female] ;
|
||||
gender_table(P) ;
|
||||
[people(P,_)].
|
||||
|
||||
bayes hair_color(P)::[dark,bright], city_conservativeness(C) ;
|
||||
hair_color_table(P) ;
|
||||
[people(P,C)].
|
||||
|
||||
bayes car_color(P)::[dark,bright], hair_color(P) ;
|
||||
car_color_table(P) ;
|
||||
[people(P,_)].
|
||||
|
||||
bayes height(P)::[tall,short], gender(P) ;
|
||||
height_table(P) ;
|
||||
[people(P,_)].
|
||||
|
||||
bayes shoe_size(P)::[big,small], height(P) ;
|
||||
shoe_size_table(P) ;
|
||||
[people(P,_)].
|
||||
|
||||
bayes guilty(P)::[y,n] ;
|
||||
guilty_table(P) ;
|
||||
[people(P,_)].
|
||||
|
||||
bayes descn(P)::[fits,dont_fit], car_color(P),
|
||||
hair_color(P), height(P), guilty(P) ;
|
||||
descn_table(P) ;
|
||||
[people(P,_)].
|
||||
|
||||
bayes witness(C), descn(Joe), descn(P2) ;
|
||||
witness_table ;
|
||||
[people(_,C), Joe=joe, P2=p2].
|
||||
|
||||
|
||||
cons_table(amsterdam,
|
||||
% special case for amsterdam: amsterdam is
|
||||
% less conservative than other cities (is it?)
|
||||
/* y */ [ 0.2,
|
||||
/* n */ 0.8 ]) :- !. % FIXME
|
||||
cons_table(_,
|
||||
/* y */ [ 0.8,
|
||||
/* n */ 0.2 ]).
|
||||
|
||||
gender_table(_,
|
||||
/* male */ [ 0.55,
|
||||
/* female */ 0.45 ]).
|
||||
|
||||
hair_color_table(_,
|
||||
/* high low */
|
||||
/* dark */ [ 0.05, 0.1,
|
||||
/* bright */ 0.95, 0.9 ]).
|
||||
|
||||
car_color_table(_,
|
||||
/* dark bright */
|
||||
/* dark */ [ 0.9, 0.2,
|
||||
/* bright */ 0.1, 0.8 ]).
|
||||
|
||||
height_table(_,
|
||||
/* male female */
|
||||
/* tall */ [ 0.6, 0.4,
|
||||
/* short */ 0.4, 0.6 ]).
|
||||
|
||||
shoe_size_table(_,
|
||||
/* tall short */
|
||||
/* big */ [ 0.9, 0.1,
|
||||
/* small */ 0.1, 0.9 ]).
|
||||
|
||||
guilty_table(_,
|
||||
/* yes */ [ 0.23,
|
||||
/* no */ 0.77 ]).
|
||||
|
||||
descn_table(_,
|
||||
/* car_color(P), hair_color(P), height(P), guilty(P) */
|
||||
/* fits */ [ 0.99, 0.5, 0.23, 0.88, 0.41, 0.3, 0.76, 0.87,
|
||||
/* fits */ 0.44, 0.43, 0.29, 0.72, 0.23, 0.91, 0.95, 0.92,
|
||||
/* dont_fit */ 0.01, 0.5, 0.77, 0.12, 0.59, 0.7, 0.24, 0.13,
|
||||
/* dont_fit */ 0.56, 0.57, 0.71, 0.28, 0.77, 0.09, 0.05, 0.08 ]).
|
||||
|
||||
witness_table(
|
||||
/* descn(Joe), descn(P2) */
|
||||
/* t */ [ 0.2, 0.45, 0.24, 0.34,
|
||||
/* f */ 0.8, 0.55, 0.76, 0.66 ]).
|
||||
|
||||
|
||||
runall(G, Wrapper) :-
|
||||
findall(G, Wrapper, L),
|
||||
execute_all(L).
|
||||
|
||||
|
||||
execute_all([]).
|
||||
execute_all(G.L) :-
|
||||
call(G),
|
||||
execute_all(L).
|
||||
|
||||
|
||||
is_joe_guilty(Guilty) :-
|
||||
witness(nyc, t),
|
||||
runall(X, ev(X)),
|
||||
guilty(joe, Guilty).
|
||||
|
||||
|
||||
% ?- is_joe_guilty(Guilty).
|
||||
|
@ -1,105 +0,0 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
|
||||
:- multifile people/2.
|
||||
:- multifile ev/1.
|
||||
|
||||
people(joe,nyc).
|
||||
people(p2, nyc).
|
||||
people(p3, nyc).
|
||||
people(p4, nyc).
|
||||
people(p5, nyc).
|
||||
|
||||
ev(descn(p2, t)).
|
||||
ev(descn(p3, t)).
|
||||
ev(descn(p4, t)).
|
||||
ev(descn(p5, t)).
|
||||
|
||||
bayes city_conservativeness(C)::[y,n] ; cons_table(C) ; [people(_,C)].
|
||||
|
||||
bayes gender(P)::[m,f] ; gender_table(P) ; [people(P,_)].
|
||||
|
||||
bayes hair_color(P)::[t,f], city_conservativeness(C) ; hair_color_table(P) ; [people(P,C)].
|
||||
|
||||
bayes car_color(P)::[t,f], hair_color(P) ; car_color_table(P); [people(P,_)].
|
||||
|
||||
bayes height(P)::[t,f], gender(P) ; height_table(P) ; [people(P,_)].
|
||||
|
||||
bayes shoe_size(P)::[t,f], height(P) ; shoe_size_table(P); [people(P,_)].
|
||||
|
||||
bayes guilty(P)::[y,n] ; guilty_table(P) ; [people(P,_)].
|
||||
|
||||
bayes descn(P)::[t,f], car_color(P), hair_color(P), height(P), guilty(P) ; descn_table(P) ; [people(P,_)].
|
||||
|
||||
bayes witness(C)::[t,f], descn(Joe), descn(P2) ; wit_table ; [people(_,C), Joe=joe, P2=p2].
|
||||
|
||||
% FIXME
|
||||
%cons_table(amsterdam, [0.2, 0.8]) :- !.
|
||||
cons_table(_, [0.8, 0.2]).
|
||||
|
||||
|
||||
gender_table(_, [0.55, 0.45]).
|
||||
|
||||
|
||||
hair_color_table(_,
|
||||
/* conservative_city */
|
||||
/* y n */
|
||||
[ 0.05, 0.1,
|
||||
0.95, 0.9 ]).
|
||||
|
||||
|
||||
car_color_table(_,
|
||||
/* t f */
|
||||
[ 0.9, 0.2,
|
||||
0.1, 0.8 ]).
|
||||
|
||||
|
||||
height_table(_,
|
||||
/* m f */
|
||||
[ 0.6, 0.4,
|
||||
0.4, 0.6 ]).
|
||||
|
||||
|
||||
shoe_size_table(_,
|
||||
/* t f */
|
||||
[ 0.9, 0.1,
|
||||
0.1, 0.9 ]).
|
||||
|
||||
|
||||
guilty_table(_, [0.23, 0.77]).
|
||||
|
||||
|
||||
descn_table(_,
|
||||
/* color, hair, height, guilt */
|
||||
/* ttttt tttf ttft ttff tfttt tftf tfft tfff ttttt fttf ftft ftff ffttt fftf ffft ffff */
|
||||
[ 0.99, 0.5, 0.23, 0.88, 0.41, 0.3, 0.76, 0.87, 0.44, 0.43, 0.29, 0.72, 0.23, 0.91, 0.95, 0.92,
|
||||
0.01, 0.5, 0.77, 0.12, 0.59, 0.7, 0.24, 0.13, 0.56, 0.57, 0.71, 0.28, 0.77, 0.09, 0.05, 0.08]).
|
||||
|
||||
|
||||
wit_table([0.2, 0.45, 0.24, 0.34,
|
||||
0.8, 0.55, 0.76, 0.66]).
|
||||
|
||||
|
||||
runall(G, Wrapper) :-
|
||||
findall(G, Wrapper, L),
|
||||
execute_all(L).
|
||||
|
||||
|
||||
execute_all([]).
|
||||
execute_all(G.L) :-
|
||||
call(G),
|
||||
execute_all(L).
|
||||
|
||||
|
||||
is_joe_guilty(Guilty) :-
|
||||
witness(nyc, t),
|
||||
runall(X, ev(X)),
|
||||
guilty(joe, Guilty).
|
||||
|
||||
|
||||
% ?- is_joe_guilty(Guilty)
|
||||
|
40
packages/CLPBN/examples/comp_workshops.pfl
Normal file
40
packages/CLPBN/examples/comp_workshops.pfl
Normal file
@ -0,0 +1,40 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
:- multifile c/2.
|
||||
|
||||
c(p1,w1).
|
||||
c(p1,w2).
|
||||
c(p1,w3).
|
||||
c(p2,w1).
|
||||
c(p2,w2).
|
||||
c(p2,w3).
|
||||
c(p3,w1).
|
||||
c(p3,w2).
|
||||
c(p3,w3).
|
||||
c(p4,w1).
|
||||
c(p4,w2).
|
||||
c(p4,w3).
|
||||
c(p5,w1).
|
||||
c(p5,w2).
|
||||
c(p5,w3).
|
||||
|
||||
markov attends(P), hot(W) ;
|
||||
[0.2, 0.8, 0.8, 0.8] ;
|
||||
[c(P,W)].
|
||||
|
||||
markov attends(P), series ;
|
||||
[0.501, 0.499, 0.499, 0.499] ;
|
||||
[c(P,_)].
|
||||
|
||||
?- series(X).
|
||||
|
@ -1,33 +0,0 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
|
||||
:- yap_flag(write_strings, off).
|
||||
|
||||
:- multifile c/2.
|
||||
|
||||
c(p1,w1).
|
||||
c(p1,w2).
|
||||
c(p1,w3).
|
||||
c(p2,w1).
|
||||
c(p2,w2).
|
||||
c(p2,w3).
|
||||
c(p3,w1).
|
||||
c(p3,w2).
|
||||
c(p3,w3).
|
||||
c(p4,w1).
|
||||
c(p4,w2).
|
||||
c(p4,w3).
|
||||
c(p5,w1).
|
||||
c(p5,w2).
|
||||
c(p5,w3).
|
||||
|
||||
markov attends(P)::[t,f], hot(W)::[t,f] ; [0.2, 0.8, 0.8, 0.8] ; [c(P,W)].
|
||||
|
||||
markov attends(P)::[t,f], series::[t,f] ; [0.501, 0.499, 0.499, 0.499] ; [c(P,_)].
|
||||
|
||||
% ?- series(X).
|
||||
|
@ -1,21 +0,0 @@
|
||||
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_pfl_flag(solver,lve).
|
||||
%:- set_pfl_flag(solver,bp), clpbn_horus:set_horus_flag(inf_alg,ve).
|
||||
%:- set_pfl_flag(solver,bp), clpbn_horus:set_horus_flag(inf_alg,bp).
|
||||
%:- set_pfl_flag(solver,bp), clpbn_horus:set_horus_flag(inf_alg,cbp).
|
||||
|
||||
|
||||
t(ann).
|
||||
t(dave).
|
||||
|
||||
% p(ann,t).
|
||||
|
||||
markov p(X)::[t,f] ; [0.1, 0.3] ; [t(X)].
|
||||
|
||||
% use standard Prolog queries: provide evidence first.
|
||||
|
||||
?- p(ann,t), p(ann,X).
|
||||
% ?- p(ann,X).
|
||||
|
@ -1,21 +0,0 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
|
||||
:- yap_flag(write_strings, off).
|
||||
|
||||
:- clpbn_horus:set_horus_flag(verbosity,5).
|
||||
|
||||
people(p1,p1).
|
||||
people(p1,p2).
|
||||
people(p2,p1).
|
||||
people(p2,p2).
|
||||
|
||||
markov p(A,A)::[t,f] ; [1.0,4.5] ; [people(A,_)].
|
||||
|
||||
markov p(A,B)::[t,f] ; [1.0,4.5] ; [people(A,B)].
|
||||
|
||||
?- p(p1,p1,X).
|
File diff suppressed because one or more lines are too long
@ -1,26 +1,15 @@
|
||||
% learn distribution for school database.
|
||||
/* Learn distribution for professor database. */
|
||||
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- use_module(library(clpbn/learning/em)).
|
||||
|
||||
bayes abi(K)::[h,m,l] ; abi_table ; [professor(K)].
|
||||
|
||||
bayes pop(K)::[h,m,l], abi(K) ; pop_table ; [professor(K)].
|
||||
|
||||
abi_table([0.3,0.3,0.4]).
|
||||
|
||||
pop_table([0.3,0.3,0.4,0.3,0.3,0.4,0.3,0.3,0.4]).
|
||||
|
||||
goal_list([/*abi(p0,h),
|
||||
abi(p1,m),
|
||||
abi(p2,m),
|
||||
abi(p3,m),*/
|
||||
abi(p4,l),
|
||||
pop(p5,h),
|
||||
abi(p5,_),
|
||||
abi(p6,_),
|
||||
pop(p7,_)]).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,gibbs).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,jt).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,hve).
|
||||
:- clpbn:set_clpbn_flag(em_solver,ve).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,bp).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,bdd).
|
||||
|
||||
professor(p0).
|
||||
professor(p1).
|
||||
@ -32,12 +21,26 @@ professor(p6).
|
||||
professor(p7).
|
||||
professor(p8).
|
||||
|
||||
%:- clpbn:set_clpbn_flag(em_solver,gibbs).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,jt).
|
||||
:- clpbn:set_clpbn_flag(em_solver,hve).
|
||||
:- clpbn:set_clpbn_flag(em_solver,ve).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,bp).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,bdd).
|
||||
bayes abi(K)::[h,m,l] ; abi_table ; [professor(K)].
|
||||
|
||||
bayes pop(K)::[h,m,l], abi(K) ; pop_table ; [professor(K)].
|
||||
|
||||
abi_table([0.3, 0.3, 0.4]).
|
||||
|
||||
pop_table([0.3, 0.3, 0.4, 0.3, 0.3, 0.4, 0.3, 0.3, 0.4]).
|
||||
|
||||
goal_list([
|
||||
/*
|
||||
abi(p0,h),
|
||||
abi(p1,m),
|
||||
abi(p2,m),
|
||||
abi(p3,m),
|
||||
*/
|
||||
abi(p4,l),
|
||||
pop(p5,h),
|
||||
abi(p5,_),
|
||||
abi(p6,_),
|
||||
pop(p7,_)]).
|
||||
|
||||
timed_main :-
|
||||
statistics(runtime, _),
|
||||
@ -47,13 +50,5 @@ timed_main :-
|
||||
|
||||
main(Lik) :-
|
||||
goal_list(L),
|
||||
% run_queries(L),
|
||||
em(L,0.01,10,_,Lik).
|
||||
|
||||
run_queries([]).
|
||||
run_queries(Q.L) :-
|
||||
call(Q),
|
||||
run_queries(L).
|
||||
|
||||
|
||||
em(L,0.01,10,_,Lik).
|
||||
|
||||
|
62
packages/CLPBN/examples/learning/school_params.yap
Normal file
62
packages/CLPBN/examples/learning/school_params.yap
Normal file
@ -0,0 +1,62 @@
|
||||
/* Learn distribution for school database. */
|
||||
|
||||
/* We do not consider aggregates yet. */
|
||||
|
||||
:- [pos:train].
|
||||
|
||||
:- ['../../examples/School/sch32'].
|
||||
|
||||
:- use_module(library(clpbn/learning/em)).
|
||||
|
||||
%:- clpbn:set_clpbn_flag(em_solver,gibbs).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,jt).
|
||||
:- clpbn:set_clpbn_flag(em_solver,ve).
|
||||
%:- clpbn:set_clpbn_flag(em_solver,bp).
|
||||
|
||||
timed_main :-
|
||||
statistics(runtime, _),
|
||||
findall(X,goal(X),L),
|
||||
em(L,0.01,10,_,Lik),
|
||||
statistics(runtime, [T,_]),
|
||||
format('Took ~d msec and Lik ~3f~n',[T,Lik]).
|
||||
|
||||
main :-
|
||||
findall(X,goal(X),L),
|
||||
em(L,0.001,10,CPTs,Lik),
|
||||
writeln(Lik:CPTs).
|
||||
|
||||
%
|
||||
% Change to 0.0, 0.1, 0.2 to make things simpler/harder
|
||||
%
|
||||
missing(0.2).
|
||||
|
||||
goal(professor_ability(P,V)) :-
|
||||
pos:professor_ability(P,V1),
|
||||
missing(X),
|
||||
( random > X -> V = V1 ; true).
|
||||
|
||||
goal(professor_popularity(P,V)) :-
|
||||
pos:professor_popularity(P,V1),
|
||||
missing(X),
|
||||
( random > X -> V = V1 ; true).
|
||||
|
||||
goal(registration_grade(P,V)) :-
|
||||
pos:registration_grade(P,V1),
|
||||
missing(X),
|
||||
( random > X -> V = V1 ; true).
|
||||
|
||||
goal(student_intelligence(P,V)) :-
|
||||
pos:student_intelligence(P,V1),
|
||||
missing(X),
|
||||
( random > X -> V = V1 ; true).
|
||||
|
||||
goal(course_difficulty(P,V)) :-
|
||||
pos:course_difficulty(P,V1),
|
||||
missing(X),
|
||||
( random > X -> V = V1 ; true).
|
||||
|
||||
goal(registration_satisfaction(P,V)) :-
|
||||
pos:registration_satisfaction(P,V1),
|
||||
missing(X),
|
||||
( random > X -> V = V1 ; true).
|
||||
|
@ -1,9 +1,18 @@
|
||||
% learn distribution for school database.
|
||||
/* Learn distribution for a sprinkler database. */
|
||||
|
||||
:- ['../sprinkler.pfl'].
|
||||
|
||||
:- use_module(library(clpbn/learning/em)).
|
||||
|
||||
%:- set_pfl_flag(em_solver,gibbs).
|
||||
%:- set_pfl_flag(em_solver,jt).
|
||||
%:- set_pfl_flag(em_solver,hve).
|
||||
%:- set_pfl_flag(em_solver,bp).
|
||||
%:- set_pfl_flag(em_solver,ve).
|
||||
:- set_pfl_flag(em_solver,bdd).
|
||||
|
||||
:- dynamic id/1.
|
||||
|
||||
data(t,t,t,t).
|
||||
data(_,t,_,t).
|
||||
data(t,t,f,f).
|
||||
@ -18,13 +27,6 @@ data(t,t,_,f).
|
||||
data(t,f,f,t).
|
||||
data(t,f,t,t).
|
||||
|
||||
%:- set_pfl_flag(em_solver,gibbs).
|
||||
%:- set_pfl_flag(em_solver,jt).
|
||||
:- set_pfl_flag(em_solver,hve).
|
||||
%:- set_pfl_flag(em_solver,bp).
|
||||
:- set_pfl_flag(em_solver,ve).
|
||||
:- set_pfl_flag(em_solver,bdd).
|
||||
|
||||
timed_main :-
|
||||
statistics(runtime, _),
|
||||
main(Lik),
|
||||
@ -33,19 +35,16 @@ timed_main :-
|
||||
|
||||
main(Lik) :-
|
||||
findall(X,scan_data(X),L),
|
||||
em(L,0.01,10,_,Lik).
|
||||
em(L,0.01,10,_,Lik).
|
||||
|
||||
scan_data(I:[wet_grass(W),sprinkler(S),rain(R),cloudy(C)]) :-
|
||||
data(W, S, R, C),
|
||||
new_id(I).
|
||||
|
||||
:- dynamic id/1.
|
||||
|
||||
new_id(I) :-
|
||||
retract(id(I)),
|
||||
I1 is I+1,
|
||||
assert(id(I1)).
|
||||
retract(id(I)),
|
||||
I1 is I+1,
|
||||
assert(id(I1)).
|
||||
|
||||
id(0).
|
||||
|
||||
|
||||
|
@ -1,5 +1,3 @@
|
||||
|
||||
|
||||
professor_ability(p0,h).
|
||||
professor_ability(p1,h).
|
||||
professor_ability(p2,m).
|
||||
@ -1250,6 +1248,7 @@ registration_grade(r854,c).
|
||||
registration_grade(r855,d).
|
||||
registration_grade(r856,c).
|
||||
|
||||
|
||||
registration_satisfaction(r0,h).
|
||||
registration_satisfaction(r1,l).
|
||||
registration_satisfaction(r2,h).
|
||||
@ -2431,3 +2430,4 @@ student_ranking(s252,b).
|
||||
student_ranking(s253,b).
|
||||
student_ranking(s254,b).
|
||||
student_ranking(s255,c).
|
||||
|
||||
|
38
packages/CLPBN/examples/social_domain1.pfl
Normal file
38
packages/CLPBN/examples/social_domain1.pfl
Normal file
@ -0,0 +1,38 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bdd).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
:- multifile people/1.
|
||||
|
||||
people @ 5.
|
||||
|
||||
people(X,Y) :-
|
||||
people(X),
|
||||
people(Y),
|
||||
X \== Y.
|
||||
|
||||
markov smokes(X) ; [1.0, 4.0552]; [people(X)].
|
||||
|
||||
markov cancer(X) ; [1.0, 9.9742]; [people(X)].
|
||||
|
||||
markov friends(X,Y) ; [1.0, 99.48432] ; [people(X,Y)].
|
||||
|
||||
markov smokes(X), cancer(X) ;
|
||||
[4.48169, 4.48169, 1.0, 4.48169] ;
|
||||
[people(X)].
|
||||
|
||||
markov friends(X,Y), smokes(X), smokes(Y) ;
|
||||
[3.004166, 3.004166, 3.004166, 3.004166, 3.004166, 1.0, 1.0, 3.004166] ;
|
||||
[people(X,Y)].
|
||||
|
||||
% ?- friends(p1,p2,X).
|
||||
|
@ -1,31 +0,0 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
|
||||
:- yap_flag(write_strings, off).
|
||||
|
||||
:- multifile people/1.
|
||||
|
||||
people @ 5.
|
||||
|
||||
people(X,Y) :-
|
||||
people(X),
|
||||
people(Y),
|
||||
X \== Y.
|
||||
|
||||
markov smokes(X)::[t,f]; [1.0, 4.0552]; [people(X)].
|
||||
|
||||
markov cancer(X)::[t,f]; [1.0, 9.9742]; [people(X)].
|
||||
|
||||
markov friends(X,Y)::[t,f] ; [1.0, 99.48432] ; [people(X,Y)].
|
||||
|
||||
markov smokes(X)::[t,f], cancer(X)::[t,f] ; [4.48169, 4.48169, 1.0, 4.48169] ; [people(X)].
|
||||
|
||||
markov friends(X,Y)::[t,f], smokes(X)::[t,f], smokes(Y)::[t,f] ;
|
||||
[3.004166, 3.004166, 3.004166, 3.004166, 3.004166, 1.0, 1.0, 3.004166] ; [people(X,Y)].
|
||||
|
||||
% ?- friends(p1,p2,X).
|
||||
|
38
packages/CLPBN/examples/social_domain2.pfl
Normal file
38
packages/CLPBN/examples/social_domain2.pfl
Normal file
@ -0,0 +1,38 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bdd).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
:- multifile people/1.
|
||||
|
||||
people @ 5.
|
||||
|
||||
people(X,Y) :-
|
||||
people(X),
|
||||
people(Y).
|
||||
% X \== Y.
|
||||
|
||||
markov smokes(X) ; [1.0, 4.0552]; [people(X)].
|
||||
|
||||
markov asthma(X) ; [1.0, 9.9742] ; [people(X)].
|
||||
|
||||
markov friends(X,Y) ; [1.0, 99.48432] ; [people(X,Y)].
|
||||
|
||||
markov asthma(X), smokes(X) ;
|
||||
[4.48169, 4.48169, 1.0, 4.48169] ;
|
||||
[people(X)].
|
||||
|
||||
markov asthma(X), friends(X,Y), smokes(Y) ;
|
||||
[3.004166, 3.004166, 3.004166, 3.004166, 3.004166, 1.0, 1.0, 3.004166] ;
|
||||
[people(X,Y)].
|
||||
|
||||
% ?- smokes(p1,t), smokes(p2,t), friends(p1,p2,X).
|
||||
|
@ -1,31 +0,0 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
|
||||
:- yap_flag(write_strings, off).
|
||||
|
||||
:- multifile people/1.
|
||||
|
||||
people @ 5.
|
||||
|
||||
people(X,Y) :-
|
||||
people(X),
|
||||
people(Y).
|
||||
% X \== Y.
|
||||
|
||||
markov smokes(X)::[t,f]; [1.0, 4.0552]; [people(X)].
|
||||
|
||||
markov asthma(X)::[t,f]; [1.0, 9.9742] ; [people(X)].
|
||||
|
||||
markov friends(X,Y)::[t,f]; [1.0, 99.48432] ; [people(X,Y)].
|
||||
|
||||
markov asthma(X)::[t,f], smokes(X)::[t,f]; [4.48169, 4.48169, 1.0, 4.48169] ; [people(X)].
|
||||
|
||||
markov asthma(X)::[t,f], friends(X,Y)::[t,f], smokes(Y)::[t,f];
|
||||
[3.004166, 3.004166, 3.004166, 3.004166, 3.004166, 1.0, 1.0, 3.004166] ; [people(X,Y)].
|
||||
|
||||
% ?- smokes(p1,t), smokes(p2,t), friends(p1,p2,X)
|
||||
|
@ -1,12 +1,15 @@
|
||||
|
||||
:- style_check(all).
|
||||
|
||||
:- ensure_loaded(library(pfl)).
|
||||
|
||||
% 1. define domain of random variables
|
||||
% not necessary if they are boolean.
|
||||
|
||||
% 2. define parfactors
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bdd).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
bayes cloudy ; cloudy_table ; [].
|
||||
|
||||
@ -16,18 +19,21 @@ bayes rain, cloudy ; rain_table ; [].
|
||||
|
||||
bayes wet_grass, sprinkler, rain ; wet_grass_table ; [].
|
||||
|
||||
cloudy_table(
|
||||
[ 0.5,
|
||||
0.5 ]).
|
||||
|
||||
% 3. define CPTs.
|
||||
sprinkler_table(
|
||||
[ 0.5, 0.9,
|
||||
0.5, 0.1 ]).
|
||||
|
||||
wet_grass_table([1.0,0.1,0.1,0.01,
|
||||
0.0,0.9,0.9,0.99]).
|
||||
rain_table(
|
||||
[ 0.8, 0.2,
|
||||
0.2, 0.8 ]).
|
||||
|
||||
sprinkler_table([0.5,0.9,
|
||||
0.5,0.1]).
|
||||
|
||||
rain_table([0.8,0.2,
|
||||
0.2,0.8]).
|
||||
|
||||
cloudy_table([0.5,0.5]).
|
||||
wet_grass_table(
|
||||
[ 1.0, 0.1, 0.1, 0.01,
|
||||
0.0, 0.9, 0.9, 0.99 ]).
|
||||
|
||||
% ?- wet_grass(X).
|
||||
|
||||
|
@ -1,33 +0,0 @@
|
||||
|
||||
:- style_check(all).
|
||||
|
||||
:- ensure_loaded(library(clpbn)).
|
||||
|
||||
wet_grass(W) :-
|
||||
sprinkler(S),
|
||||
rain(R),
|
||||
{ W = wet with p([f,t],
|
||||
([1.0,0.1,0.1,0.01,
|
||||
0.0,0.9,0.9,0.99]),
|
||||
[S,R])
|
||||
}.
|
||||
|
||||
|
||||
sprinkler(P) :-
|
||||
cloudy(C),
|
||||
{ P = sprinkler with p([f,t],
|
||||
[0.5,0.9,
|
||||
0.5,0.1],
|
||||
[C])
|
||||
}.
|
||||
|
||||
rain(R) :-
|
||||
cloudy(C),
|
||||
{ R = rain with p([f,t], [0.8,0.2,
|
||||
0.2,0.8],
|
||||
[C]) }.
|
||||
|
||||
cloudy(C) :-
|
||||
{ C = cloudy with p([f,t],[0.5,0.5],[]) }.
|
||||
|
||||
|
33
packages/CLPBN/examples/workshop_attrs.pfl
Normal file
33
packages/CLPBN/examples/workshop_attrs.pfl
Normal file
@ -0,0 +1,33 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
:- set_solver(hve).
|
||||
%:- set_solver(ve).
|
||||
%:- set_solver(jt).
|
||||
%:- set_solver(bdd).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
%:- set_solver(gibbs).
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(lkc).
|
||||
%:- set_solver(lbp).
|
||||
|
||||
:- multifile people/1.
|
||||
|
||||
people @ 5.
|
||||
|
||||
markov attends(P), attr1 ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P), attr2 ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P), attr3 ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P), attr4 ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P), attr5 ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P), attr6 ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P), series ; [0.501, 0.499, 0.499, 0.499] ; [people(P)].
|
||||
|
||||
% ?- series(X).
|
||||
|
@ -1,29 +0,0 @@
|
||||
:- use_module(library(pfl)).
|
||||
|
||||
%:- set_solver(lve).
|
||||
%:- set_solver(hve).
|
||||
%:- set_solver(bp).
|
||||
%:- set_solver(cbp).
|
||||
|
||||
:- yap_flag(write_strings, off).
|
||||
|
||||
:- multifile people/1.
|
||||
|
||||
people @ 5.
|
||||
|
||||
markov attends(P)::[t,f], attr1::[t,f] ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P)::[t,f], attr2::[t,f] ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P)::[t,f], attr3::[t,f] ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P)::[t,f], attr4::[t,f] ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P)::[t,f], attr5::[t,f] ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P)::[t,f], attr6::[t,f] ; [0.7, 0.3, 0.3, 0.3] ; [people(P)].
|
||||
|
||||
markov attends(P)::[t,f], series::[t,f] ; [0.501, 0.499, 0.499, 0.499] ; [people(P)].
|
||||
|
||||
% ?- series(X).
|
||||
|
@ -189,13 +189,12 @@ runGroundSolver (void)
|
||||
taskList = YAP_TailOfTerm (taskList);
|
||||
}
|
||||
|
||||
std::set<VarId> vids;
|
||||
for (size_t i = 0; i < tasks.size(); i++) {
|
||||
Util::addToSet (vids, tasks[i]);
|
||||
}
|
||||
|
||||
FactorGraph* mfg = fg;
|
||||
if (fg->bayesianFactors()) {
|
||||
std::set<VarId> vids;
|
||||
for (size_t i = 0; i < tasks.size(); i++) {
|
||||
Util::addToSet (vids, tasks[i]);
|
||||
}
|
||||
mfg = BayesBall::getMinimalFactorGraph (
|
||||
*fg, VarIds (vids.begin(), vids.end()));
|
||||
}
|
||||
|
@ -18,17 +18,13 @@ AndNode::weight (void) const
|
||||
{
|
||||
double lw = leftBranch_->weight();
|
||||
double rw = rightBranch_->weight();
|
||||
if (Globals::logDomain) {
|
||||
// cout << "andw1 = " << std::exp(lw + rw) << endl;
|
||||
} else {
|
||||
// cout << "andw2 = " << lw * rw << endl;
|
||||
}
|
||||
return Globals::logDomain ? lw + rw : lw * rw;
|
||||
}
|
||||
|
||||
|
||||
|
||||
stack<pair<unsigned, unsigned>> SetOrNode::nrGrsStack;
|
||||
int SetOrNode::nrPos_ = -1;
|
||||
int SetOrNode::nrNeg_ = -1;
|
||||
|
||||
|
||||
|
||||
@ -37,7 +33,8 @@ SetOrNode::weight (void) const
|
||||
{
|
||||
double weightSum = LogAware::addIdenty();
|
||||
for (unsigned i = 0; i < nrGroundings_ + 1; i++) {
|
||||
nrGrsStack.push (make_pair (nrGroundings_ - i, i));
|
||||
nrPos_ = nrGroundings_ - i;
|
||||
nrNeg_ = i;
|
||||
if (Globals::logDomain) {
|
||||
double nrCombs = Util::nrCombinations (nrGroundings_, i);
|
||||
double w = follow_->weight();
|
||||
@ -47,6 +44,8 @@ SetOrNode::weight (void) const
|
||||
weightSum += Util::nrCombinations (nrGroundings_, i) * w;
|
||||
}
|
||||
}
|
||||
nrPos_ = -1;
|
||||
nrNeg_ = -1;
|
||||
return weightSum;
|
||||
}
|
||||
|
||||
@ -55,10 +54,7 @@ SetOrNode::weight (void) const
|
||||
double
|
||||
SetAndNode::weight (void) const
|
||||
{
|
||||
double w = follow_->weight();
|
||||
return Globals::logDomain
|
||||
? w * nrGroundings_
|
||||
: std::pow (w, nrGroundings_);
|
||||
return LogAware::pow (follow_->weight(), nrGroundings_);
|
||||
}
|
||||
|
||||
|
||||
@ -82,33 +78,37 @@ IncExcNode::weight (void) const
|
||||
double
|
||||
LeafNode::weight (void) const
|
||||
{
|
||||
assert (clauses().size() == 1);
|
||||
assert (clauses()[0].isUnit());
|
||||
Clause c = clauses()[0];
|
||||
double weight = c.literals()[0].isPositive()
|
||||
? lwcnf_.posWeight (c.literals().front().lid())
|
||||
: lwcnf_.negWeight (c.literals().front().lid());
|
||||
LogVarSet lvs = c.constr().logVarSet();
|
||||
lvs -= c.ipgLogVars();
|
||||
lvs -= c.posCountedLogVars();
|
||||
lvs -= c.negCountedLogVars();
|
||||
assert (clause_->isUnit());
|
||||
if (clause_->posCountedLogVars().empty() == false
|
||||
|| clause_->negCountedLogVars().empty() == false) {
|
||||
if (SetOrNode::isSet() == false) {
|
||||
// return a NaN if we have a SetOrNode
|
||||
// ancester that is not set. This can only
|
||||
// happen when calculating the weights
|
||||
// for the edge labels in graphviz
|
||||
return 0.0 / 0.0;
|
||||
}
|
||||
}
|
||||
double weight = clause_->literals()[0].isPositive()
|
||||
? lwcnf_.posWeight (clause_->literals().front().lid())
|
||||
: lwcnf_.negWeight (clause_->literals().front().lid());
|
||||
LogVarSet lvs = clause_->constr().logVarSet();
|
||||
lvs -= clause_->ipgLogVars();
|
||||
lvs -= clause_->posCountedLogVars();
|
||||
lvs -= clause_->negCountedLogVars();
|
||||
unsigned nrGroundings = 1;
|
||||
if (lvs.empty() == false) {
|
||||
ConstraintTree ct = c.constr();
|
||||
ct.project (lvs);
|
||||
nrGroundings = ct.size();
|
||||
nrGroundings = clause_->constr().projectedCopy (lvs).size();
|
||||
}
|
||||
if (c.posCountedLogVars().empty() == false) {
|
||||
if (clause_->posCountedLogVars().empty() == false) {
|
||||
nrGroundings *= std::pow (SetOrNode::nrPositives(),
|
||||
c.nrPosCountedLogVars());
|
||||
clause_->nrPosCountedLogVars());
|
||||
}
|
||||
if (c.negCountedLogVars().empty() == false) {
|
||||
if (clause_->negCountedLogVars().empty() == false) {
|
||||
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
|
||||
c.nrNegCountedLogVars());
|
||||
clause_->nrNegCountedLogVars());
|
||||
}
|
||||
return Globals::logDomain
|
||||
? weight * nrGroundings
|
||||
: std::pow (weight, nrGroundings);
|
||||
return LogAware::pow (weight, nrGroundings);
|
||||
}
|
||||
|
||||
|
||||
@ -119,25 +119,23 @@ SmoothNode::weight (void) const
|
||||
Clauses cs = clauses();
|
||||
double totalWeight = LogAware::multIdenty();
|
||||
for (size_t i = 0; i < cs.size(); i++) {
|
||||
double posWeight = lwcnf_.posWeight (cs[i].literals()[0].lid());
|
||||
double negWeight = lwcnf_.negWeight (cs[i].literals()[0].lid());
|
||||
LogVarSet lvs = cs[i].constr().logVarSet();
|
||||
lvs -= cs[i].ipgLogVars();
|
||||
lvs -= cs[i].posCountedLogVars();
|
||||
lvs -= cs[i].negCountedLogVars();
|
||||
double posWeight = lwcnf_.posWeight (cs[i]->literals()[0].lid());
|
||||
double negWeight = lwcnf_.negWeight (cs[i]->literals()[0].lid());
|
||||
LogVarSet lvs = cs[i]->constr().logVarSet();
|
||||
lvs -= cs[i]->ipgLogVars();
|
||||
lvs -= cs[i]->posCountedLogVars();
|
||||
lvs -= cs[i]->negCountedLogVars();
|
||||
unsigned nrGroundings = 1;
|
||||
if (lvs.empty() == false) {
|
||||
ConstraintTree ct = cs[i].constr();
|
||||
ct.project (lvs);
|
||||
nrGroundings = ct.size();
|
||||
nrGroundings = cs[i]->constr().projectedCopy (lvs).size();
|
||||
}
|
||||
if (cs[i].posCountedLogVars().empty() == false) {
|
||||
if (cs[i]->posCountedLogVars().empty() == false) {
|
||||
nrGroundings *= std::pow (SetOrNode::nrPositives(),
|
||||
cs[i].nrPosCountedLogVars());
|
||||
cs[i]->nrPosCountedLogVars());
|
||||
}
|
||||
if (cs[i].negCountedLogVars().empty() == false) {
|
||||
if (cs[i]->negCountedLogVars().empty() == false) {
|
||||
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
|
||||
cs[i].nrNegCountedLogVars());
|
||||
cs[i]->nrNegCountedLogVars());
|
||||
}
|
||||
if (Globals::logDomain) {
|
||||
totalWeight += Util::logSum (posWeight, negWeight) * nrGroundings;
|
||||
@ -161,10 +159,9 @@ TrueNode::weight (void) const
|
||||
double
|
||||
CompilationFailedNode::weight (void) const
|
||||
{
|
||||
// we should not perform model counting
|
||||
// in compilation failed nodes
|
||||
// abort();
|
||||
return 0.0;
|
||||
// weighted model counting in compilation
|
||||
// failed nodes should give NaN
|
||||
return 0.0 / 0.0;
|
||||
}
|
||||
|
||||
|
||||
@ -173,15 +170,29 @@ LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
|
||||
: lwcnf_(lwcnf)
|
||||
{
|
||||
root_ = 0;
|
||||
Clauses clauses = lwcnf->clauses();
|
||||
compilationSucceeded_ = true;
|
||||
Clauses clauses = Clause::copyClauses (lwcnf->clauses());
|
||||
compile (&root_, clauses);
|
||||
exportToGraphViz("circuit.dot");
|
||||
smoothCircuit (root_);
|
||||
exportToGraphViz("circuit.smooth.dot");
|
||||
cout << "--------------------------------------------------" << endl;
|
||||
cout << "--------------------------------------------------" << endl;
|
||||
double wmc = LogAware::exp (getWeightedModelCount());
|
||||
cout << "WEIGHTED MODEL COUNT = " << wmc << endl;
|
||||
if (compilationSucceeded_) {
|
||||
smoothCircuit (root_);
|
||||
}
|
||||
if (Globals::verbosity > 1) {
|
||||
if (compilationSucceeded_) {
|
||||
double wmc = LogAware::exp (getWeightedModelCount());
|
||||
cout << "Weighted model count = " << wmc << endl << endl;
|
||||
}
|
||||
cout << "Exporting circuit to graphviz (circuit.dot)..." ;
|
||||
cout << endl << endl;
|
||||
exportToGraphViz ("circuit.dot");
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool
|
||||
LiftedCircuit::isCompilationSucceeded (void) const
|
||||
{
|
||||
return compilationSucceeded_;
|
||||
}
|
||||
|
||||
|
||||
@ -189,6 +200,7 @@ LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
|
||||
double
|
||||
LiftedCircuit::getWeightedModelCount (void) const
|
||||
{
|
||||
assert (compilationSucceeded_);
|
||||
return root_->weight();
|
||||
}
|
||||
|
||||
@ -217,12 +229,17 @@ LiftedCircuit::compile (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
if (compilationSucceeded_ == false
|
||||
&& Globals::verbosity <= 1) {
|
||||
return;
|
||||
}
|
||||
|
||||
if (clauses.empty()) {
|
||||
*follow = new TrueNode ();
|
||||
*follow = new TrueNode();
|
||||
return;
|
||||
}
|
||||
|
||||
if (clauses.size() == 1 && clauses[0].isUnit()) {
|
||||
if (clauses.size() == 1 && clauses[0]->isUnit()) {
|
||||
*follow = new LeafNode (clauses[0], *lwcnf_);
|
||||
return;
|
||||
}
|
||||
@ -251,12 +268,12 @@ LiftedCircuit::compile (
|
||||
return;
|
||||
}
|
||||
|
||||
if (tryGrounding (follow, clauses)) {
|
||||
return;
|
||||
*follow = new CompilationFailedNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[*follow] = clauses;
|
||||
explanationMap_[*follow] = "" ;
|
||||
}
|
||||
|
||||
// assert (false);
|
||||
*follow = new CompilationFailedNode (clauses);
|
||||
compilationSucceeded_ = false;
|
||||
}
|
||||
|
||||
|
||||
@ -266,37 +283,53 @@ LiftedCircuit::tryUnitPropagation (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
// cout << "ALL CLAUSES:" << endl;
|
||||
// Clause::printClauses (clauses);
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = Clause::copyClauses (clauses);
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
if (clauses[i].isUnit()) {
|
||||
// cout << clauses[i] << " is unit!" << endl;
|
||||
Clauses newClauses;
|
||||
if (clauses[i]->isUnit()) {
|
||||
Clauses propagClauses;
|
||||
for (size_t j = 0; j < clauses.size(); j++) {
|
||||
if (i != j) {
|
||||
LiteralId lid = clauses[i].literals()[0].lid();
|
||||
LogVarTypes types = clauses[i].logVarTypes (0);
|
||||
if (clauses[i].literals()[0].isPositive()) {
|
||||
if (clauses[j].containsPositiveLiteral (lid, types) == false) {
|
||||
Clause newClause = clauses[j];
|
||||
newClause.removeNegativeLiterals (lid, types);
|
||||
newClauses.push_back (newClause);
|
||||
}
|
||||
} else if (clauses[i].literals()[0].isNegative()) {
|
||||
if (clauses[j].containsNegativeLiteral (lid, types) == false) {
|
||||
Clause newClause = clauses[j];
|
||||
newClause.removePositiveLiterals (lid, types);
|
||||
newClauses.push_back (newClause);
|
||||
LiteralId lid = clauses[i]->literals()[0].lid();
|
||||
LogVarTypes types = clauses[i]->logVarTypes (0);
|
||||
if (clauses[i]->literals()[0].isPositive()) {
|
||||
if (clauses[j]->containsPositiveLiteral (lid, types) == false) {
|
||||
clauses[j]->removeNegativeLiterals (lid, types);
|
||||
if (clauses[j]->nrLiterals() > 0) {
|
||||
propagClauses.push_back (clauses[j]);
|
||||
} else {
|
||||
delete clauses[j];
|
||||
}
|
||||
} else {
|
||||
delete clauses[j];
|
||||
}
|
||||
} else if (clauses[i]->literals()[0].isNegative()) {
|
||||
if (clauses[j]->containsNegativeLiteral (lid, types) == false) {
|
||||
clauses[j]->removePositiveLiterals (lid, types);
|
||||
if (clauses[j]->nrLiterals() > 0) {
|
||||
propagClauses.push_back (clauses[j]);
|
||||
} else {
|
||||
delete clauses[j];
|
||||
}
|
||||
} else {
|
||||
delete clauses[j];
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
stringstream explanation;
|
||||
explanation << " UP on" << clauses[i].literals()[0];
|
||||
AndNode* andNode = new AndNode (clauses, explanation.str());
|
||||
Clauses leftClauses = {clauses[i]};
|
||||
compile (andNode->leftBranch(), leftClauses);
|
||||
compile (andNode->rightBranch(), newClauses);
|
||||
|
||||
AndNode* andNode = new AndNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[andNode] = backupClauses_;
|
||||
stringstream explanation;
|
||||
explanation << " UP on " << clauses[i]->literals()[0];
|
||||
explanationMap_[andNode] = explanation.str();
|
||||
}
|
||||
|
||||
Clauses unitClause = { clauses[i] };
|
||||
compile (andNode->leftBranch(), unitClause);
|
||||
compile (andNode->rightBranch(), propagClauses);
|
||||
(*follow) = andNode;
|
||||
return true;
|
||||
}
|
||||
@ -314,13 +347,16 @@ LiftedCircuit::tryIndependence (
|
||||
if (clauses.size() == 1) {
|
||||
return false;
|
||||
}
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = Clause::copyClauses (clauses);
|
||||
}
|
||||
Clauses depClauses = { clauses[0] };
|
||||
Clauses indepClauses (clauses.begin() + 1, clauses.end());
|
||||
bool finish = false;
|
||||
while (finish == false) {
|
||||
finish = true;
|
||||
for (size_t i = 0; i < indepClauses.size(); i++) {
|
||||
if (independentClause (indepClauses[i], depClauses) == false) {
|
||||
if (independentClause (*indepClauses[i], depClauses) == false) {
|
||||
depClauses.push_back (indepClauses[i]);
|
||||
indepClauses.erase (indepClauses.begin() + i);
|
||||
finish = false;
|
||||
@ -329,7 +365,11 @@ LiftedCircuit::tryIndependence (
|
||||
}
|
||||
}
|
||||
if (indepClauses.empty() == false) {
|
||||
AndNode* andNode = new AndNode (clauses, " Independence");
|
||||
AndNode* andNode = new AndNode ();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[andNode] = backupClauses_;
|
||||
explanationMap_[andNode] = " Independence" ;
|
||||
}
|
||||
compile (andNode->leftBranch(), depClauses);
|
||||
compile (andNode->rightBranch(), indepClauses);
|
||||
(*follow) = andNode;
|
||||
@ -345,27 +385,33 @@ LiftedCircuit::tryShannonDecomp (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = Clause::copyClauses (clauses);
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
const Literals& literals = clauses[i].literals();
|
||||
const Literals& literals = clauses[i]->literals();
|
||||
for (size_t j = 0; j < literals.size(); j++) {
|
||||
if (literals[j].isGround (clauses[i].constr(),clauses[i].ipgLogVars())) {
|
||||
Literal posLit (literals[j], false);
|
||||
Literal negLit (literals[j], true);
|
||||
ConstraintTree ct1 = clauses[i].constr();
|
||||
ConstraintTree ct2 = clauses[i].constr();
|
||||
Clause c1 (ct1);
|
||||
Clause c2 (ct2);
|
||||
c1.addLiteral (posLit);
|
||||
c2.addLiteral (negLit);
|
||||
Clauses leftClauses = { c1 };
|
||||
Clauses rightClauses = { c2 };
|
||||
leftClauses.insert (leftClauses.end(), clauses.begin(), clauses.end());
|
||||
rightClauses.insert (rightClauses.end(), clauses.begin(), clauses.end());
|
||||
stringstream explanation;
|
||||
explanation << " SD on " << literals[j];
|
||||
OrNode* orNode = new OrNode (clauses, explanation.str());
|
||||
compile (orNode->leftBranch(), leftClauses);
|
||||
compile (orNode->rightBranch(), rightClauses);
|
||||
if (literals[j].isGround (
|
||||
clauses[i]->constr(), clauses[i]->ipgLogVars())) {
|
||||
|
||||
Clause* c1 = lwcnf_->createClause (literals[j].lid());
|
||||
Clause* c2 = new Clause (*c1);
|
||||
c2->literals().front().complement();
|
||||
|
||||
Clauses otherClauses = Clause::copyClauses (clauses);
|
||||
clauses.push_back (c1);
|
||||
otherClauses.push_back (c2);
|
||||
|
||||
OrNode* orNode = new OrNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[orNode] = backupClauses_;
|
||||
stringstream explanation;
|
||||
explanation << " SD on " << literals[j];
|
||||
explanationMap_[orNode] = explanation.str();
|
||||
}
|
||||
|
||||
compile (orNode->leftBranch(), clauses);
|
||||
compile (orNode->rightBranch(), otherClauses);
|
||||
(*follow) = orNode;
|
||||
return true;
|
||||
}
|
||||
@ -381,10 +427,13 @@ LiftedCircuit::tryInclusionExclusion (
|
||||
CircuitNode** follow,
|
||||
Clauses& clauses)
|
||||
{
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = Clause::copyClauses (clauses);
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
Literals depLits = { clauses[i].literals().front() };
|
||||
Literals indepLits (clauses[i].literals().begin() + 1,
|
||||
clauses[i].literals().end());
|
||||
Literals depLits = { clauses[i]->literals().front() };
|
||||
Literals indepLits (clauses[i]->literals().begin() + 1,
|
||||
clauses[i]->literals().end());
|
||||
bool finish = false;
|
||||
while (finish == false) {
|
||||
finish = true;
|
||||
@ -402,40 +451,44 @@ LiftedCircuit::tryInclusionExclusion (
|
||||
for (size_t j = 0; j < depLits.size(); j++) {
|
||||
lvs1 |= depLits[j].logVarSet();
|
||||
}
|
||||
if (clauses[i].constr().isCountNormalized (lvs1) == false) {
|
||||
if (clauses[i]->constr().isCountNormalized (lvs1) == false) {
|
||||
break;
|
||||
}
|
||||
LogVarSet lvs2;
|
||||
for (size_t j = 0; j < indepLits.size(); j++) {
|
||||
lvs2 |= indepLits[j].logVarSet();
|
||||
}
|
||||
if (clauses[i].constr().isCountNormalized (lvs2) == false) {
|
||||
if (clauses[i]->constr().isCountNormalized (lvs2) == false) {
|
||||
break;
|
||||
}
|
||||
Clause c1 (clauses[i].constr().projectedCopy (lvs1));
|
||||
Clause* c1 = new Clause (clauses[i]->constr().projectedCopy (lvs1));
|
||||
for (size_t j = 0; j < depLits.size(); j++) {
|
||||
c1.addLiteral (depLits[j]);
|
||||
c1->addLiteral (depLits[j]);
|
||||
}
|
||||
Clause c2 (clauses[i].constr().projectedCopy (lvs2));
|
||||
Clause* c2 = new Clause (clauses[i]->constr().projectedCopy (lvs2));
|
||||
for (size_t j = 0; j < indepLits.size(); j++) {
|
||||
c2.addLiteral (indepLits[j]);
|
||||
c2->addLiteral (indepLits[j]);
|
||||
}
|
||||
Clauses plus1Clauses = clauses;
|
||||
Clauses plus2Clauses = clauses;
|
||||
Clauses minusClauses = clauses;
|
||||
plus1Clauses.erase (plus1Clauses.begin() + i);
|
||||
plus2Clauses.erase (plus2Clauses.begin() + i);
|
||||
minusClauses.erase (minusClauses.begin() + i);
|
||||
|
||||
clauses.erase (clauses.begin() + i);
|
||||
Clauses plus1Clauses = Clause::copyClauses (clauses);
|
||||
Clauses plus2Clauses = Clause::copyClauses (clauses);
|
||||
|
||||
plus1Clauses.push_back (c1);
|
||||
plus2Clauses.push_back (c2);
|
||||
minusClauses.push_back (c1);
|
||||
minusClauses.push_back (c2);
|
||||
stringstream explanation;
|
||||
explanation << " IncExc on clause nº " << i + 1;
|
||||
IncExcNode* ieNode = new IncExcNode (clauses, explanation.str());
|
||||
clauses.push_back (c1);
|
||||
clauses.push_back (c2);
|
||||
|
||||
IncExcNode* ieNode = new IncExcNode();
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[ieNode] = backupClauses_;
|
||||
stringstream explanation;
|
||||
explanation << " IncExc on clause nº " << i + 1;
|
||||
explanationMap_[ieNode] = explanation.str();
|
||||
}
|
||||
compile (ieNode->plus1Branch(), plus1Clauses);
|
||||
compile (ieNode->plus2Branch(), plus2Clauses);
|
||||
compile (ieNode->minusBranch(), minusClauses);
|
||||
compile (ieNode->minusBranch(), clauses);
|
||||
*follow = ieNode;
|
||||
return true;
|
||||
}
|
||||
@ -452,20 +505,26 @@ LiftedCircuit::tryIndepPartialGrounding (
|
||||
{
|
||||
// assumes that all literals have logical variables
|
||||
// else, shannon decomp was possible
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = Clause::copyClauses (clauses);
|
||||
}
|
||||
LogVars rootLogVars;
|
||||
LogVarSet lvs = clauses[0].ipgCandidates();
|
||||
LogVarSet lvs = clauses[0]->ipgCandidates();
|
||||
for (size_t i = 0; i < lvs.size(); i++) {
|
||||
rootLogVars.clear();
|
||||
rootLogVars.push_back (lvs[i]);
|
||||
ConstraintTree ct = clauses[0].constr().projectedCopy ({lvs[i]});
|
||||
ConstraintTree ct = clauses[0]->constr().projectedCopy ({lvs[i]});
|
||||
if (tryIndepPartialGroundingAux (clauses, ct, rootLogVars)) {
|
||||
Clauses newClauses = clauses;
|
||||
for (size_t j = 0; j < clauses.size(); j++) {
|
||||
newClauses[j].addIpgLogVar (rootLogVars[j]);
|
||||
clauses[j]->addIpgLogVar (rootLogVars[j]);
|
||||
}
|
||||
SetAndNode* node = new SetAndNode (ct.size(), clauses);
|
||||
*follow = node;
|
||||
compile (node->follow(), newClauses);
|
||||
SetAndNode* setAndNode = new SetAndNode (ct.size());
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[setAndNode] = backupClauses_;
|
||||
explanationMap_[setAndNode] = " IPG" ;
|
||||
}
|
||||
*follow = setAndNode;
|
||||
compile (setAndNode->follow(), clauses);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
@ -481,9 +540,9 @@ LiftedCircuit::tryIndepPartialGroundingAux (
|
||||
LogVars& rootLogVars)
|
||||
{
|
||||
for (size_t i = 1; i < clauses.size(); i++) {
|
||||
LogVarSet lvs = clauses[i].ipgCandidates();
|
||||
LogVarSet lvs = clauses[i]->ipgCandidates();
|
||||
for (size_t j = 0; j < lvs.size(); j++) {
|
||||
ConstraintTree ct2 = clauses[i].constr().projectedCopy ({lvs[j]});
|
||||
ConstraintTree ct2 = clauses[i]->constr().projectedCopy ({lvs[j]});
|
||||
if (ct.tupleSet() == ct2.tupleSet()) {
|
||||
rootLogVars.push_back (lvs[j]);
|
||||
break;
|
||||
@ -496,7 +555,7 @@ LiftedCircuit::tryIndepPartialGroundingAux (
|
||||
// verifies if the IPG logical vars appear in the same positions
|
||||
unordered_map<LiteralId, size_t> positions;
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
const Literals& literals = clauses[i].literals();
|
||||
const Literals& literals = clauses[i]->literals();
|
||||
for (size_t j = 0; j < literals.size(); j++) {
|
||||
size_t idx = literals[j].indexOfLogVar (rootLogVars[i]);
|
||||
assert (idx != literals[j].nrLogVars());
|
||||
@ -522,27 +581,36 @@ LiftedCircuit::tryAtomCounting (
|
||||
Clauses& clauses)
|
||||
{
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
if (clauses[i].nrPosCountedLogVars() > 0
|
||||
|| clauses[i].nrNegCountedLogVars() > 0) {
|
||||
if (clauses[i]->nrPosCountedLogVars() > 0
|
||||
|| clauses[i]->nrNegCountedLogVars() > 0) {
|
||||
// only allow one atom counting node per branch
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if (Globals::verbosity > 1) {
|
||||
backupClauses_ = Clause::copyClauses (clauses);
|
||||
}
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
Literals literals = clauses[i].literals();
|
||||
Literals literals = clauses[i]->literals();
|
||||
for (size_t j = 0; j < literals.size(); j++) {
|
||||
if (literals[j].nrLogVars() == 1
|
||||
&& ! clauses[i].isIpgLogVar (literals[j].logVars().front())
|
||||
&& ! clauses[i].isCountedLogVar (literals[j].logVars().front())) {
|
||||
unsigned nrGroundings = clauses[i].constr().projectedCopy (
|
||||
&& ! clauses[i]->isIpgLogVar (literals[j].logVars().front())
|
||||
&& ! clauses[i]->isCountedLogVar (literals[j].logVars().front())) {
|
||||
unsigned nrGroundings = clauses[i]->constr().projectedCopy (
|
||||
literals[j].logVars()).size();
|
||||
SetOrNode* setOrNode = new SetOrNode (nrGroundings, clauses);
|
||||
Clause c1 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
||||
Clause c2 (clauses[i].constr().projectedCopy (literals[j].logVars()));
|
||||
c1.addLiteral (literals[j]);
|
||||
c2.addLiteralComplemented (literals[j]);
|
||||
c1.addPosCountedLogVar (literals[j].logVars().front());
|
||||
c2.addNegCountedLogVar (literals[j].logVars().front());
|
||||
SetOrNode* setOrNode = new SetOrNode (nrGroundings);
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[setOrNode] = backupClauses_;
|
||||
explanationMap_[setOrNode] = " AC" ;
|
||||
}
|
||||
Clause* c1 = new Clause (
|
||||
clauses[i]->constr().projectedCopy (literals[j].logVars()));
|
||||
Clause* c2 = new Clause (
|
||||
clauses[i]->constr().projectedCopy (literals[j].logVars()));
|
||||
c1->addLiteral (literals[j]);
|
||||
c2->addLiteralComplemented (literals[j]);
|
||||
c1->addPosCountedLogVar (literals[j].logVars().front());
|
||||
c2->addNegCountedLogVar (literals[j].logVars().front());
|
||||
clauses.push_back (c1);
|
||||
clauses.push_back (c2);
|
||||
shatterCountedLogVars (clauses);
|
||||
@ -557,36 +625,6 @@ LiftedCircuit::tryAtomCounting (
|
||||
|
||||
|
||||
|
||||
bool
|
||||
LiftedCircuit::tryGrounding (
|
||||
CircuitNode**,
|
||||
Clauses&)
|
||||
{
|
||||
return false;
|
||||
/*
|
||||
size_t bestClauseIdx = 0;
|
||||
size_t bestLogVarIdx = 0;
|
||||
unsigned minNrSymbols = Util::maxUnsigned();
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
LogVarSet lvs = clauses[i].constr().logVars();
|
||||
ConstraintTree ct = clauses[i].constr();
|
||||
for (unsigned j = 0; j < lvs.size(); j++) {
|
||||
unsigned nrSymbols = ct.nrSymbols (lvs[j]);
|
||||
if (nrSymbols < minNrSymbols) {
|
||||
minNrSymbols = nrSymbols;
|
||||
bestClauseIdx = i;
|
||||
bestLogVarIdx = j;
|
||||
}
|
||||
}
|
||||
}
|
||||
LogVar bestLogVar = clauses[bestClauseIdx].constr().logVars()[bestLogVarIdx];
|
||||
ConstraintTrees cts = clauses[bestClauseIdx].constr().ground (bestLogVar);
|
||||
return true;
|
||||
*/
|
||||
}
|
||||
|
||||
|
||||
|
||||
void
|
||||
LiftedCircuit::shatterCountedLogVars (Clauses& clauses)
|
||||
{
|
||||
@ -617,26 +655,26 @@ LiftedCircuit::shatterCountedLogVarsAux (
|
||||
size_t idx1,
|
||||
size_t idx2)
|
||||
{
|
||||
Literals lits1 = clauses[idx1].literals();
|
||||
Literals lits2 = clauses[idx2].literals();
|
||||
Literals lits1 = clauses[idx1]->literals();
|
||||
Literals lits2 = clauses[idx2]->literals();
|
||||
for (size_t i = 0; i < lits1.size(); i++) {
|
||||
for (size_t j = 0; j < lits2.size(); j++) {
|
||||
if (lits1[i].lid() == lits2[j].lid()) {
|
||||
LogVars lvs1 = lits1[i].logVars();
|
||||
LogVars lvs2 = lits2[j].logVars();
|
||||
for (size_t k = 0; k < lvs1.size(); k++) {
|
||||
if (clauses[idx1].isCountedLogVar (lvs1[k])
|
||||
&& clauses[idx2].isCountedLogVar (lvs2[k]) == false) {
|
||||
clauses.push_back (clauses[idx2]);
|
||||
clauses[idx2].addPosCountedLogVar (lvs2[k]);
|
||||
clauses.back().addNegCountedLogVar (lvs2[k]);
|
||||
if (clauses[idx1]->isCountedLogVar (lvs1[k])
|
||||
&& clauses[idx2]->isCountedLogVar (lvs2[k]) == false) {
|
||||
clauses.push_back (new Clause (*clauses[idx2]));
|
||||
clauses[idx2]->addPosCountedLogVar (lvs2[k]);
|
||||
clauses.back()->addNegCountedLogVar (lvs2[k]);
|
||||
return true;
|
||||
}
|
||||
if (clauses[idx2].isCountedLogVar (lvs2[k])
|
||||
&& clauses[idx1].isCountedLogVar (lvs1[k]) == false) {
|
||||
clauses.push_back (clauses[idx1]);
|
||||
clauses[idx1].addPosCountedLogVar (lvs1[k]);
|
||||
clauses.back().addNegCountedLogVar (lvs1[k]);
|
||||
if (clauses[idx2]->isCountedLogVar (lvs2[k])
|
||||
&& clauses[idx1]->isCountedLogVar (lvs1[k]) == false) {
|
||||
clauses.push_back (new Clause (*clauses[idx1]));
|
||||
clauses[idx1]->addPosCountedLogVar (lvs1[k]);
|
||||
clauses.back()->addNegCountedLogVar (lvs1[k]);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
@ -654,7 +692,7 @@ LiftedCircuit::independentClause (
|
||||
Clauses& otherClauses) const
|
||||
{
|
||||
for (size_t i = 0; i < otherClauses.size(); i++) {
|
||||
if (Clause::independentClauses (clause, otherClauses[i]) == false) {
|
||||
if (Clause::independentClauses (clause, *otherClauses[i]) == false) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
@ -699,7 +737,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
||||
propagLits |= lids2;
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
case CircuitNodeType::AND_NODE: {
|
||||
AndNode* casted = dynamic_cast<AndNode*>(node);
|
||||
LitLvTypesSet lids1 = smoothCircuit (*casted->leftBranch());
|
||||
@ -724,7 +762,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
||||
bool typeFound = false;
|
||||
for (size_t k = 0; k < propagLits.size(); k++) {
|
||||
if (litSet[i].first == propagLits[k].lid()
|
||||
&& containsTypes (allTypes[j], propagLits[k].logVarTypes())) {
|
||||
&& containsTypes (propagLits[k].logVarTypes(), allTypes[j])) {
|
||||
typeFound = true;
|
||||
break;
|
||||
}
|
||||
@ -735,18 +773,23 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
||||
}
|
||||
}
|
||||
createSmoothNode (missingLids, casted->follow());
|
||||
for (size_t i = 0; i < propagLits.size(); i++) {
|
||||
propagLits[i].setAllFullLogVars();
|
||||
// setAllFullLogVars() can cause repeated elements in
|
||||
// the set. Fix this by reconstructing the set again
|
||||
LitLvTypesSet copy = propagLits;
|
||||
propagLits.clear();
|
||||
for (size_t i = 0; i < copy.size(); i++) {
|
||||
copy[i].setAllFullLogVars();
|
||||
propagLits.insert (copy[i]);
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
case CircuitNodeType::SET_AND_NODE: {
|
||||
SetAndNode* casted = dynamic_cast<SetAndNode*>(node);
|
||||
propagLits = smoothCircuit (*casted->follow());
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
case CircuitNodeType::INC_EXC_NODE: {
|
||||
IncExcNode* casted = dynamic_cast<IncExcNode*>(node);
|
||||
LitLvTypesSet lids1 = smoothCircuit (*casted->plus1Branch());
|
||||
@ -759,17 +802,18 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
||||
propagLits |= lids2;
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
case CircuitNodeType::LEAF_NODE: {
|
||||
LeafNode* casted = dynamic_cast<LeafNode*>(node);
|
||||
propagLits.insert (LitLvTypes (
|
||||
node->clauses()[0].literals()[0].lid(),
|
||||
node->clauses()[0].logVarTypes(0)));
|
||||
casted->clause()->literals()[0].lid(),
|
||||
casted->clause()->logVarTypes(0)));
|
||||
}
|
||||
|
||||
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
return propagLits;
|
||||
}
|
||||
|
||||
@ -781,25 +825,38 @@ LiftedCircuit::createSmoothNode (
|
||||
CircuitNode** prev)
|
||||
{
|
||||
if (missingLits.empty() == false) {
|
||||
if (Globals::verbosity > 1) {
|
||||
unordered_map<CircuitNode*, Clauses>::iterator it;
|
||||
it = originClausesMap_.find (*prev);
|
||||
if (it != originClausesMap_.end()) {
|
||||
backupClauses_ = it->second;
|
||||
} else {
|
||||
backupClauses_ = Clause::copyClauses (
|
||||
{((dynamic_cast<LeafNode*>(*prev))->clause())});
|
||||
}
|
||||
}
|
||||
Clauses clauses;
|
||||
for (size_t i = 0; i < missingLits.size(); i++) {
|
||||
LiteralId lid = missingLits[i].lid();
|
||||
const LogVarTypes& types = missingLits[i].logVarTypes();
|
||||
Clause c = lwcnf_->createClause (lid);
|
||||
Clause* c = lwcnf_->createClause (lid);
|
||||
for (size_t j = 0; j < types.size(); j++) {
|
||||
LogVar X = c.literals().front().logVars()[j];
|
||||
LogVar X = c->literals().front().logVars()[j];
|
||||
if (types[j] == LogVarType::POS_LV) {
|
||||
c.addPosCountedLogVar (X);
|
||||
c->addPosCountedLogVar (X);
|
||||
} else if (types[j] == LogVarType::NEG_LV) {
|
||||
c.addNegCountedLogVar (X);
|
||||
c->addNegCountedLogVar (X);
|
||||
}
|
||||
}
|
||||
c.addLiteralComplemented (c.literals()[0]);
|
||||
c->addLiteralComplemented (c->literals()[0]);
|
||||
clauses.push_back (c);
|
||||
}
|
||||
SmoothNode* smoothNode = new SmoothNode (clauses, *lwcnf_);
|
||||
*prev = new AndNode ((*prev)->clauses(), smoothNode,
|
||||
*prev, " Smoothing");
|
||||
*prev = new AndNode (smoothNode, *prev);
|
||||
if (Globals::verbosity > 1) {
|
||||
originClausesMap_[*prev] = backupClauses_;
|
||||
explanationMap_[*prev] = " Smoothing" ;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -815,7 +872,8 @@ LiftedCircuit::getAllPossibleTypes (unsigned nrLogVars) const
|
||||
return {{LogVarType::POS_LV},{LogVarType::NEG_LV}};
|
||||
}
|
||||
vector<LogVarTypes> res;
|
||||
Indexer indexer (vector<unsigned> (nrLogVars, 2));
|
||||
Ranges ranges (nrLogVars, 2);
|
||||
Indexer indexer (ranges);
|
||||
while (indexer.valid()) {
|
||||
LogVarTypes types;
|
||||
for (size_t i = 0; i < nrLogVars; i++) {
|
||||
@ -906,7 +964,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∨\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -930,7 +988,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∧\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -954,7 +1012,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∨(X)\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -972,7 +1030,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
|
||||
os << auxNode << " [" << opStyle << "label=\"∧(X)\"]" << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -991,7 +1049,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
|
||||
os << auxNode << " [" << opStyle << "label=\"+ - +\"]" ;
|
||||
os << endl;
|
||||
os << escapeNode (node) << " -> " << auxNode;
|
||||
os << " [label=\"" << node->explanation() << "\"]" ;
|
||||
os << " [label=\"" << getExplanationString (node) << "\"]" ;
|
||||
os << endl;
|
||||
|
||||
os << auxNode << " -> " ;
|
||||
@ -1054,22 +1112,38 @@ LiftedCircuit::escapeNode (const CircuitNode* node) const
|
||||
|
||||
|
||||
|
||||
string
|
||||
LiftedCircuit::getExplanationString (CircuitNode* node)
|
||||
{
|
||||
return Util::contains (explanationMap_, node)
|
||||
? explanationMap_[node]
|
||||
: "" ;
|
||||
}
|
||||
|
||||
|
||||
|
||||
void
|
||||
LiftedCircuit::printClauses (
|
||||
const CircuitNode* node,
|
||||
CircuitNode* node,
|
||||
ofstream& os,
|
||||
string extraOptions)
|
||||
{
|
||||
const Clauses& clauses = node->clauses();
|
||||
if (node->clauses().empty() == false) {
|
||||
os << escapeNode (node);
|
||||
os << " [shape=box," << extraOptions << "label=\"" ;
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
if (i != 0) os << "\\n" ;
|
||||
os << clauses[i];
|
||||
}
|
||||
os << "\"]" ;
|
||||
os << endl;
|
||||
Clauses clauses;
|
||||
if (Util::contains (originClausesMap_, node)) {
|
||||
clauses = originClausesMap_[node];
|
||||
} else if (getCircuitNodeType (node) == CircuitNodeType::LEAF_NODE) {
|
||||
clauses = { (dynamic_cast<LeafNode*>(node))->clause() } ;
|
||||
} else if (getCircuitNodeType (node) == CircuitNodeType::SMOOTH_NODE) {
|
||||
clauses = (dynamic_cast<SmoothNode*>(node))->clauses();
|
||||
}
|
||||
assert (clauses.empty() == false);
|
||||
os << escapeNode (node);
|
||||
os << " [shape=box," << extraOptions << "label=\"" ;
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
if (i != 0) os << "\\n" ;
|
||||
os << *clauses[i];
|
||||
}
|
||||
os << "\"]" ;
|
||||
os << endl;
|
||||
}
|
||||
|
||||
|
@ -23,20 +23,9 @@ enum CircuitNodeType {
|
||||
class CircuitNode
|
||||
{
|
||||
public:
|
||||
CircuitNode (const Clauses& clauses, string explanation = "")
|
||||
: clauses_(clauses), explanation_(explanation) { }
|
||||
|
||||
const Clauses& clauses (void) const { return clauses_; }
|
||||
|
||||
Clauses clauses (void) { return clauses_; }
|
||||
CircuitNode (void) { }
|
||||
|
||||
virtual double weight (void) const = 0;
|
||||
|
||||
string explanation (void) const { return explanation_; }
|
||||
|
||||
private:
|
||||
Clauses clauses_;
|
||||
string explanation_;
|
||||
};
|
||||
|
||||
|
||||
@ -44,9 +33,7 @@ class CircuitNode
|
||||
class OrNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
OrNode (const Clauses& clauses, string explanation = "")
|
||||
: CircuitNode (clauses, explanation),
|
||||
leftBranch_(0), rightBranch_(0) { }
|
||||
OrNode (void) : CircuitNode(), leftBranch_(0), rightBranch_(0) { }
|
||||
|
||||
CircuitNode** leftBranch (void) { return &leftBranch_; }
|
||||
CircuitNode** rightBranch (void) { return &rightBranch_; }
|
||||
@ -63,24 +50,10 @@ class OrNode : public CircuitNode
|
||||
class AndNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
AndNode (const Clauses& clauses, string explanation = "")
|
||||
: CircuitNode (clauses, explanation),
|
||||
leftBranch_(0), rightBranch_(0) { }
|
||||
|
||||
AndNode (
|
||||
const Clauses& clauses,
|
||||
CircuitNode* leftBranch,
|
||||
CircuitNode* rightBranch,
|
||||
string explanation = "")
|
||||
: CircuitNode (clauses, explanation),
|
||||
leftBranch_(leftBranch), rightBranch_(rightBranch) { }
|
||||
|
||||
AndNode (
|
||||
CircuitNode* leftBranch,
|
||||
CircuitNode* rightBranch,
|
||||
string explanation = "")
|
||||
: CircuitNode ({}, explanation),
|
||||
leftBranch_(leftBranch), rightBranch_(rightBranch) { }
|
||||
AndNode (void) : CircuitNode(), leftBranch_(0), rightBranch_(0) { }
|
||||
|
||||
AndNode (CircuitNode* leftBranch, CircuitNode* rightBranch)
|
||||
: CircuitNode(), leftBranch_(leftBranch), rightBranch_(rightBranch) { }
|
||||
|
||||
CircuitNode** leftBranch (void) { return &leftBranch_; }
|
||||
CircuitNode** rightBranch (void) { return &rightBranch_; }
|
||||
@ -97,23 +70,24 @@ class AndNode : public CircuitNode
|
||||
class SetOrNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
SetOrNode (unsigned nrGroundings, const Clauses& clauses)
|
||||
: CircuitNode (clauses, " AC"), follow_(0),
|
||||
nrGroundings_(nrGroundings) { }
|
||||
SetOrNode (unsigned nrGroundings)
|
||||
: CircuitNode(), follow_(0), nrGroundings_(nrGroundings) { }
|
||||
|
||||
CircuitNode** follow (void) { return &follow_; }
|
||||
|
||||
static unsigned nrPositives (void) { return nrGrsStack.top().first; }
|
||||
static unsigned nrPositives (void) { return nrPos_; }
|
||||
|
||||
static unsigned nrNegatives (void) { return nrGrsStack.top().second; }
|
||||
static unsigned nrNegatives (void) { return nrNeg_; }
|
||||
|
||||
static bool isSet (void) { return nrPos_ >= 0; }
|
||||
|
||||
double weight (void) const;
|
||||
|
||||
private:
|
||||
CircuitNode* follow_;
|
||||
unsigned nrGroundings_;
|
||||
|
||||
static stack<pair<unsigned, unsigned>> nrGrsStack;
|
||||
static int nrPos_;
|
||||
static int nrNeg_;
|
||||
};
|
||||
|
||||
|
||||
@ -121,9 +95,8 @@ class SetOrNode : public CircuitNode
|
||||
class SetAndNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
SetAndNode (unsigned nrGroundings, const Clauses& clauses)
|
||||
: CircuitNode (clauses, " IPG"), follow_(0),
|
||||
nrGroundings_(nrGroundings) { }
|
||||
SetAndNode (unsigned nrGroundings)
|
||||
: CircuitNode(), follow_(0), nrGroundings_(nrGroundings) { }
|
||||
|
||||
CircuitNode** follow (void) { return &follow_; }
|
||||
|
||||
@ -139,9 +112,8 @@ class SetAndNode : public CircuitNode
|
||||
class IncExcNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
IncExcNode (const Clauses& clauses, string explanation)
|
||||
: CircuitNode (clauses, explanation), plus1Branch_(0),
|
||||
plus2Branch_(0), minusBranch_(0) { }
|
||||
IncExcNode (void)
|
||||
: CircuitNode(), plus1Branch_(0), plus2Branch_(0), minusBranch_(0) { }
|
||||
|
||||
CircuitNode** plus1Branch (void) { return &plus1Branch_; }
|
||||
CircuitNode** plus2Branch (void) { return &plus2Branch_; }
|
||||
@ -160,12 +132,17 @@ class IncExcNode : public CircuitNode
|
||||
class LeafNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
LeafNode (const Clause& clause, const LiftedWCNF& lwcnf)
|
||||
: CircuitNode (Clauses() = {clause}), lwcnf_(lwcnf) { }
|
||||
LeafNode (Clause* clause, const LiftedWCNF& lwcnf)
|
||||
: CircuitNode(), clause_(clause), lwcnf_(lwcnf) { }
|
||||
|
||||
const Clause* clause (void) const { return clause_; }
|
||||
|
||||
Clause* clause (void) { return clause_; }
|
||||
|
||||
double weight (void) const;
|
||||
|
||||
private:
|
||||
Clause* clause_;
|
||||
const LiftedWCNF& lwcnf_;
|
||||
};
|
||||
|
||||
@ -175,11 +152,16 @@ class SmoothNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
SmoothNode (const Clauses& clauses, const LiftedWCNF& lwcnf)
|
||||
: CircuitNode (clauses), lwcnf_(lwcnf) { }
|
||||
|
||||
double weight (void) const;
|
||||
: CircuitNode(), clauses_(clauses), lwcnf_(lwcnf) { }
|
||||
|
||||
const Clauses& clauses (void) const { return clauses_; }
|
||||
|
||||
Clauses clauses (void) { return clauses_; }
|
||||
|
||||
double weight (void) const;
|
||||
|
||||
private:
|
||||
Clauses clauses_;
|
||||
const LiftedWCNF& lwcnf_;
|
||||
};
|
||||
|
||||
@ -188,7 +170,7 @@ class SmoothNode : public CircuitNode
|
||||
class TrueNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
TrueNode (void) : CircuitNode ({}) { }
|
||||
TrueNode (void) : CircuitNode() { }
|
||||
|
||||
double weight (void) const;
|
||||
};
|
||||
@ -198,8 +180,7 @@ class TrueNode : public CircuitNode
|
||||
class CompilationFailedNode : public CircuitNode
|
||||
{
|
||||
public:
|
||||
CompilationFailedNode (const Clauses& clauses)
|
||||
: CircuitNode (clauses) { }
|
||||
CompilationFailedNode (void) : CircuitNode() { }
|
||||
|
||||
double weight (void) const;
|
||||
};
|
||||
@ -209,7 +190,9 @@ class CompilationFailedNode : public CircuitNode
|
||||
class LiftedCircuit
|
||||
{
|
||||
public:
|
||||
LiftedCircuit (const LiftedWCNF* lwcnf);
|
||||
LiftedCircuit (const LiftedWCNF* lwcnf);
|
||||
|
||||
bool isCompilationSucceeded (void) const;
|
||||
|
||||
double getWeightedModelCount (void) const;
|
||||
|
||||
@ -234,8 +217,6 @@ class LiftedCircuit
|
||||
|
||||
bool tryAtomCounting (CircuitNode** follow, Clauses& clauses);
|
||||
|
||||
bool tryGrounding (CircuitNode** follow, Clauses& clauses);
|
||||
|
||||
void shatterCountedLogVars (Clauses& clauses);
|
||||
|
||||
bool shatterCountedLogVarsAux (Clauses& clauses);
|
||||
@ -261,13 +242,20 @@ class LiftedCircuit
|
||||
|
||||
void exportToGraphViz (CircuitNode* node, ofstream&);
|
||||
|
||||
void printClauses (const CircuitNode* node, ofstream&,
|
||||
void printClauses (CircuitNode* node, ofstream&,
|
||||
string extraOptions = "");
|
||||
|
||||
string escapeNode (const CircuitNode* node) const;
|
||||
|
||||
string getExplanationString (CircuitNode* node);
|
||||
|
||||
CircuitNode* root_;
|
||||
const LiftedWCNF* lwcnf_;
|
||||
|
||||
Clauses backupClauses_;
|
||||
unordered_map<CircuitNode*, Clauses> originClausesMap_;
|
||||
unordered_map<CircuitNode*, string> explanationMap_;
|
||||
bool compilationSucceeded_;
|
||||
};
|
||||
|
||||
#endif // HORUS_LIFTEDCIRCUIT_H
|
||||
|
@ -21,6 +21,10 @@ LiftedKc::solveQuery (const Grounds& query)
|
||||
LiftedOperations::runWeakBayesBall (pfList_, query);
|
||||
lwcnf_ = new LiftedWCNF (pfList_);
|
||||
circuit_ = new LiftedCircuit (lwcnf_);
|
||||
if (circuit_->isCompilationSucceeded() == false) {
|
||||
cerr << "error: compilation failed" << endl;
|
||||
abort();
|
||||
}
|
||||
vector<PrvGroup> groups;
|
||||
Ranges ranges;
|
||||
for (size_t i = 0; i < query.size(); i++) {
|
||||
|
@ -33,11 +33,6 @@ Literal::toString (
|
||||
{
|
||||
stringstream ss;
|
||||
negated_ ? ss << "¬" : ss << "" ;
|
||||
// if (negated_ == false) {
|
||||
// posWeight_ < 0.0 ? ss << "λ" : ss << "Θ" ;
|
||||
// } else {
|
||||
// negWeight_ < 0.0 ? ss << "λ" : ss << "Θ" ;
|
||||
// }
|
||||
ss << "λ" ;
|
||||
ss << lid_ ;
|
||||
if (logVars_.empty() == false) {
|
||||
@ -65,7 +60,8 @@ Literal::toString (
|
||||
|
||||
|
||||
|
||||
std::ostream& operator<< (ostream &os, const Literal& lit)
|
||||
std::ostream&
|
||||
operator<< (ostream &os, const Literal& lit)
|
||||
{
|
||||
os << lit.toString();
|
||||
return os;
|
||||
@ -261,7 +257,7 @@ LogVarTypes
|
||||
Clause::logVarTypes (size_t litIdx) const
|
||||
{
|
||||
LogVarTypes types;
|
||||
const LogVars lvs = literals_[litIdx].logVars();
|
||||
const LogVars& lvs = literals_[litIdx].logVars();
|
||||
for (size_t i = 0; i < lvs.size(); i++) {
|
||||
if (posCountedLvs_.contains (lvs[i])) {
|
||||
types.push_back (LogVarType::POS_LV);
|
||||
@ -308,17 +304,31 @@ Clause::independentClauses (Clause& c1, Clause& c2)
|
||||
|
||||
|
||||
|
||||
Clauses
|
||||
Clause::copyClauses (const Clauses& clauses)
|
||||
{
|
||||
Clauses copy;
|
||||
copy.reserve (clauses.size());
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
copy.push_back (new Clause (*clauses[i]));
|
||||
}
|
||||
return copy;
|
||||
}
|
||||
|
||||
|
||||
|
||||
void
|
||||
Clause::printClauses (const Clauses& clauses)
|
||||
{
|
||||
for (size_t i = 0; i < clauses.size(); i++) {
|
||||
cout << clauses[i] << endl;
|
||||
cout << *clauses[i] << endl;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
std::ostream& operator<< (ostream &os, const Clause& clause)
|
||||
std::ostream&
|
||||
operator<< (ostream &os, const Clause& clause)
|
||||
{
|
||||
for (unsigned i = 0; i < clause.literals_.size(); i++) {
|
||||
if (i != 0) os << " v " ;
|
||||
@ -349,57 +359,86 @@ Clause::getLogVarSetExcluding (size_t idx) const
|
||||
|
||||
|
||||
|
||||
std::ostream&
|
||||
operator<< (std::ostream &os, const LitLvTypes& lit)
|
||||
{
|
||||
os << lit.lid_ << "<" ;
|
||||
for (size_t i = 0; i < lit.lvTypes_.size(); i++) {
|
||||
switch (lit.lvTypes_[i]) {
|
||||
case LogVarType::FULL_LV: os << "F" ; break;
|
||||
case LogVarType::POS_LV: os << "P" ; break;
|
||||
case LogVarType::NEG_LV: os << "N" ; break;
|
||||
}
|
||||
}
|
||||
os << ">" ;
|
||||
return os;
|
||||
}
|
||||
|
||||
|
||||
|
||||
LiftedWCNF::LiftedWCNF (const ParfactorList& pfList)
|
||||
: freeLiteralId_(0), pfList_(pfList)
|
||||
{
|
||||
addIndicatorClauses (pfList);
|
||||
addParameterClauses (pfList);
|
||||
|
||||
/*
|
||||
// INCLUSION-EXCLUSION TEST
|
||||
vector<vector<string>> names = {
|
||||
// {"a1","b1"},{"a2","b2"},{"a1","b3"}
|
||||
{"b1","a1"},{"b2","a2"},{"b3","a1"}
|
||||
};
|
||||
Clause c1 (names);
|
||||
c1.addLiteral (Literal (0, LogVars() = {0}));
|
||||
c1.addLiteral (Literal (1, LogVars() = {1}));
|
||||
clauses_.push_back(c1);
|
||||
freeLiteralId_ ++ ;
|
||||
freeLiteralId_ ++ ;
|
||||
*/
|
||||
|
||||
/*
|
||||
// ATOM-COUNTING TEST
|
||||
// INCLUSION-EXCLUSION TEST
|
||||
clauses_.clear();
|
||||
vector<vector<string>> names = {
|
||||
{"p1","p1"},{"p1","p2"},{"p1","p3"},
|
||||
{"a1","b1"},{"a2","b2"}
|
||||
};
|
||||
Clause* c1 = new Clause (names);
|
||||
c1->addLiteral (Literal (0, LogVars() = {0}));
|
||||
c1->addLiteral (Literal (1, LogVars() = {1}));
|
||||
clauses_.push_back(c1);
|
||||
*/
|
||||
|
||||
/*
|
||||
// INDEPENDENT PARTIAL GROUND TEST
|
||||
clauses_.clear();
|
||||
vector<vector<string>> names = {
|
||||
{"a1","b1"},{"a2","b2"}
|
||||
};
|
||||
Clause* c1 = new Clause (names);
|
||||
c1->addLiteral (Literal (0, LogVars() = {0,1}));
|
||||
c1->addLiteral (Literal (1, LogVars() = {0,1}));
|
||||
clauses_.push_back(c1);
|
||||
Clause* c2 = new Clause (names);
|
||||
c2->addLiteral (Literal (2, LogVars() = {0}));
|
||||
c2->addLiteral (Literal (1, LogVars() = {0,1}));
|
||||
clauses_.push_back(c2);
|
||||
*/
|
||||
|
||||
/*
|
||||
// ATOM-COUNTING TEST
|
||||
clauses_.clear();
|
||||
vector<vector<string>> names = {
|
||||
{"p1","p1"},{"p1","p2"},{"p1","p3"},
|
||||
{"p2","p1"},{"p2","p2"},{"p2","p3"},
|
||||
{"p3","p1"},{"p3","p2"},{"p3","p3"}
|
||||
};
|
||||
Clause c1 (names);
|
||||
c1.addLiteral (Literal (0, LogVars() = {0}));
|
||||
c1.addLiteralComplemented (Literal (1, {0,1}));
|
||||
Clause* c1 = new Clause (names);
|
||||
c1->addLiteral (Literal (0, LogVars() = {0}));
|
||||
c1->addLiteralComplemented (Literal (1, {0,1}));
|
||||
clauses_.push_back(c1);
|
||||
Clause c2 (names);
|
||||
c2.addLiteral (Literal (0, LogVars()={0}));
|
||||
c2.addLiteralComplemented (Literal (1, {1,0}));
|
||||
Clause* c2 = new Clause (names);
|
||||
c2->addLiteral (Literal (0, LogVars()={0}));
|
||||
c2->addLiteralComplemented (Literal (1, {1,0}));
|
||||
clauses_.push_back(c2);
|
||||
addWeight (0, LogAware::log(3.0), LogAware::log(4.0));
|
||||
addWeight (1, LogAware::log(2.0), LogAware::log(5.0));
|
||||
freeLiteralId_ = 2;
|
||||
*/
|
||||
|
||||
cout << "FORMULA INDICATORS:" << endl;
|
||||
printFormulaIndicators();
|
||||
cout << endl;
|
||||
|
||||
cout << "WEIGHTS:" << endl;
|
||||
printWeights();
|
||||
cout << endl;
|
||||
|
||||
cout << "CLAUSES:" << endl;
|
||||
printClauses();
|
||||
cout << endl;
|
||||
if (Globals::verbosity > 1) {
|
||||
cout << "FORMULA INDICATORS:" << endl;
|
||||
printFormulaIndicators();
|
||||
cout << endl;
|
||||
cout << "WEIGHTED INDICATORS:" << endl;
|
||||
printWeights();
|
||||
cout << endl;
|
||||
cout << "CLAUSES:" << endl;
|
||||
printClauses();
|
||||
cout << endl;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -448,23 +487,22 @@ LiftedWCNF::prvGroupLiterals (PrvGroup prvGroup)
|
||||
|
||||
|
||||
|
||||
Clause
|
||||
Clause*
|
||||
LiftedWCNF::createClause (LiteralId lid) const
|
||||
{
|
||||
for (size_t i = 0; i < clauses_.size(); i++) {
|
||||
const Literals& literals = clauses_[i].literals();
|
||||
const Literals& literals = clauses_[i]->literals();
|
||||
for (size_t j = 0; j < literals.size(); j++) {
|
||||
if (literals[j].lid() == lid) {
|
||||
ConstraintTree ct = clauses_[i].constr();
|
||||
ct.project (literals[j].logVars());
|
||||
Clause clause (ct);
|
||||
clause.addLiteral (literals[j]);
|
||||
return clause;
|
||||
ConstraintTree ct = clauses_[i]->constr().projectedCopy (
|
||||
literals[j].logVars());
|
||||
Clause* c = new Clause (ct);
|
||||
c->addLiteral (literals[j]);
|
||||
return c;
|
||||
}
|
||||
}
|
||||
}
|
||||
abort(); // we should not reach this point
|
||||
return Clause (ConstraintTree({}));
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
@ -475,36 +513,34 @@ LiftedWCNF::getLiteralId (PrvGroup prvGroup, unsigned range)
|
||||
assert (Util::contains (map_, prvGroup));
|
||||
return map_[prvGroup][range];
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
void
|
||||
LiftedWCNF::addIndicatorClauses (const ParfactorList& pfList)
|
||||
{
|
||||
ParfactorList::const_iterator it = pfList.begin();
|
||||
set<PrvGroup> allGroups;
|
||||
while (it != pfList.end()) {
|
||||
const ProbFormulas& formulas = (*it)->arguments();
|
||||
for (size_t i = 0; i < formulas.size(); i++) {
|
||||
if (Util::contains (allGroups, formulas[i].group()) == false) {
|
||||
allGroups.insert (formulas[i].group());
|
||||
ConstraintTree tempConstr = *(*it)->constr();
|
||||
tempConstr.project (formulas[i].logVars());
|
||||
Clause clause (tempConstr);
|
||||
if (Util::contains (map_, formulas[i].group()) == false) {
|
||||
ConstraintTree tempConstr = (*it)->constr()->projectedCopy(
|
||||
formulas[i].logVars());
|
||||
Clause* clause = new Clause (tempConstr);
|
||||
vector<LiteralId> lids;
|
||||
for (size_t j = 0; j < formulas[i].range(); j++) {
|
||||
clause.addLiteral (Literal (freeLiteralId_, formulas[i].logVars()));
|
||||
clause->addLiteral (Literal (freeLiteralId_, formulas[i].logVars()));
|
||||
lids.push_back (freeLiteralId_);
|
||||
freeLiteralId_ ++;
|
||||
}
|
||||
clauses_.push_back (clause);
|
||||
for (size_t j = 0; j < formulas[i].range() - 1; j++) {
|
||||
for (size_t k = j + 1; k < formulas[i].range(); k++) {
|
||||
ConstraintTree tempConstr2 = *(*it)->constr();
|
||||
tempConstr2.project (formulas[i].logVars());
|
||||
Clause clause2 (tempConstr2);
|
||||
clause2.addLiteralComplemented (Literal (clause.literals()[j]));
|
||||
clause2.addLiteralComplemented (Literal (clause.literals()[k]));
|
||||
ConstraintTree tempConstr2 = (*it)->constr()->projectedCopy (
|
||||
formulas[i].logVars());
|
||||
Clause* clause2 = new Clause (tempConstr2);
|
||||
clause2->addLiteralComplemented (Literal (clause->literals()[j]));
|
||||
clause2->addLiteralComplemented (Literal (clause->literals()[k]));
|
||||
clauses_.push_back (clause2);
|
||||
}
|
||||
}
|
||||
@ -532,24 +568,24 @@ LiftedWCNF::addParameterClauses (const ParfactorList& pfList)
|
||||
// ¬θxi|u1,...,un v λu1 -> tempClause
|
||||
// ¬θxi|u1,...,un v λu2 -> tempClause
|
||||
double posWeight = (**it)[indexer];
|
||||
addWeight (paramVarLid, posWeight, 1.0);
|
||||
addWeight (paramVarLid, posWeight, LogAware::one());
|
||||
|
||||
Clause clause1 (*(*it)->constr());
|
||||
Clause* clause1 = new Clause (*(*it)->constr());
|
||||
|
||||
for (unsigned i = 0; i < groups.size(); i++) {
|
||||
LiteralId lid = getLiteralId (groups[i], indexer[i]);
|
||||
|
||||
clause1.addLiteralComplemented (
|
||||
clause1->addLiteralComplemented (
|
||||
Literal (lid, (*it)->argument(i).logVars()));
|
||||
|
||||
ConstraintTree ct = *(*it)->constr();
|
||||
Clause tempClause (ct);
|
||||
tempClause.addLiteralComplemented (Literal (
|
||||
Clause* tempClause = new Clause (ct);
|
||||
tempClause->addLiteralComplemented (Literal (
|
||||
paramVarLid, (*it)->constr()->logVars()));
|
||||
tempClause.addLiteral (Literal (lid, (*it)->argument(i).logVars()));
|
||||
tempClause->addLiteral (Literal (lid, (*it)->argument(i).logVars()));
|
||||
clauses_.push_back (tempClause);
|
||||
}
|
||||
clause1.addLiteral (Literal (paramVarLid, (*it)->constr()->logVars()));
|
||||
clause1->addLiteral (Literal (paramVarLid, (*it)->constr()->logVars()));
|
||||
clauses_.push_back (clause1);
|
||||
freeLiteralId_ ++;
|
||||
++ indexer;
|
||||
@ -559,9 +595,13 @@ LiftedWCNF::addParameterClauses (const ParfactorList& pfList)
|
||||
}
|
||||
|
||||
|
||||
|
||||
void
|
||||
LiftedWCNF::printFormulaIndicators (void) const
|
||||
{
|
||||
if (map_.empty()) {
|
||||
return;
|
||||
}
|
||||
set<PrvGroup> allGroups;
|
||||
ParfactorList::const_iterator it = pfList_.begin();
|
||||
while (it != pfList_.end()) {
|
||||
@ -570,8 +610,8 @@ LiftedWCNF::printFormulaIndicators (void) const
|
||||
if (Util::contains (allGroups, formulas[i].group()) == false) {
|
||||
allGroups.insert (formulas[i].group());
|
||||
cout << formulas[i] << " | " ;
|
||||
ConstraintTree tempCt = *(*it)->constr();
|
||||
tempCt.project (formulas[i].logVars());
|
||||
ConstraintTree tempCt = (*it)->constr()->projectedCopy (
|
||||
formulas[i].logVars());
|
||||
cout << tempCt.tupleSet();
|
||||
cout << " indicators => " ;
|
||||
vector<LiteralId> indicators =
|
||||
@ -603,8 +643,6 @@ LiftedWCNF::printWeights (void) const
|
||||
void
|
||||
LiftedWCNF::printClauses (void) const
|
||||
{
|
||||
for (unsigned i = 0; i < clauses_.size(); i++) {
|
||||
cout << clauses_[i] << endl;
|
||||
}
|
||||
Clause::printClauses (clauses_);
|
||||
}
|
||||
|
||||
|
@ -74,6 +74,10 @@ class Clause
|
||||
void addLiteral (const Literal& l) { literals_.push_back (l); }
|
||||
|
||||
const Literals& literals (void) const { return literals_; }
|
||||
|
||||
Literals& literals (void) { return literals_; }
|
||||
|
||||
size_t nrLiterals (void) const { return literals_.size(); }
|
||||
|
||||
const ConstraintTree& constr (void) const { return constr_; }
|
||||
|
||||
@ -128,9 +132,11 @@ class Clause
|
||||
void removeLiteral (size_t litIdx);
|
||||
|
||||
static bool independentClauses (Clause& c1, Clause& c2);
|
||||
|
||||
static vector<Clause*> copyClauses (const vector<Clause*>& clauses);
|
||||
|
||||
static void printClauses (const vector<Clause>& clauses);
|
||||
|
||||
static void printClauses (const vector<Clause*>& clauses);
|
||||
|
||||
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
||||
|
||||
private:
|
||||
@ -143,7 +149,7 @@ class Clause
|
||||
ConstraintTree constr_;
|
||||
};
|
||||
|
||||
typedef vector<Clause> Clauses;
|
||||
typedef vector<Clause*> Clauses;
|
||||
|
||||
|
||||
|
||||
@ -159,7 +165,10 @@ class LitLvTypes
|
||||
if (types1.lid_ < types2.lid_) {
|
||||
return true;
|
||||
}
|
||||
return types1.lvTypes_ < types2.lvTypes_;
|
||||
if (types1.lid_ == types2.lid_) {
|
||||
return types1.lvTypes_ < types2.lvTypes_;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
@ -173,6 +182,8 @@ class LitLvTypes
|
||||
void setAllFullLogVars (void) {
|
||||
std::fill (lvTypes_.begin(), lvTypes_.end(), LogVarType::FULL_LV); }
|
||||
|
||||
friend std::ostream& operator<< (std::ostream &os, const LitLvTypes& lit);
|
||||
|
||||
private:
|
||||
LiteralId lid_;
|
||||
LogVarTypes lvTypes_;
|
||||
@ -199,7 +210,7 @@ class LiftedWCNF
|
||||
|
||||
vector<LiteralId> prvGroupLiterals (PrvGroup prvGroup);
|
||||
|
||||
Clause createClause (LiteralId lid) const;
|
||||
Clause* createClause (LiteralId lid) const;
|
||||
|
||||
void printFormulaIndicators (void) const;
|
||||
|
||||
|
Reference in New Issue
Block a user