diff --git a/.build.xml.swp b/.build.xml.swp new file mode 100644 index 00000000..45413d24 Binary files /dev/null and b/.build.xml.swp differ diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..5e56e040 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/bin diff --git a/.travis.yml b/.travis.yml index 4651be32..29f9bfe8 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,12 @@ +sudo: required + language: java +services: + - docker + +before_install: + - docker build -t meyer/java . + script: - - ant; - - ant test; + - docker run meyer/java /bin/sh -c "ant; ant test;" diff --git a/Dockerfile b/Dockerfile index e465a44f..85e22cf3 100644 --- a/Dockerfile +++ b/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/19007361/green # Download and extract Z3 RUN mkdir z3 diff --git a/README.md b/README.md index aedc3ddc..fc81562d 100644 --- a/README.md +++ b/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/19007361/green.svg?branch=master)](https://travis-ci.org/wvisser/green?branch=master) Notes: @@ -6,3 +6,22 @@ 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. +Task 1: + +Hello so I changed the test20 in SATCanonizerTest so that the 3rd argument +(expected output) is the correct canonical form of the given expression + +Task 2: + +I added this to my .travis.yml: + +sudo: required +services: + - docker +before_install: + - docker build -t meyer/java . +script: + - docker run meyer/java /bin/sh -c "ant; ant test;" + + MY GITHUB FOLDER: + https://github.com/19007361/green diff --git a/build.xml b/build.xml index 0c29bed8..696cebe4 100644 --- a/build.xml +++ b/build.xml @@ -95,7 +95,7 @@ - + @@ -103,6 +103,7 @@ + diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java new file mode 100644 index 00000000..67ddafd8 --- /dev/null +++ b/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.SortedMap; +import java.util.SortedSet; +import java.util.Stack; +import java.util.TreeMap; +import java.util.TreeSet; +import java.util.logging.Level; +import java.util.Arrays; + +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); + } + + @Override + public Set processRequest(Instance instance) { + @SuppressWarnings("unchecked") + Set result = (Set) instance.getData(getClass()); + if (result == null) { + final Map map = new HashMap(); + 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; + } + + @Override + public void report(Reporter reporter) { + reporter.report(getClass().getSimpleName(), "invocations = " + invocations); + } + + public Expression propagate(Expression expression, + Map map) { + try { + log.log(Level.FINEST, "Before Propagation: " + expression); + invocations++; + OrderingVisitor orderingVisitor = new OrderingVisitor(); + expression.accept(orderingVisitor); + expression = orderingVisitor.getExpression(); + + //TODO: step 2 + + 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; + } + + private static class OrderingVisitor extends Visitor { + + private Stack stack; + + public OrderingVisitor() { + stack = new Stack(); + } + + public Expression getExpression() { + Expression x = stack.pop(); + + System.out.println(Arrays.toString(stack.toArray())); + return x; + } + + @Override + public void postVisit(IntConstant constant) { + stack.push(constant); + System.out.println(Arrays.toString(stack.toArray())); + } + + @Override + public void postVisit(IntVariable variable) { + stack.push(variable); + System.out.println(Arrays.toString(stack.toArray())); + } + + @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) { + Expression r = stack.pop(); + Expression l = stack.pop(); + if ((r instanceof IntVariable) + && (l instanceof IntVariable) + && (((IntVariable) r).getName().compareTo( + ((IntVariable) l).getName()) < 0)) { + stack.push(new Operation(nop, r, l)); + } else if ((r instanceof IntVariable) + && (l instanceof IntConstant)) { + stack.push(new Operation(nop, r, l)); + } else { + stack.push(operation); + } + } else if (op.getArity() == 2) { + Expression r = stack.pop(); + Expression l = stack.pop(); + stack.push(new Operation(op, l, r)); + } else { + for (int i = op.getArity(); i > 0; i--) { + stack.pop(); + } + stack.push(operation); + } + } + + } + +} diff --git a/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java b/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java new file mode 100644 index 00000000..3467234a --- /dev/null +++ b/src/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.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(); + } + + @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)"); + } + + 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); + } + +} diff --git a/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java b/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java new file mode 100644 index 00000000..623e95df --- /dev/null +++ b/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java @@ -0,0 +1,183 @@ +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 SimplificationConstantPropogationTest { + + 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.simplify", + "za.ac.sun.cs.green.service.simplify.ConstantPropogation"); + + 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)&&(y==9)"); + } + + @Test + public void test01() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c2 = new IntConstant(10); + IntConstant c3 = new IntConstant(2); + 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.LT, o2, c2); // o3 : (x+y) < 10 + Operation oi = new Operation(Operation.Operator.SUB, y, c); // oi : y-1 + Operation o4 = new Operation(Operation.Operator.EQ, oi, c3); // o4 : y-1 = 2 + Operation o5 = new Operation(Operation.Operator.AND, o1, o3); // o5 : (x = 1) && (x+y < 10) + Operation o = new Operation(Operation.Operator.AND, o5, o4); // o = (x = 1) && (x+y < 10) && (y-1 = 2) + // (x = 1) && (x+y < 10) && (y-1 = 2) + check(o, "(x==1)&&(y==3)"); + } + + @Test + public void test02() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o = new Operation(Operation.Operator.LT, c1, c2); + check(o, "0==0"); + } + + @Test + public void test03() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o = new Operation(Operation.Operator.GT, c1, c2); + check(o, "0==1"); + } + + @Test + public void test04() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o1 = new Operation(Operation.Operator.LT, c1, c2); + Operation o2 = new Operation(Operation.Operator.GT, c1, c2); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + check(o, "0==1"); + } + + + + + @Test + public void test05() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c2 = new IntConstant(10); + IntConstant c3 = new IntConstant(2); + Operation o1 = new Operation(Operation.Operator.EQ, c, x); + Operation o2 = new Operation(Operation.Operator.ADD, x, y); + Operation o3 = new Operation(Operation.Operator.LT, o2, c2); + Operation oi = new Operation(Operation.Operator.SUB, y, c); + Operation o4 = new Operation(Operation.Operator.EQ, c3, oi); + Operation o5 = new Operation(Operation.Operator.AND, o1, o3); + Operation o = new Operation(Operation.Operator.AND, o5, o4); + check(o, "(1==x)&&(3==y)"); + } + + @Test + public void test06() { + 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); + Operation o1 = new Operation(Operation.Operator.EQ, x, y); + Operation o2 = new Operation(Operation.Operator.EQ, y, z); + Operation o3 = new Operation(Operation.Operator.EQ, z, c); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + o = new Operation(Operation.Operator.AND, o, o3); + check(o, "(x==1)&&((y==1)&&(z==1))"); + } + + @Test + public void test07() { + 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(2); + IntConstant c1 = new IntConstant(4); + Operation o1 = new Operation(Operation.Operator.MUL, x, y); + Operation o2 = new Operation(Operation.Operator.EQ, z, o1); // z = x * y + Operation o3 = new Operation(Operation.Operator.EQ, x, c); // x = 2 + Operation o4 = new Operation(Operation.Operator.ADD, y, x); + Operation o5 = new Operation(Operation.Operator.EQ, o4, c1); // x+y = 4 + + Operation o = new Operation(Operation.Operator.AND, o2, o3); // z = x * y && x = 2 + o = new Operation(Operation.Operator.AND, o, o5); // z = x * y && x = 2 && x+y = 4 + check(o, "(z==4)&&((x==2)&&(y==2))"); + } + + @Test + public void test08() { + IntVariable x = new IntVariable("x", 0, 99); + IntConstant c = new IntConstant(2); + IntConstant c1 = new IntConstant(4); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); + Operation o2 = new Operation(Operation.Operator.EQ, x, c1); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + + check(o, "0==1"); + } + + + + + +} diff --git a/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java b/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java index bc03d3ab..c07316b6 100644 --- a/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java +++ b/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java @@ -52,11 +52,11 @@ 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 + "\""); diff --git a/task1.md b/task1.md new file mode 100644 index 00000000..d25e8ea1 --- /dev/null +++ b/task1.md @@ -0,0 +1,2 @@ +Hello so I changed the test20 in SATCanonizerTest so that the 3rd argument +(expected output) is the correct canonical form of the given expression diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java index d48bb8c9..8d913b9f 100644 --- a/test/za/ac/sun/cs/green/EntireSuite.java +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -20,6 +20,8 @@ import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Scanner0Test; import za.ac.sun.cs.green.service.bounder.BounderTest; import za.ac.sun.cs.green.service.canonizer.SATCanonizerTest; +import za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest; +//import za.ac.sun.cs.green.service.simplify.SimplificationConstantPropogationTest; import za.ac.sun.cs.green.service.choco.SATChocoTest; import za.ac.sun.cs.green.service.cvc3.SATCVC3Test; import za.ac.sun.cs.green.service.factorizer.SATFactorizerTest; @@ -35,8 +37,10 @@ @RunWith(Suite.class) @Suite.SuiteClasses({ - SATCanonizerTest.class, - SATZ3Test.class + // SATCanonizerTest.class, + // SATZ3Test.class, + OnlyConstantPropogationTest.class +//, SimplifiedConstantPropogationTest.class, }) public class EntireSuite { @@ -75,9 +79,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() { diff --git a/test/za/ac/sun/cs/green/service/canonizer/.SATCanonizerTest.java.swp b/test/za/ac/sun/cs/green/service/canonizer/.SATCanonizerTest.java.swp new file mode 100644 index 00000000..031fa3df Binary files /dev/null and b/test/za/ac/sun/cs/green/service/canonizer/.SATCanonizerTest.java.swp differ diff --git a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java index 03f62ccf..0904dd94 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -293,7 +293,6 @@ 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); @@ -301,7 +300,6 @@ public void test20() { 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"); } -*/ }