Development mirror of Jussi Rintanen’s planner Madagascar https://research.ics.aalto.fi/software/sat/madagascar/
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 

109 lines
2.1 KiB

cfma Cgroundfma(Sfma *,int *);
void Cgroundfmalist(Sfmalist *fs,int *ptr,int *b) {
while(fs != NULL) {
*(ptr++) = Cgroundfma(fs->hd,b);
fs = fs->tl;
}
}
cfma Cgroundfma(Sfma *sf,int *b) {
int *vals;
int i,cnt;
Sfmalist *fs;
cfma f;
switch(Sfmatypeof(sf)) {
case STRUE: return cTRUE;
case SFALSE: return cFALSE;
case Sconj:
f = (cfma)malloc(sizeof(int *) * (sf->cnt + 1));
Cgroundfmalist(sf->juncts,f+1,b);
f[0] = 1+(sf->cnt << 1);
return f;
case Sdisj:
f = (cfma)malloc(sizeof(int *) * (sf->cnt + 1));
Cgroundfmalist(sf->juncts,f+1,b);
f[0] = (sf->cnt << 1);
return f;
case Seq:
if(bvalue(sf->p1,b) == bvalue(sf->p2,b)) {
return cTRUE;
} else {
return cFALSE;
}
case Sneq:
if(bvalue(sf->p1,b) == bvalue(sf->p2,b)) {
return cFALSE;
} else {
return cTRUE;
}
case Spatom: return cPATOM(atomindex(sf->a,b));
case Snatom: return cNATOM(atomindex(sf->a,b));
case Sforall: /* Iterate over all values of the variable. */
cnt = getdomainsize(sf->ss->t);
f = (cfma)malloc(sizeof(int *) * (cnt + 1));
f[0] = (cnt << 1) + 1;
vals = getdomain(sf->ss->t);
for(i=0;i<cnt;i++) {
b[-1-sf->ss->v] = vals[i];
f[i+1] = Cgroundfma(sf->f,b);
}
return f;
case Sforsome: /* Iterate over all values of the variable. */
cnt = getdomainsize(sf->ss->t);
f = (cfma)malloc(sizeof(int *) * (cnt + 1));
f[0] = (cnt << 1);
vals = getdomain(sf->ss->t);
for(i=0;i<cnt;i++) {
b[-1-sf->ss->v] = vals[i];
f[i+1] = Cgroundfma(sf->f,b);
}
return f;
}
}
void printcfma(cfma f) {
int i;
if(((int)f)&1) { /* Atom */
switch(((int)f)&7) {
case cTRUEtag: printf("TRUE"); break;
case cFALSEtag: printf("FALSE"); break;
case cPATOMtag: printatomi((((int)f) >> 3)); break;
case cNATOMtag: printf("NOT "); printatomi((((int)f) >> 3)); break;
}
} else {
int cnt;
if(((int)(*f))&1) printf("(AND"); else printf("(OR");
cnt = ((int)(*f)) >> 1;
for(i=0;i<cnt;i++) {
printf(" ");
printcfma(f[i+1]);
}
printf(")");
}
printf("\n");
}