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    }