    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    /* Generates maximal clauses, when valid tries to "shrink" to a
    017     minimal valid subclause.  */
    018
    019    public class EnumMaxClausesFindMinAbstractor implements Abstractor {
    020
    021            private /*@ non_null @*/ jbddManager bddManager;
    022
    023            private /*@ non_null @*/ jbdd R;
    024            private /*@ non_null @*/ Vector clauses = new Vector();
    025            // invariant: R = conjunction of clauses
    026
    027            private boolean noisy = Boolean.getBoolean("PANOISY");
    028
    029            private static boolean doRestrict = !Boolean.getBoolean("NORESTRICT");
    030
    031            public EnumMaxClausesFindMinAbstractor(/*@ non_null @*/ jbddManager bddManager) {
    032                    // bddManager.jbdd_num_vars
    033                    this.bddManager = bddManager;
    034                    R = bddManager.jbdd_zero();
    035            }
    036
    037            public /*@ non_null @*/ jbdd get() {
    038                    return R;
    039            }
    040
    041            public /*@ non_null @*/ Vector getClauses() {
    042                    return clauses;
    043            }
    044
    045            public boolean union(/*@ non_null @*/ Prover prover) {
    046
    047                    int notImpliedOldR = 0, impliedR = 0, ndisj=0;
    048
    049                    jbdd oldR = R;
    050                    Vector oldClauses = clauses;
    051
    052                    R = bddManager.jbdd_one();
    053                    clauses = new Vector();
    054
    055                    GenerateMaxClauses gen = new GenerateMaxClauses( bddManager );
    056
    057                    gen.restrict( oldR.jbdd_not() );
    058
    059                    for(int i=0; i<oldClauses.size(); i++) {
    060                            jbdd d = (jbdd)oldClauses.elementAt(i);
    061                            if( prover.check(d) ) {
    062                                    if( noisy ) say("Invariant still valid: "+prover.printClause(d));
    063                                    R = jbdd.jbdd_and( R, d, true, true );
    064                                    clauses.addElement(d);
    065                                    if(doRestrict) gen.restrict( d );
    066                            }
    067                    }
    068
    069                    jbdd bdd;
    070                    while( (bdd = gen.next()) != null ) {
    071
    072                            ndisj++;
    073                            if( noisy ) say("bdd = "+prover.printClause( bdd ));
    074
    075                            if( !oldR.jbdd_leq( bdd, true, true ) ) {
    076                                    notImpliedOldR++;
    077                                    say("not implied by oldR");
    078                                    continue;
    079                            }
    080
    081                            if( R.jbdd_leq( bdd, true, true ) ) {
    082                                    impliedR++;
    083                                    say("implied by curInv");
    084                                    continue;
    085                            }
    086
    087                            if( prover.check(bdd)) {
    088                                    // bdd valid, find subset that is valid
    089                                    jbdd minClause = findMinClauseValid( oldR, prover, bddManager.jbdd_zero(), bdd);
    090                                    if( noisy ) say("Invariant: "+prover.printClause(minClause));
    091                                    R = jbdd.jbdd_and( R, minClause, true, true );
    092                                    clauses.addElement(minClause);
    093                                    if(doRestrict) gen.restrict( minClause );
    094                            } else {
    095                                    //bdd.jbdd_free();
    096                            }
    097                    }
    098                    System.out.println("Clauses: "+ndisj
    099                                    +" notImpliedOldR="+notImpliedOldR
    100                                    +" impliedR="+impliedR);
    101                    System.out.println("Prover: "+prover.report());
    102
    103                    return oldR.jbdd_equal( R );
    104            }
    105
    106            private jbdd findMinClauseValid(/*@ non_null @*/ jbdd oldR,
    107                            /*@ non_null @*/ Prover prover,
    108                            /*@ non_null @*/ jbdd a,
    109                            /*@ non_null @*/ jbdd b)
    110            {
    111                    if( noisy )
    112                            say( "findMinClauseValid("+prover.printClause(a)+", "+prover.printClause(b)+")");
    113
    114                    if( !b.jbdd_is_tautology(false)) {
    115                            jbdd t = bddManager.jbdd_get_variable( b.jbdd_top_var_id() );
    116                            jbdd thn = b.jbdd_then();
    117                            jbdd b1, b2;
    118                            if( thn.jbdd_is_tautology(true)) {
    119                                    b1 = t;
    120                                    b2 = b.jbdd_else();
    121                            } else {
    122                                    b1 = jbdd.jbdd_ite( t, bddManager.jbdd_zero(), bddManager.jbdd_one(),
    123                                                    true, true, true );
    124                                    b2 = thn;
    125                            }
    126                            jbdd aorb2 = jbdd.jbdd_or( a, b2, true, true );
    127                            if( oldR.jbdd_leq( aorb2, true, true ) &&
    128                                            prover.check(aorb2) ) {
    129                                    return findMinClauseValid( oldR, prover, a, b2 );
    130                            } else {
    131                                    return findMinClauseValid( oldR, prover, jbdd.jbdd_or( a, b1, true, true), b2 );
    132                            }
    133                    } else {
    134                            return a;
    135                    }
    136            }
    137
    138            /* UNUSED
    139             private jbdd invertLiterals(jbdd t) {
    140             if( t.jbdd_is_tautology( true ) || t.jbdd_is_tautology( false ) ) {
    141             return t;
    142             } else {
    143             return jbdd.jbdd_ite( t.jbdd_top_var(),
    144             t.jbdd_else(),
    145             t.jbdd_then(),
    146             true, true, true );
    147             }
    148             }
    149             */
    150
    151            private void say(/*@ non_null @*/ String s) {
    152                    if( noisy ) {
    153                            System.out.println(s);
    154                    }
    155            }
    156
    157    }