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