    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    }