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 }