only OnlyConstantPropagation finished

.travis.yml

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

build.xml

@@ -96,6 +96,7 @@
     	<echo message="java.library.path = ${z3lib};${cvc3lib}"/>
         <mkdir dir="${junit.dir}"/>
         <junit fork="yes" printsummary="withOutAndErr" haltonfailure = "yes">
+            <formatter type="plain" usefile="false"/>
             <formatter type="xml"/>
             <test name="za.ac.sun.cs.green.EntireSuite" todir="${junit.dir}"/>
             <env key="DYLD_LIBRARY_PATH" value="lib"/>
@@ -110,7 +111,6 @@
             <report format="frames" todir="${junit.dir}"/>
         </junitreport>
     </target>
-
 <!--
     TARGET: package
 -->

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

@@ -0,0 +1,194 @@
+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.expr.Variable;
+import za.ac.sun.cs.green.expr.Visitor;
+import za.ac.sun.cs.green.expr.VisitorException;
+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;
+
+public class ConstantPropogation extends BasicService {
+
+
+    private int invocations = 0;
+
+    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) {
+			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);
+			final Instance f = new Instance(getSolver(), instance.getSource(), null , e);
+			result = Collections.singleton(i);
+			instance.setData(getClass(), result);
+		}
+		return result;
+	}
+
+	@Override
+	public void report(Reporter reporter) {
+			reporter.report(getClass().getSimpleName(), "invocations = " + invocations);
+	}
+
+	public Expression propagateConstants(Expression expr, Map<Variable, Variable> map) {
+			 try {
+					 log.log(Level.FINEST, "Before Constant Propagation: " + expr);
+					 invocations++;
+					 cPvisitor cPv = new cPvisitor();
+				 	 cPvisitor cpVVtest = new cPvisitor();
+					 expr.accept(cPv);
+				 	 Expression propTest;
+					 Expression prop = cPv.getExpression();
+					 log.log(Level.FINEST, "After Constant Propagation: " + prop);
+					 return prop;
+			 } catch (VisitorException ex) {
+					 log.log(Level.SEVERE, "Something is not right.", ex);
+			 }
+
+			 return null;
+	 }
+
+
+
+	 private static class cPvisitor extends Visitor {
+		 		private Stack<Expression> stack;
+		 		private Stack<Expression> stackyMcStackStack;
+		 		private Map<IntVariable, IntConstant> Vmap;
+				private Map<IntVariable , IntConstant> mappy;
+
+ 				public cPvisitor() {
+ 					 stack = new Stack<Expression>();
+					 stackyMcStackStack = new Stack<Expression>();
+					 Vmap = new TreeMap<IntVariable, IntConstant>();
+					 mappy = new TreeMap<IntVariable , IntConstant>();
+ 				}
+
+ 		public Expression getExpression() {
+			Expression ex = null;
+			if(stack.isEmpty()){
+						return null;
+
+					}else{
+						ex = stack.pop();
+
+					}
+		 				return ex;
+ 		}
+
+ 		@Override
+ 		public void postVisit(Constant cons) {
+			if(cons instanceof IntConstant){
+				stack.push(cons);
+				stackyMcStackStack.push(cons);
+			} else {
+
+					stack.clear();
+					stackyMcStackStack.clear();
+				}
+
+
+ 		}
+
+ 		@Override
+ 		public void postVisit(Variable var) {
+			if(var instanceof IntVariable){
+				stack.push(var);
+				stackyMcStackStack.push(var);
+			} else {
+					stack.clear();
+					stackyMcStackStack.clear();
+				}
+
+
+ 		}
+
+ 		@Override
+ 		public void postVisit(Operation operation) throws VisitorException {
+      			Operation.Operator op = operation.getOperator();
+			Operation.Operator nop = null;
+			switch (op) {
+			case EQ:
+				nop = Operation.Operator.EQ;
+				break;
+			case NE:
+				nop = Operation.Operator.NE;
+				break;
+			case LT:
+				nop = Operation.Operator.GT;
+				break;
+			case LE:
+				nop = Operation.Operator.GE;
+				break;
+			case GT:
+				nop = Operation.Operator.LT;
+				break;
+			case GE:
+				nop = Operation.Operator.LE;
+				break;
+			default:
+				break;
+			}
+			if (nop != null) {
+				if(stackyMcStackStack.size()>=2){
+					Expression rR = stackyMcStackStack.pop();
+					Expression lL = stackyMcStackStack.pop();	
+					   if((lL instanceof IntVariable) && (rR instanceof IntConstant)){
+					  mappy.put((IntVariable)lL ,(IntConstant) rR);
+				      }else if((rR instanceof IntVariable) && (lL instanceof IntConstant)){
+					  mappy.put((IntVariable)rR,(IntConstant)lL);
+				      }
+	 			 }
+			}
+
+
+      if(stack.size()>=2){
+          Expression r = stack.pop();
+	  Expression l = stack.pop();
+	  Operation.Operator oper = op;
+          if(oper.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(oper,l,r));
+            } else if(!oper.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(oper , l , r));
+            }
+          }
+      }
+      //return null;
+ 		}
+
+ 	}
+
+

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

@@ -14,7 +14,8 @@
 import org.junit.runners.Suite;
 
 import com.microsoft.z3.Context;
-
+import za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest;
+import za.ac.sun.cs.green.service.simplify.SimplificationConstantPropogationTest;
 import cvc3.ValidityChecker;
 import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Parser0Test;
 import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Scanner0Test;
@@ -32,11 +33,14 @@
 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.OnlyConstantPropogationTest;
 
 @RunWith(Suite.class)
 @Suite.SuiteClasses({
-	SATCanonizerTest.class,
-	SATZ3Test.class
+	//SATCanonizerTest.class,
+	//SATZ3Test.class
+	OnlyConstantPropogationTest.class,
+	//SimplificationConstantPropogationTest.class
 })
 
 public class EntireSuite {
@@ -67,7 +71,8 @@ public class EntireSuite {
 				barvinok = p.getProperty("barvinokpath");
 				z3 = p.getProperty("z3path");
 			} catch (IOException e) {
-				// do nothing
+				 //do nothing
+
 			}
 		}
 		LATTE_PATH = latte;

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