257 lines
6.4 KiB
C
257 lines
6.4 KiB
C
|
/*
|
||
|
|
LPAD and CP-Logic interpreter
|
||
|
|
|
||
|
|
Copyright (c) 2007, Fabrizio Riguzzi
|
||
|
|
|
||
|
|
This package uses the library cudd, see http://vlsi.colorado.edu/~fabio/CUDD/
|
||
|
|
for the relative license.
|
||
|
|
|
||
|
|
|
||
|
|
This file contains the functions for interfacing Yap and C
|
||
|
|
The arguments of the predicate compute_prob are parsed and translated into C data
|
||
|
|
structures
|
||
|
|
*/
|
||
|
|
|
||
|
|
#include "cplint.h"
|
||
|
|
#include <math.h>
|
||
|
|
#include <stdlib.h>
|
||
|
|
#include <string.h>
|
||
|
|
|
||
|
|
|
||
|
|
unsigned long dividend;
|
||
|
|
|
||
|
|
FILE *open_file (char *filename, const char *mode);
|
||
|
|
void reverse(char s[]);
|
||
|
|
static int compute_prob(void);
|
||
|
|
|
||
|
|
void createVars(array_t * vars, YAP_Term t,DdManager * mgr, array_t * bVar2mVar,int create_dot, char inames[1000][20])
|
||
|
|
/* adds the boolean variables to the BDD and returns
|
||
|
|
an array_t containing them (array_t is defined in the util library of glu)
|
||
|
|
returns also the names of the variables to be used to save the ADD in dot format
|
||
|
|
*/
|
||
|
|
{
|
||
|
|
YAP_Term varTerm,probTerm;
|
||
|
|
int varIndex,nVal,i,b;
|
||
|
|
variable v;
|
||
|
|
char numberVar[10],numberBit[10];
|
||
|
|
double p;
|
||
|
|
b=0;
|
||
|
|
|
||
|
|
while(YAP_IsPairTerm(t))
|
||
|
|
{
|
||
|
|
varTerm=YAP_HeadOfTerm(t);
|
||
|
|
varIndex=YAP_IntOfTerm(YAP_HeadOfTerm(varTerm));
|
||
|
|
|
||
|
|
varTerm=YAP_TailOfTerm(varTerm);
|
||
|
|
nVal=YAP_IntOfTerm(YAP_HeadOfTerm(varTerm));
|
||
|
|
varTerm=YAP_TailOfTerm(varTerm);
|
||
|
|
probTerm=YAP_HeadOfTerm(varTerm);
|
||
|
|
v.nVal=nVal;
|
||
|
|
v.nBit=(int)ceil(log(nVal)/log(2));
|
||
|
|
v.probabilities=array_alloc(double,0);
|
||
|
|
v.booleanVars=array_alloc(DdNode *,0);
|
||
|
|
for (i=0;i<nVal;i++)
|
||
|
|
{
|
||
|
|
if (create_dot)
|
||
|
|
{
|
||
|
|
strcpy(inames[b+i],"X");
|
||
|
|
sprintf(numberVar,"%d",varIndex);
|
||
|
|
strcat(inames[b+i],numberVar);
|
||
|
|
strcat(inames[b+i],"_");
|
||
|
|
sprintf(numberBit,"%d",i);
|
||
|
|
strcat(inames[b+i],numberBit);
|
||
|
|
}
|
||
|
|
p=YAP_FloatOfTerm(YAP_HeadOfTerm(probTerm));
|
||
|
|
array_insert(double,v.probabilities,i,p);
|
||
|
|
probTerm=YAP_TailOfTerm(probTerm);
|
||
|
|
array_insert(DdNode *,v.booleanVars,i,Cudd_bddIthVar(mgr,b+i));
|
||
|
|
array_insert(int,bVar2mVar,b+i,varIndex);
|
||
|
|
}
|
||
|
|
Cudd_MakeTreeNode(mgr,b,nVal,MTR_FIXED);
|
||
|
|
b=b+nVal;
|
||
|
|
array_insert(variable,vars,varIndex,v);
|
||
|
|
t=YAP_TailOfTerm(t);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
void createExpression(array_t * expression, YAP_Term t)
|
||
|
|
/* returns the expression as an array_t of terms (cubes) starting from the prolog lists of terms
|
||
|
|
each term is an array_t of factors obtained from a prolog list of factors
|
||
|
|
each factor is a couple (index of variable, index of value) obtained from a prolog list containing
|
||
|
|
two integers
|
||
|
|
*/
|
||
|
|
{
|
||
|
|
YAP_Term termTerm,factorTerm;
|
||
|
|
factor f;
|
||
|
|
int i,j;
|
||
|
|
array_t * term;
|
||
|
|
|
||
|
|
i=0;
|
||
|
|
while(YAP_IsPairTerm(t))
|
||
|
|
{
|
||
|
|
term=array_alloc(factor,0);
|
||
|
|
termTerm=YAP_HeadOfTerm(t);
|
||
|
|
j=0;
|
||
|
|
while(YAP_IsPairTerm(termTerm))
|
||
|
|
{
|
||
|
|
factorTerm=YAP_HeadOfTerm(termTerm);
|
||
|
|
f.var=YAP_IntOfTerm(YAP_HeadOfTerm(factorTerm));
|
||
|
|
f.value=YAP_IntOfTerm(YAP_HeadOfTerm(YAP_TailOfTerm(factorTerm)));
|
||
|
|
array_insert(factor,term,j,f);
|
||
|
|
termTerm=YAP_TailOfTerm(termTerm);
|
||
|
|
j++;
|
||
|
|
}
|
||
|
|
array_insert(array_t *,expression,i,term);
|
||
|
|
t=YAP_TailOfTerm(t);
|
||
|
|
i++;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
static int compute_prob(void)
|
||
|
|
/* this is the function that implements the compute_prob predicate used in pp.pl
|
||
|
|
*/
|
||
|
|
{
|
||
|
|
YAP_Term out,arg1,arg2,arg3,arg4;
|
||
|
|
array_t * variables,* expression, * bVar2mVar;
|
||
|
|
DdNode * function, * add;
|
||
|
|
DdManager * mgr;
|
||
|
|
int nBVar,i,j,intBits,create_dot;
|
||
|
|
FILE * file;
|
||
|
|
DdNode * array[1];
|
||
|
|
char * onames[1];
|
||
|
|
char inames[1000][20];
|
||
|
|
char * names[1000];
|
||
|
|
GHashTable * nodes; /* hash table that associates nodes with their probability if already
|
||
|
|
computed, it is defined in glib */
|
||
|
|
Cudd_ReorderingType order;
|
||
|
|
arg1=YAP_ARG1;
|
||
|
|
arg2=YAP_ARG2;
|
||
|
|
arg3=YAP_ARG3;
|
||
|
|
arg4=YAP_ARG4;
|
||
|
|
|
||
|
|
mgr=Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
|
||
|
|
variables=array_alloc(variable,0);
|
||
|
|
bVar2mVar=array_alloc(int,0);
|
||
|
|
create_dot=YAP_IntOfTerm(arg4);
|
||
|
|
createVars(variables,arg1,mgr,bVar2mVar,create_dot,inames);
|
||
|
|
//Cudd_PrintInfo(mgr,stderr);
|
||
|
|
|
||
|
|
/* automatic variable reordering, default method CUDD_REORDER_SIFT used */
|
||
|
|
//printf("status %d\n",Cudd_ReorderingStatus(mgr,&order));
|
||
|
|
//printf("order %d\n",order);
|
||
|
|
|
||
|
|
Cudd_AutodynEnable(mgr,CUDD_REORDER_SAME);
|
||
|
|
/* Cudd_AutodynEnable(mgr, CUDD_REORDER_RANDOM_PIVOT);
|
||
|
|
printf("status %d\n",Cudd_ReorderingStatus(mgr,&order));
|
||
|
|
printf("order %d\n",order);
|
||
|
|
printf("%d",CUDD_REORDER_RANDOM_PIVOT);
|
||
|
|
*/
|
||
|
|
|
||
|
|
|
||
|
|
expression=array_alloc(array_t *,0);
|
||
|
|
createExpression(expression,arg2);
|
||
|
|
|
||
|
|
function=retFunction(mgr,expression,variables);
|
||
|
|
/* the BDD build by retFunction is converted to an ADD (algebraic decision diagram)
|
||
|
|
because it is easier to interpret and to print */
|
||
|
|
add=Cudd_BddToAdd(mgr,function);
|
||
|
|
//Cudd_PrintInfo(mgr,stderr);
|
||
|
|
|
||
|
|
if (create_dot)
|
||
|
|
/* if specified by the user, a dot file for the BDD is written to cpl.dot */
|
||
|
|
{
|
||
|
|
nBVar=array_n(bVar2mVar);
|
||
|
|
for(i=0;i<nBVar;i++)
|
||
|
|
names[i]=inames[i];
|
||
|
|
array[0]=add;
|
||
|
|
onames[0]="Out";
|
||
|
|
file = open_file("cpl.dot", "w");
|
||
|
|
Cudd_DumpDot(mgr,1,array,names,onames,file);
|
||
|
|
fclose(file);
|
||
|
|
}
|
||
|
|
|
||
|
|
nodes=g_hash_table_new(my_hash,my_equal);
|
||
|
|
intBits=sizeof(unsigned int)*8;
|
||
|
|
/* dividend is a global variable used by my_hash
|
||
|
|
it is equal to an unsigned int with binary representation 11..1 */
|
||
|
|
dividend=1;
|
||
|
|
for(j=1;j<intBits;j++)
|
||
|
|
{
|
||
|
|
dividend=(dividend<<1)+1;
|
||
|
|
}
|
||
|
|
out=YAP_MkFloatTerm(Prob(add,variables,bVar2mVar,nodes));
|
||
|
|
g_hash_table_foreach (nodes,dealloc,NULL);
|
||
|
|
g_hash_table_destroy(nodes);
|
||
|
|
Cudd_Quit(mgr);
|
||
|
|
array_free(variables);
|
||
|
|
array_free(bVar2mVar);
|
||
|
|
array_free(expression);
|
||
|
|
return(YAP_Unify(out,arg3));
|
||
|
|
}
|
||
|
|
/*
|
||
|
|
int compare(char *a, char *b)
|
||
|
|
{
|
||
|
|
int aval,bval;
|
||
|
|
aval=(int) *((DdNode **)a);
|
||
|
|
aval=(int) *((DdNode **)b);
|
||
|
|
|
||
|
|
if (aval<bval)
|
||
|
|
return -1;
|
||
|
|
else
|
||
|
|
if (aval>bval)
|
||
|
|
return 1;
|
||
|
|
else
|
||
|
|
return 0;
|
||
|
|
}
|
||
|
|
*/
|
||
|
|
void init_my_predicates()
|
||
|
|
/* function required by YAP for intitializing the predicates defined by a C function*/
|
||
|
|
{
|
||
|
|
YAP_UserCPredicate("compute_prob",compute_prob,4);
|
||
|
|
}
|
||
|
|
FILE *
|
||
|
|
open_file(char *filename, const char *mode)
|
||
|
|
/* opens a file */
|
||
|
|
{
|
||
|
|
FILE *fp;
|
||
|
|
|
||
|
|
if ((fp = fopen(filename, mode)) == NULL) {
|
||
|
|
perror(filename);
|
||
|
|
exit(1);
|
||
|
|
}
|
||
|
|
return fp;
|
||
|
|
|
||
|
|
}
|
||
|
|
void reverse(char s[])
|
||
|
|
/* reverses a string */
|
||
|
|
{
|
||
|
|
int i,c,j;
|
||
|
|
for (i=0,j=strlen(s)-1;i<j;i++,j--)
|
||
|
|
{
|
||
|
|
c=s[i];
|
||
|
|
s[i]=s[j];
|
||
|
|
s[j]=c;
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
gint my_equal(gconstpointer v,gconstpointer v2)
|
||
|
|
/* function used by GHashTable to compare two keys */
|
||
|
|
{
|
||
|
|
DdNode *a,*b;
|
||
|
|
a=*(DdNode **)v;
|
||
|
|
b=*(DdNode **)v2;
|
||
|
|
return (a==b);
|
||
|
|
}
|
||
|
|
guint my_hash(gconstpointer key)
|
||
|
|
/* function used by GHashTable to hash a key */
|
||
|
|
{
|
||
|
|
unsigned int h;
|
||
|
|
h=(unsigned int)((unsigned long) *((DdNode **)key) % dividend);
|
||
|
|
return h;
|
||
|
|
}
|
||
|
|
void dealloc(gpointer key,gpointer value,gpointer user_data)
|
||
|
|
{
|
||
|
|
free(key);
|
||
|
|
free(value);
|
||
|
|
}
|