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 }