Constant progration

.travis.yml

@@ -1,5 +1,11 @@
 language: java
 
+services:
+ - docker
+
+before_install:
+  - docker build -t green .
+
+
 script:
- - ant;
- - ant test;
+  - docker run 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/xaniniehaus/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/XaniNiehaus/green.svg?branch=master)](https://travis-ci.org/XaniNiehaus/green)
 
 Notes:
 

build.xml

@@ -96,7 +96,7 @@
     	<echo message="java.library.path = ${z3lib};${cvc3lib}"/>
         <mkdir dir="${junit.dir}"/>
         <junit fork="yes" printsummary="withOutAndErr" haltonfailure = "yes">
-            <formatter type="xml"/>
+            <formatter type="plain" usefile="false"/>
             <test name="za.ac.sun.cs.green.EntireSuite" todir="${junit.dir}"/>
             <env key="DYLD_LIBRARY_PATH" value="lib"/>
             <env key="LD_LIBRARY_PATH" value="lib"/>

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

@@ -0,0 +1,158 @@
+package za.ac.sun.cs.green.service.simplify;
+
+import za.ac.sun.cs.green.Green;
+import za.ac.sun.cs.green.Instance;
+import za.ac.sun.cs.green.expr.*;
+import za.ac.sun.cs.green.service.BasicService;
+
+import java.util.*;
+
+public class ConstantPropogation extends BasicService {
+    public ConstantPropogation(Green solver) {
+        super(solver);
+    }
+
+    @Override
+    public Set<Instance> processRequest(Instance instance) {
+        @SuppressWarnings("unchecked")
+        Set<Instance> result = (Set<Instance>) instance.getData(getClass());
+        if (result == null) {
+            try {
+                final Map<Variable, Variable> map = new HashMap<Variable, Variable>();
+                final Expression e = instance.getFullExpression();
+                ConstantCheckerVisitor checkerVisitor = new ConstantCheckerVisitor();
+                e.accept(checkerVisitor);
+                ConstantPropagatorVisitor propagatorVisitor = new ConstantPropagatorVisitor(checkerVisitor.getMap());
+                e.accept(propagatorVisitor);
+                Expression propagated = propagatorVisitor.getExpression();
+                final Instance i = new Instance(getSolver(), instance.getSource(), null, propagated);
+                result = Collections.singleton(i);
+                instance.setData(getClass(), result);
+            } catch (VisitorException e1) {
+                e1.printStackTrace();
+            }
+        }
+        return result;
+    }
+
+    private static class ConstantCheckerVisitor extends Visitor {
+
+        private int location;
+        private Stack<Expression> stack;
+        private HashMap<String, Pair> map;
+
+        public ConstantCheckerVisitor() {
+            location = 0;
+            stack = new Stack<Expression>();
+            map = new HashMap<String, Pair>();
+        }
+
+        @Override
+        public void postVisit(IntConstant constant) {
+            location++;
+            stack.push(constant);
+        }
+
+        @Override
+        public void postVisit(IntVariable variable) {
+            location++;
+            stack.push(variable);
+        }
+
+        @Override
+        public void postVisit(Operation operation) throws VisitorException {
+            location++;
+            if (operation.getOperator() != Operation.Operator.EQ) {
+                stack.push(operation);
+                return;
+            }
+            Expression a = stack.pop();
+            Expression b = stack.pop();
+            if (a instanceof Constant && b instanceof Variable) {
+                map.put(b.toString(), new Pair(a, location));
+            } else if (a instanceof Variable && b instanceof Constant) {
+                map.put(a.toString(), new Pair(b, location));
+            }
+            stack.push(operation);
+        }
+
+        public HashMap<String, Pair> getMap() {
+            return map;
+        }
+    }
+
+    private static class ConstantPropagatorVisitor extends Visitor {
+
+        private int location;
+        private Stack<Expression> stack;
+        private Map<String, Pair> map;
+
+        public ConstantPropagatorVisitor(HashMap<String, Pair> map) {
+            location = 0;
+            stack = new Stack<Expression>();
+            this.map = map;
+        }
+
+        @Override
+        public void postVisit(IntConstant constant) {
+            location++;
+            stack.push(constant);
+        }
+
+        @Override
+        public void postVisit(IntVariable variable) {
+            location++;
+            stack.push(variable);
+        }
+
+        @Override
+        public void postVisit(Operation operation) throws VisitorException {
+            location++;
+            Expression a = stack.pop();
+            Expression b = stack.pop();
+            if (map.containsKey(a.toString())) {
+                if (location != map.get(a.toString()).getGetLocation()) {
+                    Expression temp = new Operation(operation.getOperator(), a, map.get(b.toString()).getExpr());
+                    stack.push(temp);
+                    return;
+                }
+                stack.push(new Operation(operation.getOperator(), b, a));
+            } else if (map.containsKey(b.toString())) {
+                if (location != map.get(b.toString()).getGetLocation()) {
+                    Expression temp = new Operation(operation.getOperator(), map.get(b.toString()).getExpr(), a);
+                    stack.push(temp);
+                    return;
+                }
+                stack.push(new Operation(operation.getOperator(), b, a));
+            } else {
+                Expression temp = new Operation(operation.getOperator(), b, a);
+                stack.push(temp);
+            }
+
+        }
+
+        public Expression getExpression() {
+            return stack.pop();
+        }
+
+    }
+
+    private static class Pair {
+        Expression expr;
+        int location;
+
+        Pair(Expression expr, int location) {
+            this.expr = expr;
+            this.location = location;
+        }
+
+        public int getGetLocation() {
+            return location;
+        }
+
+        public Expression getExpr() {
+            return expr;
+        }
+    }
+
+}

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 OnlyConstantPropogationTest {
+
+	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)&&((1+y)==10)");
+	}
+
+}