diff --git a/.travis.yml b/.travis.yml index 4651be32..0bb6694c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,10 @@ language: java +services: + - docker + +before_install: + - docker build -t green . + script: - - ant; - - ant test; + - docker run green /bin/sh -c "ant; ant test;" diff --git a/Dockerfile b/Dockerfile index e465a44f..de7460a1 100644 --- a/Dockerfile +++ b/Dockerfile @@ -15,7 +15,13 @@ RUN apt install patchelf -y RUN apt install libgomp1 # Clone down the GreenSolver repository -RUN git clone https://github.com/wvisser/green +RUN git clone https://github.com/wiesnerbernard/green + +# +WORKDIR /green +RUN git fetch +RUN git checkout constantPropogation +WORKDIR / # Download and extract Z3 RUN mkdir z3 diff --git a/README.md b/README.md index aedc3ddc..23f04309 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build Status](https://travis-ci.org/wvisser/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master) +[![Build Status](https://travis-ci.org/wiesnerbernard/green.svg?branch=master)](https://travis-ci.org/wiesnerbernard/green?branch=master) Notes: diff --git a/build.xml b/build.xml index 0c29bed8..3bd65aae 100644 --- a/build.xml +++ b/build.xml @@ -102,6 +102,7 @@ + diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java new file mode 100644 index 00000000..583aa77f --- /dev/null +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -0,0 +1,144 @@ +package za.ac.sun.cs.green.service.simplify; + +import java.util.Collections; +import java.util.HashMap; +import java.util.Map; +import java.util.Set; +import java.util.SortedMap; +import java.util.SortedSet; +import java.util.Stack; +import java.util.TreeMap; +import java.util.TreeSet; +import java.util.logging.Level; + +import za.ac.sun.cs.green.Instance; +import za.ac.sun.cs.green.Green; +import za.ac.sun.cs.green.expr.Expression; +import za.ac.sun.cs.green.service.BasicService; +import za.ac.sun.cs.green.util.Reporter; +import za.ac.sun.cs.green.expr.Constant; +import za.ac.sun.cs.green.expr.IntConstant; +import za.ac.sun.cs.green.expr.IntVariable; +import za.ac.sun.cs.green.expr.Operation; +import za.ac.sun.cs.green.expr.Variable; +import za.ac.sun.cs.green.expr.Visitor; +import za.ac.sun.cs.green.expr.VisitorException; + +public class ConstantPropagation extends BasicService { + private int invocations = 0; + + public ConstantPropagation(Green solver) { + super(solver); + } + + /** + * Taken from SATCanonizerService.java + */ + @Override + public Set processRequest(Instance instance) { + @SuppressWarnings("unchecked") + Set result = (Set) instance.getData(getClass()); + if (result == null) { + final Map map = new HashMap(); + final Expression e = propagate(instance.getFullExpression(), map); + final Instance i = new Instance(getSolver(), instance.getSource(), null, e); + result = Collections.singleton(i); + instance.setData(getClass(), result); + } + return result; + } + + /** + * Taken from SATCanonizerService.java + */ + @Override + public void report(Reporter reporter) { + reporter.report(getClass().getSimpleName(), "invocations = " + invocations); + } + + /** + * Based off of the same method in SATCanonizerService.java + * @param expression: expression to propagate + * map: hashmap of variables + * @return updated expression + */ + public Expression propagate(Expression expression, + Map map) { + try { + log.log(Level.FINEST, "Before Propagation: " + expression); + invocations++; + OrderingVisitor orderingVisitor = new OrderingVisitor(); + expression.accept(orderingVisitor); + expression = orderingVisitor.getExpression(); + log.log(Level.FINEST, "After Propagation: " + expression); + return expression; + } catch (VisitorException x) { + log.log(Level.SEVERE, + "encountered an exception -- this should not be happening!", + x); + } + return null; + } + + /** + * Class to handle propagation of constants + */ + private static class OrderingVisitor extends Visitor { + + private Map hashmap; + private Stack stack; + + public OrderingVisitor() { + stack = new Stack(); + hashmap = new HashMap(); //Added a hash map to store constants propagated to variables + } + + public Expression getExpression() { + return stack.pop(); + } + + @Override + public void postVisit(IntConstant constant) { + stack.push(constant); + } + + @Override + public void postVisit(IntVariable variable) { + stack.push(variable); + } + + /** + * This method propagates a constant through the expression, replacing all instances of a certain variable + * with a constant value. + * @param operation: the current operator that must be handled + */ + @Override + public void postVisit(Operation operation) throws VisitorException { + Operation.Operator op = operation.getOperator(); + if (stack.size() >= 2) { + Expression right = stack.pop(); + Expression left = stack.pop(); + if (op == Operation.Operator.EQ) { //checks for '==' + //if there is a variable to the right of the operator and an integer integer to the left + //then assign the integer value to a key corresponding to the variable + if (right instanceof IntConstant && left instanceof IntVariable) { + hashmap.put((IntVariable) left, (IntConstant) right); + } + //form the new operation and push it to the stack + Operation nop = new Operation(operation.getOperator(), left, right); + stack.push(nop); + } else { + // If the the current expression is not of the type above create a new expression and push + // it to the stack + if (hashmap.containsKey(left)) { + left = hashmap.get(left); + } else if (hashmap.containsKey(right)) { + right = hashmap.get(right); + } + Operation nop = new Operation(operation.getOperator(), left, right); + stack.push(nop); + } + } + } + } +} diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java index d48bb8c9..b084784c 100644 --- a/test/za/ac/sun/cs/green/EntireSuite.java +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -32,11 +32,13 @@ import za.ac.sun.cs.green.util.ParallelSATTest; import za.ac.sun.cs.green.util.SetServiceTest; import za.ac.sun.cs.green.util.SetTaskManagerTest; +import za.ac.sun.cs.green.service.simplify.ConstantPropagationTest; @RunWith(Suite.class) @Suite.SuiteClasses({ - SATCanonizerTest.class, - SATZ3Test.class + //SATCanonizerTest.class, + //SATZ3Test.class + ConstantPropagationTest.class }) public class EntireSuite { diff --git a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java index 03f62ccf..412a3d05 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -293,7 +293,7 @@ public void test19() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); check(o1, "2<=2", "0==0"); } -/* + @Test public void test20() { IntConstant c1 = new IntConstant(2); @@ -303,5 +303,4 @@ public void test20() { Operation o3 = new Operation(Operation.Operator.AND, o1, o2); check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); } -*/ } diff --git a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java new file mode 100644 index 00000000..6dde24f1 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java @@ -0,0 +1,74 @@ +package za.ac.sun.cs.green.service.simplify; + +import static org.junit.Assert.*; + +import java.util.Arrays; +import java.util.Properties; +import java.util.SortedSet; +import java.util.TreeSet; + +import org.junit.BeforeClass; +import org.junit.Test; + +import za.ac.sun.cs.green.Instance; +import za.ac.sun.cs.green.Green; +import za.ac.sun.cs.green.expr.Expression; +import za.ac.sun.cs.green.expr.IntConstant; +import za.ac.sun.cs.green.expr.IntVariable; +import za.ac.sun.cs.green.expr.Operation; +import za.ac.sun.cs.green.util.Configuration; + +public class ConstantPropagationTest { + + public static Green solver; + + @BeforeClass + public static void initialize() { + solver = new Green(); + Properties props = new Properties(); + props.setProperty("green.services", "sat"); + props.setProperty("green.service.sat", "(simplify sink)"); + //props.setProperty("green.service.sat", "(canonize sink)"); + props.setProperty("green.service.sat.simplify", + "za.ac.sun.cs.green.service.simplify.ConstantPropagation"); + //props.setProperty("green.service.sat.canonize", + // "za.ac.sun.cs.green.service.canonizer.SATCanonizerService"); + + props.setProperty("green.service.sat.sink", + "za.ac.sun.cs.green.service.sink.SinkService"); + Configuration config = new Configuration(solver, props); + config.configure(); + } + + private void finalCheck(String observed, String expected) { + assertEquals(expected, observed); + } + + private void check(Expression expression, String expected) { + Instance i = new Instance(solver, null, null, expression); + Expression e = i.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + Object result = i.request("sat"); + assertNotNull(result); + assertEquals(Instance.class, result.getClass()); + Instance j = (Instance) result; + finalCheck(j.getExpression().toString(), expected); + } + + @Test + public void test00() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntVariable z = new IntVariable("z", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c10 = new IntConstant(10); + IntConstant c3 = new IntConstant(3); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : x = 1 + Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : (x + y) + Operation o3 = new Operation(Operation.Operator.EQ, o2, c10); // o3 : x+y = 10 + Operation o4 = new Operation(Operation.Operator.AND, o1, o3); // o4 : x = 1 && (x+y) = 10 + check(o4, "(x==1)&&((1+y)==10)"); + } + +} diff --git a/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java new file mode 100644 index 00000000..c7995ac6 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java @@ -0,0 +1,186 @@ +package za.ac.sun.cs.green.service.simplify; + +import static org.junit.Assert.*; + +import java.util.Arrays; +import java.util.Properties; +import java.util.SortedSet; +import java.util.TreeSet; + +import org.junit.BeforeClass; +import org.junit.Test; + +import za.ac.sun.cs.green.Instance; +import za.ac.sun.cs.green.Green; +import za.ac.sun.cs.green.expr.Expression; +import za.ac.sun.cs.green.expr.IntConstant; +import za.ac.sun.cs.green.expr.IntVariable; +import za.ac.sun.cs.green.expr.Operation; +import za.ac.sun.cs.green.util.Configuration; + +public class SimplificationConstantPropogationTest { + + public static Green solver; + + @BeforeClass + public static void initialize() { + solver = new Green(); + Properties props = new Properties(); + props.setProperty("green.services", "sat"); + props.setProperty("green.service.sat", "(simplify sink)"); + //props.setProperty("green.service.sat", "(canonize sink)"); + props.setProperty("green.service.sat.simplify", + "za.ac.sun.cs.green.service.simplify.ConstantPropogation"); + //props.setProperty("green.service.sat.canonize", + // "za.ac.sun.cs.green.service.canonizer.SATCanonizerService"); + + props.setProperty("green.service.sat.sink", + "za.ac.sun.cs.green.service.sink.SinkService"); + Configuration config = new Configuration(solver, props); + config.configure(); + } + + private void finalCheck(String observed, String expected) { + assertEquals(expected, observed); + } + + private void check(Expression expression, String expected) { + Instance i = new Instance(solver, null, null, expression); + Expression e = i.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + Object result = i.request("sat"); + assertNotNull(result); + assertEquals(Instance.class, result.getClass()); + Instance j = (Instance) result; + finalCheck(j.getExpression().toString(), expected); + } + + @Test + public void test00() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntVariable z = new IntVariable("z", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c10 = new IntConstant(10); + IntConstant c3 = new IntConstant(3); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : x = 1 + Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : (x + y) + Operation o3 = new Operation(Operation.Operator.EQ, o2, c10); // o3 : x+y = 10 + Operation o4 = new Operation(Operation.Operator.AND, o1, o3); // o4 : x = 1 && (x+y) = 10 + check(o4, "(x==1)&&(y==9)"); + } + + @Test + public void test01() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c2 = new IntConstant(10); + IntConstant c3 = new IntConstant(2); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : (x = 1) + Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : x + y + Operation o3 = new Operation(Operation.Operator.LT, o2, c2); // o3 : (x+y) < 10 + Operation oi = new Operation(Operation.Operator.SUB, y, c); // oi : y-1 + Operation o4 = new Operation(Operation.Operator.EQ, oi, c3); // o4 : y-1 = 2 + Operation o5 = new Operation(Operation.Operator.AND, o1, o3); // o5 : (x = 1) && (x+y < 10) + Operation o = new Operation(Operation.Operator.AND, o5, o4); // o = (x = 1) && (x+y < 10) && (y-1 = 2) + // (x = 1) && (x+y < 10) && (y-1 = 2) + check(o, "(x==1)&&(y==3)"); + } + + @Test + public void test02() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o = new Operation(Operation.Operator.LT, c1, c2); + check(o, "0==0"); + } + + @Test + public void test03() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o = new Operation(Operation.Operator.GT, c1, c2); + check(o, "0==1"); + } + + @Test + public void test04() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o1 = new Operation(Operation.Operator.LT, c1, c2); + Operation o2 = new Operation(Operation.Operator.GT, c1, c2); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + check(o, "0==1"); + } + + + + + @Test + public void test05() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c2 = new IntConstant(10); + IntConstant c3 = new IntConstant(2); + Operation o1 = new Operation(Operation.Operator.EQ, c, x); + Operation o2 = new Operation(Operation.Operator.ADD, x, y); + Operation o3 = new Operation(Operation.Operator.LT, o2, c2); + Operation oi = new Operation(Operation.Operator.SUB, y, c); + Operation o4 = new Operation(Operation.Operator.EQ, c3, oi); + Operation o5 = new Operation(Operation.Operator.AND, o1, o3); + Operation o = new Operation(Operation.Operator.AND, o5, o4); + check(o, "(1==x)&&(3==y)"); + } + + @Test + public void test06() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntVariable z = new IntVariable("z", 0 , 99); + IntConstant c = new IntConstant(1); + Operation o1 = new Operation(Operation.Operator.EQ, x, y); + Operation o2 = new Operation(Operation.Operator.EQ, y, z); + Operation o3 = new Operation(Operation.Operator.EQ, z, c); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + o = new Operation(Operation.Operator.AND, o, o3); + check(o, "(x==1)&&((y==1)&&(z==1))"); + } + + @Test + public void test07() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntVariable z = new IntVariable("z", 0 , 99); + IntConstant c = new IntConstant(2); + IntConstant c1 = new IntConstant(4); + Operation o1 = new Operation(Operation.Operator.MUL, x, y); + Operation o2 = new Operation(Operation.Operator.EQ, z, o1); // z = x * y + Operation o3 = new Operation(Operation.Operator.EQ, x, c); // x = 2 + Operation o4 = new Operation(Operation.Operator.ADD, y, x); + Operation o5 = new Operation(Operation.Operator.EQ, o4, c1); // x+y = 4 + + Operation o = new Operation(Operation.Operator.AND, o2, o3); // z = x * y && x = 2 + o = new Operation(Operation.Operator.AND, o, o5); // z = x * y && x = 2 && x+y = 4 + check(o, "(z==4)&&((x==2)&&(y==2))"); + } + + @Test + public void test08() { + IntVariable x = new IntVariable("x", 0, 99); + IntConstant c = new IntConstant(2); + IntConstant c1 = new IntConstant(4); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); + Operation o2 = new Operation(Operation.Operator.EQ, x, c1); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + + check(o, "0==1"); + } + + + + + +}