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 }