public List < Assignment > enumerateAllModels ( final BDD bdd , final Collection < Variable > variables ) { final Set < Assignment > res = new HashSet <> ( ) ; final List < byte [ ] > models = this . kernel . allSat ( bdd . index ( ) ) ; final SortedSet < Integer > temp ; if ( variables == null ) temp = new TreeSet <> ( this . var2idx . values ( ) ) ; else { temp = new TreeSet <> ( ) ; for ( final Map . Entry < Variable , Integer > e : this . var2idx . entrySet ( ) ) if ( variables . contains ( e . getKey ( ) ) ) temp . add ( e . getValue ( ) ) ; } final int [ ] relevantIndices = new int [ temp . size ( ) ] ; int count = 0 ; for ( final Integer i : temp ) relevantIndices [ count ++ ] = i ; for ( final byte [ ] model : models ) { final List < Assignment > allAssignments = new LinkedList <> ( ) ; generateAllModels ( allAssignments , model , relevantIndices , 0 ) ; res . addAll ( allAssignments ) ; } return new ArrayList <> ( res ) ; }
Enumerates all models of a given BDD wrt . a given set of variables .