| 1 | package performance;
|
|---|
| 2 |
|
|---|
| 3 | import static org.junit.Assert.assertEquals;
|
|---|
| 4 |
|
|---|
| 5 | import java.util.Arrays;
|
|---|
| 6 |
|
|---|
| 7 | import org.junit.Test;
|
|---|
| 8 |
|
|---|
| 9 | import dev.civl.sarl.SARL;
|
|---|
| 10 | import dev.civl.sarl.IF.SymbolicUniverse;
|
|---|
| 11 | import dev.civl.sarl.IF.expr.BooleanExpression;
|
|---|
| 12 | import dev.civl.sarl.IF.expr.NumericExpression;
|
|---|
| 13 | import dev.civl.sarl.IF.expr.NumericSymbolicConstant;
|
|---|
| 14 | import dev.civl.sarl.IF.expr.SymbolicConstant;
|
|---|
| 15 | import dev.civl.sarl.IF.type.SymbolicArrayType;
|
|---|
| 16 | import dev.civl.sarl.IF.type.SymbolicFunctionType;
|
|---|
| 17 | import dev.civl.sarl.IF.type.SymbolicType;
|
|---|
| 18 |
|
|---|
| 19 | public class PerformanceTest {
|
|---|
| 20 |
|
|---|
| 21 | static public BooleanExpression slowNegationFormula(boolean unsat,
|
|---|
| 22 | SymbolicUniverse u) {
|
|---|
| 23 | // types:
|
|---|
| 24 | SymbolicType intType = u.integerType();
|
|---|
| 25 | SymbolicArrayType arrayType = u.arrayType(intType);
|
|---|
| 26 | SymbolicFunctionType funcType = u.functionType(
|
|---|
| 27 | Arrays.asList(arrayType, intType, intType, intType, intType),
|
|---|
| 28 | u.booleanType());
|
|---|
| 29 | // constants:
|
|---|
| 30 | NumericSymbolicConstant X_N = (NumericSymbolicConstant) u
|
|---|
| 31 | .symbolicConstant(u.stringObject("X_N"), u.integerType());
|
|---|
| 32 | NumericSymbolicConstant Y0 = (NumericSymbolicConstant) u
|
|---|
| 33 | .symbolicConstant(u.stringObject("Y0"), intType);
|
|---|
| 34 | NumericSymbolicConstant Y1 = (NumericSymbolicConstant) u
|
|---|
| 35 | .symbolicConstant(u.stringObject("Y1"), intType);
|
|---|
| 36 | NumericSymbolicConstant Y2 = (NumericSymbolicConstant) u
|
|---|
| 37 | .symbolicConstant(u.stringObject("Y2"), intType);
|
|---|
| 38 | NumericSymbolicConstant Y3 = (NumericSymbolicConstant) u
|
|---|
| 39 | .symbolicConstant(u.stringObject("Y3"), intType);
|
|---|
| 40 | BooleanExpression Y4 = (BooleanExpression) u
|
|---|
| 41 | .symbolicConstant(u.stringObject("Y4"), u.booleanType());
|
|---|
| 42 | BooleanExpression Y5 = (BooleanExpression) u
|
|---|
| 43 | .symbolicConstant(u.stringObject("Y5"), u.booleanType());
|
|---|
| 44 | NumericSymbolicConstant Y6 = (NumericSymbolicConstant) u
|
|---|
| 45 | .symbolicConstant(u.stringObject("Y6"), intType);
|
|---|
| 46 | NumericSymbolicConstant Y7 = (NumericSymbolicConstant) u
|
|---|
| 47 | .symbolicConstant(u.stringObject("Y7"), intType);
|
|---|
| 48 | SymbolicConstant array = u.symbolicConstant(u.stringObject("X_a"),
|
|---|
| 49 | arrayType);
|
|---|
| 50 | SymbolicConstant isDuplet = u
|
|---|
| 51 | .symbolicConstant(u.stringObject("is_duplet"), funcType);
|
|---|
| 52 | // clauses:
|
|---|
| 53 | BooleanExpression clauses[] = new BooleanExpression[17];
|
|---|
| 54 |
|
|---|
| 55 | clauses[0] = u.lessThan(u.oneInt(), X_N);
|
|---|
| 56 | clauses[1] = u.or(u.equals(u.oneInt(), u.subtract(X_N, Y7)), Y5);
|
|---|
| 57 | clauses[2] = u.or(u.equals(Y6, u.add(Y0, u.oneInt())), u.not(Y4));
|
|---|
| 58 | clauses[3] = u.or(u.equals(Y7, u.add(Y2, u.oneInt())), u.not(Y5));
|
|---|
| 59 | clauses[4] = u.or(u.equals(Y0, u.zeroInt()), Y4);
|
|---|
| 60 | clauses[5] = u.or(u.equals(Y2, u.zeroInt()), Y5);
|
|---|
| 61 | clauses[6] = u.or(u.lessThanEquals(u.add(Y0, u.oneInt()), Y1),
|
|---|
| 62 | u.not(Y4));
|
|---|
| 63 | clauses[7] = u.or(u.lessThanEquals(u.add(Y2, u.oneInt()), Y3),
|
|---|
| 64 | u.not(Y5));
|
|---|
| 65 | clauses[8] = u.or(u.lessThanEquals(Y1, u.subtract(X_N, u.oneInt())),
|
|---|
| 66 | u.not(Y4));
|
|---|
| 67 | clauses[9] = u.or(u.lessThanEquals(Y3, u.subtract(X_N, u.oneInt())),
|
|---|
| 68 | u.not(Y5));
|
|---|
| 69 | clauses[10] = u.or(u.lessThanEquals(u.oneInt(), Y6), u.not(Y4));
|
|---|
| 70 | clauses[11] = u.or(u.lessThanEquals(u.oneInt(), Y7), u.not(Y5));
|
|---|
| 71 | clauses[12] = u.or(
|
|---|
| 72 | u.neq(u.zeroInt(),
|
|---|
| 73 | u.subtract((NumericExpression) u.arrayRead(array, Y0),
|
|---|
| 74 | (NumericExpression) u.arrayRead(array, Y2))),
|
|---|
| 75 | u.not(Y5));
|
|---|
| 76 | clauses[13] = u.or(
|
|---|
| 77 | (BooleanExpression) u.apply(isDuplet,
|
|---|
| 78 | Arrays.asList(array, u.zeroInt(), X_N, Y0, Y1)),
|
|---|
| 79 | u.not(Y4));
|
|---|
| 80 | clauses[14] = u.or(
|
|---|
| 81 | (BooleanExpression) u.apply(isDuplet,
|
|---|
| 82 | Arrays.asList(array, u.zeroInt(), X_N, Y2, Y3)),
|
|---|
| 83 | u.not(Y5));
|
|---|
| 84 | clauses[15] = u.or(u.equals(u.oneInt(), u.subtract(X_N, Y6)), Y4);
|
|---|
| 85 | if (unsat)
|
|---|
| 86 | clauses[16] = u.lessThan(X_N, u.zeroInt());
|
|---|
| 87 | else
|
|---|
| 88 | clauses[16] = u.trueExpression();
|
|---|
| 89 | // ret:
|
|---|
| 90 | return u.and(Arrays.asList(clauses));
|
|---|
| 91 | }
|
|---|
| 92 |
|
|---|
| 93 | /**
|
|---|
| 94 | * The negation of <code>
|
|---|
| 95 | * 0 <= X_N - 1*Y7 - 1 &&
|
|---|
| 96 | * 0 <= X_N - 3 &&
|
|---|
| 97 | * 0 <= Y6 &&
|
|---|
| 98 | * 0 <= Y7 &&
|
|---|
| 99 | * (is_duplet(X_a,0,X_N,Y0,Y1) || (!Y4)) &&
|
|---|
| 100 | * (is_duplet(X_a,0,X_N,Y2,Y3) || (!Y5)) &&
|
|---|
| 101 | * ((0 == X_N - 1*Y6 - 1) || Y4) &&
|
|---|
| 102 | * ((0 == X_N - 1*Y7 - 1) || Y5) &&
|
|---|
| 103 | * ((0 == Y0 - 1*Y6 + 1) || (!Y4)) &&
|
|---|
| 104 | * ((0 == Y2 - 1*Y7 + 1) || (!Y5)) &&
|
|---|
| 105 | * ((0 == Y0) || Y4) &&
|
|---|
| 106 | * ((0 == Y2) || Y5) &&
|
|---|
| 107 | * ((Y0 - 1*Y1 + 1 <= 0) || (!Y4)) &&
|
|---|
| 108 | * ((Y2 - 1*Y3 + 1 <= 0) || (!Y5)) &&
|
|---|
| 109 | * ((0 <= X_N - 1*Y1 - 1) || (!Y4)) &&
|
|---|
| 110 | * ((0 <= X_N - 1*Y3 - 1) || (!Y5)) &&
|
|---|
| 111 | * ((0 <= Y6 - 1) || (!Y4)) &&
|
|---|
| 112 | * ((0 <= Y7 - 1) || (!Y5)) &&
|
|---|
| 113 | * ((0 != X_a[Y0] - 1*X_a[Y2]) || (!Y5)) &&
|
|---|
| 114 | * 0 <= X_N - 1*Y6 - 1 &&
|
|---|
| 115 | * X_N <= 0
|
|---|
| 116 | * </code>
|
|---|
| 117 | */
|
|---|
| 118 | @Test
|
|---|
| 119 | public void slowNegation() {
|
|---|
| 120 | SymbolicUniverse u = SARL.newStandardUniverse();
|
|---|
| 121 | // test:
|
|---|
| 122 | BooleanExpression negation = u.not(slowNegationFormula(true, u));
|
|---|
| 123 |
|
|---|
| 124 | assertEquals(u.trueExpression(),
|
|---|
| 125 | u.reasoner(u.trueExpression()).simplify(negation));
|
|---|
| 126 | }
|
|---|
| 127 | }
|
|---|
