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 16 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 @@
/GREEN/nbproject/private/
3 changes: 3 additions & 0 deletions .nfs0000000004601a41000000db
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Trying location provider `geoclue2'...
Using provider `geoclue2'.
Using method `randr'.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't "git add .".

3 changes: 3 additions & 0 deletions .nfs00000000046050a8000000dc
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Trying location provider `geoclue2'...
Using provider `geoclue2'.
Using method `randr'.
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
17 changes: 17 additions & 0 deletions bin/build.properties
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# Build properties for green.
#
# It is OK to to change these properties if they do not agree with your
# setup, but do not commit it to the repository.

#target = 1.7
#source = 1.7
#bootpath = /Library/Java/JavaVirtualMachines/jdk1.7.0_75.jdk/Contents/Home/jre/lib/rt.jar

target = 1.8
source = 1.8
bootpath = /Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home/jre/lib/rt.jar

cvc3lib = /Users/jaco/Documents/RESEARCH/SYMEXE/cvc3-2.4.1/java/lib
lattepath = /Users/jaco/Documents/RESEARCH/latte-integrale-1.7.3/latte-int-1.7.3/code/latte/count
z3path = /Users/jaco/Documents/RESEARCH/SYMEXE/Z3/build/z3
z3lib = ${basedir}/lib
172 changes: 172 additions & 0 deletions bin/junit/TEST-za.ac.sun.cs.green.EntireSuite.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,172 @@
<?xml version="1.0" encoding="UTF-8" ?>

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't push your bin directory. You only want to check in source code into your remote repo.

