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    import javafe.ast.Expr;
014    
015    import mocha.wrappers.jbdd.*;
016    
017    /* Predicate abstraction implementation using a binary decision tree [Graf-Saidi '97].
018     */
019    
020    public class BinaryDecisionTreeAbstractor implements Abstractor {
021    
022        private /*@ non_null @*/ jbddManager bddManager;
023        private int numPredicates;
024    
025        private /*@ non_null @*/ jbdd R;
026        private /*@ non_null @*/ Vector clauses = new Vector();
027        // invariant: R = conjunction of clauses
028    
029        public BinaryDecisionTreeAbstractor(/*@ non_null @*/ jbddManager bddManager) {
030            this.numPredicates = bddManager.jbdd_num_vars();
031            this.bddManager = bddManager;
032            R = bddManager.jbdd_zero();
033        }
034            
035        public /*@ non_null @*/ jbdd get() {
036            return R;
037        }
038    
039        public /*@ non_null @*/ Vector getClauses() {
040            return clauses;
041        }
042    
043        public boolean union(/*@ non_null @*/ Prover p) {
044            // System.out.println("Inside union");
045    
046            clauses = new Vector();
047            abstractHelper(0, "  ", bddManager.jbdd_zero(), clauses, p);
048    
049            jbdd oldR = R;
050            R = bddManager.jbdd_one();
051            for(int i=0; i<clauses.size(); i++) {
052                R = jbdd.jbdd_and(R, (jbdd)clauses.elementAt(i), true, true);
053            }
054            
055            return oldR.jbdd_equal( R );
056    
057        }
058    
059        /* 0 <= n <= numPredicates */
060        /* Implementation that computes a disjunction of conjuncts */
061    
062        private void abstractHelper(int n, String m, 
063                                    jbdd curTruthAss, 
064                                    /*@ non_null @*/ Vector clauses, 
065                                    /*@ non_null @*/ Prover p) {    
066            // System.out.println("Inside abstractHelper: n = " + n);
067    
068            if (n == numPredicates) 
069                return;
070    
071            jbdd varBdd = bddManager.jbdd_get_variable(n);
072    
073            for(int sign=0; sign<2; sign++) {
074    
075                String m1 = m + n + (sign==0 ? "F" : "T") + " "; 
076                //System.out.println("Checking "+m1);
077    
078                jbdd tmpTruthAss = jbdd.jbdd_or(curTruthAss, varBdd, true, (sign==1) );
079    
080                if( R.jbdd_leq(tmpTruthAss,true,true) &&
081                    p.check(tmpTruthAss) ) {
082                    clauses.addElement( tmpTruthAss );
083                } else {
084                    abstractHelper(n+1, m1, tmpTruthAss, clauses, p);
085                }
086            }
087    
088            //varBdd.jbdd_free();
089        }
090    
091    }