SE547: Integer Test Code [2006/04/27]

file:simplebdd/test/TestArith.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: import simplebdd.integer.IntVar;
00004: import simplebdd.integer.IntConst;
00005: import simplebdd.integer.IntPred;
00006: 
00007: public class TestArith {
00008:   public static void main (String[] args) {
00009:     int max;
00010:     try {
00011:       max = Integer.parseInt (args[0]);
00012:     } catch (Exception e) {
00013:       System.out.println("Usage: TestArith max");
00014:       return;
00015:     }
00016:     new TestArith(max).run ();
00017:   }
00018:   
00019:   final IntVar x;
00020:   final IntVar y;
00021:   final IntVar z;
00022:   final IntConst zero;
00023:   final IntConst one;
00024:   final int bits;
00025:   TestArith (int bits) {
00026:     this.x = IntVar.factory.build (bits, "x");
00027:     this.y = IntVar.factory.build (bits, "y");
00028:     this.z = IntVar.factory.build (bits, "z");
00029:     this.zero = IntConst.factory.build (bits, 0);
00030:     this.one = IntConst.factory.build (bits, 1);
00031:     this.bits = bits;
00032:   }
00033:   
00034:   void runtest (IntPred p, boolean expectedValue) {
00035:     String trueString  = (expectedValue? "Good. " : "BAD!! ");
00036:     String falseString = (expectedValue? "BAD!! " : "Good. ");
00037:     if (p.isTautology ()) {
00038:       System.out.println 
00039:         (trueString + p + " is always true");
00040:     } else {
00041:       IntConst xSoln = p.not ().solution (x);
00042:       IntConst ySoln = p.not ().and (x.eq (xSoln)).solution (y);
00043:       IntConst zSoln = p.not ().and (x.eq (xSoln)).and (y.eq (ySoln)).solution (z);
00044:       System.out.println 
00045:         (falseString + p + " is sometimes false: " +
00046:          "x = " + xSoln + ", " +
00047:          "y = " + ySoln + ", " +
00048:          "z = " + zSoln +
00049:          ".");
00050:     }
00051:   }
00052:   
00053:   public void run () {
00054:     runtest (x.plus (y).eq (y.plus (x)), true);
00055:     runtest (x.plus (zero).eq (x), true);
00056:     runtest (x.plus (y.plus (z)).eq (x.plus (y).plus (z)), true);
00057:     runtest (x.geq (zero), true);
00058:     runtest (x.eq (zero), false);
00059:     runtest (x.gtr (zero), false);
00060:     runtest (x.plus (one).gtr (x), false);
00061:     runtest (x.plus (y).geq (x), false);
00062:     runtest (x.plus (x).eq (x), false);
00063:     runtest (x.plus (x).gtr (x), false);
00064:     runtest (x.plus (one).eq (x), false);
00065:   }
00066:   
00067: }
00068:

