Propogation of constants.

.travis.yml

@@ -1,5 +1,11 @@
+sudo: required
+services:
+- docker
+
 language: java
 
+before_install:
+  - docker build -t dijkstradev/z3green .
+
 script:
- - ant;
- - ant test;
+ - docker run dijkstradev/z3green /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/dijkstradev/green
 
 # Download and extract Z3
 RUN mkdir z3

README.md

@@ -1,8 +1,7 @@
-[![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/dijkstradev/green.svg?branch=master)](https://travis-ci.org/dijkstradev/green)
 
 Notes:
 
 The first step is to update "build.properties" with your local
 settings.  You do not need to set z3 and latte, but in that case
 some unit tests won't run.
-

src/za/ac/sun/cs/green/expr/Operation.java

@@ -49,11 +49,11 @@ public static enum Operator {
 		// String Operations
 		SUBSTRING("SUBSTRING", 3, Fix.POSTFIX),
 		CONCAT("CONCAT", 2, Fix.POSTFIX),
-		TRIM("TRIM", 1, Fix.POSTFIX), 
+		TRIM("TRIM", 1, Fix.POSTFIX),
 		REPLACE("REPLACE", 3, Fix.POSTFIX),
-		REPLACEFIRST("REPLACEFIRST", 3, Fix.POSTFIX),  
+		REPLACEFIRST("REPLACEFIRST", 3, Fix.POSTFIX),
 		TOLOWERCASE("TOLOWERCASE", 2, Fix.POSTFIX),
-		TOUPPERCASE("TOUPPERCASE", 2, Fix.POSTFIX), 
+		TOUPPERCASE("TOUPPERCASE", 2, Fix.POSTFIX),
 		VALUEOF("VALUEOF", 2, Fix.POSTFIX),
 		// String Comparators
 		NOTCONTAINS("NOTCONTAINS", 2, Fix.POSTFIX),

src/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.java

@@ -73,7 +73,7 @@ public Expression canonize(Expression expression,
 			return canonized;
 		} catch (VisitorException x) {
 			log.log(Level.SEVERE,
-					"encountered an exception -- this should not be happening!",
+					"encountered an exception -- this should not be happening - probably will!",
 					x);
 		}
 		return null;

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

@@ -0,0 +1,131 @@
+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 ConstantPropogation extends BasicService {
+
+	public ConstantPropogation(Green solver){
+		super(solver);
+	}
+
+	@Override
+	public Set<Instance> processRequest(Instance instance) {
+		Expression expression = instance.getFullExpression();
+		log.log(Level.FINEST, "Before propogation: " + expression);
+		final Expression e = propegate(expression);
+		final Instance i = new Instance(getSolver(), instance.getSource(), null, e);
+		log.log(Level.FINEST, "After propogation: " + i.getExpression());
+		return Collections.singleton(i);
+	}
+
+	private Expression propegate(Expression expression){
+		try {
+			PropogationVisitor propogationVisitor = new PropogationVisitor();
+			expression.accept(propogationVisitor);
+			return propogationVisitor.getExpression();
+		} catch (VisitorException ex){
+			log.log(Level.SEVERE, "This should not be happening - probably will.",ex);
+		}
+		return null;
+	}
+
+	private static class PropogationVisitor extends Visitor {
+
+		private Map<Expression, Expression> constants;
+		private Stack<Expression> stack;
+
+		public Expression getExpression() {
+			return stack.pop();
+		}
+
+		public PropogationVisitor() {
+			stack = new Stack<Expression>();
+			this.constants = new HashMap<Expression, Expression>();
+		}
+
+		@Override
+		public void postVisit(IntConstant constant) {
+			stack.push(constant);
+		}
+
+		@Override
+		public void postVisit(IntVariable variable) {
+			stack.push(variable);
+		}
+
+		@Override
+		public void postVisit(Operation operation) throws VisitorException {
+			Operation.Operator op = operation.getOperator();
+
+			Expression r = stack.pop();
+			Expression l = stack.pop();
+
+			r = propegateForward(r, l);
+			l = propegateForward(l, r);
+
+			if (op.equals(Operation.Operator.EQ)) {
+				extractEquality(r, l);
+				extractEquality(l, r);
+			}
+
+			/* Handles the case if an equality was discovered after a potential variable to change
+			has already been visited. e.i. (x + y) is visited before ('x = 1') */
+			if (l instanceof Operation) {
+				// visit left branch of parse tree
+				l.accept(this);
+				stack.push(new Operation(op, stack.pop(), r));
+			} else {
+				stack.push(new Operation(op, l, r));
+			}
+		}
+
+	/**
+		* Determines if an 'x = 1' case exists between r and l.
+		*
+		* @param r The potential 'x'
+		* @param l The corresponding '1'
+		*/
+		private void extractEquality(Expression r, Expression l) {
+			if ((r instanceof IntVariable) && (l instanceof IntConstant)) {
+				constants.putIfAbsent(r, l);
+			}
+		}
+
+	/**
+		* Replaces an IntVariable with IntConstant if IntVariable is in 'constants'.
+		* Excludes the case where 'x = 1' --> '1 = 1'
+		*
+		* @param r IntVariable to be replaced
+		* @param l Expression to test for '1 == 1' case. (if l is an IntConstant).
+		* @return r if r is not in 'constants' else the new IntVariable
+		*/
+		private Expression propegateForward(Expression r, Expression l) {
+			IntConstant var;
+			return (var = (IntConstant) constants.get(r)) != null
+							&& r instanceof IntVariable && !(l instanceof IntConstant) ? var : r;
+		}
+	}
+
+}

src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java

@@ -52,16 +52,16 @@ public Object execute0(Service parent, Instance parentInstance, Service service,
 			result = service.allChildrenDone(instance, result);
 		}
 		if (parent != null) {
-			result = parent.childDone(parentInstance, service, instance, result); 
+			result = parent.childDone(parentInstance, service, instance, result);
 		}
 		return result;
 	}
-	
+
 	@Override
 	public Object process(final String serviceName, final Instance instance) {
 		log.info("processing serviceName=\"" + serviceName + "\"");
 		processedCount++;
-		final Set<Service> services = solver.getService(serviceName);
+		final Set<Service> services = solver.getService(serviceName); //serviceName = sat,
 		return execute(null, null, services, Collections.singleton(instance));
 	}
 

test/za/ac/sun/cs/green/EntireSuite.java

@@ -29,14 +29,16 @@
 import za.ac.sun.cs.green.service.slicer.SATSlicerTest;
 import za.ac.sun.cs.green.service.z3.SATZ3JavaTest;
 import za.ac.sun.cs.green.service.z3.SATZ3Test;
+import za.ac.sun.cs.green.service.simplify.ConstantPropogationTest;
 import za.ac.sun.cs.green.util.ParallelSATTest;
 import za.ac.sun.cs.green.util.SetServiceTest;
 import za.ac.sun.cs.green.util.SetTaskManagerTest;
 
 @RunWith(Suite.class)
 @Suite.SuiteClasses({
 	SATCanonizerTest.class,
-	SATZ3Test.class
+	SATZ3Test.class,
+	ConstantPropogationTest.class
 })
 
 public class EntireSuite {
@@ -75,9 +77,9 @@ public class EntireSuite {
 		Z3_PATH = z3;
 		HAS_Z3 = checkZ3Presence();
 		if (!HAS_Z3) {
-		  System.out.println("Z3 Not Available, no tests for it will be executed");	
+		  System.out.println("Z3 Not Available, no tests for it will be executed");
 		}
-		
+
 	}
 
 	private static boolean checkCVC3Presence() {

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

@@ -72,17 +72,17 @@ private void check(Expression expression, Expression parentExpression, String fu
 
 	@Test
 	public void test01() {
-		IntVariable v = new IntVariable("aa", 0, 99);
-		IntConstant c = new IntConstant(0);
-		Operation o = new Operation(Operation.Operator.EQ, v, c);
+		IntVariable v = new IntVariable("aa", 0, 99);  // v ->  0 < aa < 99
+		IntConstant c = new IntConstant(0);  // c -> 0
+		Operation o = new Operation(Operation.Operator.EQ, v, c); // v = c
 		check(o, "aa==0", "1*v==0");
 	}
 
 	@Test
 	public void test02() {
 		IntVariable v1 = new IntVariable("aa", 0, 99);
 		IntConstant c1 = new IntConstant(0);
-		Operation o1 = new Operation(Operation.Operator.EQ, v1, c1);
+		Operation o1 = new Operation(Operation.Operator.EQ, v1, c1); //
 		IntVariable v2 = new IntVariable("bb", 0, 99);
 		IntConstant c2 = new IntConstant(1);
 		Operation o2 = new Operation(Operation.Operator.NE, v2, c2);
@@ -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");
+		Operation o1 = new Operation(Operation.Operator.LE, c1, c1); // 2 <= 2
+		Operation o2 = new Operation(Operation.Operator.LT, v1, c1); // (0<aa<99) < 2 <= 2 --> 0 < aa <=2 --> aa<=2
+		Operation o3 = new Operation(Operation.Operator.AND, o1, o2); // 2<=2 &&
+		check(o3, "(2<=2)&&(aa<2)", "1*v+-1<=0");
 	}
-*/
+
 }

test/za/ac/sun/cs/green/service/simplify/ConstantPropogationTest.java

@@ -0,0 +1,76 @@
+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 ConstantPropogationTest {
+
+	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)");
+	}
+
+}