    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