    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    }