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 009 import javafe.util.Set; 010 import javafe.util.Location; 011 import javafe.util.Assert; 012 import javafe.util.StackVector; 013 014 import mocha.wrappers.jbdd.*; 015 016 /* Predicate abstraction implementation that works by enumerating 017 clauses in order of increasing length [Saidi-Shankar'99]. 018 */ 019 020 public class EnumClausesAbstractor implements Abstractor { 021 022 private boolean noisy = Boolean.getBoolean("PANOISY"); 023 024 private /*@ non_null @*/ jbddManager bddManager; 025 026 private /*@ non_null @*/ jbdd R; 027 private /*@ non_null @*/ Vector clauses = new Vector(); 028 private /*@ non_null @*/ Vector enumSizes; 029 private int size; 030 031 public EnumClausesAbstractor(/*@ non_null @*/ jbddManager bddManager) { 032 say("creating"); 033 this.bddManager = bddManager; 034 R = bddManager.jbdd_zero(); 035 this.enumSizes = new Vector(); 036 037 String s = System.getProperty("PA3n"); 038 039 int i; 040 while( (i=s.indexOf('.')) != -1 ) { 041 String t = s.substring(0, i); 042 say(t); 043 int ti = Integer.parseInt(t); 044 ti = Math.min( ti, bddManager.jbdd_num_vars() ); 045 Integer I = new Integer( ti ); 046 if( !enumSizes.contains(I) ) { 047 enumSizes.addElement( I ); 048 size = Math.max( ti, size ); 049 } 050 s = s.substring(i+1); 051 } 052 if( s.length() != 0 ) { 053 Assert.fail("Last character in PA3n should be a dot; instead found \""+s+"\""); 054 } 055 say("Enum clauses of length: "+enumSizes); 056 } 057 058 public /*@ non_null @*/ jbdd get() { 059 return R; 060 } 061 062 public /*@ non_null @*/ Vector getClauses() { 063 return clauses; 064 } 065 066 public boolean union(/*@ non_null @*/ Prover prover) { 067 068 jbdd valid = bddManager.jbdd_one(); 069 Vector validClauses = new Vector(); 070 071 Vector allInvalidClauses = new Vector(); 072 Vector invalidClausesPre = new Vector(); 073 invalidClausesPre.add( bddManager.jbdd_zero() ); 074 075 boolean[] notAvailVar = new boolean[bddManager.jbdd_num_vars()]; 076 077 boolean bools[] = { false, true }; 078 079 int queriesConsideredTotal=0, queriesTriedTotal=0, queriesValidTotal=0; 080 081 for(int i=1; i <= size; i++) { 082 boolean inV = enumSizes.contains( new Integer(i) ); 083 084 int queriesConsidered=0, queriesTried=0, queriesValid=0; 085 say("Considering invariants of length "+i); 086 087 Vector invalidClauses = new Vector(); 088 089 for(Enumeration e = invalidClausesPre.elements(); e.hasMoreElements(); ) { 090 jbdd d = (jbdd)e.nextElement(); 091 092 int topVar = d.jbdd_is_tautology(false) ? bddManager.jbdd_num_vars() : d.jbdd_top_var_id(); 093 if( topVar < notAvailVar.length && notAvailVar[topVar]) { 094 // mentions a var known to be always true/always false 095 continue; 096 } 097 int nextVar = topVar - 1; 098 099 for(int varNdx=nextVar; varNdx >=0; varNdx--) { 100 101 if( notAvailVar[varNdx] ) continue; 102 103 jbdd varBdd = bddManager.jbdd_get_variable( varNdx ); 104 105 for(int sign=0; sign < 2; sign++) { 106 107 jbdd newD = jbdd.jbdd_or(d, varBdd, true, bools[sign]); 108 109 if( noisy ) say("newD = "+prover.printClause( newD )); 110 111 queriesConsidered++; 112 113 // check if var already included with same sign 114 if( newD.jbdd_equal( d ) ) { 115 say("ERROR: included with same sign"); 116 continue; 117 } 118 119 // check if var already included with different sign 120 if( newD.jbdd_is_tautology(true) ) { 121 say("ERROR: included with different sign"); 122 continue; 123 } 124 125 // check if newD redundant 126 if( valid.jbdd_leq( newD, true, true ) ) { 127 say("redundant"); 128 continue; 129 } 130 131 // check if newD contradictory 132 if( valid.jbdd_leq( newD, true, false ) ) { 133 say("contradictory"); 134 continue; 135 }; 136 137 // Chk if newD an extension of something in validClauses 138 139 boolean newDMaybeValid = true; 140 141 if( !R.jbdd_leq( newD, true, true ) ) { 142 newDMaybeValid = false; 143 say("not implied by R"); 144 } 145 146 if( !inV ) { 147 invalidClauses.add( newD ); 148 say("Not in v"); 149 continue; 150 } 151 152 if( newDMaybeValid ) { 153 154 // newD is possible invariant, 155 // see if there exists d in allInvalidClauses such that 156 // valid => (newD => d) 157 // if so, newD is not valid 158 // Optimized check is (valid /\ newD) => d 159 160 jbdd validAndNewD = jbdd.jbdd_and(valid, newD, true, true); 161 162 for(Enumeration e2 = allInvalidClauses.elements(); 163 e2.hasMoreElements() && newDMaybeValid; ) { 164 jbdd d2 = (jbdd)e2.nextElement(); 165 if( validAndNewD.jbdd_leq( d2, true, true ) ) { 166 // newD not a tautology 167 newDMaybeValid = false; 168 say("invalid by earlier test"); 169 170 } 171 } 172 173 validAndNewD.jbdd_free(); 174 } 175 176 if( newDMaybeValid ) { 177 178 // newD is possible invariant, call simplify 179 boolean newDvalid = prover. check(newD); 180 if( noisy ) say( "SIMPLIFY: "+(newDvalid ? "valid" : "invalid")); 181 queriesTried++; 182 183 if( newDvalid ) { 184 queriesValid++; 185 186 // say("Invariant: "); 187 validClauses.add( newD ); 188 jbdd t = jbdd.jbdd_and( valid, newD, true, true ); 189 valid.jbdd_free(); 190 valid = t; 191 192 if( i == 1 ) { 193 // have asserted a literal 194 // remove that variable from consideration in other 195 // disjunctions 196 notAvailVar[varNdx] = true; 197 } 198 199 continue; 200 } 201 } 202 203 // newD not tautology or contradictory 204 // maybe some extension is an invariant 205 invalidClauses.add( newD ); 206 allInvalidClauses.add( newD ); 207 } // signs 208 } // var 209 } // invalidClausesPre 210 invalidClausesPre = invalidClauses; 211 System.out.println("Queries of size "+i 212 +": Considered "+ queriesConsidered 213 +" tried "+queriesTried 214 +" valid "+queriesValid); 215 216 queriesConsideredTotal += queriesConsidered; 217 queriesTriedTotal += queriesTried; 218 queriesValidTotal += queriesValid; 219 } // i 220 System.out.println("Queries of all sizes" 221 +": Considered "+ queriesConsideredTotal 222 +" tried "+queriesTriedTotal 223 +" valid "+queriesValidTotal); 224 System.out.println("Prover: "+prover.report()); 225 226 if( R.jbdd_equal( valid ) ) { 227 say("fixpt"); 228 return true; 229 } else { 230 R = valid; 231 clauses = validClauses; 232 233 return false; 234 } 235 } 236 237 private void say(String s) { 238 if( noisy ) { 239 System.out.println(s); 240 } 241 } 242 243 }