This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/cplint/cplint_yap.c

230 lines
5.8 KiB
C
Raw Normal View History

/*
2011-10-22 15:33:04 +01:00
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.
2011-10-22 15:33:04 +01:00
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>
2017-11-27 13:36:19 +00:00
FILE *open_file (char *file_name, const char *mode);
2015-02-03 03:00:37 +00:00
static YAP_Bool compute_prob(void);
2010-07-27 15:53:47 +01:00
variables createVars(YAP_Term t,DdManager * mgr, int create_dot, char inames[1000][20])
/* adds the boolean variables to the BDD and returns
2010-07-27 15:53:47 +01:00
the array vars containing them
returns also the names of the variables to be used to save the ADD in dot format
*/
{
2011-10-22 15:33:04 +01:00
YAP_Term varTerm,probTerm;
int varIndex,nVal,i,b;
variable v;
char numberVar[10],numberBit[10];
double p;
variables vars;
vars.varar=NULL;
vars.bVar2mVar=NULL;
b=0;
vars.nVar=0;
varIndex=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=(double *) malloc(nVal* sizeof(double));
v.booleanVars=(DdNode * *) malloc(v.nBit* sizeof(DdNode *));
for (i=0;i<nVal;i++)
{
p=YAP_FloatOfTerm(YAP_HeadOfTerm(probTerm));
v.probabilities[i]=p;
probTerm=YAP_TailOfTerm(probTerm);
}
for (i=0;i<v.nBit;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);
}
v.booleanVars[i]=Cudd_bddIthVar(mgr,b+i);
vars.bVar2mVar=(int *)realloc(vars.bVar2mVar,(b+i+1)*sizeof(int));
vars.bVar2mVar[b+i]=varIndex;
}
Cudd_MakeTreeNode(mgr,b,v.nBit,MTR_FIXED);
b=b+v.nBit;
vars.varar=(variable *) realloc(vars.varar,(varIndex+1)* sizeof(variable));
vars.varar[varIndex]=v;
t=YAP_TailOfTerm(t);
}
vars.nVar=varIndex+1;
vars.nBVar=b;
return vars;
}
2010-07-27 15:53:47 +01:00
expr createExpression(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
*/
{
2011-10-22 15:33:04 +01:00
YAP_Term termTerm,factorTerm;
factor f;
int i,j;
term term1;
expr expression;
expression.terms=NULL;
i=0;
while(YAP_IsPairTerm(t))
{
term1.factors=NULL;
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)));
term1.factors=(factor *)realloc(term1.factors,(j+1)* sizeof(factor));
term1.factors[j]=f;
termTerm=YAP_TailOfTerm(termTerm);
j++;
}
term1.nFact=j;
expression.terms=(term *)realloc(expression.terms,(i+1)* sizeof(term));
expression.terms[i]=term1;
t=YAP_TailOfTerm(t);
i++;
}
expression.nTerms=i;
return(expression);
}
2015-02-03 03:00:37 +00:00
static YAP_Bool compute_prob(void)
/* this is the function that implements the compute_prob predicate used in pp.pl
*/
{
2011-10-22 15:33:04 +01:00
YAP_Term out,arg1,arg2,arg3,arg4;
variables vars;
expr expression;
DdNode * function;
DdManager * mgr;
2017-11-11 02:15:59 +00:00
int nBVar,i,create_dot;
2011-10-22 15:33:04 +01:00
FILE * file;
DdNode * array[1];
double prob;
2018-11-23 00:01:55 +00:00
char const * onames[1];
2011-10-22 15:33:04 +01:00
char inames[1000][20];
2018-11-23 00:01:55 +00:00
char const * names[1000];
2011-10-22 15:33:04 +01:00
tablerow * nodes;
arg1=YAP_ARG1;
arg2=YAP_ARG2;
arg3=YAP_ARG3;
arg4=YAP_ARG4;
mgr=Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
create_dot=YAP_IntOfTerm(arg4);
vars=createVars(arg1,mgr,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);
2011-10-22 15:33:04 +01:00
printf("%d",CUDD_REORDER_RANDOM_PIVOT);
*/
2011-10-22 15:33:04 +01:00
expression=createExpression(arg2);
function=retFunction(mgr,expression,vars);
/* 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=vars.nBVar;
for(i=0;i<nBVar;i++)
names[i]=inames[i];
array[0]=function;
onames[0]="Out";
file = open_file("cpl.dot", "w");
2018-11-23 00:01:55 +00:00
Cudd_DumpDot(mgr,1,array,names,onames,file);
2011-10-22 15:33:04 +01:00
fclose(file);
}
nodes=init_table(vars.nBVar);
prob=Prob(function,vars,nodes);
out=YAP_MkFloatTerm(prob);
destroy_table(nodes,vars.nBVar);
Cudd_Quit(mgr);
for(i=0;i<vars.nVar;i++)
{
free(vars.varar[i].probabilities);
free(vars.varar[i].booleanVars);
}
free(vars.varar);
free(vars.bVar2mVar);
for(i=0;i<expression.nTerms;i++)
{
free(expression.terms[i].factors);
}
free(expression.terms);
return(YAP_Unify(out,arg3));
}
void init_my_predicates()
/* function required by YAP for intitializing the predicates defined by a C function*/
{
YAP_UserCPredicate("compute_prob",compute_prob,4);
}
2011-10-22 15:33:04 +01:00
2017-11-27 13:36:19 +00:00
FILE * open_file(char *file_name, const char *mode)
/* opens a file */
{
2011-10-22 15:33:04 +01:00
FILE *fp;
2017-11-27 13:36:19 +00:00
if ((fp = fopen(file_name, mode)) == NULL)
2011-10-22 15:33:04 +01:00
{
2017-11-27 13:36:19 +00:00
perror(file_name);
2011-10-22 15:33:04 +01:00
exit(1);
}
return fp;
}