00001: package simplebdd.integer;
00002:
00003: import simplebdd.bool.BoolPred;
00004:
00005: public interface IntPred {
00006: public static IntPred T = new TrueImpl ();
00007: public static IntPred F = new FalseImpl ();
00008:
00009: public IntPred not ();
00010: public IntPred and (IntPred p);
00011: public IntPred or (IntPred p);
00012: public IntPred impl (IntPred p);
00013: public IntPred iff (IntPred p);
00014:
00015: public boolean isTautology ();
00016: public IntConst solution (IntVar x);
00017:
00018: public BoolPred contents ();
00019: }
00020:
00021: abstract class IntPredAbst implements IntPred {
00022: final BoolPred contents;
00023: IntPredAbst (BoolPred contents) { this.contents = contents; }
00024:
00025: public final BoolPred contents () { return this.contents; }
00026:
00027: public final IntPred not () { return new NotImpl (this); }
00028: public final IntPred and (IntPred p) { return new AndImpl (this, p); }
00029: public final IntPred or (IntPred p) { return new OrImpl (this, p); }
00030: public final IntPred impl (IntPred p) { return new ImplImpl (this, p); }
00031: public final IntPred iff (IntPred p) { return new IffImpl (this, p); }
00032:
00033: public final boolean isTautology () { return this.contents == BoolPred.T; }
00034:
00035: public final IntConst solution (IntVar var) {
00036: int result = 0;
00037: int mask = 1;
00038: BoolPred prop = this.contents ();
00039: if (prop == BoolPred.F) {
00040: throw new RuntimeException
00041: ("Can't solve " + this + " for " + var + " since it is unsatisfiable");
00042: }
00043: for (int i=0; i<var.bits(); i++) {
00044: if (prop.and (var.bit (i).not ()) == BoolPred.F) {
00045: result = result + mask;
00046: prop = prop.and (var.bit (i));
00047: } else {
00048: prop = prop.and (var.bit (i).not ());
00049: }
00050: mask = mask * 2;
00051: }
00052: return IntConst.factory.build (var.bits (), result);
00053: }
00054:
00055: protected static void sameBits (IntExp e, IntExp f) {
00056: if (e.bits () != f.bits ()) {
00057: throw new RuntimeException ("Expressions " + e + " and " + f + " have different bit lengths");
00058: }
00059: }
00060:
00061: }
00062:
00063: class TrueImpl extends IntPredAbst {
00064: TrueImpl () { super (BoolPred.T); }
00065: public String toString () { return "true"; }
00066: }
00067:
00068: class FalseImpl extends IntPredAbst {
00069: FalseImpl () { super (BoolPred.F); }
00070: public String toString () { return "false"; }
00071: }
00072:
00073: class NotImpl extends IntPredAbst {
00074: final IntPred p;
00075: NotImpl (IntPred p) { super (p.contents ().not ()); this.p = p; }
00076: public String toString () { return "!" + p; }
00077: }
00078:
00079: class AndImpl extends IntPredAbst {
00080: final IntPred p; final IntPred q;
00081: AndImpl (IntPred p, IntPred q) { super (p.contents ().and (q.contents ())); this.p = p; this.q = q; }
00082: public String toString () { return "(" + p + " && " + q + ")"; }
00083: }
00084:
00085: class OrImpl extends IntPredAbst {
00086: final IntPred p; final IntPred q;
00087: OrImpl (IntPred p, IntPred q) { super (p.contents ().or (q.contents ())); this.p = p; this.q = q; }
00088: public String toString () { return "(" + p + " || " + q + ")"; }
00089: }
00090:
00091: class ImplImpl extends IntPredAbst {
00092: final IntPred p; final IntPred q;
00093: ImplImpl (IntPred p, IntPred q) { super (p.contents ().impl (q.contents ())); this.p = p; this.q = q; }
00094: public String toString () { return "(" + p + " ==> " + q + ")"; }
00095: }
00096:
00097: class IffImpl extends IntPredAbst {
00098: final IntPred p; final IntPred q;
00099: IffImpl (IntPred p, IntPred q) { super (p.contents ().iff (q.contents ())); this.p = p; this.q = q; }
00100: public String toString () { return "(" + p + " <=> " + q + ")"; }
00101: }
00102:
00103: class EqImpl extends IntPredAbst {
00104: final IntExp e; final IntExp f;
00105: EqImpl (IntExp e, IntExp f) { super (mkContents (e, f)); this.e = e; this.f = f; }
00106: public String toString () { return "(" + e + " == " + f + ")"; }
00107:
00108: private static BoolPred mkContents (IntExp e, IntExp f) {
00109: BoolPred result = BoolPred.T;
00110: sameBits (e, f);
00111: for (int i=0; i<e.bits (); i++) {
00112: result = result.and (e.bit (i).iff (f.bit (i)));
00113: }
00114: return result;
00115: }
00116: }
00117:
00118: class GeqImpl extends IntPredAbst {
00119: final IntExp e; final IntExp f;
00120: GeqImpl (IntExp e, IntExp f) { super (mkContents (e, f)); this.e = e; this.f = f; }
00121: public String toString () { return "(" + e + " >= " + f + ")"; }
00122:
00123: private static BoolPred mkContents (IntExp e, IntExp f) {
00124: BoolPred result = BoolPred.T;
00125: sameBits (e, f);
00126: for (int i=0; i<e.bits (); i++) {
00127: result = e.bit (i).ite (f.bit (i).not ().or (result), f.bit(i).not ().and (result));
00128: }
00129: return result;
00130: }
00131: }
00132:
00133: class GtrImpl extends IntPredAbst {
00134: final IntExp e; final IntExp f;
00135: GtrImpl (IntExp e, IntExp f) { super (mkContents (e, f)); this.e = e; this.f = f; }
00136: public String toString () { return "(" + e + " > " + f + ")"; }
00137:
00138: private static BoolPred mkContents (IntExp e, IntExp f) {
00139: BoolPred result = BoolPred.F;
00140: sameBits (e, f);
00141: for (int i=0; i<e.bits (); i++) {
00142: result = e.bit (i).ite (f.bit (i).not ().or (result), f.bit(i).not ().and (result));
00143: }
00144: return result;
00145: }
00146: }
00147:
00148: abstract class IntExpAbst implements IntExp {
00149: final BoolPred[] bits;
00150:
00151: IntExpAbst (BoolPred[] bits) { this.bits = bits; }
00152:
00153: public final IntExp plus (IntExp e) { return new PlusImpl (this, e); }
00154: public final IntExp minus (IntExp e) { return new MinusImpl (this, e); }
00155:
00156: public final IntPred eq (IntExp e) { return new EqImpl (this, e); }
00157: public final IntPred geq (IntExp e) { return new GeqImpl (this, e); }
00158: public final IntPred gtr (IntExp e) { return new GtrImpl (this, e); }
00159:
00160: public final int bits () { return bits.length; }
00161: public final BoolPred bit (int i) { return bits[i]; }
00162: }
00163:
00164: class ConstImpl extends IntExpAbst implements IntConst {
00165: final int val;
00166: ConstImpl (int bits, int val) { super (mkBits (bits, val)); this.val = val; }
00167: public String toString () { return "" + val; }
00168: public int val () { return this.val; }
00169:
00170: private static BoolPred[] mkBits (int bits, int val) {
00171: BoolPred[] result = new BoolPred[bits];
00172: for (int i=0; i<bits; i++) {
00173: result[i] = (val%2 == 1 ? BoolPred.T : BoolPred.F);
00174: val = val/2;
00175: }
00176: return result;
00177: }
00178: }
00179:
00180: class VarImpl extends IntExpAbst implements IntVar {
00181: final String name;
00182: VarImpl (int bits, String name) { super (mkBits (bits, name)); this.name = name; }
00183: public String toString () { return name; }
00184:
00185: private static BoolPred[] mkBits (int bits, String name) {
00186: BoolPred[] result = new BoolPred[bits];
00187: for (int i=0; i<bits; i++) {
00188: result[i] = BoolPred.factory.buildVar ("[" + i + "]" + name);
00189: }
00190: return result;
00191: }
00192: }
00193:
00194: class PlusImpl extends IntExpAbst {
00195: final IntExp e; final IntExp f;
00196: PlusImpl (IntExp e, IntExp f) { super (mkBits (e, f)); this.e = e; this.f = f; }
00197: public String toString () { return "(" + e + " + " + f + ")"; }
00198:
00199: private static BoolPred[] mkBits (IntExp e, IntExp f) {
00200: IntPredAbst.sameBits (e, f);
00201: BoolPred[] result = new BoolPred[e.bits ()];
00202: BoolPred carry = BoolPred.F;
00203: for (int i=0; i<result.length; i++) {
00204: result[i] = e.bit (i).xor (f.bit (i)).xor (carry);
00205: carry = carry.ite (e.bit (i).or (f.bit (i)), e.bit (i).and (f.bit (i)));
00206: }
00207: return result;
00208: }
00209: }
00210:
00211: class MinusImpl extends IntExpAbst {
00212: final IntExp e; final IntExp f;
00213: MinusImpl (IntExp e, IntExp f) { super (mkBits (e, f)); this.e = e; this.f = f; }
00214: public String toString () { return "(" + e + " - " + f + ")"; }
00215:
00216: static BoolPred[] mkBits (IntExp e, IntExp f) {
00217: // TODO
00218: }
00219: }
00220:
00221: class IntConstFactoryImpl implements IntConstFactory {
00222: public IntConst build (int bits, int val) {
00223: return new ConstImpl (bits, val);
00224: }
00225: }
00226:
00227: class IntVarFactoryImpl implements IntVarFactory {
00228: public IntVar build (int bits, String name) {
00229: return new VarImpl (bits, name);
00230: }
00231: }
00232:
00233:
|