file:simplebdd/test/TestArithBrute.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: interface Test {
00004:   public boolean isTautology (int max); 
00005:   public boolean expectedValue (); 
00006: }
00007: 
00008: abstract class Test1 implements Test {
00009:   public abstract boolean test (int x);
00010:   public boolean isTautology (int max) {
00011:     for (int i=0; i < max; i++) {
00012:       if (!test (i)) { return false; }
00013:     }
00014:     return true;
00015:   }
00016: }
00017: 
00018: abstract class Test2 implements Test {
00019:   public abstract boolean test (int x, int y);
00020:   public boolean isTautology (int max) {
00021:     for (int i=0; i < max; i++) {
00022:       for (int j=0; j < max; j++) {
00023:         if (!test (i,j)) { return false; }
00024:       }
00025:     }
00026:     return true;
00027:   }
00028: }
00029: 
00030: abstract class Test3 implements Test {
00031:   public abstract  boolean test (int x, int y, int z);
00032:   public boolean isTautology (int max) {
00033:     for (int i=0; i < max; i++) {
00034:       for (int j=0; j < max; j++) {
00035:         for (int k=0; k < max; k++) {
00036:           if (!test (i,j, k)) { return false; }
00037:         }
00038:       }
00039:     }
00040:     return true;
00041:   }
00042: }
00043: 
00044: public class TestArithBrute {
00045:   public static void main (String[] args) {
00046:     int max;
00047:     try {
00048:       max = Integer.parseInt (args[0]);
00049:     } catch (Exception e) {
00050:       System.out.println("Usage: TestArithBrute max");
00051:       return;
00052:     }
00053:     new TestArithBrute(max).run ();
00054:   }
00055:   
00056:   final int bits;
00057:   final int max;
00058:   final Test[] test;
00059:   TestArithBrute (int bits) {
00060:     int[] x = new int[] {1,2,3};
00061:     x[0]=1;
00062:     x[1]=2;
00063:     x[2]=3;
00064:     this.bits = bits;
00065:     this.max = 1 << (bits-1);
00066:     this.test  = new Test[] {
00067:       new Test2 () {
00068:         public String toString () { return "x+y=y+x"; }
00069:         public boolean expectedValue () { return true; }
00070:         public boolean test (int x, int y) {
00071:           return (x+y)%max == (y+x)%max;
00072:         } },
00073:       new Test1 () {
00074:         public String toString () { return "x+0=x"; }
00075:         public boolean expectedValue () { return true; }
00076:         public boolean test (int x) {
00077:           return (x+0)%max == x;
00078:         } },
00079:       new Test3 () {
00080:         public String toString () { return "x+(y+z)=(x+y)+z"; }
00081:         public boolean expectedValue () { return true; }
00082:         public boolean test (int x, int y, int z) {
00083:           return (x+((y+z)%max))%max == (((x+y)%max)+z)%max;
00084:         } },
00085:       new Test1 () {
00086:         public String toString () { return "x>=0"; }
00087:         public boolean expectedValue () { return true; }
00088:         public boolean test (int x) {
00089:           return x>=0;
00090:         } },
00091:       new Test1 () {
00092:         public String toString () { return "X+1>x"; }
00093:         public boolean expectedValue () { return false; }
00094:         public boolean test (int x) {
00095:           return (x+1)%max > x;
00096:         } },
00097:       new Test1 () {
00098:         public String toString () { return "x+x=x"; }
00099:         public boolean expectedValue () { return false; }
00100:         public boolean test (int x) {
00101:           return (x+x)%max == x;
00102:         } },
00103:       new Test1 () {
00104:         public String toString () { return "x+x>x"; }
00105:         public boolean expectedValue () { return false; }
00106:         public boolean test (int x) {
00107:           return (x+x)%max > x;
00108:         } },
00109:       new Test1 () {
00110:         public String toString () { return "x+1=x"; }
00111:         public boolean expectedValue () { return false; }
00112:         public boolean test (int x) {
00113:           return (x+1)%max == x;
00114:         } },
00115:       new Test1 () {
00116:         public String toString () { return "x>0"; }
00117:         public boolean expectedValue () { return false; }
00118:         public boolean test (int x) {
00119:           return x>0;
00120:         } }
00121:     };
00122:   }
00123:   
00124:   public void run () {
00125:     for (int i = 0; i<test.length; i++) {
00126:       String trueString  = (test[i].expectedValue() ? "Good. " : "BAD!! ");
00127:       String falseString = (test[i].expectedValue() ? "BAD!! " : "Good. ");
00128:       if (test[i].isTautology (max)) {
00129:         System.out.println (trueString + test[i] + " is always true");
00130:       } else {
00131:         System.out.println (falseString + test[i] + " is sometimes false");
00132:       }
00133:     }
00134:   }
00135: }
00136:

file:simplebdd/test/TestSubtraction.java [source] [doc-public] [doc-private]

00001: package simplebdd.test;
00002: 
00003: public class TestSubtraction extends TestArith {
00004:   public static void main (String[] args) {
00005:     int max;
00006:     try {
00007:       max = Integer.parseInt (args[0]);
00008:     } catch (Exception e) {
00009:       System.out.println("Usage: TestSubtraction max");
00010:       return;
00011:     }
00012:     new TestSubtraction(max).run ();
00013:   }
00014:   
00015:   TestSubtraction (int bits) { super (bits); }
00016:   
00017:   public void run () {
00018:     runtest (x.minus (zero).eq (x), true);
00019:     runtest (x.minus (x).eq (zero), true);
00020:     runtest (x.plus (y).minus (y).eq (x), true);
00021:     runtest (x.plus (y).minus (x).eq (y), true);
00022:     runtest (x.minus (y).plus (y).eq (x), true);
00023:     runtest (x.minus (y.plus (z)).eq (x.minus (y).minus (z)), true);
00024:     runtest (x.gtr (x.minus (one)), false);
00025:     runtest (x.geq (x.minus (y)), false);
00026:     runtest (x.gtr (x.minus (y)), false);
00027:     runtest (x.eq (x.minus (y)), false);
00028:   }
00029:   
00030: }
00031: