BuDDy: bdd_allsat

void bdd_allsat	(	BDD	r,
		bddallsathandler	handler
	)

Finds all satisfying variable assignments.

Iterates through all legal variable assignments (those that make the BDD come true) for the bdd r and calls the callback handler handler for each of them. The array passed to handler contains one entry for each of the globally defined variables. Each entry is either 0 if the variable is false, 1 if it is true, and -1 if it is a don't care. The following is an example of a callback handler that prints 'X' for don't cares, '0' for zero, and '1' for one:

 void allsatPrintHandler(char* varset, int size) 
 { 
   for (int v=0; v<size; ++v) 
   { 
      cout << (varset[v] < 0 ? 'X' : (char)('0' + varset[v])); 
   } 
   cout << endl; 
 }

The handler can be used like this:

 bdd_allsat(r, * allsatPrintHandler);

See also:: bdd_satone bdd_satoneset, bdd_fullsatone, bdd_satcount, bdd_satcountln