Constant propogation

.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;"

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

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:
 

build.xml

@@ -102,6 +102,7 @@
             <env key="LD_LIBRARY_PATH" value="lib"/>
             <sysproperty key="java.library.path" value="${z3lib}:${cvc3lib}"/>
             <classpath refid="green.classpath"/>
+            <formatter type="plain" usefile="false"/>
         </junit>
         <junitreport todir="${junit.dir}">
             <fileset dir="${junit.dir}">

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<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 = 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<Variable, Variable> 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<IntVariable, IntConstant> hashmap;
+		private Stack<Expression> stack;
+
+		public OrderingVisitor() {
+			stack = new Stack<Expression>();
+			hashmap = new HashMap<IntVariable, IntConstant>(); //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);
+				} 
+			} 
+		}
+	}
+}

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 {

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");
 	}
-*/
 }

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)");
+	}
+
+}