Joshua Coetzer pull request

.travis.yml

@@ -1,5 +1,12 @@
+sudo: required
+
 language: java
 
+services:
+  - docker
+
+before_install:
+  - docker build -t joshua/green .
+
 script:
- - ant;
- - ant test;
+  - docker run joshua/green /bin/sh -c "ant; ant test"

Dockerfile

@@ -15,7 +15,7 @@ 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/Cezkarma/green
 
 # Download and extract Z3
 RUN mkdir z3

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/Cezkarma/green.svg?branch=master)](https://travis-ci.org/Cezkarma/green.svg?branch=master)
 
 Notes:
 

src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java

@@ -0,0 +1,160 @@
+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.Stack;
+import java.util.TreeMap;
+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 {
+
+    /**
+     * Number of times the slicer has been invoked.
+     */
+    private int invocations = 0;
+
+    public ConstantPropagation(Green solver) {
+        super(solver);
+    }
+
+	/**
+	 * this method processes a request and returns the result
+	 */
+    @Override
+    public Set<Instance> processRequest(Instance instance) {
+        @SuppressWarnings("unchecked")
+        Set<Instance> result = (Set<Instance>) instance.getData(getClass());
+        if (result == null) {
+            final Map<Variable, Variable> map = new HashMap<Variable, Variable>();
+            final Expression e = propagateConstants(instance.getFullExpression(), map);
+            final Instance i = new Instance(getSolver(), instance.getSource(), null, e);
+            result = Collections.singleton(i);
+            instance.setData(getClass(), result);
+        }
+
+        return result;
+    }
+
+	/**
+	 * this method reports and is indifferent from the method found in the canonizer
+	 */
+    @Override
+    public void report(Reporter reporter) {
+        reporter.report(getClass().getSimpleName(), "invocations = " + invocations);
+    }
+
+	/**
+	 * this method is used to apply propagation to the constants
+	 */
+    public Expression propagateConstants(Expression expression, Map<Variable, Variable> map) {
+        try {
+            log.log(Level.FINEST, "Before Constant Propagation: " + expression);
+            invocations++;
+
+            ConstantPropagationVisitor constantPropagationVisitor = new ConstantPropagationVisitor();
+            expression.accept(constantPropagationVisitor);
+            Expression propagated = constantPropagationVisitor.getExpression();
+
+            log.log(Level.FINEST, "After Constant Propagation: " + propagated);
+            return propagated;
+        } catch (VisitorException x) {
+            log.log(Level.SEVERE, "encountered an exception -- this should not be happening!", x);
+        }
+
+        return null;
+    }
+
+    private static class ConstantPropagationVisitor extends Visitor {
+        private Stack<Expression> stack;
+        private Map<IntVariable, IntConstant> vMap;
+
+		/**
+	 	* this is the constructor
+	 	*/
+        public ConstantPropagationVisitor() {
+            stack = new Stack<Expression>();
+            vMap = new TreeMap<IntVariable, IntConstant>();
+        }
+
+		/**
+	 	* get the expression
+	 	*/
+        public Expression getExpression() {
+            Expression e = null;
+            if (stack.isEmpty()) {
+                return e;
+            } else {
+            	e = stack.pop();
+            }
+
+            return e;
+        }
+
+		/**
+	 	* pushes a constant onto the stack
+	 	*/
+        @Override
+        public void postVisit(Constant constant) {
+            if (!(constant instanceof IntConstant)) {
+                stack.clear();
+            } else {
+                stack.push(constant);
+            }
+        }
+
+		/**
+	 	* pushes a variable onto the stack
+	 	*/
+        @Override
+        public void postVisit(Variable variable) {
+            if (!(variable instanceof IntVariable)) {
+                stack.clear();
+            } else {
+                stack.push(variable);
+            }
+        }
+
+		/**
+	 	* pushes a new operation onto the stack
+	 	*/
+        @Override
+        public void postVisit(Operation operation) throws VisitorException {
+            int ss = stack.size();
+            if (ss > 1) {
+                Expression r = stack.pop();
+                Expression l = stack.pop();
+                Operation.Operator op = operation.getOperator();
+                if (op.equals(Operation.Operator.EQ)) {
+                    if ((l instanceof IntVariable) && (r instanceof IntConstant)) {
+                        vMap.put((IntVariable) l, (IntConstant) r);
+                    } else if ((r instanceof IntVariable) && (l instanceof IntConstant)) {
+                        vMap.put((IntVariable) r, (IntConstant) l);
+                    }
+                    stack.push(new Operation(op, l, r));
+                } else if (!op.equals(Operation.Operator.EQ)) {
+                    if (vMap.containsKey(l)) {
+                        l = vMap.get(l);
+                    } else if (vMap.containsKey(r)) {
+                        r = vMap.get(r);
+                    }
+                    stack.push(new Operation(op, l, r));
+                }
+            }
+        }
+    }
+}

test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java

@@ -293,15 +293,15 @@ 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);
 		IntVariable v1 = new IntVariable("aa", 0, 99);
 		Operation o1 = new Operation(Operation.Operator.LE, c1, c1);
 		Operation o2 = new Operation(Operation.Operator.LT, v1, c1);
 		Operation o3 = new Operation(Operation.Operator.AND, o1, o2);
-		check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0");
+		check(o3, "(2<=2)&&(aa<2)", "1*v+-1<=0");
 	}
-*/
+
 }

test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.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 OnlyConstantPropagationTest {
+
+    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)");
+    }
+
+}