00001
00041 #include "calInt.h"
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061 static char defaultTerminalId[]="terminal XXXXXXXXXX XXXXXXXXXX";
00062 static char defaultVarName[]="var.XXXXXXXXXX";
00063
00064
00065
00066
00067
00068
00069
00072
00073
00074
00075
00076 static void Chars(char c, int n, FILE *fp);
00077 static void BddPrintTopVar(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env, FILE *fp);
00078 static void BddPrintBddStep(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env, FILE *fp, CalHashTable_t* hashTable, int indentation);
00079 static char * BddTerminalId(Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env);
00080 static void BddTerminalValueAux(Cal_BddManager_t *bddManager, Cal_Bdd_t f, CalAddress_t *value1, CalAddress_t *value2);
00081
00085
00086
00087
00110 void
00111 Cal_BddPrintBdd(Cal_BddManager bddManager,
00112 Cal_Bdd fUserBdd, Cal_VarNamingFn_t VarNamingFn,
00113 Cal_TerminalIdFn_t TerminalIdFn,
00114 Cal_Pointer_t env, FILE *fp)
00115 {
00116 long next;
00117 CalHashTable_t *hashTable;
00118
00119 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager,fUserBdd);
00120 CalBddMarkSharedNodes(bddManager, f);
00121 hashTable = CalHashTableOneInit(bddManager, sizeof(long));
00122 next = 0;
00123 CalBddNumberSharedNodes(bddManager, f, hashTable, &next);
00124 BddPrintBddStep(bddManager, f, VarNamingFn, TerminalIdFn, env, fp,
00125 hashTable, 0);
00126 CalHashTableOneQuit(hashTable);
00127 }
00128
00129
00130
00131
00143 char *
00144 CalBddVarName(Cal_BddManager_t *bddManager, Cal_Bdd_t v,
00145 Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env)
00146 {
00147 char *name;
00148 if (VarNamingFn){
00149 Cal_Bdd userV = CalBddGetExternalBdd(bddManager, v);
00150 name = (*VarNamingFn)(bddManager, userV, env);
00151 Cal_BddFree(bddManager, userV);
00152 }
00153 else
00154 name=0;
00155 if (!name){
00156 sprintf(defaultVarName, "var.%d", CalBddGetBddIndex(bddManager, v));
00157 name = defaultVarName;
00158 }
00159 return (name);
00160 }
00161
00173 void
00174 CalBddNumberSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
00175 CalHashTable_t *hashTable, long *next)
00176 {
00177 Cal_Bdd_t thenBdd, elseBdd;
00178 int mark;
00179
00180 if (CalBddIsBddConst(f) || ((1 << CalBddTypeAux(bddManager, f)) &
00181 ((1 << CAL_BDD_TYPE_POSVAR) |
00182 (1 << CAL_BDD_TYPE_NEGVAR))))
00183 return;
00184 mark = CalBddGetMark(f);
00185 if (mark == 0) return;
00186 if (mark == 2) {
00187 CalHashTableOneInsert(hashTable, f, (char *)next);
00188 ++*next;
00189 }
00190 CalBddPutMark(f, 0);
00191 CalBddGetThenBdd(f, thenBdd);
00192 CalBddGetElseBdd(f, elseBdd);
00193 CalBddNumberSharedNodes(bddManager, thenBdd, hashTable, next);
00194 CalBddNumberSharedNodes(bddManager, elseBdd, hashTable, next);
00195 }
00196
00208 void
00209 CalBddMarkSharedNodes(Cal_BddManager_t *bddManager, Cal_Bdd_t f)
00210 {
00211 int mark;
00212 Cal_Bdd_t thenBdd, elseBdd;
00213
00214 if (CalBddIsOutPos(f) == 0){
00215 CalBddNot(f,f);
00216 }
00217 if (CalBddIsBddConst(f) || CalBddTypeAux(bddManager, f) ==
00218 CAL_BDD_TYPE_POSVAR)
00219 return;
00220 if ((mark = CalBddGetMark(f))){
00221 if (mark == 1){
00222 CalBddPutMark(f, 2);
00223 return;
00224 }
00225 }
00226 CalBddPutMark(f, 1);
00227 CalBddGetThenBdd(f, thenBdd);
00228 CalBddGetElseBdd(f, elseBdd);
00229 CalBddMarkSharedNodes(bddManager, thenBdd);
00230 CalBddMarkSharedNodes(bddManager, elseBdd);
00231 }
00232
00233
00234
00235
00236
00248 static void
00249 Chars(char c, int n,FILE *fp)
00250 {
00251 int i;
00252 for (i=0; i < n; ++i){
00253 fputc(c, fp);
00254 }
00255 }
00256
00257
00269 static void
00270 BddPrintTopVar(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
00271 Cal_VarNamingFn_t VarNamingFn, Cal_Pointer_t env, FILE *fp)
00272 {
00273 Cal_Bdd_t ifVar;
00274 ifVar = CalBddIf(bddManager, f);
00275 fputs(CalBddVarName(bddManager, ifVar, VarNamingFn, env), fp);
00276 fputc('\n', fp);
00277 }
00278
00279 static void
00291 BddPrintBddStep(Cal_BddManager_t *bddManager,
00292 Cal_Bdd_t f, Cal_VarNamingFn_t VarNamingFn,
00293 Cal_TerminalIdFn_t TerminalIdFn,
00294 Cal_Pointer_t env, FILE *fp, CalHashTable_t* hashTable,
00295 int indentation)
00296 {
00297 int negated;
00298 long *number;
00299 Cal_Bdd_t fNot, thenBdd, elseBdd;
00300
00301 Chars(' ', indentation, fp);
00302 switch (CalBddTypeAux(bddManager, f)){
00303 case CAL_BDD_TYPE_ZERO:
00304 case CAL_BDD_TYPE_ONE:
00305 fputs(BddTerminalId(bddManager, f, TerminalIdFn, env), fp);
00306 fputc('\n', fp);
00307 break;
00308 case CAL_BDD_TYPE_NEGVAR:
00309 fputc('!', fp);
00310
00311 case CAL_BDD_TYPE_POSVAR:
00312 BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00313 break;
00314 case CAL_BDD_TYPE_NONTERMINAL:
00315 CalBddNot(f, fNot);
00316 if (CalHashTableOneLookup(hashTable, fNot, Cal_Nil(char *))){
00317 f = fNot;
00318 negated = 1;
00319 }
00320 else {
00321 negated=0;
00322 }
00323 CalHashTableOneLookup(hashTable, f, (char **)&number);
00324 if (number && *number < 0){
00325 if (negated)
00326 fputc('!', fp);
00327 fprintf(fp, "subformula %d\n", (int)-*number-1);
00328 }
00329 else {
00330 if (number){
00331 fprintf(fp, "%d: ", (int) *number);
00332 *number= -*number-1;
00333 }
00334 fputs("if ", fp);
00335 BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00336 CalBddGetThenBdd(f, thenBdd);
00337 BddPrintBddStep(bddManager, thenBdd, VarNamingFn,
00338 TerminalIdFn, env, fp, hashTable, indentation+2);
00339 Chars(' ', indentation, fp);
00340 fputs("else if !", fp);
00341 BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00342 CalBddGetElseBdd(f, elseBdd);
00343 BddPrintBddStep(bddManager, elseBdd, VarNamingFn,
00344 TerminalIdFn, env, fp, hashTable, indentation+2);
00345 Chars(' ', indentation, fp);
00346 fputs("endif ", fp);
00347 BddPrintTopVar(bddManager, f, VarNamingFn, env, fp);
00348 }
00349 break;
00350 default:
00351 CalBddFatalMessage("BddPrintBddStep: unknown type returned by Cal_BddType");
00352 }
00353 }
00354
00366 static char *
00367 BddTerminalId(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
00368 Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env)
00369 {
00370 char *id;
00371 CalAddress_t v1, v2;
00372 BddTerminalValueAux(bddManager, f, &v1, &v2);
00373 if (TerminalIdFn) id = (*TerminalIdFn)(bddManager, v1, v2, env);
00374 else id=0;
00375 if (!id){
00376 if (CalBddIsBddOne(bddManager, f)) return ("1");
00377 if (CalBddIsBddZero(bddManager, f)) return ("0");
00378 sprintf(defaultTerminalId, "terminal %ld %ld", (long)v1, (long)v2);
00379 id = defaultTerminalId;
00380 }
00381 return (id);
00382 }
00383
00384
00385
00397 static void
00398 BddTerminalValueAux(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
00399 CalAddress_t *value1, CalAddress_t *value2)
00400 {
00401 if (CalBddIsOutPos(f)){
00402 *value1 = (CalAddress_t)CalBddGetThenBddNode(f);
00403 *value2 = (CalAddress_t)CalBddGetElseBddNode(f);
00404 }
00405 else
00406 (*bddManager->TransformFn)(bddManager,
00407 (CalAddress_t)CalBddGetThenBddNode(f),
00408 (CalAddress_t)CalBddGetElseBddNode(f),
00409 value1, value2, bddManager->transformEnv);
00410 }
00411
00412
00413
00414
00415
00416
00417
00418
