From 2480682d11872bb190455a6d63cd7f52aae1bce4 Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 10:25:11 +0200 Subject: [PATCH 01/56] Changed travis --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index aedc3ddc..f8913b11 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/marcdefaria/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master) Notes: From 6e4ed0968747741fccb7a37df4171c265a4d97a4 Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 10:45:03 +0200 Subject: [PATCH 02/56] Uncommented broken test --- .../ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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..d09af7c9 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -60,7 +60,7 @@ private void check(Expression expression, Expression parentExpression, String fu Instance i1 = new Instance(solver, null, parentExpression); Instance i2 = new Instance(solver, i1, expression); Expression e = i2.getExpression(); - assertTrue(e.equals(expression)); + assertTrue(e SATCanonizerTest there is one testcase that is commented out. .equals(expression)); assertEquals(expression.toString(), e.toString()); assertEquals(full, i2.getFullExpression().toString()); Object result = i2.request("sat"); @@ -293,7 +293,7 @@ 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); @@ -303,5 +303,5 @@ public void test20() { Operation o3 = new Operation(Operation.Operator.AND, o1, o2); check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); } -*/ + } From e6cdce72eaeab28c2f97937689b496e1b56284fd Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 10:54:44 +0200 Subject: [PATCH 03/56] Fixed self made error in SAT --- .../ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 d09af7c9..29dfc3c3 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -60,7 +60,7 @@ private void check(Expression expression, Expression parentExpression, String fu Instance i1 = new Instance(solver, null, parentExpression); Instance i2 = new Instance(solver, i1, expression); Expression e = i2.getExpression(); - assertTrue(e SATCanonizerTest there is one testcase that is commented out. .equals(expression)); + assertTrue(e.equals(expression)); assertEquals(expression.toString(), e.toString()); assertEquals(full, i2.getFullExpression().toString()); Object result = i2.request("sat"); @@ -100,7 +100,7 @@ public void test03() { Operation o2 = new Operation(Operation.Operator.NE, v2, c2); check(o1, o2, "(aa==0)&&(bb!=1)", "1*v==0"); } - + @Test public void test04() { IntVariable v1 = new IntVariable("aa", 0, 99); @@ -217,7 +217,7 @@ public void test12() { IntConstant c2 = new IntConstant(3); IntVariable v1 = new IntVariable("aa", 0, 99); IntVariable v2 = new IntVariable("bb", 0, 99); - Operation o1 = new Operation(Operation.Operator.ADD, c1, c2); + Operation o1 = new Operation(Operation.Operator.ADD, c1,What happened? The build failed, c2); Operation o2 = new Operation(Operation.Operator.MUL, o1, v1); Operation o3 = new Operation(Operation.Operator.LT, o2, v2); check(o3, "((2+3)*aa) Date: Tue, 24 Jul 2018 10:57:31 +0200 Subject: [PATCH 04/56] Fixed unforced error --- test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 29dfc3c3..b6851009 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -217,7 +217,7 @@ public void test12() { IntConstant c2 = new IntConstant(3); IntVariable v1 = new IntVariable("aa", 0, 99); IntVariable v2 = new IntVariable("bb", 0, 99); - Operation o1 = new Operation(Operation.Operator.ADD, c1,What happened? The build failed, c2); + Operation o1 = new Operation(Operation.Operator.ADD, c1, c2); Operation o2 = new Operation(Operation.Operator.MUL, o1, v1); Operation o3 = new Operation(Operation.Operator.LT, o2, v2); check(o3, "((2+3)*aa) Date: Tue, 24 Jul 2018 11:30:44 +0200 Subject: [PATCH 05/56] added a hello message --- build.xml | 1 + 1 file changed, 1 insertion(+) diff --git a/build.xml b/build.xml index 0c29bed8..266f2d21 100644 --- a/build.xml +++ b/build.xml @@ -103,6 +103,7 @@ + From 429d903ddcbcd12e7674e5f536cedd92cfe5c11c Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 11:33:21 +0200 Subject: [PATCH 06/56] trying to fix errors --- build.xml | 1 - 1 file changed, 1 deletion(-) diff --git a/build.xml b/build.xml index 266f2d21..0c29bed8 100644 --- a/build.xml +++ b/build.xml @@ -103,7 +103,6 @@ - From 7cfdaa53653642a001d8e0a92eb9362ca4df84d9 Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 11:46:36 +0200 Subject: [PATCH 07/56] trying to echo contents of file --- build.xml | 1 + 1 file changed, 1 insertion(+) diff --git a/build.xml b/build.xml index 0c29bed8..53f69cd9 100644 --- a/build.xml +++ b/build.xml @@ -109,6 +109,7 @@ + From 1cb7112d568d71d8b3d5c13d9793a7a5e4f007dd Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 12:12:32 +0200 Subject: [PATCH 11/56] trying to make syntax errors go away --- build.xml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/build.xml b/build.xml index 08512ddb..faf4f359 100644 --- a/build.xml +++ b/build.xml @@ -108,18 +108,9 @@ - - + - - - - - - - - From 9a892e69c8743545a0e10eafc690add4c84fb928 Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 24 Jul 2018 12:28:27 +0200 Subject: [PATCH 12/56] Added an equal sign to the one test case --- test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 b6851009..c0e7c604 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,7 +301,7 @@ 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"); } } From d72e8d47d0b865b328bf8856baa091e84e2d7768 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 11:13:38 +0200 Subject: [PATCH 13/56] Trying to make docker image work --- .travis.yml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/.travis.yml b/.travis.yml index 4651be32..9f7a0a54 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,16 @@ +sudo: required + language: java +services: + - docker + +before_install: + - docker build -t carlad/sinatra + - docker run -d -p 127.0.0.1:80:4567 carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec foreman start;" + - docker ps -a + - docker run carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec rake test" + script: - ant; - ant test; From 8c5a22e5171d67deab58902652f4ba1dbad45f38 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 11:40:31 +0200 Subject: [PATCH 14/56] Just trying to docker build --- .travis.yml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index 9f7a0a54..3d76db2f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,10 +6,7 @@ services: - docker before_install: - - docker build -t carlad/sinatra - - docker run -d -p 127.0.0.1:80:4567 carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec foreman start;" - - docker ps -a - - docker run carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec rake test" + - docker build - < Dockerfile script: - ant; From 512447e606ac005f1d169b5c1e1dc43113312440 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 11:48:44 +0200 Subject: [PATCH 15/56] image docker --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 3d76db2f..996ca700 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,7 +6,7 @@ services: - docker before_install: - - docker build - < Dockerfile + - docker build -< /Dockerfile script: - ant; From 804aa9f2c16c6ebaa60b322cce0cd0a8b25c0347 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 11:50:41 +0200 Subject: [PATCH 16/56] docker image --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 996ca700..865f2368 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,7 +6,7 @@ services: - docker before_install: - - docker build -< /Dockerfile + - docker build -t /green/Dockerfile script: - ant; From b233aaa0ec4d05c78dc3f0da185b423cc60b5a25 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 11:54:21 +0200 Subject: [PATCH 17/56] docker attempt --- .travis.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 865f2368..8e6c0867 100644 --- a/.travis.yml +++ b/.travis.yml @@ -5,9 +5,6 @@ language: java services: - docker -before_install: - - docker build -t /green/Dockerfile - script: - ant; - ant test; From bbd751567e85ec931529d394d2bab0d9772577f2 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 11:57:56 +0200 Subject: [PATCH 18/56] reverted to original travis.yml --- .travis.yml | 5 ----- 1 file changed, 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index 8e6c0867..4651be32 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,10 +1,5 @@ -sudo: required - language: java -services: - - docker - script: - ant; - ant test; From c831331369979e5050ee79d375ec0cab54747496 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Thu, 26 Jul 2018 12:00:21 +0200 Subject: [PATCH 19/56] added sudo: required --- .travis.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.travis.yml b/.travis.yml index 4651be32..48988924 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,3 +1,5 @@ +sudo: required + language: java script: From c384c2d4cbdd0343968c3536cfa185d1ae9bc783 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:03:24 +0200 Subject: [PATCH 20/56] added services: docker --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index 48988924..8e6c0867 100644 --- a/.travis.yml +++ b/.travis.yml @@ -2,6 +2,9 @@ sudo: required language: java +services: + - docker + script: - ant; - ant test; From 35d470a8b03e7ca311183b37decbd48618bfb2ec Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:14:34 +0200 Subject: [PATCH 21/56] trying to install docker --- .travis.yml | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 8e6c0867..694c8abd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,10 +1,24 @@ sudo: required +dist: trusty +install: + # Update docker-engine using Ubuntu 'trusty' apt repo + - > + curl -sSL "https://get.docker.com/gpg" | + sudo -E apt-key add - + - > + echo "deb https://apt.dockerproject.org/repo ubuntu-trusty main" | + sudo tee -a /etc/apt/sources.list + - sudo apt-get update + - > + sudo apt-get -o Dpkg::Options::="--force-confdef" \ + -o Dpkg::Options::="--force-confold" --assume-yes install docker-engine + - docker version + # Update docker-compose via pip + - sudo pip install docker-compose + - docker-compose version language: java -services: - - docker - script: - ant; - ant test; From 39b9c381023e93de7750c25a60fb797f18335e19 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:20:04 +0200 Subject: [PATCH 22/56] trying to install docker-ce --- .travis.yml | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/.travis.yml b/.travis.yml index 694c8abd..d07268ce 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,19 +4,9 @@ dist: trusty install: # Update docker-engine using Ubuntu 'trusty' apt repo - > - curl -sSL "https://get.docker.com/gpg" | - sudo -E apt-key add - + sudo apt-get update - > - echo "deb https://apt.dockerproject.org/repo ubuntu-trusty main" | - sudo tee -a /etc/apt/sources.list - - sudo apt-get update - - > - sudo apt-get -o Dpkg::Options::="--force-confdef" \ - -o Dpkg::Options::="--force-confold" --assume-yes install docker-engine - - docker version - # Update docker-compose via pip - - sudo pip install docker-compose - - docker-compose version + sudo apt-get install docker-ce language: java script: From 9a9cf713a1fd0f81ac429a335e864a86d9fd160e Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:28:21 +0200 Subject: [PATCH 23/56] added serices: docker --- .travis.yml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/.travis.yml b/.travis.yml index d07268ce..63f111a1 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,12 +1,8 @@ sudo: required dist: trusty -install: - # Update docker-engine using Ubuntu 'trusty' apt repo - - > - sudo apt-get update - - > - sudo apt-get install docker-ce +services: docker + language: java script: From ad9a54f1c959c236e29945bcf3948dc56b32e44a Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:31:47 +0200 Subject: [PATCH 24/56] added before_install --- .travis.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.travis.yml b/.travis.yml index 63f111a1..f387788f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,6 +3,12 @@ dist: trusty services: docker +before_install: + - docker build -t carlad/sinatra . + - docker run -d -p 127.0.0.1:80:4567 carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec foreman start;" + - docker ps -a + - docker run carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec rake test" + language: java script: From 85211295e1b36e99e25198040a0f93fa03db1a86 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:36:50 +0200 Subject: [PATCH 25/56] trying to fix before_installll --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index f387788f..d14f032c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -5,9 +5,9 @@ services: docker before_install: - docker build -t carlad/sinatra . - - docker run -d -p 127.0.0.1:80:4567 carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec foreman start;" + - docker run -d -p 127.0.0.1:80:4567 carlad/sinatra /bin/sh -c "cd carla/sinatra; bundle exec foreman start;" - docker ps -a - - docker run carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec rake test" + - docker run carlad/sinatra /bin/sh -c "cd carla/sinatra; bundle exec rake test" language: java From aaea4aef62687e05ad7e2fd63a9558dfcc5ea264 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:44:34 +0200 Subject: [PATCH 26/56] trying to set up docker again --- .travis.yml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index d14f032c..600b107e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,11 +3,8 @@ dist: trusty services: docker -before_install: - - docker build -t carlad/sinatra . - - docker run -d -p 127.0.0.1:80:4567 carlad/sinatra /bin/sh -c "cd carla/sinatra; bundle exec foreman start;" - - docker ps -a - - docker run carlad/sinatra /bin/sh -c "cd carla/sinatra; bundle exec rake test" +before_script: + - docker-compose up --build -d language: java From 0c3df3317c4c9f96a9723027723aafad94fd092c Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 12:55:45 +0200 Subject: [PATCH 27/56] fixing before_script --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 600b107e..02459365 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,7 +4,7 @@ dist: trusty services: docker before_script: - - docker-compose up --build -d + - docker-compose up language: java From d28b264051f44139715d973fdaf42aecb66cfbb6 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:02:39 +0200 Subject: [PATCH 28/56] added a docker-compose.yml file --- docker-compose.yml | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 docker-compose.yml diff --git a/docker-compose.yml b/docker-compose.yml new file mode 100644 index 00000000..899cf444 --- /dev/null +++ b/docker-compose.yml @@ -0,0 +1,8 @@ +version: '3' +services: + web: + build: . + ports: + - "5000:5000" + redis: + image: "redis:alpine" From 724cdae54e1e876c54cb0f4327a3e8d5b4a8de70 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:07:14 +0200 Subject: [PATCH 29/56] fixing docker compose --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 02459365..600b107e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,7 +4,7 @@ dist: trusty services: docker before_script: - - docker-compose up + - docker-compose up --build -d language: java From 8e79d82385a898c3c3ca5933c0f1fd438719e6e4 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:14:03 +0200 Subject: [PATCH 30/56] Added after_script --- .travis.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.travis.yml b/.travis.yml index 600b107e..2305f24e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -11,3 +11,6 @@ language: java script: - ant; - ant test; + +after_script: + - docker-compose down From cc1ab1cc370f9a8956df70e5ed23f856b51af4b1 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:21:23 +0200 Subject: [PATCH 31/56] added before_script stuff --- .travis.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 2305f24e..16c6f9fa 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,7 +4,10 @@ dist: trusty services: docker before_script: - - docker-compose up --build -d +- sudo rm /usr/local/bin/docker-compose + - curl -L https://github.com/docker/compose/releases/download/${DOCKER_COMPOSE_VERSION}/docker-compose-`uname -s`-`uname -m` > docker-compose + - chmod +x docker-compose + - sudo mv docker-compose /usr/local/bin language: java From 18e44f0112b9ff3695e64ee59d71312a5373f203 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:24:21 +0200 Subject: [PATCH 32/56] trying to fix before_script --- .travis.yml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index 16c6f9fa..144e8570 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,10 +4,9 @@ dist: trusty services: docker before_script: -- sudo rm /usr/local/bin/docker-compose - - curl -L https://github.com/docker/compose/releases/download/${DOCKER_COMPOSE_VERSION}/docker-compose-`uname -s`-`uname -m` > docker-compose - - chmod +x docker-compose - - sudo mv docker-compose /usr/local/bin +- sudo rm /usr/local/bin/docker-compose +- chmod +x docker-compose +- sudo mv docker-compose /usr/local/bin language: java From 0322502cb3d939f0f90d0550f67249ac7d57f1e5 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:32:00 +0200 Subject: [PATCH 33/56] added docker ps --- .travis.yml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index 144e8570..c05c5cac 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,14 +3,11 @@ dist: trusty services: docker -before_script: -- sudo rm /usr/local/bin/docker-compose -- chmod +x docker-compose -- sudo mv docker-compose /usr/local/bin - language: java script: + - docker-compose up --build -d + - docker ps - ant; - ant test; From f5471c7a901fa0dbc35d2ef4ab30cd95a96d0f37 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:41:21 +0200 Subject: [PATCH 34/56] added a docker hello-world --- .travis.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index c05c5cac..e8b8fe2d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -7,7 +7,8 @@ language: java script: - docker-compose up --build -d - - docker ps + - docker ps -a + - docker run hello-world - ant; - ant test; From d5bd7e3eda38c05d8250c0ba4c95fcdcd642ae89 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 13:55:47 +0200 Subject: [PATCH 35/56] added docker run -t -i ant --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index e8b8fe2d..b95c6734 100644 --- a/.travis.yml +++ b/.travis.yml @@ -9,8 +9,8 @@ script: - docker-compose up --build -d - docker ps -a - docker run hello-world - - ant; - - ant test; + - docker run -t -i ant; + - docker run -t -i ant test; after_script: - docker-compose down From 0888c5baf9b1ff4f078b5fd407305f2545d3b9ee Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 14:03:45 +0200 Subject: [PATCH 36/56] added docker images --- .travis.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index b95c6734..3e96661e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -9,8 +9,7 @@ script: - docker-compose up --build -d - docker ps -a - docker run hello-world - - docker run -t -i ant; - - docker run -t -i ant test; + - docker images after_script: - docker-compose down From 9816108241bed892e8b24052f59bd6328b7999a5 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 14:11:05 +0200 Subject: [PATCH 37/56] added volumes to docker-compose.yml --- docker-compose.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docker-compose.yml b/docker-compose.yml index 899cf444..11c099f5 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -1,8 +1,10 @@ -version: '3' +version: '2' services: web: build: . ports: - "5000:5000" + volumes: + - .:/code redis: image: "redis:alpine" From 482bfd44d6d719fcebc29fde31c06208a6dfd153 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 14:28:17 +0200 Subject: [PATCH 38/56] made a few chagnes on dockerfile --- .travis.yml.swp | Bin 0 -> 12288 bytes Dockerfile | 4 ++++ docker-compose.yml | 1 + 3 files changed, 5 insertions(+) create mode 100644 .travis.yml.swp diff --git a/.travis.yml.swp b/.travis.yml.swp new file mode 100644 index 0000000000000000000000000000000000000000..4e5923e2e398045f4c5a97ca1d4a58fff6e19779 GIT binary patch literal 12288 zcmeI&Jx>%t7zgkNOM*fq^n=!Wi*N~K>BPpuP!LFn5i{%#=jiUvIxmMbTGP?OCxH^a z0e%7!`~uWAJ|oLZAg9+V|4IJYo7rdQ<=1U)H)qyfzY+7DE^(V6+B;l-doVdlV^c(x zw0RuDQu>5N*OkbHiRI2taT{2Y@ys}~?*Q(BynCo`ao>i(&JKoB^ zcAcH795@|rKmY>63IxBEEIg*U*%veMk>}5*#pKh~VV_1F1Rwwb2tWV=5P$##An+du z_-2H@@i`u~XBls=BX_QC7Z(UX00Izz00bZa0SG_<0uX=z1pYw*SrDB)AzFwp{`~*{ z)%*Vi|MOIi1V z?5RwAlzqw7T<$_)MAg4Lc^aHe%ed(Mh3}92-ir8hi~Eli!=B^vv_ez<(8cx~1&XvpBm52)Md?vgN&hJo!%7j&) IgSM)mUmM1-{Qv*} literal 0 HcmV?d00001 diff --git a/Dockerfile b/Dockerfile index e465a44f..6f3a62ff 100644 --- a/Dockerfile +++ b/Dockerfile @@ -35,3 +35,7 @@ RUN mv z3-4.7.1-x64-ubuntu-16.04/ z3/ WORKDIR /green/ RUN sed -i '16s/.*/z3path = \/z3\/z3\/bin\/z3/' build.properties RUN sed -i '17s/.*/z3lib = \/z3\/z3\/bin/' build.properties + +#add the test +ADD ant +ADD ant-test diff --git a/docker-compose.yml b/docker-compose.yml index 11c099f5..2976981d 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -2,6 +2,7 @@ version: '2' services: web: build: . + dockerfile: Dockerfile ports: - "5000:5000" volumes: From be88478322130e267e062f2e1f15a88a79ef6033 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 14:31:07 +0200 Subject: [PATCH 39/56] removed dockerfile: Dockerfile from docker-compose.yml --- docker-compose.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/docker-compose.yml b/docker-compose.yml index 2976981d..11c099f5 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -2,7 +2,6 @@ version: '2' services: web: build: . - dockerfile: Dockerfile ports: - "5000:5000" volumes: From 685cc095a8644543d4f3be8fee3dbd5ee7225a3b Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 14:42:14 +0200 Subject: [PATCH 40/56] added 'RUN ant' to dockerfile --- Dockerfile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Dockerfile b/Dockerfile index 6f3a62ff..c06a814a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -36,6 +36,6 @@ WORKDIR /green/ RUN sed -i '16s/.*/z3path = \/z3\/z3\/bin\/z3/' build.properties RUN sed -i '17s/.*/z3lib = \/z3\/z3\/bin/' build.properties -#add the test -ADD ant -ADD ant-test +#run the test +RUN ant +RUN ant test From b35806548a8567120781571102e200a5db6125d8 Mon Sep 17 00:00:00 2001 From: "marcdefaria@gmail.com" Date: Thu, 26 Jul 2018 14:52:07 +0200 Subject: [PATCH 41/56] removed docker run helloworld --- .travis.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 3e96661e..1d840f3f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -8,8 +8,6 @@ language: java script: - docker-compose up --build -d - docker ps -a - - docker run hello-world - - docker images after_script: - docker-compose down From 08c33f3b308923de0c7f6ab677081b168a10898b Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 31 Jul 2018 10:34:46 +0200 Subject: [PATCH 42/56] Added verbose output and failing test case --- build.xml | 4 ++-- .../ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/build.xml b/build.xml index faf4f359..46321a09 100644 --- a/build.xml +++ b/build.xml @@ -95,8 +95,8 @@ - - + + 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 c0e7c604..953f316f 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -77,7 +77,10 @@ public void test01() { Operation o = new Operation(Operation.Operator.EQ, v, c); check(o, "aa==0", "1*v==0"); } + /* Changed last line from "check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0");" + to check(o3, "(aa=<0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); + */ @Test public void test02() { IntVariable v1 = new IntVariable("aa", 0, 99); @@ -87,7 +90,7 @@ public void test02() { IntConstant c2 = new IntConstant(1); Operation o2 = new Operation(Operation.Operator.NE, v2, c2); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); + check(o3, "(aa=<0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); } @Test From 6bec708ce572129db4b2cfc9039fd38bd4637d9c Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 31 Jul 2018 10:42:56 +0200 Subject: [PATCH 43/56] Changed dockerfile to get tests cases from my github --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index c06a814a..46ebc64c 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/marcdefaria/green # Download and extract Z3 RUN mkdir z3 From e36b4bf68c2535cefc8c53e18d259912cc9997d1 Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 31 Jul 2018 10:49:44 +0200 Subject: [PATCH 44/56] Corrected failing test case --- test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 953f316f..7c7b9fb1 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -90,7 +90,7 @@ public void test02() { IntConstant c2 = new IntConstant(1); Operation o2 = new Operation(Operation.Operator.NE, v2, c2); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(aa=<0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); + check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); } @Test From 0dd13ee32129ab636b2ce87026c29e77cd5728af Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 31 Jul 2018 11:09:57 +0200 Subject: [PATCH 45/56] Added build status of travis to repo --- README.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index f8913b11..5ca9ab6a 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,9 @@ -[![Build Status](https://travis-ci.org/marcdefaria/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master) +[![Build Status](https://travis-ci.org/marcdefaria/green.svg?branch=master)](https://travis-ci.org/marcdefaria/green) -Notes: +(https://travis-ci.org/wvisser/green.svg?branch=master) +Notes: +HvQSDNw9jQZYGx6mw8N0Bg 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. From 8a755ca02ca4399e3a3dd40f81c961e9b7417af9 Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 31 Jul 2018 11:11:00 +0200 Subject: [PATCH 46/56] Corrected README.md file --- README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/README.md b/README.md index 5ca9ab6a..0b682bb2 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,5 @@ [![Build Status](https://travis-ci.org/marcdefaria/green.svg?branch=master)](https://travis-ci.org/marcdefaria/green) -(https://travis-ci.org/wvisser/green.svg?branch=master) - Notes: HvQSDNw9jQZYGx6mw8N0Bg The first step is to update "build.properties" with your local From 6e6dde1f48db6eb8c797a6ab7d2e11ec77945e0b Mon Sep 17 00:00:00 2001 From: Mr MJ De Faria <19923929@sun.ac.za> Date: Tue, 31 Jul 2018 13:14:23 +0200 Subject: [PATCH 47/56] Added 2 new test cases to canonizer --- .../OnlyConstantPropogationTest.java | 74 +++++++ ...SimplificationConstantPropogationTest.java | 186 ++++++++++++++++++ 2 files changed, 260 insertions(+) create mode 100644 test/za/ac/sun/cs/green/service/canonizer/OnlyConstantPropogationTest.java create mode 100644 test/za/ac/sun/cs/green/service/canonizer/SimplificationConstantPropogationTest.java diff --git a/test/za/ac/sun/cs/green/service/canonizer/OnlyConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/canonizer/OnlyConstantPropogationTest.java new file mode 100644 index 00000000..c5554c33 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/canonizer/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)"); + } + +} diff --git a/test/za/ac/sun/cs/green/service/canonizer/SimplificationConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/canonizer/SimplificationConstantPropogationTest.java new file mode 100644 index 00000000..c7995ac6 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/canonizer/SimplificationConstantPropogationTest.java @@ -0,0 +1,186 @@ +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", "(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)&&(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"); + } + + + + + +} From 8719fc59c45d7f1b93abb0670026a81b4672b0cc Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Sat, 11 Aug 2018 15:57:13 +0200 Subject: [PATCH 48/56] Added import for first test to EntireSuite.java --- test/za/ac/sun/cs/green/EntireSuite.java | 1 + 1 file changed, 1 insertion(+) diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java index d48bb8c9..97407cb4 100644 --- a/test/za/ac/sun/cs/green/EntireSuite.java +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -32,6 +32,7 @@ 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.canonizer.OnlyConstantPropogationTest; @RunWith(Suite.class) @Suite.SuiteClasses({ From f6abdb38ce23019428095d62293e8c3e9b2151a6 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Sat, 11 Aug 2018 16:06:32 +0200 Subject: [PATCH 49/56] Moved test cases to service/simplify --- test/za/ac/sun/cs/green/EntireSuite.java | 2 +- .../{canonizer => simplify}/OnlyConstantPropogationTest.java | 0 .../SimplificationConstantPropogationTest.java | 0 3 files changed, 1 insertion(+), 1 deletion(-) rename test/za/ac/sun/cs/green/service/{canonizer => simplify}/OnlyConstantPropogationTest.java (100%) rename test/za/ac/sun/cs/green/service/{canonizer => simplify}/SimplificationConstantPropogationTest.java (100%) diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java index 97407cb4..f7ce0768 100644 --- a/test/za/ac/sun/cs/green/EntireSuite.java +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -32,7 +32,7 @@ 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.canonizer.OnlyConstantPropogationTest; +import za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest; @RunWith(Suite.class) @Suite.SuiteClasses({ diff --git a/test/za/ac/sun/cs/green/service/canonizer/OnlyConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java similarity index 100% rename from test/za/ac/sun/cs/green/service/canonizer/OnlyConstantPropogationTest.java rename to test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java diff --git a/test/za/ac/sun/cs/green/service/canonizer/SimplificationConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java similarity index 100% rename from test/za/ac/sun/cs/green/service/canonizer/SimplificationConstantPropogationTest.java rename to test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java From b0ee0226e78bc40a3b5605d1bacb0d9ee9ab22ea Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Sun, 12 Aug 2018 10:01:03 +0200 Subject: [PATCH 50/56] deleted entireSuite.java --- test/za/ac/sun/cs/green/EntireSuite.java | 149 ----------------------- 1 file changed, 149 deletions(-) delete mode 100644 test/za/ac/sun/cs/green/EntireSuite.java diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java deleted file mode 100644 index f7ce0768..00000000 --- a/test/za/ac/sun/cs/green/EntireSuite.java +++ /dev/null @@ -1,149 +0,0 @@ -package za.ac.sun.cs.green; - -import java.io.ByteArrayOutputStream; -import java.io.File; -import java.io.IOException; -import java.io.InputStream; -import java.util.HashMap; -import java.util.Properties; - -import org.apache.commons.exec.CommandLine; -import org.apache.commons.exec.DefaultExecutor; -import org.apache.commons.exec.PumpStreamHandler; -import org.junit.runner.RunWith; -import org.junit.runners.Suite; - -import com.microsoft.z3.Context; - -import cvc3.ValidityChecker; -import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Parser0Test; -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.choco.SATChocoTest; -import za.ac.sun.cs.green.service.cvc3.SATCVC3Test; -import za.ac.sun.cs.green.service.factorizer.SATFactorizerTest; -import za.ac.sun.cs.green.service.latte.CountLattETest; -import za.ac.sun.cs.green.service.latte.CountLattEWithBounderTest; -import za.ac.sun.cs.green.service.slicer.ParallelSATSlicerTest; -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.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 -}) - -public class EntireSuite { - - public static final String LATTE_PATH; - - public static final String BARVINOK_PATH; - - public static final String Z3_PATH; - - public static final boolean HAS_CVC3 = false; - - public static final boolean HAS_LATTE = false; - - public static final boolean HAS_Z3; - - public static final boolean HAS_Z3JAVA = false; - - static { - String latte = null, z3 = null, barvinok = null; - InputStream is = EntireSuite.class.getClassLoader() - .getResourceAsStream("build.properties"); - if (is != null) { - Properties p = new Properties(); - try { - p.load(is); - latte = p.getProperty("lattepath"); - barvinok = p.getProperty("barvinokpath"); - z3 = p.getProperty("z3path"); - } catch (IOException e) { - // do nothing - } - } - LATTE_PATH = latte; - BARVINOK_PATH = barvinok; - Z3_PATH = z3; - HAS_Z3 = checkZ3Presence(); - if (!HAS_Z3) { - System.out.println("Z3 Not Available, no tests for it will be executed"); - } - - } - - private static boolean checkCVC3Presence() { - try { - ValidityChecker.create(); - } catch (SecurityException x) { - return false; - } catch (UnsatisfiedLinkError x) { - System.out.println(""); - x.printStackTrace(); - return false; - } - return true; - } - - private static boolean checkLattEPresence() { - if (LATTE_PATH == null) { - return false; - } - final String DIRNAME = System.getProperty("java.io.tmpdir"); - String result = ""; - try { - ByteArrayOutputStream outputStream = new ByteArrayOutputStream(); - DefaultExecutor executor = new DefaultExecutor(); - executor.setStreamHandler(new PumpStreamHandler(outputStream)); - executor.setWorkingDirectory(new File(DIRNAME)); - executor.setExitValues(null); - executor.execute(CommandLine.parse(LATTE_PATH)); - result = outputStream.toString(); - } catch (IOException x) { - x.printStackTrace(); - return false; - } - return result.trim().startsWith("This is LattE integrale"); - } - - private static boolean checkZ3Presence() { - final String DIRNAME = System.getProperty("java.io.tmpdir"); - String result = ""; - try { - ByteArrayOutputStream outputStream = new ByteArrayOutputStream(); - DefaultExecutor executor = new DefaultExecutor(); - executor.setStreamHandler(new PumpStreamHandler(outputStream)); - executor.setWorkingDirectory(new File(DIRNAME)); - executor.setExitValues(null); - executor.execute(CommandLine.parse(Z3_PATH + " -h")); - result = outputStream.toString(); - } catch (IOException e) { - return false; - } - return result.startsWith("Z3 [version "); - } - - private static boolean checkZ3JavaPresence() { - HashMap cfg = new HashMap(); - cfg.put("model", "false"); - try { - new Context(cfg); - } catch (Exception x) { - return false; - } catch (UnsatisfiedLinkError x) { - x.printStackTrace(); - return false; - } - return true; - } - -} From bfc2f9fc0953b28c942ea40c3dfaf9d4ff669ef1 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Sun, 12 Aug 2018 10:02:39 +0200 Subject: [PATCH 51/56] Added EntireSuite.java back --- test/za/ac/sun/cs/green/EntireSuite.java | 149 +++++++++++++++++++++++ 1 file changed, 149 insertions(+) create mode 100644 test/za/ac/sun/cs/green/EntireSuite.java diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java new file mode 100644 index 00000000..f7ce0768 --- /dev/null +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -0,0 +1,149 @@ +package za.ac.sun.cs.green; + +import java.io.ByteArrayOutputStream; +import java.io.File; +import java.io.IOException; +import java.io.InputStream; +import java.util.HashMap; +import java.util.Properties; + +import org.apache.commons.exec.CommandLine; +import org.apache.commons.exec.DefaultExecutor; +import org.apache.commons.exec.PumpStreamHandler; +import org.junit.runner.RunWith; +import org.junit.runners.Suite; + +import com.microsoft.z3.Context; + +import cvc3.ValidityChecker; +import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Parser0Test; +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.choco.SATChocoTest; +import za.ac.sun.cs.green.service.cvc3.SATCVC3Test; +import za.ac.sun.cs.green.service.factorizer.SATFactorizerTest; +import za.ac.sun.cs.green.service.latte.CountLattETest; +import za.ac.sun.cs.green.service.latte.CountLattEWithBounderTest; +import za.ac.sun.cs.green.service.slicer.ParallelSATSlicerTest; +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.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 +}) + +public class EntireSuite { + + public static final String LATTE_PATH; + + public static final String BARVINOK_PATH; + + public static final String Z3_PATH; + + public static final boolean HAS_CVC3 = false; + + public static final boolean HAS_LATTE = false; + + public static final boolean HAS_Z3; + + public static final boolean HAS_Z3JAVA = false; + + static { + String latte = null, z3 = null, barvinok = null; + InputStream is = EntireSuite.class.getClassLoader() + .getResourceAsStream("build.properties"); + if (is != null) { + Properties p = new Properties(); + try { + p.load(is); + latte = p.getProperty("lattepath"); + barvinok = p.getProperty("barvinokpath"); + z3 = p.getProperty("z3path"); + } catch (IOException e) { + // do nothing + } + } + LATTE_PATH = latte; + BARVINOK_PATH = barvinok; + Z3_PATH = z3; + HAS_Z3 = checkZ3Presence(); + if (!HAS_Z3) { + System.out.println("Z3 Not Available, no tests for it will be executed"); + } + + } + + private static boolean checkCVC3Presence() { + try { + ValidityChecker.create(); + } catch (SecurityException x) { + return false; + } catch (UnsatisfiedLinkError x) { + System.out.println(""); + x.printStackTrace(); + return false; + } + return true; + } + + private static boolean checkLattEPresence() { + if (LATTE_PATH == null) { + return false; + } + final String DIRNAME = System.getProperty("java.io.tmpdir"); + String result = ""; + try { + ByteArrayOutputStream outputStream = new ByteArrayOutputStream(); + DefaultExecutor executor = new DefaultExecutor(); + executor.setStreamHandler(new PumpStreamHandler(outputStream)); + executor.setWorkingDirectory(new File(DIRNAME)); + executor.setExitValues(null); + executor.execute(CommandLine.parse(LATTE_PATH)); + result = outputStream.toString(); + } catch (IOException x) { + x.printStackTrace(); + return false; + } + return result.trim().startsWith("This is LattE integrale"); + } + + private static boolean checkZ3Presence() { + final String DIRNAME = System.getProperty("java.io.tmpdir"); + String result = ""; + try { + ByteArrayOutputStream outputStream = new ByteArrayOutputStream(); + DefaultExecutor executor = new DefaultExecutor(); + executor.setStreamHandler(new PumpStreamHandler(outputStream)); + executor.setWorkingDirectory(new File(DIRNAME)); + executor.setExitValues(null); + executor.execute(CommandLine.parse(Z3_PATH + " -h")); + result = outputStream.toString(); + } catch (IOException e) { + return false; + } + return result.startsWith("Z3 [version "); + } + + private static boolean checkZ3JavaPresence() { + HashMap cfg = new HashMap(); + cfg.put("model", "false"); + try { + new Context(cfg); + } catch (Exception x) { + return false; + } catch (UnsatisfiedLinkError x) { + x.printStackTrace(); + return false; + } + return true; + } + +} From 7cf5524ea4ee989af8b9b7b6a1cc2ef4f83afc19 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Sun, 12 Aug 2018 10:50:33 +0200 Subject: [PATCH 52/56] Removed /canonizer --- .../service/canonizer/SATCanonizerTest.java | 310 ------------------ .../service/canonizer/SATCanonizerTest2.java | 82 ----- .../.OnlyConstantPropogationTest.java.swp | Bin 0 -> 12288 bytes 3 files changed, 392 deletions(-) delete mode 100644 test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java delete mode 100644 test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.java create mode 100644 test/za/ac/sun/cs/green/service/simplify/.OnlyConstantPropogationTest.java.swp diff --git a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java deleted file mode 100644 index 7c7b9fb1..00000000 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ /dev/null @@ -1,310 +0,0 @@ -package za.ac.sun.cs.green.service.canonizer; - -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 SATCanonizerTest { - - 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", "(slice (canonize sink))"); - props.setProperty("green.service.sat.slice", "za.ac.sun.cs.green.service.slicer.SATSlicerService"); - 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) { - String s0 = observed.replaceAll("[()]", ""); - String s1 = s0.replaceAll("v[0-9]", "v"); - SortedSet s2 = new TreeSet(Arrays.asList(s1.split("&&"))); - SortedSet s3 = new TreeSet(Arrays.asList(expected)); - assertEquals(s3, s2); - } - - private void check(Expression expression, String full, String... expected) { - Instance i = new Instance(solver, null, null, expression); - Expression e = i.getExpression(); - assertTrue(e.equals(expression)); - assertEquals(expression.toString(), e.toString()); - assertEquals(full, i.getFullExpression().toString()); - Object result = i.request("sat"); - assertNotNull(result); - assertEquals(Instance.class, result.getClass()); - Instance j = (Instance) result; - finalCheck(j.getExpression().toString(), expected); - } - - private void check(Expression expression, Expression parentExpression, String full, String... expected) { - Instance i1 = new Instance(solver, null, parentExpression); - Instance i2 = new Instance(solver, i1, expression); - Expression e = i2.getExpression(); - assertTrue(e.equals(expression)); - assertEquals(expression.toString(), e.toString()); - assertEquals(full, i2.getFullExpression().toString()); - Object result = i2.request("sat"); - assertNotNull(result); - assertEquals(Instance.class, result.getClass()); - Instance j = (Instance) result; - finalCheck(j.getExpression().toString(), expected); - } - - @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); - check(o, "aa==0", "1*v==0"); - } - /* Changed last line from "check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0");" - to check(o3, "(aa=<0)&&(bb!=1)", "1*v==0", "1*v+-1!=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); - IntVariable v2 = new IntVariable("bb", 0, 99); - IntConstant c2 = new IntConstant(1); - Operation o2 = new Operation(Operation.Operator.NE, v2, c2); - Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); - } - - @Test - public void test03() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntConstant c1 = new IntConstant(0); - 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); - check(o1, o2, "(aa==0)&&(bb!=1)", "1*v==0"); - } - - @Test - public void test04() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntConstant c1 = new IntConstant(0); - Operation o1 = new Operation(Operation.Operator.EQ, v1, c1); - IntConstant c2 = new IntConstant(1); - Operation o2 = new Operation(Operation.Operator.NE, v1, c2); - check(o1, o2, "(aa==0)&&(aa!=1)", "1*v==0", "1*v+-1!=0"); - } - - @Test - public void test05() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - Operation o1 = new Operation(Operation.Operator.EQ, v1, v2); - IntVariable v3 = new IntVariable("cc", 0, 99); - Operation o2 = new Operation(Operation.Operator.EQ, v2, v3); - IntVariable v4 = new IntVariable("dd", 0, 99); - Operation o3 = new Operation(Operation.Operator.EQ, v3, v4); - IntVariable v5 = new IntVariable("ee", 0, 99); - Operation o4 = new Operation(Operation.Operator.EQ, v4, v5); - Operation o34 = new Operation(Operation.Operator.AND, o3, o4); - Operation o234 = new Operation(Operation.Operator.AND, o2, o34); - check(o1, o234, "(aa==bb)&&((bb==cc)&&((cc==dd)&&(dd==ee)))", "1*v+-1*v==0", "1*v+-1*v==0", "1*v+-1*v==0", - "1*v+-1*v==0"); - } - - @Test - public void test06() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - Operation o1 = new Operation(Operation.Operator.EQ, v1, v2); - IntVariable v3 = new IntVariable("cc", 0, 99); - Operation o2 = new Operation(Operation.Operator.EQ, v2, v3); - IntVariable v4 = new IntVariable("dd", 0, 99); - Operation o3 = new Operation(Operation.Operator.EQ, v3, v4); - IntVariable v5 = new IntVariable("ee", 0, 99); - IntVariable v6 = new IntVariable("ff", 0, 99); - Operation o4 = new Operation(Operation.Operator.EQ, v5, v6); - Operation o34 = new Operation(Operation.Operator.AND, o3, o4); - Operation o234 = new Operation(Operation.Operator.AND, o2, o34); - check(o1, o234, "(aa==bb)&&((bb==cc)&&((cc==dd)&&(ee==ff)))", "1*v+-1*v==0", "1*v+-1*v==0", "1*v+-1*v==0"); - } - - @Test - public void test07() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - IntVariable v3 = new IntVariable("cc", 0, 99); - IntVariable v4 = new IntVariable("dd", 0, 99); - IntVariable v5 = new IntVariable("ee", 0, 99); - IntVariable v6 = new IntVariable("ff", 0, 99); - IntVariable v7 = new IntVariable("gg", 0, 99); - Operation o1 = new Operation(Operation.Operator.LT, v1, new Operation(Operation.Operator.ADD, v2, v3)); - Operation o2 = new Operation(Operation.Operator.LT, v2, new Operation(Operation.Operator.ADD, v4, v5)); - Operation o3 = new Operation(Operation.Operator.LT, v3, new Operation(Operation.Operator.ADD, v6, v7)); - Operation o23 = new Operation(Operation.Operator.AND, o2, o3); - check(o1, o23, "(aa<(bb+cc))&&((bb<(dd+ee))&&(cc<(ff+gg)))", "1*v+-1*v+-1*v+1<=0", "1*v+-1*v+-1*v+1<=0", - "1*v+-1*v+-1*v+1<=0"); - } - - @Test - public void test08() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - IntVariable v3 = new IntVariable("cc", 0, 99); - IntVariable v4 = new IntVariable("dd", 0, 99); - IntVariable v5 = new IntVariable("ee", 0, 99); - IntVariable v6 = new IntVariable("ff", 0, 99); - IntVariable v7 = new IntVariable("gg", 0, 99); - IntVariable v8 = new IntVariable("hh", 0, 99); - Operation o1 = new Operation(Operation.Operator.LT, v1, new Operation(Operation.Operator.ADD, v2, v3)); - Operation o2 = new Operation(Operation.Operator.LT, v2, new Operation(Operation.Operator.ADD, v4, v5)); - Operation o3 = new Operation(Operation.Operator.LT, v6, new Operation(Operation.Operator.ADD, v7, v8)); - Operation o23 = new Operation(Operation.Operator.AND, o2, o3); - check(o1, o23, "(aa<(bb+cc))&&((bb<(dd+ee))&&(ff<(gg+hh)))", "1*v+-1*v+-1*v+1<=0", "1*v+-1*v+-1*v+1<=0"); - } - - @Test - public void test09() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - IntVariable v3 = new IntVariable("cc", 0, 99); - Operation o1 = new Operation(Operation.Operator.ADD, v1, v2); - Operation o2 = new Operation(Operation.Operator.ADD, v1, v3); - Operation o3 = new Operation(Operation.Operator.LT, o1, o2); - check(o3, "(aa+bb)<(aa+cc)", "1*v+-1*v+1<=0"); - } - - @Test - public void test10() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - IntVariable v3 = new IntVariable("cc", 0, 99); - Operation o1 = new Operation(Operation.Operator.ADD, v1, v2); - Operation o2 = new Operation(Operation.Operator.SUB, v1, v3); - Operation o3 = new Operation(Operation.Operator.LT, o1, o2); - check(o3, "(aa+bb)<(aa-cc)", "1*v+1*v+1<=0"); - } - - @Test - public void test11() { - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - Operation o1 = new Operation(Operation.Operator.ADD, v1, v2); - Operation o2 = new Operation(Operation.Operator.SUB, v2, v1); - Operation o3 = new Operation(Operation.Operator.LT, o1, o2); - check(o3, "(aa+bb)<(bb-aa)", "2*v+1<=0"); - } - - @Test - public void test12() { - IntConstant c1 = new IntConstant(2); - IntConstant c2 = new IntConstant(3); - IntVariable v1 = new IntVariable("aa", 0, 99); - IntVariable v2 = new IntVariable("bb", 0, 99); - Operation o1 = new Operation(Operation.Operator.ADD, c1, c2); - Operation o2 = new Operation(Operation.Operator.MUL, o1, v1); - Operation o3 = new Operation(Operation.Operator.LT, o2, v2); - check(o3, "((2+3)*aa) s2 = new TreeSet(Arrays.asList(s1.split("&&"))); - SortedSet s3 = new TreeSet(Arrays.asList(expected)); - assertEquals(s2, s3); - } - - private void check(Expression expression, String full, String... expected) { - Instance i = new Instance(solver, null, null, expression); - Expression e = i.getExpression(); - assertTrue(e.equals(expression)); - assertEquals(expression.toString(), e.toString()); - assertEquals(full, i.getFullExpression().toString()); - Object result = i.request("sat"); - assertNotNull(result); - assertEquals(Instance.class, result.getClass()); - Instance j = (Instance) result; - finalCheck(j.getExpression().toString(), expected); - } - - private void check(Expression expression, Expression parentExpression, String full, String... expected) { - Instance i1 = new Instance(solver, null, parentExpression); - Instance i2 = new Instance(solver, i1, expression); - Expression e = i2.getExpression(); - assertTrue(e.equals(expression)); - assertEquals(expression.toString(), e.toString()); - assertEquals(full, i2.getFullExpression().toString()); - Object result = i2.request("sat"); - assertNotNull(result); - assertEquals(Instance.class, result.getClass()); - Instance j = (Instance) result; - finalCheck(j.getExpression().toString(), expected); - } - - @Test - public void test23() { - IntVariable x5 = new IntVariable("x5", 0, 99); - IntConstant c1 = new IntConstant(1); - IntConstant c0 = new IntConstant(0); - Operation o2b = new Operation(Operation.Operator.NE, x5, x5); - Operation o2a = new Operation(Operation.Operator.NOT, o2b); - check(o2a, "!(x5!=x5)", "0==0"); - } - -} diff --git a/test/za/ac/sun/cs/green/service/simplify/.OnlyConstantPropogationTest.java.swp b/test/za/ac/sun/cs/green/service/simplify/.OnlyConstantPropogationTest.java.swp new file mode 100644 index 0000000000000000000000000000000000000000..d15500c94b0f94b84a9414df23e7f8dbdd3f53dd GIT binary patch literal 12288 zcmeI2O=~1Y7{_ZxTt_#$>OomS%27g(X{%?Ffb52d$s|Yw6J=s9vWH5iGIrAG?(LWC zOk`I)3LXSSFM=rETyVdEdh#k7Q9ppNpocwpU;ourJv}pe=+PFYkplCI!mFO z?TH{woMyNeWvPg1%k@Oy3OX}8>$GDb0w)zo>Kt%~yH1h?j+^NAM8x}^E1bmJi+pdp z>#PNSw;2XW%7gTcIE=zJPrWc$hdmVZLnVD|X<*=WtK1-i?{H;@` zfEln+z$jo8FbWt2i~>dhqkvK1G%JusXUKaH;65$FYx;U-=&Enc#VBADFbWt2i~>dh zqkvJsC}0#Y3K#{90!D%VpaOi0ki+{4dFlal9{>L@e*gdSC?P+Co8VjUDd>XBpa~Yi z^I!s;1GgR_7Vy~37iFgK8W#v8{ix8HTV!*1`OOe zi}>Is_yD{NZbO?dz#@1CJPj@Yso9gje2fA{0i(eGNr7vGRIZUq#eGM(yH+@B)2h{( zpKsJACoQWn)ve)sy;iNw!DcNIab9&r!&y2{196r1nylV8roM$STUcGPY1jZWwK?iI z((MxMz_mdqC#lszczIK&gTZIU3BLR$;!fMtMfX(j85w-4n@1cBI6Y3lg(dX1W7Dn< zH;r&shfbkkFj`}rXtH|<=IUULV&Dk15~M{X8+D7Z_BC2iYuF4LDZ%^g6}aQuejx$>l*9cn2b8t%dbwaWk0KamGqqgi^^zr!C5E8H5@xxxKf+s`6cx zbG(k?pr~3!XQ`B0zkbHjH}@{Oe^1_tbnR{1iYzk59C{+5xx9Mil+AjTsg0zczAB5F z)dPLTLA|s%>b$^9J?>*V^>Mc-w!>KDM-6t&phq5xs_1k0-J_1o{G6gAilOD+L(Oy; zr}T&goTZ*G=d|1xb0e(fd7$6sICf98?0Y?oV_Ph(6K%^=XOwBK*C>PHWdJd?Kw;cw zI~gX0$@fmrw`}g4pVCWKo3mWVb Date: Sun, 12 Aug 2018 11:01:36 +0200 Subject: [PATCH 53/56] Added canonizer back --- .../service/canonizer/SATCanonizerTest.java | 310 ++++++++++++++++++ .../service/canonizer/SATCanonizerTest2.java | 82 +++++ 2 files changed, 392 insertions(+) create mode 100644 test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java create mode 100644 test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.java diff --git a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java new file mode 100644 index 00000000..7c7b9fb1 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -0,0 +1,310 @@ +package za.ac.sun.cs.green.service.canonizer; + +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 SATCanonizerTest { + + 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", "(slice (canonize sink))"); + props.setProperty("green.service.sat.slice", "za.ac.sun.cs.green.service.slicer.SATSlicerService"); + 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) { + String s0 = observed.replaceAll("[()]", ""); + String s1 = s0.replaceAll("v[0-9]", "v"); + SortedSet s2 = new TreeSet(Arrays.asList(s1.split("&&"))); + SortedSet s3 = new TreeSet(Arrays.asList(expected)); + assertEquals(s3, s2); + } + + private void check(Expression expression, String full, String... expected) { + Instance i = new Instance(solver, null, null, expression); + Expression e = i.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + assertEquals(full, i.getFullExpression().toString()); + Object result = i.request("sat"); + assertNotNull(result); + assertEquals(Instance.class, result.getClass()); + Instance j = (Instance) result; + finalCheck(j.getExpression().toString(), expected); + } + + private void check(Expression expression, Expression parentExpression, String full, String... expected) { + Instance i1 = new Instance(solver, null, parentExpression); + Instance i2 = new Instance(solver, i1, expression); + Expression e = i2.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + assertEquals(full, i2.getFullExpression().toString()); + Object result = i2.request("sat"); + assertNotNull(result); + assertEquals(Instance.class, result.getClass()); + Instance j = (Instance) result; + finalCheck(j.getExpression().toString(), expected); + } + + @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); + check(o, "aa==0", "1*v==0"); + } + /* Changed last line from "check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0");" + to check(o3, "(aa=<0)&&(bb!=1)", "1*v==0", "1*v+-1!=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); + IntVariable v2 = new IntVariable("bb", 0, 99); + IntConstant c2 = new IntConstant(1); + Operation o2 = new Operation(Operation.Operator.NE, v2, c2); + Operation o3 = new Operation(Operation.Operator.AND, o1, o2); + check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0"); + } + + @Test + public void test03() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntConstant c1 = new IntConstant(0); + 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); + check(o1, o2, "(aa==0)&&(bb!=1)", "1*v==0"); + } + + @Test + public void test04() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntConstant c1 = new IntConstant(0); + Operation o1 = new Operation(Operation.Operator.EQ, v1, c1); + IntConstant c2 = new IntConstant(1); + Operation o2 = new Operation(Operation.Operator.NE, v1, c2); + check(o1, o2, "(aa==0)&&(aa!=1)", "1*v==0", "1*v+-1!=0"); + } + + @Test + public void test05() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + Operation o1 = new Operation(Operation.Operator.EQ, v1, v2); + IntVariable v3 = new IntVariable("cc", 0, 99); + Operation o2 = new Operation(Operation.Operator.EQ, v2, v3); + IntVariable v4 = new IntVariable("dd", 0, 99); + Operation o3 = new Operation(Operation.Operator.EQ, v3, v4); + IntVariable v5 = new IntVariable("ee", 0, 99); + Operation o4 = new Operation(Operation.Operator.EQ, v4, v5); + Operation o34 = new Operation(Operation.Operator.AND, o3, o4); + Operation o234 = new Operation(Operation.Operator.AND, o2, o34); + check(o1, o234, "(aa==bb)&&((bb==cc)&&((cc==dd)&&(dd==ee)))", "1*v+-1*v==0", "1*v+-1*v==0", "1*v+-1*v==0", + "1*v+-1*v==0"); + } + + @Test + public void test06() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + Operation o1 = new Operation(Operation.Operator.EQ, v1, v2); + IntVariable v3 = new IntVariable("cc", 0, 99); + Operation o2 = new Operation(Operation.Operator.EQ, v2, v3); + IntVariable v4 = new IntVariable("dd", 0, 99); + Operation o3 = new Operation(Operation.Operator.EQ, v3, v4); + IntVariable v5 = new IntVariable("ee", 0, 99); + IntVariable v6 = new IntVariable("ff", 0, 99); + Operation o4 = new Operation(Operation.Operator.EQ, v5, v6); + Operation o34 = new Operation(Operation.Operator.AND, o3, o4); + Operation o234 = new Operation(Operation.Operator.AND, o2, o34); + check(o1, o234, "(aa==bb)&&((bb==cc)&&((cc==dd)&&(ee==ff)))", "1*v+-1*v==0", "1*v+-1*v==0", "1*v+-1*v==0"); + } + + @Test + public void test07() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + IntVariable v3 = new IntVariable("cc", 0, 99); + IntVariable v4 = new IntVariable("dd", 0, 99); + IntVariable v5 = new IntVariable("ee", 0, 99); + IntVariable v6 = new IntVariable("ff", 0, 99); + IntVariable v7 = new IntVariable("gg", 0, 99); + Operation o1 = new Operation(Operation.Operator.LT, v1, new Operation(Operation.Operator.ADD, v2, v3)); + Operation o2 = new Operation(Operation.Operator.LT, v2, new Operation(Operation.Operator.ADD, v4, v5)); + Operation o3 = new Operation(Operation.Operator.LT, v3, new Operation(Operation.Operator.ADD, v6, v7)); + Operation o23 = new Operation(Operation.Operator.AND, o2, o3); + check(o1, o23, "(aa<(bb+cc))&&((bb<(dd+ee))&&(cc<(ff+gg)))", "1*v+-1*v+-1*v+1<=0", "1*v+-1*v+-1*v+1<=0", + "1*v+-1*v+-1*v+1<=0"); + } + + @Test + public void test08() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + IntVariable v3 = new IntVariable("cc", 0, 99); + IntVariable v4 = new IntVariable("dd", 0, 99); + IntVariable v5 = new IntVariable("ee", 0, 99); + IntVariable v6 = new IntVariable("ff", 0, 99); + IntVariable v7 = new IntVariable("gg", 0, 99); + IntVariable v8 = new IntVariable("hh", 0, 99); + Operation o1 = new Operation(Operation.Operator.LT, v1, new Operation(Operation.Operator.ADD, v2, v3)); + Operation o2 = new Operation(Operation.Operator.LT, v2, new Operation(Operation.Operator.ADD, v4, v5)); + Operation o3 = new Operation(Operation.Operator.LT, v6, new Operation(Operation.Operator.ADD, v7, v8)); + Operation o23 = new Operation(Operation.Operator.AND, o2, o3); + check(o1, o23, "(aa<(bb+cc))&&((bb<(dd+ee))&&(ff<(gg+hh)))", "1*v+-1*v+-1*v+1<=0", "1*v+-1*v+-1*v+1<=0"); + } + + @Test + public void test09() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + IntVariable v3 = new IntVariable("cc", 0, 99); + Operation o1 = new Operation(Operation.Operator.ADD, v1, v2); + Operation o2 = new Operation(Operation.Operator.ADD, v1, v3); + Operation o3 = new Operation(Operation.Operator.LT, o1, o2); + check(o3, "(aa+bb)<(aa+cc)", "1*v+-1*v+1<=0"); + } + + @Test + public void test10() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + IntVariable v3 = new IntVariable("cc", 0, 99); + Operation o1 = new Operation(Operation.Operator.ADD, v1, v2); + Operation o2 = new Operation(Operation.Operator.SUB, v1, v3); + Operation o3 = new Operation(Operation.Operator.LT, o1, o2); + check(o3, "(aa+bb)<(aa-cc)", "1*v+1*v+1<=0"); + } + + @Test + public void test11() { + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + Operation o1 = new Operation(Operation.Operator.ADD, v1, v2); + Operation o2 = new Operation(Operation.Operator.SUB, v2, v1); + Operation o3 = new Operation(Operation.Operator.LT, o1, o2); + check(o3, "(aa+bb)<(bb-aa)", "2*v+1<=0"); + } + + @Test + public void test12() { + IntConstant c1 = new IntConstant(2); + IntConstant c2 = new IntConstant(3); + IntVariable v1 = new IntVariable("aa", 0, 99); + IntVariable v2 = new IntVariable("bb", 0, 99); + Operation o1 = new Operation(Operation.Operator.ADD, c1, c2); + Operation o2 = new Operation(Operation.Operator.MUL, o1, v1); + Operation o3 = new Operation(Operation.Operator.LT, o2, v2); + check(o3, "((2+3)*aa) s2 = new TreeSet(Arrays.asList(s1.split("&&"))); + SortedSet s3 = new TreeSet(Arrays.asList(expected)); + assertEquals(s2, s3); + } + + private void check(Expression expression, String full, String... expected) { + Instance i = new Instance(solver, null, null, expression); + Expression e = i.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + assertEquals(full, i.getFullExpression().toString()); + Object result = i.request("sat"); + assertNotNull(result); + assertEquals(Instance.class, result.getClass()); + Instance j = (Instance) result; + finalCheck(j.getExpression().toString(), expected); + } + + private void check(Expression expression, Expression parentExpression, String full, String... expected) { + Instance i1 = new Instance(solver, null, parentExpression); + Instance i2 = new Instance(solver, i1, expression); + Expression e = i2.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + assertEquals(full, i2.getFullExpression().toString()); + Object result = i2.request("sat"); + assertNotNull(result); + assertEquals(Instance.class, result.getClass()); + Instance j = (Instance) result; + finalCheck(j.getExpression().toString(), expected); + } + + @Test + public void test23() { + IntVariable x5 = new IntVariable("x5", 0, 99); + IntConstant c1 = new IntConstant(1); + IntConstant c0 = new IntConstant(0); + Operation o2b = new Operation(Operation.Operator.NE, x5, x5); + Operation o2a = new Operation(Operation.Operator.NOT, o2b); + check(o2a, "!(x5!=x5)", "0==0"); + } + +} From 30d444dbff6889b688ddc9f004038084eeffe86a Mon Sep 17 00:00:00 2001 From: = <=> Date: Sun, 12 Aug 2018 15:25:31 +0200 Subject: [PATCH 54/56] Added simplify folder with tests to green/src/.../service --- .../simplify/OnlyConstantPropogationTest.java | 74 +++++++ ...SimplificationConstantPropogationTest.java | 186 ++++++++++++++++++ 2 files changed, 260 insertions(+) create mode 100644 src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java create mode 100644 src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java 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..c5554c33 --- /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.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)"); + } + +} 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..c7995ac6 --- /dev/null +++ b/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java @@ -0,0 +1,186 @@ +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", "(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)&&(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"); + } + + + + + +} From a41f98bdf7ed60ad036c54bdd57549cc952793b4 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Mon, 13 Aug 2018 13:20:20 +0200 Subject: [PATCH 55/56] Added OnlyConstantPropogationService.java --- .../OnlyConstantPropogationService.java | 682 ++++++++++++++++++ .../simplify/OnlyConstantPropogationTest.java | 74 -- ...SimplificationConstantPropogationTest.java | 186 ----- 3 files changed, 682 insertions(+), 260 deletions(-) create mode 100644 src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java delete mode 100644 src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java delete mode 100644 src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java diff --git a/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java b/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java new file mode 100644 index 00000000..267b4729 --- /dev/null +++ b/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java @@ -0,0 +1,682 @@ +package za.ac.sun.cs.green.service.canonizer; + +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 OnlyConstantPropogationService extends BasicService { + + /** + * Number of times the slicer has been invoked. + */ + private int invocations = 0; + + public OnlyConstantPropogationService(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 = canonize(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 canonize(Expression expression, + Map map) { + try { + log.log(Level.FINEST, "Before Canonization: " + expression); + invocations++; + OrderingVisitor orderingVisitor = new OrderingVisitor(); + expression.accept(orderingVisitor); + expression = orderingVisitor.getExpression(); + CanonizationVisitor canonizationVisitor = new CanonizationVisitor(); + expression.accept(canonizationVisitor); + Expression canonized = canonizationVisitor.getExpression(); + if (canonized != null) { + canonized = new Renamer(map, + canonizationVisitor.getVariableSet()).rename(canonized); + } + log.log(Level.FINEST, "After Canonization: " + canonized); + return canonized; + } 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() { + return stack.pop(); + } + + @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(); + 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); + } + } + + } + + private static class CanonizationVisitor extends Visitor { + + private Stack stack; + + private SortedSet conjuncts; + + private SortedSet variableSet; + + private Map lowerBounds; + + private Map upperBounds; + + private IntVariable boundVariable; + + private Integer bound; + + private int boundCoeff; + + private boolean unsatisfiable; + + private boolean linearInteger; + + public CanonizationVisitor() { + stack = new Stack(); + conjuncts = new TreeSet(); + variableSet = new TreeSet(); + unsatisfiable = false; + linearInteger = true; + } + + public SortedSet getVariableSet() { + return variableSet; + } + + public Expression getExpression() { + if (!linearInteger) { + return null; + } else if (unsatisfiable) { + return Operation.FALSE; + } else { + if (!stack.isEmpty()) { + Expression x = stack.pop(); + if (x.equals(Operation.FALSE)) { + return Operation.FALSE; + } else if (!x.equals(Operation.TRUE)) { + conjuncts.add(x); + } + } + SortedSet newConjuncts = processBounds(); +// new TreeSet(); + Expression c = null; + for (Expression e : newConjuncts) { + if (e.equals(Operation.FALSE)) { + return Operation.FALSE; + } else if (e instanceof Operation) { + Operation o = (Operation) e; + if (o.getOperator() == Operation.Operator.GT) { + e = new Operation(Operation.Operator.LT, scale(-1, + o.getOperand(0)), o.getOperand(1)); + } else if (o.getOperator() == Operation.Operator.GE) { + e = new Operation(Operation.Operator.LE, scale(-1, + o.getOperand(0)), o.getOperand(1)); + } + o = (Operation) e; + if (o.getOperator() == Operation.Operator.GT) { + e = new Operation(Operation.Operator.GE, merge( + o.getOperand(0), new IntConstant(-1)), + o.getOperand(1)); + } else if (o.getOperator() == Operation.Operator.LT) { + e = new Operation(Operation.Operator.LE, merge( + o.getOperand(0), new IntConstant(1)), + o.getOperand(1)); + } + } + if (c == null) { + c = e; + } else { + c = new Operation(Operation.Operator.AND, c, e); + } + } + return (c == null) ? Operation.TRUE : c; + } + } + + private SortedSet processBounds() { + return conjuncts; + } + + @SuppressWarnings("unused") + private void extractBound(Expression e) throws VisitorException { + if (e instanceof Operation) { + Operation o = (Operation) e; + Expression lhs = o.getOperand(0); + Operation.Operator op = o.getOperator(); + if (isBound(lhs)) { + switch (op) { + case EQ: + lowerBounds.put(boundVariable, bound * boundCoeff); + upperBounds.put(boundVariable, bound * boundCoeff); + break; + case LT: + if (boundCoeff == 1) { + upperBounds.put(boundVariable, bound * -1 - 1); + } else { + lowerBounds.put(boundVariable, bound + 1); + } + break; + case LE: + if (boundCoeff == 1) { + upperBounds.put(boundVariable, bound * -1); + } else { + lowerBounds.put(boundVariable, bound); + } + break; + case GT: + if (boundCoeff == 1) { + lowerBounds.put(boundVariable, bound * -1 + 1); + } else { + upperBounds.put(boundVariable, bound - 1); + } + break; + case GE: + if (boundCoeff == 1) { + lowerBounds.put(boundVariable, bound * -1); + } else { + upperBounds.put(boundVariable, bound); + } + break; + default: + break; + } + } + } + } + + private boolean isBound(Expression lhs) { + if (!(lhs instanceof Operation)) { + return false; + } + Operation o = (Operation) lhs; + if (o.getOperator() == Operation.Operator.MUL) { + if (!(o.getOperand(0) instanceof IntConstant)) { + return false; + } + if (!(o.getOperand(1) instanceof IntVariable)) { + return false; + } + boundVariable = (IntVariable) o.getOperand(1); + bound = 0; + if ((((IntConstant) o.getOperand(0)).getValue() == 1) + || (((IntConstant) o.getOperand(0)).getValue() == -1)) { + boundCoeff = ((IntConstant) o.getOperand(0)).getValue(); + return true; + } else { + return false; + } + } else if (o.getOperator() == Operation.Operator.ADD) { + if (!(o.getOperand(1) instanceof IntConstant)) { + return false; + } + bound = ((IntConstant) o.getOperand(1)).getValue(); + if (!(o.getOperand(0) instanceof Operation)) { + return false; + } + Operation p = (Operation) o.getOperand(0); + if (!(p.getOperand(0) instanceof IntConstant)) { + return false; + } + if (!(p.getOperand(1) instanceof IntVariable)) { + return false; + } + boundVariable = (IntVariable) p.getOperand(1); + if ((((IntConstant) p.getOperand(0)).getValue() == 1) + || (((IntConstant) p.getOperand(0)).getValue() == -1)) { + boundCoeff = ((IntConstant) p.getOperand(0)).getValue(); + return true; + } else { + return false; + } + } else { + return false; + } + } + + @Override + public void postVisit(Constant constant) { + if (linearInteger && !unsatisfiable) { + if (constant instanceof IntConstant) { + stack.push(constant); + } else { + stack.clear(); + linearInteger = false; + } + } + } + + @Override + public void postVisit(Variable variable) { + if (linearInteger && !unsatisfiable) { + if (variable instanceof IntVariable) { + variableSet.add((IntVariable) variable); + stack.push(new Operation(Operation.Operator.MUL, Operation.ONE, + variable)); + } else { + stack.clear(); + linearInteger = false; + } + } + } + + @Override + public void postVisit(Operation operation) throws VisitorException { + if (!linearInteger || unsatisfiable) { + return; + } + Operation.Operator op = operation.getOperator(); + switch (op) { + case AND: + if (!stack.isEmpty()) { + Expression x = stack.pop(); + if (!x.equals(Operation.TRUE)) { + conjuncts.add(x); + } + } + if (!stack.isEmpty()) { + Expression x = stack.pop(); + if (!x.equals(Operation.TRUE)) { + conjuncts.add(x); + } + } + break; + case EQ: + case NE: + case LT: + case LE: + case GT: + case GE: + if (!stack.isEmpty()) { + Expression e = merge(scale(-1, stack.pop()), stack.pop()); + if (e instanceof IntConstant) { + int v = ((IntConstant) e).getValue(); + boolean b = true; + if (op == Operation.Operator.EQ) { + b = v == 0; + } else if (op == Operation.Operator.NE) { + b = v != 0; + } else if (op == Operation.Operator.LT) { + b = v < 0; + } else if (op == Operation.Operator.LE) { + b = v <= 0; + } else if (op == Operation.Operator.GT) { + b = v > 0; + } else if (op == Operation.Operator.GE) { + b = v >= 0; + } + if (b) { + stack.push(Operation.TRUE); + } else { + stack.push(Operation.FALSE); + // unsatisfiable = true; + } + } else { + stack.push(new Operation(op, e, Operation.ZERO)); + } + } + break; + case ADD: + stack.push(merge(stack.pop(), stack.pop())); + break; + case SUB: + stack.push(merge(scale(-1, stack.pop()), stack.pop())); + break; + case MUL: + if (stack.size() >= 2) { + Expression r = stack.pop(); + Expression l = stack.pop(); + if ((l instanceof IntConstant) && (r instanceof IntConstant)) { + int li = ((IntConstant) l).getValue(); + int ri = ((IntConstant) r).getValue(); + stack.push(new IntConstant(li * ri)); + } else if (l instanceof IntConstant) { + int li = ((IntConstant) l).getValue(); + stack.push(scale(li, r)); + } else if (r instanceof IntConstant) { + int ri = ((IntConstant) r).getValue(); + stack.push(scale(ri, l)); + } else { + stack.clear(); + linearInteger = false; + } + } + break; + case NOT: + if (!stack.isEmpty()) { + Expression e = stack.pop(); + if (e.equals(Operation.TRUE)) { + e = Operation.FALSE; + } else if (e.equals(Operation.FALSE)) { + e = Operation.TRUE; + } else if (e instanceof Operation) { + Operation o = (Operation) e; + switch (o.getOperator()) { + case NOT: + e = o.getOperand(0); + break; + case EQ: + e = new Operation(Operation.Operator.NE, o.getOperand(0), o.getOperand(1)); + break; + case NE: + e = new Operation(Operation.Operator.EQ, o.getOperand(0), o.getOperand(1)); + break; + case GE: + e = new Operation(Operation.Operator.LT, o.getOperand(0), o.getOperand(1)); + break; + case GT: + e = new Operation(Operation.Operator.LE, o.getOperand(0), o.getOperand(1)); + break; + case LE: + e = new Operation(Operation.Operator.GT, o.getOperand(0), o.getOperand(1)); + break; + case LT: + e = new Operation(Operation.Operator.GE, o.getOperand(0), o.getOperand(1)); + break; + default: + break; + } + } else { + // We just drop the NOT?? + } + stack.push(e); + } else { + // We just drop the NOT?? + } + break; + default: + break; + } + } + + private Expression merge(Expression left, Expression right) { + Operation l = null; + Operation r = null; + int s = 0; + if (left instanceof IntConstant) { + s = ((IntConstant) left).getValue(); + } else { + if (hasRightConstant(left)) { + s = getRightConstant(left); + l = getLeftOperation(left); + } else { + l = (Operation) left; + } + } + if (right instanceof IntConstant) { + s += ((IntConstant) right).getValue(); + } else { + if (hasRightConstant(right)) { + s += getRightConstant(right); + r = getLeftOperation(right); + } else { + r = (Operation) right; + } + } + SortedMap coefficients = new TreeMap(); + IntConstant c; + Variable v; + Integer k; + + // Collect the coefficients of l + if (l != null) { + while (l.getOperator() == Operation.Operator.ADD) { + Operation o = (Operation) l.getOperand(1); + assert (o.getOperator() == Operation.Operator.MUL); + c = (IntConstant) o.getOperand(0); + v = (IntVariable) o.getOperand(1); + coefficients.put(v, c.getValue()); + l = (Operation) l.getOperand(0); + } + assert (l.getOperator() == Operation.Operator.MUL); + c = (IntConstant) l.getOperand(0); + v = (IntVariable) l.getOperand(1); + coefficients.put(v, c.getValue()); + } + + // Collect the coefficients of r + if (r != null) { + while (r.getOperator() == Operation.Operator.ADD) { + Operation o = (Operation) r.getOperand(1); + assert (o.getOperator() == Operation.Operator.MUL); + c = (IntConstant) o.getOperand(0); + v = (IntVariable) o.getOperand(1); + k = coefficients.get(v); + if (k == null) { + coefficients.put(v, c.getValue()); + } else { + coefficients.put(v, c.getValue() + k); + } + r = (Operation) r.getOperand(0); + } + assert (r.getOperator() == Operation.Operator.MUL); + c = (IntConstant) r.getOperand(0); + v = (IntVariable) r.getOperand(1); + k = coefficients.get(v); + if (k == null) { + coefficients.put(v, c.getValue()); + } else { + coefficients.put(v, c.getValue() + k); + } + } + + Expression lr = null; + for (Map.Entry e : coefficients.entrySet()) { + int coef = e.getValue(); + if (coef != 0) { + Operation term = new Operation(Operation.Operator.MUL, + new IntConstant(coef), e.getKey()); + if (lr == null) { + lr = term; + } else { + lr = new Operation(Operation.Operator.ADD, lr, term); + } + } + } + if ((lr == null) || (lr instanceof IntConstant)) { + return new IntConstant(s); + } else if (s == 0) { + return lr; + } else { + return new Operation(Operation.Operator.ADD, lr, + new IntConstant(s)); + } + } + + private boolean hasRightConstant(Expression expression) { + return isAddition(expression) + && (getRightExpression(expression) instanceof IntConstant); + } + + private int getRightConstant(Expression expression) { + return ((IntConstant) getRightExpression(expression)).getValue(); + } + + private Expression getLeftExpression(Expression expression) { + return ((Operation) expression).getOperand(0); + } + + private Expression getRightExpression(Expression expression) { + return ((Operation) expression).getOperand(1); + } + + private Operation getLeftOperation(Expression expression) { + return (Operation) getLeftExpression(expression); + } + + private boolean isAddition(Expression expression) { + return ((Operation) expression).getOperator() == Operation.Operator.ADD; + } + + private Expression scale(int factor, Expression expression) { + if (factor == 0) { + return Operation.ZERO; + } + if (expression instanceof IntConstant) { + return new IntConstant(factor + * ((IntConstant) expression).getValue()); + } else if (expression instanceof IntVariable) { + return expression; + } else { + assert (expression instanceof Operation); + Operation o = (Operation) expression; + Operation.Operator p = o.getOperator(); + Expression l = scale(factor, o.getOperand(0)); + Expression r = scale(factor, o.getOperand(1)); + return new Operation(p, l, r); + } + } + + } + + private static class Renamer extends Visitor { + + private Map map; + + private Stack stack; + + public Renamer(Map map, + SortedSet variableSet) { + this.map = map; + stack = new Stack(); + } + + public Expression rename(Expression expression) throws VisitorException { + expression.accept(this); + return stack.pop(); + } + + @Override + public void postVisit(IntVariable variable) { + Variable v = map.get(variable); + if (v == null) { + v = new IntVariable("v" + map.size(), variable.getLowerBound(), + variable.getUpperBound()); + map.put(variable, v); + } + stack.push(v); + } + + @Override + public void postVisit(IntConstant constant) { + stack.push(constant); + } + + @Override + public void postVisit(Operation operation) { + int arity = operation.getOperator().getArity(); + Expression operands[] = new Expression[arity]; + for (int i = arity; i > 0; i--) { + operands[i - 1] = stack.pop(); + } + stack.push(new Operation(operation.getOperator(), operands)); + } + + } + +} diff --git a/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java b/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java deleted file mode 100644 index c5554c33..00000000 --- a/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java +++ /dev/null @@ -1,74 +0,0 @@ -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)"); - } - -} diff --git a/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java b/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java deleted file mode 100644 index c7995ac6..00000000 --- a/src/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java +++ /dev/null @@ -1,186 +0,0 @@ -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", "(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)&&(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"); - } - - - - - -} From 5afe89a7266516a42fbf577590fbada66ae68284 Mon Sep 17 00:00:00 2001 From: marcdefaria Date: Mon, 13 Aug 2018 19:34:27 +0200 Subject: [PATCH 56/56] Created the Constant Propogation tests, but still cant get tests to run --- ...nstantPropogationService.java => ConstantPropogation.java} | 4 ++-- .../green/service/simplify/OnlyConstantPropogationTest.java | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) rename src/za/ac/sun/cs/green/service/simplify/{OnlyConstantPropogationService.java => ConstantPropogation.java} (99%) diff --git a/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropogation.java similarity index 99% rename from src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java rename to src/za/ac/sun/cs/green/service/simplify/ConstantPropogation.java index 267b4729..d29e3b94 100644 --- a/src/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationService.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropogation.java @@ -24,14 +24,14 @@ import za.ac.sun.cs.green.expr.Visitor; import za.ac.sun.cs.green.expr.VisitorException; -public class OnlyConstantPropogationService extends BasicService { +public class ConstantPropogation extends BasicService { /** * Number of times the slicer has been invoked. */ private int invocations = 0; - public OnlyConstantPropogationService(Green solver) { + public ConstantPropogation(Green solver) { super(solver); } diff --git a/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java index c5554c33..772d5c5c 100644 --- a/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java +++ b/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java @@ -25,6 +25,7 @@ public class OnlyConstantPropogationTest { @BeforeClass public static void initialize() { solver = new Green(); + System.out.println("hello llaow"); Properties props = new Properties(); props.setProperty("green.services", "sat"); props.setProperty("green.service.sat", "(simplify sink)");