<testsuite errors="0" failures="1" hostname="localhost" name="za.ac.sun.cs.green.EntireSuite" skipped="0" tests="1" time="0.182" timestamp="2018-08-14T08:36:57">
<properties>
<property name="java.vendor" value="Oracle Corporation" />
<property name="sun.java.launcher" value="SUN_STANDARD" />
<property name="sun.management.compiler" value="HotSpot 64-Bit Tiered Compilers" />
<property name="os.name" value="Linux" />
<property name="sun.boot.class.path" value="/usr/lib/jvm/java-8-oracle/jre/lib/resources.jar:/usr/lib/jvm/java-8-oracle/jre/lib/rt.jar:/usr/lib/jvm/java-8-oracle/jre/lib/sunrsasign.jar:/usr/lib/jvm/java-8-oracle/jre/lib/jsse.jar:/usr/lib/jvm/java-8-oracle/jre/lib/jce.jar:/usr/lib/jvm/java-8-oracle/jre/lib/charsets.jar:/usr/lib/jvm/java-8-oracle/jre/lib/jfr.jar:/usr/lib/jvm/java-8-oracle/jre/classes" />
<property name="env.PWD" value="/home/19007361/rw344/green" />
<property name="env.LANG" value="en_ZA.UTF-8" />
<property name="java.vm.specification.vendor" value="Oracle Corporation" />
<property name="ant.home" value="/usr/share/ant" />
<property name="java.runtime.version" value="1.8.0_111-b14" />
<property name="env.XDG_VTNR" value="7" />
<property name="env.DISPLAY" value=":0" />
<property name="user.name" value="19007361" />
<property name="env._" value="/usr/bin/ant" />
<property name="env.USER" value="19007361" />
<property name="env.SHELL" value="/bin/bash" />
<property name="env.DESKTOP_SESSION" value="ubuntu" />
<property name="env.XDG_DATA_DIRS" value="/usr/local/share:/usr/share:/var/lib/snapd/desktop" />
<property name="env.NLSPATH" value="/usr/dt/lib/nls/msg/%L/%N.cat" />
<property name="env.PATH" value="/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/usr/lib/jvm/java-8-oracle/bin:/usr/lib/jvm/java-8-oracle/db/bin:/usr/lib/jvm/java-8-oracle/jre/bin:/opt/openmpi-2.1.2/.openmpi/bin" />
<property name="env.XDG_CURRENT_DESKTOP" value="Unity" />
<property name="user.language" value="en" />
<property name="env.XDG_SESSION_DESKTOP" value="ubuntu" />
<property name="sun.boot.library.path" value="/usr/lib/jvm/java-8-oracle/jre/lib/amd64" />
<property name="ant.project.default-target" value="build" />
<property name="ant.project.name" value="green" />
<property name="java.version" value="1.8.0_111" />
<property name="user.timezone" value="" />
<property name="sun.arch.data.model" value="64" />
<property name="env.MATHEMATICA_HOME" value="/opt/Wolfram/Mathematica/11.0" />
<property name="java.endorsed.dirs" value="/usr/lib/jvm/java-8-oracle/jre/lib/endorsed" />
<property name="env.DERBY_HOME" value="/usr/lib/jvm/java-8-oracle/db" />
<property name="sun.cpu.isalist" value="" />
<property name="green.srcpath" value="/home/19007361/rw344/green/src:/home/19007361/rw344/green/test" />
<property name="sun.jnu.encoding" value="UTF-8" />
<property name="file.encoding.pkg" value="sun.io" />
<property name="env.SHLVL" value="2" />
<property name="file.separator" value="/" />
<property name="java.specification.name" value="Java Platform API Specification" />
<property name="java.class.version" value="52.0" />
<property name="env.GDMSESSION" value="ubuntu" />
<property name="user.country" value="ZA" />
<property name="java.home" value="/usr/lib/jvm/java-8-oracle/jre" />
<property name="z3lib" value="/home/19007361/rw344/green/lib" />
<property name="java.vm.info" value="mixed mode" />
<property name="env.LOGNAME" value="19007361" />
<property name="ant.file" value="/home/19007361/rw344/green/build.xml" />
<property name="os.version" value="4.4.0-130-generic" />
<property name="ant.file.type.green" value="file" />
<property name="env.J2REDIR" value="/usr/lib/jvm/java-8-oracle/jre" />
<property name="ant.file.green" value="/home/19007361/rw344/green/build.xml" />
<property name="path.separator" value=":" />
<property name="java.vm.version" value="25.111-b14" />
<property name="cvc3lib" value="/Users/jaco/Documents/RESEARCH/SYMEXE/cvc3-2.4.1/java/lib" />
<property name="env.LANGUAGE" value="en_ZA:en" />
<property name="ant.library.dir" value="/usr/share/ant/lib" />
<property name="output.dir" value="bin" />
<property name="env.XDG_SESSION_PATH" value="/org/freedesktop/DisplayManager/Session0" />
<property name="env.QT_QPA_PLATFORMTHEME" value="appmenu-qt5" />
<property name="env.XDG_SESSION_TYPE" value="x11" />
<property name="env.JAVA_HOME" value="/usr/lib/jvm/java-8-oracle" />
<property name="java.awt.printerjob" value="sun.print.PSPrinterJob" />
<property name="env.TERM" value="xterm-256color" />
<property name="sun.io.unicode.encoding" value="UnicodeLittle" />
<property name="awt.toolkit" value="sun.awt.X11.XToolkit" />
<property name="env.BASH_VERSION" value="4.3.48(1)-release" />
<property name="env.GDM_LANG" value="en_US" />
<property name="user.home" value="/home/19007361" />
<property name="target" value="1.8" />
<property name="java.specification.vendor" value="Oracle Corporation" />
<property name="jar.file" value="green.jar" />
<property name="env.VTE_VERSION" value="4205" />
<property name="env.WINDOWID" value="12582922" />
<property name="java.vendor.url" value="http://java.oracle.com/" />
<property name="java.library.path" value="/home/19007361/rw344/green/lib:/Users/jaco/Documents/RESEARCH/SYMEXE/cvc3-2.4.1/java/lib" />
<property name="junit.dir" value="bin/junit" />
<property name="java.vm.vendor" value="Oracle Corporation" />
<property name="env.XDG_SEAT" value="seat0" />
<property name="java.runtime.name" value="Java(TM) SE Runtime Environment" />
<property name="ant.version" value="Apache Ant(TM) version 1.9.6 compiled on July 8 2015" />
<property name="java.class.path" value="/home/19007361/rw344/green/bin:/home/19007361/rw344/green/lib/apfloat.jar:/home/19007361/rw344/green/lib/commons-exec-1.2.jar:/home/19007361/rw344/green/lib/junit_4.8.2.jar:/home/19007361/rw344/green/lib/org.hamcrest.core_1.1.0.jar:/home/19007361/rw344/green/lib/choco-solver-3.3.1.jar:/home/19007361/rw344/green/lib/slf4j-api-1.7.12.jar:/home/19007361/rw344/green/lib/slf4j-simple-1.7.12.jar:/home/19007361/rw344/green/lib/trove-3.1a1.jar:/home/19007361/rw344/green/lib/choco-solver-2.1.3.jar:/home/19007361/rw344/green/lib/libcvc3.jar:/home/19007361/rw344/green/lib/com.microsoft.z3.jar:/home/19007361/rw344/green/lib/jedis-2.0.0.jar:/usr/share/ant/lib/junit.jar:/usr/share/java/ant-launcher-1.9.6.jar:/usr/share/ant/lib/ant.jar:/usr/share/ant/lib/ant-junit.jar:/usr/share/ant/lib/ant-junit4.jar" />
<property name="sun.java.command" value="org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner za.ac.sun.cs.green.EntireSuite skipNonTests=false filtertrace=true haltOnError=false haltOnFailure=true formatter=org.apache.tools.ant.taskdefs.optional.junit.SummaryJUnitResultFormatter showoutput=true outputtoformatters=true logfailedtests=true threadid=0 logtestlistenerevents=false formatter=org.apache.tools.ant.taskdefs.optional.junit.XMLJUnitResultFormatter,/home/19007361/rw344/green/bin/junit/TEST-za.ac.sun.cs.green.EntireSuite.xml crashfile=/home/19007361/rw344/green/junitvmwatcher8473763171262493617.properties propsfile=/home/19007361/rw344/green/junit6962175800415359436.properties" />
<property name="env.XDG_SESSION_ID" value="c2" />
<property name="env.XFILESEARCHPATH" value="/usr/dt/app-defaults/%L/Dt" />
<property name="java.vm.specification.name" value="Java Virtual Machine Specification" />
<property name="ant.file.type" value="file" />
<property name="java.vm.specification.version" value="1.8" />
<property name="sun.os.patch.level" value="unknown" />
<property name="sun.cpu.endian" value="little" />
<property name="env.HOME" value="/home/19007361" />
<property name="debuglevel" value="source,lines,vars" />
<property name="lattepath" value="/Users/jaco/Documents/RESEARCH/latte-integrale-1.7.3/latte-int-1.7.3/code/latte/count" />
<property name="env.XDG_SEAT_PATH" value="/org/freedesktop/DisplayManager/Seat0" />
<property name="java.io.tmpdir" value="/tmp" />
<property name="env.LD_LIBRARY_PATH" value=":/opt/openmpi-2.1.2/.openmpi/lib/" />
<property name="java.vendor.url.bug" value="http://bugreport.sun.com/bugreport/" />
<property name="java.awt.graphicsenv" value="sun.awt.X11GraphicsEnvironment" />
<property name="os.arch" value="amd64" />
<property name="env.XDG_RUNTIME_DIR" value="/run/user/19007361" />
<property name="java.ext.dirs" value="/usr/lib/jvm/java-8-oracle/jre/lib/ext:/usr/java/packages/lib/ext" />
<property name="user.dir" value="/home/19007361/rw344/green" />
<property name="env.XAUTHORITY" value="/home/19007361/.Xauthority" />
<property name="env.J2SDKDIR" value="/usr/lib/jvm/java-8-oracle" />
<property name="line.separator" value="&#xa;" />
<property name="java.vm.name" value="Java HotSpot(TM) 64-Bit Server VM" />
<property name="basedir" value="/home/19007361/rw344/green" />
<property name="env.XDG_GREETER_DATA_DIR" value="/var/lib/lightdm-data/19007361" />
<property name="ant.java.version" value="1.8" />
<property name="ant.core.lib" value="/usr/share/ant/lib/ant.jar" />
<property name="source" value="1.8" />
<property name="file.encoding" value="UTF-8" />
<property name="bootpath" value="/Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home/jre/lib/rt.jar" />
<property name="z3path" value="/Users/jaco/Documents/RESEARCH/SYMEXE/Z3/build/z3" />
<property name="java.specification.version" value="1.8" />
<property name="ant.project.invoked-targets" value="test" />
</properties>
<testcase classname="za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest" name="test00" time="0.024">
<failure message="expected:&lt;(x==1)&amp;&amp;(([1]+y)==10)&gt; but was:&lt;(x==1)&amp;&amp;(([x]+y)==10)&gt;" type="junit.framework.AssertionFailedError">junit.framework.AssertionFailedError: expected:&lt;(x==1)&amp;&amp;(([1]+y)==10)&gt; but was:&lt;(x==1)&amp;&amp;(([x]+y)==10)&gt;
at za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest.finalCheck(OnlyConstantPropogationTest.java:59)
at za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest.check(OnlyConstantPropogationTest.java:71)
at za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest.test00(OnlyConstantPropogationTest.java:55)
</failure>
</testcase>
<system-out><![CDATA[Z3 Not Available, no tests for it will be executed
[20180814 10:36:57][za.ac.sun.cs.green.Green <init>][FINEST] Solver("anonymous1") created
[20180814 10:36:57][za.ac.sun.cs.green.Green registerService][INFO] register service: name="sat", subservice=za.ac.sun.cs.green.service.simplify.ConstantPropagation
[20180814 10:36:57][za.ac.sun.cs.green.Green registerService][INFO] register service: name="za.ac.sun.cs.green.service.simplify.ConstantPropagation", subservice=za.ac.sun.cs.green.service.sink.SinkService
[20180814 10:36:57][za.ac.sun.cs.green.taskmanager.SerialTaskManager process][INFO] processing serviceName="sat"
[20180814 10:36:57][za.ac.sun.cs.green.service.simplify.ConstantPropagation propagate][FINEST] Before Propagation: (x==1)&&((x+y)==10)
-------------------
-------------------
Stack after var push:
-------------------
-------------------
[x]
-------------------
-------------------
Stack after cons push:
-------------------
-------------------
[x, 1]
-------------------
-------------------
Stack after var push:
-------------------
-------------------
[x==1, x]
-------------------
-------------------
Stack after var push:
-------------------
-------------------
[x==1, x, y]
-------------------
-------------------
Stack after cons push:
-------------------
-------------------
[x==1, x+y, 10]
-------------------
-------------------
Stack after pop:
-------------------
-------------------
[]
[20180814 10:36:57][za.ac.sun.cs.green.service.simplify.ConstantPropagation propagate][FINEST] After Propagation: (x==1)&&((x+y)==10)
]]></system-out>
<system-err><![CDATA[]]></system-err>
</testsuite>
Loading