    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    }