001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.pa.generic;
004    
005    import java.util.Hashtable;
006    import java.util.Enumeration;
007    import java.util.Vector;
008    import java.io.*;
009    
010    import mocha.wrappers.jbdd.*;
011    
012    /* Enumerates maximal clauses.
013     */
014    
015    public class GenerateMaxClauses {
016    
017        private jbddManager bddmanager;
018        jbdd bdd;
019        boolean maxClause[];
020    
021        public GenerateMaxClauses(jbddManager bddmanager) {
022            this.bddmanager = bddmanager;
023            bdd = bddmanager.jbdd_one();
024            maxClause = new boolean[ bddmanager.jbdd_num_vars() ];
025    
026            for( int i=0; i<bddmanager.jbdd_num_vars(); i++ ) {
027                maxClause[i] = true;
028            }
029    
030        }
031    
032        public void restrict(jbdd to) {
033            bdd = jbdd.jbdd_and( bdd, to, true, true);
034        }
035    
036        /** Put next max clause compatible with b into maxClause[i..n-1]
037         * and return true (if such max clause exists),
038         * or put true  into maxClause[i..n-1]
039         * and return false.
040         */ 
041    
042        public boolean findValidMaxClause(int i, jbdd b) {
043    
044            if( b.jbdd_is_tautology(true) ) return true;
045    
046            if( i == bddmanager.jbdd_num_vars() ) return false;
047    
048            for(;;) {
049                if( findValidMaxClause(i+1,
050                         (i == b.jbdd_top_var_id())
051                         ? ( maxClause[i] ? b.jbdd_then() : b.jbdd_else())
052                         : b )) {
053                    return true;
054                } else if( maxClause[i] == false) {
055                    maxClause[i] = true;
056                    return false;
057                } else {
058                    maxClause[i] = false;
059                    // go around loop
060                }
061            }
062        }
063            
064        public jbdd next() {
065            
066            if( maxClause == null ) return null;
067    
068            if( findValidMaxClause( 0, bdd ) == false ) {
069                maxClause = null;
070                return null;
071            }
072    
073            // Put maxClause into a bdd, 
074            jbdd t = bddmanager.jbdd_zero();
075            for( int i=bddmanager.jbdd_num_vars()-1; i>=0; i-- ) {
076                jbdd varBdd = bddmanager.jbdd_get_variable( i );
077                t = jbdd.jbdd_or( t, varBdd, true, !maxClause[i] );
078                // System.out.println("maxClause["+i+"]="+maxClause[i] );
079            }
080    
081            // decrement maxClause
082            int i;
083            for( i=bddmanager.jbdd_num_vars()-1; i>=0 && maxClause[i] == false; i-- ) {
084                maxClause[i] = true;
085            }
086    
087            if( i >= 0 ) {
088                maxClause[i] = false;
089            } else {
090                // tried all maxClauses
091                maxClause = null;
092            }
093    
094            return t;
095        }
096    }