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 }