001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.pa.generic;
004    
005    import java.util.*;
006    import javafe.util.*;
007    import mocha.wrappers.jbdd.*;
008    
009    /* The prover interface works on bdds. This is a wrapper that is
010       optimized for Disjunctions, and avoids converting to bdds where
011       possible.
012    */
013    
014    public class DisjunctionProver {
015    
016        public static final int VALID = 0;
017        public static final int INVALID = 1;
018        public static final int UNKNOWN = 2;
019        
020        private ArrayList valid = new ArrayList();
021        private ArrayList invalid = new ArrayList();
022    
023        private Prover prover;
024        private jbddManager bddManager;
025    
026    
027        public DisjunctionProver(Prover prover, jbddManager bddManager) {
028            this.prover = prover;
029            this.bddManager = bddManager;
030        }
031    
032        public int quickCheck(Disjunction d) {
033            for(Iterator it = valid.iterator(); it.hasNext(); ) {
034                // see if valid[i] => query
035                if( implies((Disjunction)it.next(), d) ) {
036                    return VALID;
037                }
038            }
039    
040            for(Iterator it = invalid.iterator(); it.hasNext(); ) {
041                // see if query => invalid[i]
042                if( implies(d, (Disjunction)it.next()) ) {
043                    return INVALID;
044                }
045            }
046    
047            jbdd bdd = disjToBdd( d );
048            int r = prover.quickCheck( bdd );
049            bdd.jbdd_free();
050            
051            switch( r ) {
052              case Prover.VALID:
053                valid.add( new Disjunction(d) );
054                return VALID;
055                
056              case Prover.INVALID:
057                invalid.add( new Disjunction(d) );
058                return INVALID;
059            }
060            
061            return UNKNOWN;
062        }
063    
064    
065    
066        public boolean check(Disjunction d) {
067            int r = quickCheck( d );
068            switch( r ) {
069              case VALID: 
070                return true;
071              case INVALID: 
072                return false;
073              case UNKNOWN: 
074                  {
075                      jbdd bdd = disjToBdd( d );
076                      // Assert.notFalse( prover.quickCheck(bdd) == prover.UNKNOWN );
077                      
078                      boolean b = prover.check( bdd );
079                      if( b ) {
080                          valid.add( new Disjunction(d) );
081                      } else {
082                          invalid.add( new Disjunction(d) );
083                      }
084                      return b;
085                  }
086              default:
087                Assert.fail("");
088                return true;
089            }
090        }
091    
092        public String printClause(Disjunction d) {
093            return prover.printClause(disjToBdd(d));
094        }
095    
096        public String report() {
097            return prover.report();
098        }
099    
100        public boolean implies(Disjunction d1, Disjunction d2) {
101            Assert.notFalse( (d1.stars & d1.bits) == 0 );
102            Assert.notFalse( (d2.stars & d2.bits) == 0 );
103            Assert.notFalse( (~d2.stars & d2.bits) == d2.bits );
104            boolean r = ((d2.stars & ~d1.stars) == 0) 
105                       && ((d2.bits & ~d1.stars) == d1.bits);
106            return r;
107        }
108    
109        jbdd disjToBdd(Disjunction d) {
110            // Put choice into a bdd, 
111            jbdd t = bddManager.jbdd_zero();
112            for( int i=bddManager.jbdd_num_vars()-1; i>=0; i-- ) {
113                long b = 1<<i;
114                if( (d.stars & b) == 0 ) {
115                    // no star
116                    jbdd varBdd = bddManager.jbdd_get_variable( i );
117                    jbdd t2 = jbdd.jbdd_or( t, varBdd, true, (d.bits & b) != 0 );
118                    // t.jbdd_free();
119                    t = t2;
120                }
121            }
122            return t;
123        }
124    
125    
126    }
127