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 }