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    }