Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

It's not done, but it's fine #61

Open
wants to merge 18 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file added .build.xml.swp
Binary file not shown.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
/bin
11 changes: 9 additions & 2 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -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;"
2 changes: 1 addition & 1 deletion Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
21 changes: 20 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,27 @@
[![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:

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
3 changes: 2 additions & 1 deletion build.xml
Original file line number Diff line number Diff line change
Expand Up @@ -95,14 +95,15 @@
<target name="test">
<echo message="java.library.path = ${z3lib};${cvc3lib}"/>
<mkdir dir="${junit.dir}"/>
<junit fork="yes" printsummary="withOutAndErr" haltonfailure = "yes">
<junit showoutput="true" fork="yes" printsummary="on" haltonfailure = "yes">
<formatter type="xml"/>
<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"/>
<sysproperty key="java.library.path" value="${z3lib}:${cvc3lib}"/>
<classpath refid="green.classpath"/>
</junit>

<junitreport todir="${junit.dir}">
<fileset dir="${junit.dir}">
<include name="TEST-*.xml"/>
Expand Down
160 changes: 160 additions & 0 deletions src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java
Original file line number Diff line number Diff line change
@@ -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<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;
}

@Override
public void report(Reporter reporter) {
reporter.report(getClass().getSimpleName(), "invocations = " + invocations);
}

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();

//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<Expression> stack;

public OrderingVisitor() {
stack = new Stack<Expression>();
}

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

}

}
Original file line number Diff line number Diff line change
@@ -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);
}

}
Loading