From bc3f6b3fde5fa34100262006f3f24736327367d1 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 10:18:50 +0200 Subject: [PATCH 01/66] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index aedc3ddc..833bd349 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/wiesnerbernard/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master) Notes: From f90f0fb18d159bdadb3a29f3a6d5035ae8015a49 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 10:27:24 +0200 Subject: [PATCH 02/66] Removed commented test20 --- .../za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 3 +-- 1 file changed, 1 insertion(+), 2 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..412a3d05 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -293,7 +293,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,4 @@ public void test20() { Operation o3 = new Operation(Operation.Operator.AND, o1, o2); check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); } -*/ } From a3af55dd71cffed5673b64de8ee1972cf7aa4d2e Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 10:38:32 +0200 Subject: [PATCH 03/66] ChangedExpectedOutput of testcase 20 --- 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 412a3d05..686c41cf 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,6 +301,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); + check(o3, "(2<=2)&&(aa<2)", "1*v0+-1<0"); } } From 5a151fd50a06e50bbfc786001f7ae7443edad397 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 10:41:10 +0200 Subject: [PATCH 04/66] Update SATCanonizerTest.java --- 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 686c41cf..36548923 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,6 +301,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "1*v0+-1<0"); + check(o3, "(aa<2)&&(2<=2)", "1*v0+-1<0"); } } From ee8ab4904b081765828c51d577ae13bb7295313d Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 10:48:37 +0200 Subject: [PATCH 05/66] Update SATCanonizerTest.java --- 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 36548923..412a3d05 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,6 +301,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(aa<2)&&(2<=2)", "1*v0+-1<0"); + check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); } } From 6b00ae446ce955cf0128d511178d41ede95ac3be Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 10:55:05 +0200 Subject: [PATCH 06/66] Update SATCanonizerTest.java --- 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 412a3d05..b15a2da8 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,6 +301,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); + check(o3, "(2<=2)&&(aa<2)", "1*v+-1<2"); } } From c6b68ba5bb03abd8f3e1969230c9aaaf1400b654 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:12:58 +0200 Subject: [PATCH 07/66] Update SATCanonizerTest.java --- test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 1 + 1 file changed, 1 insertion(+) 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 b15a2da8..d1c6f751 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -53,6 +53,7 @@ private void check(Expression expression, String full, String... expected) { assertNotNull(result); assertEquals(Instance.class, result.getClass()); Instance j = (Instance) result; + System.out.println(j.getExpression().toString() + " ===== " + expected); finalCheck(j.getExpression().toString(), expected); } From a2e98c4bc8f15f31a6ca92d6ffa84a11a86675a0 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:14:39 +0200 Subject: [PATCH 08/66] Update SATCanonizerTest.java --- 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 d1c6f751..a179afac 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -302,6 +302,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "1*v+-1<2"); + check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); } } From 3da952dd78ab2e5ab322691e65bfdb89519d2a64 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:20:43 +0200 Subject: [PATCH 09/66] Update SATCanonizerTest.java --- 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 a179afac..d38416f2 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -302,6 +302,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); + check(o3, "(2<=2)&&(aa<2)", "((1*v+-1)<=0"); } } From 00677a8650339ba6a8dc79a8fa8af2cece89d63b Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:27:25 +0200 Subject: [PATCH 10/66] Update SATCanonizerTest.java --- test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 1 + 1 file changed, 1 insertion(+) 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 d38416f2..18007731 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -40,6 +40,7 @@ private void finalCheck(String observed, String[] expected) { String s1 = s0.replaceAll("v[0-9]", "v"); SortedSet s2 = new TreeSet(Arrays.asList(s1.split("&&"))); SortedSet s3 = new TreeSet(Arrays.asList(expected)); + System.out.println("======================================================"); assertEquals(s3, s2); } From 535a23a02bcf2f03de6eb3fae88504ddd8abdd97 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:31:23 +0200 Subject: [PATCH 11/66] Update SATCanonizerTest.java --- test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java | 2 -- 1 file changed, 2 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 18007731..41ce3c26 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -40,7 +40,6 @@ private void finalCheck(String observed, String[] expected) { String s1 = s0.replaceAll("v[0-9]", "v"); SortedSet s2 = new TreeSet(Arrays.asList(s1.split("&&"))); SortedSet s3 = new TreeSet(Arrays.asList(expected)); - System.out.println("======================================================"); assertEquals(s3, s2); } @@ -54,7 +53,6 @@ private void check(Expression expression, String full, String... expected) { assertNotNull(result); assertEquals(Instance.class, result.getClass()); Instance j = (Instance) result; - System.out.println(j.getExpression().toString() + " ===== " + expected); finalCheck(j.getExpression().toString(), expected); } From bf5f1ed489d8e1cf5b5587434467ebea2a5e5fae Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:32:17 +0200 Subject: [PATCH 12/66] Update SATCanonizerTest.java --- 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 41ce3c26..794e456b 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,6 +301,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "((1*v+-1)<=0"); + check(o3, "(2<=2)&&(aa<2)", "1*v+-1<=0"); } } From dd3d3d99b052a0c3639bbc8ed5b021eed7962cd6 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 11:57:40 +0200 Subject: [PATCH 13/66] Update build.xml --- build.xml | 1 + 1 file changed, 1 insertion(+) diff --git a/build.xml b/build.xml index 0c29bed8..3bd65aae 100644 --- a/build.xml +++ b/build.xml @@ -102,6 +102,7 @@ + From 0e715033e3c07da95c581206887852799f52021c Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 12:04:25 +0200 Subject: [PATCH 14/66] Update .travis.yml --- .travis.yml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.travis.yml b/.travis.yml index 4651be32..45d7ff9e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,15 @@ 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; + - bundle exec rake test From 5900cf966741fc37318796923ffcc3ceff402723 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 12:14:01 +0200 Subject: [PATCH 15/66] Update .travis.yml --- .travis.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index 45d7ff9e..a7efc5c7 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,10 +4,10 @@ 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 build -t wiesnerbernard/Dockerfile . + - docker run -d -p 127.0.0.1:80:4567 wiesnerbernard/Dockerfile /bin/sh -c "cd wiesnerbernard/Dockerfile; bundle exec foreman start;" - docker ps -a - - docker run carlad/sinatra /bin/sh -c "cd /root/sinatra; bundle exec rake test" + - docker run Dockerfile /bin/sh -c "cd wiesnerbernard/Dockerfile; bundle exec rake test" script: - ant; From 0ea9bc013b6ddb415b27b5e9e4a9be226760ec3c Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 24 Jul 2018 12:28:18 +0200 Subject: [PATCH 16/66] Update .travis.yml --- .travis.yml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index a7efc5c7..0bb6694c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,12 +4,7 @@ services: - docker before_install: - - docker build -t wiesnerbernard/Dockerfile . - - docker run -d -p 127.0.0.1:80:4567 wiesnerbernard/Dockerfile /bin/sh -c "cd wiesnerbernard/Dockerfile; bundle exec foreman start;" - - docker ps -a - - docker run Dockerfile /bin/sh -c "cd wiesnerbernard/Dockerfile; bundle exec rake test" - + - docker build -t green . + script: - - ant; - - ant test; - - bundle exec rake test + - docker run green /bin/sh -c "ant; ant test;" From 5a3a8cf8f63f9d2432def3cab82fec72fcd6fe20 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 30 Jul 2018 20:07:32 +0200 Subject: [PATCH 17/66] Update SATCanonizerTest.java --- 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 794e456b..412a3d05 100644 --- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -301,6 +301,6 @@ public void test20() { Operation o1 = new Operation(Operation.Operator.LE, c1, c1); Operation o2 = new Operation(Operation.Operator.LT, v1, c1); Operation o3 = new Operation(Operation.Operator.AND, o1, o2); - check(o3, "(2<=2)&&(aa<2)", "1*v+-1<=0"); + check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0"); } } From f07162cd2447cc4aa96d3632d91fd12c02eb44b7 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 30 Jul 2018 20:36:59 +0200 Subject: [PATCH 18/66] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 833bd349..0750af8d 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build Status](https://travis-ci.org/wiesnerbernard/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master) +[![Build Status](https://travis-ci.org/wiesnerbernard/green.svg?branch=master)](https://travis-ci.org/wiesnerbernard/green.svg?branch=master) Notes: From de3beb6e8f64f48072b644da630f640456385103 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 31 Jul 2018 09:33:13 +0200 Subject: [PATCH 19/66] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0750af8d..23f04309 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build Status](https://travis-ci.org/wiesnerbernard/green.svg?branch=master)](https://travis-ci.org/wiesnerbernard/green.svg?branch=master) +[![Build Status](https://travis-ci.org/wiesnerbernard/green.svg?branch=master)](https://travis-ci.org/wiesnerbernard/green?branch=master) Notes: From 8e4355cb09ff901e408c0e8b607dbaf9f7a294ba Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 31 Jul 2018 09:36:26 +0200 Subject: [PATCH 20/66] Update Dockerfile --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index e465a44f..221e91ae 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/wiesnerbernard/green # Download and extract Z3 RUN mkdir z3 From 1fa086dbada2d1f83873669c872a5f6ad56e696d Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Sun, 12 Aug 2018 19:04:13 +0200 Subject: [PATCH 21/66] Create ConstantPropagation.java --- src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java | 1 + 1 file changed, 1 insertion(+) create mode 100644 src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -0,0 +1 @@ + From fa2c29785a07b09329a9f44d5a72a87edaffb32c Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Sun, 12 Aug 2018 19:23:26 +0200 Subject: [PATCH 22/66] Create ConstantPropagationTest.java --- .../simplify/ConstantPropagationTest.java | 74 +++++++++++++++++++ 1 file changed, 74 insertions(+) create mode 100644 test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java diff --git a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java new file mode 100644 index 00000000..c5554c33 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.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)"); + } + +} From 5c3a91260fd82a467aac66394b9ed2f26935c622 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Sun, 12 Aug 2018 20:45:21 +0200 Subject: [PATCH 23/66] Update ConstantPropagation.java --- .../service/simplify/ConstantPropagation.java | 73 +++++++++++++++++++ 1 file changed, 73 insertions(+) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 8b137891..f8cb6922 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -1 +1,74 @@ +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; + +public class ConstantPropagation extends BasicService { + private int invocations = 0; + + public ConstantPropapagtion(Green solver) { + super(solver); + } + + @Override + public Set processRequest(Instance instance) { + @SuppressWarnings("unchecked") + Set result = (Set) instance.getData(getClass()); + if (result == null) { + final Map map = new HashMap(); + final Expression e = propagate(instance.getFullExpression(), map); + final Instance i = new Instance(getSolver(), instance.getSource(), null, e); + result = Collections.singleton(i); + instance.setData(getClass(), result); + } + return result; + } + + @Override + public void report(Reporter reporter) { + reporter.report(getClass().getSimpleName(), "invocations = " + invocations); + } + + public Expression propagate(Expression expression, + Map map) { + //try { + log.log(Level.FINEST, "Before Propagation " + expression); + invocations++; + //OrderingVisitor orderingVisitor = new OrderingVisitor(); + //expression.accept(orderingVisitor); + //expression = orderingVisitor.getExpression(); + //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; + } From fcc823e40a1bebfe9d505bc1f2623cc123277222 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 13:24:07 +0200 Subject: [PATCH 24/66] Update Dockerfile --- Dockerfile | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Dockerfile b/Dockerfile index 221e91ae..c9c3ad3b 100644 --- a/Dockerfile +++ b/Dockerfile @@ -17,6 +17,12 @@ RUN apt install libgomp1 # Clone down the GreenSolver repository RUN git clone https://github.com/wiesnerbernard/green +# +WORKDIR /green +RUN git fetch +RUN git checkout ConstanPropagation +WORKDIR / + # Download and extract Z3 RUN mkdir z3 WORKDIR z3 From e766afc9fde91cb362719955b827ab5bf5298f6f Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 13:24:33 +0200 Subject: [PATCH 25/66] Update Dockerfile --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index c9c3ad3b..857a7b63 100644 --- a/Dockerfile +++ b/Dockerfile @@ -20,7 +20,7 @@ RUN git clone https://github.com/wiesnerbernard/green # WORKDIR /green RUN git fetch -RUN git checkout ConstanPropagation +RUN git checkout constanPropagation WORKDIR / # Download and extract Z3 From ea624036a03a8c9d4e31a6dee36f6c0501bbe287 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 13:29:21 +0200 Subject: [PATCH 26/66] Update Dockerfile --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 857a7b63..28feef44 100644 --- a/Dockerfile +++ b/Dockerfile @@ -20,7 +20,7 @@ RUN git clone https://github.com/wiesnerbernard/green # WORKDIR /green RUN git fetch -RUN git checkout constanPropagation +RUN git checkout constantPropagation WORKDIR / # Download and extract Z3 From 2ec4cb97ebd55cec4759a58f45a61159052f565d Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 13:31:57 +0200 Subject: [PATCH 27/66] Update Dockerfile --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 28feef44..de7460a1 100644 --- a/Dockerfile +++ b/Dockerfile @@ -20,7 +20,7 @@ RUN git clone https://github.com/wiesnerbernard/green # WORKDIR /green RUN git fetch -RUN git checkout constantPropagation +RUN git checkout constantPropogation WORKDIR / # Download and extract Z3 From 79181b9218e0ad051e72df007cd7dcb1145c070a Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 13:39:40 +0200 Subject: [PATCH 28/66] Update ConstantPropagation.java --- src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index f8cb6922..3e8895f5 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -72,3 +72,4 @@ public Expression propagate(Expression expression, //} return null; } +} From d33774667f9c21686e8ecdf690b7a903a1f09241 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 13:44:05 +0200 Subject: [PATCH 29/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 3e8895f5..f4a932af 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -25,7 +25,7 @@ public class ConstantPropagation extends BasicService { private int invocations = 0; - public ConstantPropapagtion(Green solver) { + public ConstantPropagtion(Green solver) { super(solver); } From fbea38acbcb46f34166ddb703e6d9785b659bc35 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 14:11:00 +0200 Subject: [PATCH 30/66] Update ConstantPropagation.java --- .../service/simplify/ConstantPropagation.java | 639 +++++++++++++++++- 1 file changed, 620 insertions(+), 19 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index f4a932af..02f3e442 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -50,26 +50,627 @@ public void report(Reporter reporter) { public Expression propagate(Expression expression, Map map) { - //try { - log.log(Level.FINEST, "Before Propagation " + expression); + try { + log.log(Level.FINEST, "Before Propagation: " + 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); - //} + OrderingVisitor orderingVisitor = new OrderingVisitor(); + expression.accept(orderingVisitor); + expression = orderingVisitor.getExpression(); + PropagationVisitor canonizationVisitor = new PropagationVisitor(); + expression.accept(canonizationVisitor); + Expression propagated = propagationVisitor.getExpression(); + if (propagated != null) { + propagated = new Renamer(map, + propagationVisitor.getVariableSet()).rename(canonized); + } + log.log(Level.FINEST, "After Canonization: " + propagated); + return propagated; + } 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 PropagationVisitor 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 PropagationVisitor() { + 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)); + } + + } + } From cfa3e08e8467608acb9942a419be51d12f60aacd Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 14:17:50 +0200 Subject: [PATCH 31/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 02f3e442..18ec785c 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -21,6 +21,8 @@ import za.ac.sun.cs.green.expr.IntVariable; import za.ac.sun.cs.green.expr.Operation; import za.ac.sun.cs.green.expr.Variable; +import za.ac.sun.cs.green.expr.Visitor; +import za.ac.sun.cs.green.expr.VisitorException; public class ConstantPropagation extends BasicService { private int invocations = 0; From df7167c10f4516fb8c1c0e35f7a2fdd50ee33c04 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 14:32:17 +0200 Subject: [PATCH 32/66] Update ConstantPropagation.java --- .../cs/green/service/simplify/ConstantPropagation.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 18ec785c..7e981389 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -25,13 +25,13 @@ import za.ac.sun.cs.green.expr.VisitorException; public class ConstantPropagation extends BasicService { - private int invocations = 0; + private int invocations = 0; - public ConstantPropagtion(Green solver) { + public ConstantPropagation(Green solver) { super(solver); } - @Override + @Override public Set processRequest(Instance instance) { @SuppressWarnings("unchecked") Set result = (Set) instance.getData(getClass()); @@ -45,12 +45,12 @@ public Set processRequest(Instance instance) { return result; } - @Override + @Override public void report(Reporter reporter) { reporter.report(getClass().getSimpleName(), "invocations = " + invocations); } - public Expression propagate(Expression expression, + public Expression propagate(Expression expression, Map map) { try { log.log(Level.FINEST, "Before Propagation: " + expression); From 39799a6f4bf92f30fdcba4f6c821b954036594fa Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 14:39:24 +0200 Subject: [PATCH 33/66] Update ConstantPropagation.java --- .../cs/green/service/simplify/ConstantPropagation.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 7e981389..79a8c3c3 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -1,4 +1,4 @@ -package za.ac.sun.cs.green.service.canonizer; +package za.ac.sun.cs.green.service.simplify; import java.util.Collections; import java.util.HashMap; @@ -58,14 +58,14 @@ public Expression propagate(Expression expression, OrderingVisitor orderingVisitor = new OrderingVisitor(); expression.accept(orderingVisitor); expression = orderingVisitor.getExpression(); - PropagationVisitor canonizationVisitor = new PropagationVisitor(); - expression.accept(canonizationVisitor); + PropagationVisitor propagationVisitor = new PropagationVisitor(); + expression.accept(propagationVisitor); Expression propagated = propagationVisitor.getExpression(); if (propagated != null) { propagated = new Renamer(map, - propagationVisitor.getVariableSet()).rename(canonized); + propagationVisitor.getVariableSet()).rename(propagated); } - log.log(Level.FINEST, "After Canonization: " + propagated); + log.log(Level.FINEST, "After Propagation: " + propagated); return propagated; } catch (VisitorException x) { log.log(Level.SEVERE, From 93140fceb7050f91056831e51a91724a4ca34be7 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 14:57:08 +0200 Subject: [PATCH 34/66] Update ConstantPropagationTest.java --- .../sun/cs/green/service/simplify/ConstantPropagationTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java index c5554c33..1d2d5920 100644 --- a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java +++ b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java @@ -18,7 +18,7 @@ import za.ac.sun.cs.green.expr.Operation; import za.ac.sun.cs.green.util.Configuration; -public class OnlyConstantPropogationTest { +public class ConstantPropogationTest { public static Green solver; From 8fc0d1cf9fec3f8a8aa55a87345f824b23f5614f Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 15:00:38 +0200 Subject: [PATCH 35/66] Update ConstantPropagationTest.java --- .../sun/cs/green/service/simplify/ConstantPropagationTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java index 1d2d5920..e449e5b8 100644 --- a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java +++ b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java @@ -18,7 +18,7 @@ import za.ac.sun.cs.green.expr.Operation; import za.ac.sun.cs.green.util.Configuration; -public class ConstantPropogationTest { +public class ConstantPropagationTest { public static Green solver; From a2273013ccdd62a140dbeef2f7a1c9b44b2bd437 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 17:41:04 +0200 Subject: [PATCH 36/66] Update ConstantPropagation.java --- .../green/service/simplify/ConstantPropagation.java | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 79a8c3c3..453c842f 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -58,15 +58,16 @@ public Expression propagate(Expression expression, OrderingVisitor orderingVisitor = new OrderingVisitor(); expression.accept(orderingVisitor); expression = orderingVisitor.getExpression(); - PropagationVisitor propagationVisitor = new PropagationVisitor(); - expression.accept(propagationVisitor); - Expression propagated = propagationVisitor.getExpression(); + //PropagationVisitor propagationVisitor = new PropagationVisitor(); + //expression.accept(propagationVisitor); + //Expression propagated = propagationVisitor.getExpression(); if (propagated != null) { - propagated = new Renamer(map, - propagationVisitor.getVariableSet()).rename(propagated); + //propagated = new Renamer(map, + // propagationVisitor.getVariableSet()).rename(propagated); } log.log(Level.FINEST, "After Propagation: " + propagated); - return propagated; + return expression; + //return propagated; } catch (VisitorException x) { log.log(Level.SEVERE, "encountered an exception -- this should not be happening!", From 58768a58a975bf52f95b22f36dfcb4ec197a7e79 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 17:53:19 +0200 Subject: [PATCH 37/66] Removed Redundent code and added print statement to check output --- .../service/simplify/ConstantPropagation.java | 526 +----------------- 1 file changed, 2 insertions(+), 524 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 453c842f..5722c9fb 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -127,6 +127,8 @@ public void postVisit(Operation operation) throws VisitorException { if (nop != null) { Expression r = stack.pop(); Expression l = stack.pop(); + System.out.println(l + " "+ nop + " " + r); + if ((r instanceof IntVariable) && (l instanceof IntVariable) && (((IntVariable) r).getName().compareTo( @@ -152,528 +154,4 @@ public void postVisit(Operation operation) throws VisitorException { } - private static class PropagationVisitor 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 PropagationVisitor() { - 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)); - } - - } - } From 1a7a40096148438bee40ecdf05c830ad897dc6f0 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 17:56:51 +0200 Subject: [PATCH 38/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 5722c9fb..c72ac0cd 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -61,10 +61,10 @@ public Expression propagate(Expression expression, //PropagationVisitor propagationVisitor = new PropagationVisitor(); //expression.accept(propagationVisitor); //Expression propagated = propagationVisitor.getExpression(); - if (propagated != null) { + //if (propagated != null) { //propagated = new Renamer(map, // propagationVisitor.getVariableSet()).rename(propagated); - } + //} log.log(Level.FINEST, "After Propagation: " + propagated); return expression; //return propagated; From 08cbf642212ec49ed67ada1fe76bf8909bf96923 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 18:12:43 +0200 Subject: [PATCH 39/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index c72ac0cd..4f8e2e34 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -65,7 +65,7 @@ public Expression propagate(Expression expression, //propagated = new Renamer(map, // propagationVisitor.getVariableSet()).rename(propagated); //} - log.log(Level.FINEST, "After Propagation: " + propagated); + log.log(Level.FINEST, "After Propagation: " + expression); return expression; //return propagated; } catch (VisitorException x) { From 9788f7ec495ad30c5d5641d4fa587872328f33ba Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 18:18:02 +0200 Subject: [PATCH 40/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 4f8e2e34..1b9394ba 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -127,7 +127,7 @@ public void postVisit(Operation operation) throws VisitorException { if (nop != null) { Expression r = stack.pop(); Expression l = stack.pop(); - System.out.println(l + " "+ nop + " " + r); + System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+l + " "+ nop + " " + r+"<<<<<<<<<<<<<<<<<<<<<); if ((r instanceof IntVariable) && (l instanceof IntVariable) From ec4db4d2844a9921c28f5d3c40875bce619616d3 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 18:22:21 +0200 Subject: [PATCH 41/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 1b9394ba..483139a4 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -127,7 +127,7 @@ public void postVisit(Operation operation) throws VisitorException { if (nop != null) { Expression r = stack.pop(); Expression l = stack.pop(); - System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+l + " "+ nop + " " + r+"<<<<<<<<<<<<<<<<<<<<<); + System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+l + " "+ nop + " " + r+"<<<<<<<<<<<<<<<<<<<<<"); if ((r instanceof IntVariable) && (l instanceof IntVariable) From 74bb9af72e5b40c419cc17c2dfb26eecf99a9d89 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 19:35:28 +0200 Subject: [PATCH 42/66] Update EntireSuite.java --- test/za/ac/sun/cs/green/EntireSuite.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java index d48bb8c9..8a66445c 100644 --- a/test/za/ac/sun/cs/green/EntireSuite.java +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -32,11 +32,13 @@ 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.util.ConstantPropagationTest; @RunWith(Suite.class) @Suite.SuiteClasses({ - SATCanonizerTest.class, - SATZ3Test.class + //SATCanonizerTest.class, + //SATZ3Test.class + ConstantPropagationTest.class }) public class EntireSuite { From efd32d33984812278960b0e6b627034531c7ad34 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 19:48:42 +0200 Subject: [PATCH 43/66] Update EntireSuite.java --- test/za/ac/sun/cs/green/EntireSuite.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java index 8a66445c..b084784c 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.util.ConstantPropagationTest; +import za.ac.sun.cs.green.service.simplify.ConstantPropagationTest; @RunWith(Suite.class) @Suite.SuiteClasses({ From b56d333e8893b63ec3d276ae133c1e271aedb200 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 20:31:08 +0200 Subject: [PATCH 44/66] Update ConstantPropagationTest.java --- .../sun/cs/green/service/simplify/ConstantPropagationTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java index e449e5b8..6dde24f1 100644 --- a/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java +++ b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java @@ -30,7 +30,7 @@ public static void initialize() { 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"); + "za.ac.sun.cs.green.service.simplify.ConstantPropagation"); //props.setProperty("green.service.sat.canonize", // "za.ac.sun.cs.green.service.canonizer.SATCanonizerService"); From 934d7cebb2c53d07f5e18c0c969c13154ee26cce Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:08:24 +0200 Subject: [PATCH 45/66] Update ConstantPropagation.java --- .../service/simplify/ConstantPropagation.java | 27 ++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 483139a4..db18ffaa 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -77,11 +77,13 @@ public Expression propagate(Expression expression, } private static class OrderingVisitor extends Visitor { - + + private Map map; private Stack stack; public OrderingVisitor() { stack = new Stack(); + map = new HashMap(); } public Expression getExpression() { @@ -101,7 +103,26 @@ public void postVisit(IntVariable variable) { @Override public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); - Operation.Operator nop = null; + if (stack.size() > 2) + if (op == EQ) { + Expression right = stack.pop(); + Expression left = stack.pop(); + if (left instanceOf IntVariable) { + if (map.containsKey(left)) { + left = map.get(left) + } + } + + if (right instanceOf IntVariable) { + if (map.containsKey(right)) { + right = map.get(right) + } + } + } + Operation nop = new Operation(operation.getOperator(), left, right); + stack.push(nop); + + /* Operation.Operator nop = null; switch (op) { case EQ: nop = Operation.Operator.EQ; @@ -149,7 +170,7 @@ public void postVisit(Operation operation) throws VisitorException { stack.pop(); } stack.push(operation); - } + }*/ } } From bf8ddf585b376a82149f57f9309e0eeb7da8e9ed Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:12:01 +0200 Subject: [PATCH 46/66] First attempt :) --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index db18ffaa..64f944c5 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -103,7 +103,7 @@ public void postVisit(IntVariable variable) { @Override public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); - if (stack.size() > 2) + if (stack.size() > 2) { if (op == EQ) { Expression right = stack.pop(); Expression left = stack.pop(); @@ -121,7 +121,7 @@ public void postVisit(Operation operation) throws VisitorException { } Operation nop = new Operation(operation.getOperator(), left, right); stack.push(nop); - + } /* Operation.Operator nop = null; switch (op) { case EQ: From cbc448b73aeece02543af103127b40df48af51d2 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:16:46 +0200 Subject: [PATCH 47/66] fixed few errors --- .../cs/green/service/simplify/ConstantPropagation.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 64f944c5..ae42dabc 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -107,15 +107,15 @@ public void postVisit(Operation operation) throws VisitorException { if (op == EQ) { Expression right = stack.pop(); Expression left = stack.pop(); - if (left instanceOf IntVariable) { + if (left instanceof IntVariable) { if (map.containsKey(left)) { - left = map.get(left) + left = map.get(left); } } - if (right instanceOf IntVariable) { + if (right instanceof IntVariable) { if (map.containsKey(right)) { - right = map.get(right) + right = map.get(right); } } } From 6ff87e1155580a32c7f23b6d478843f2941bbe09 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:33:58 +0200 Subject: [PATCH 48/66] Testing for constant assignment --- .../service/simplify/ConstantPropagation.java | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index ae42dabc..3a9b8310 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -104,23 +104,21 @@ public void postVisit(IntVariable variable) { public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); if (stack.size() > 2) { - if (op == EQ) { + if (op == Operation.Operator.EQ) { Expression right = stack.pop(); Expression left = stack.pop(); - if (left instanceof IntVariable) { + if (left instanceof IntConstant && right instanceof IntVariable) { + map.put((IntVariable) l, (IntConstant) r); if (map.containsKey(left)) { left = map.get(left); } } - if (right instanceof IntVariable) { - if (map.containsKey(right)) { - right = map.get(right); - } - } - } - Operation nop = new Operation(operation.getOperator(), left, right); - stack.push(nop); + Operation nop = new Operation(operation.getOperator(), left, right); + System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+left + " "+ nop + " " + right+"<<<<<<<<<<<<<<<<<<<<<"); + + stack.push(nop); + } } /* Operation.Operator nop = null; switch (op) { From 8106ff8e0d6354eb3ccaf425bc2603556964de33 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:37:19 +0200 Subject: [PATCH 49/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 3a9b8310..05591cf3 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -108,7 +108,7 @@ public void postVisit(Operation operation) throws VisitorException { Expression right = stack.pop(); Expression left = stack.pop(); if (left instanceof IntConstant && right instanceof IntVariable) { - map.put((IntVariable) l, (IntConstant) r); + map.put((IntVariable) left, (IntConstant) right); if (map.containsKey(left)) { left = map.get(left); } From d4c6d9c1792dfa82f3dca7341afc0a35aeb4b720 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:51:20 +0200 Subject: [PATCH 50/66] Update changes to include all expressions --- .../service/simplify/ConstantPropagation.java | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 05591cf3..d9c1a1bf 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -119,7 +119,23 @@ public void postVisit(Operation operation) throws VisitorException { stack.push(nop); } - } + } else if (left instanceof IntaVariable || right instanceof IntVariable) { + if (map.containsKey(left)) { + left = map.get(left); + } else if (map.containsKey) { + right = map.get(right); + } + Operation nop = new Operation(operation.getOperator(), left, right); + stack.push(nop); + } else { + Operation nop = new Operation(operation.getOperator(), left, right); + stack.push(nop); + } + } else { + for (int i = op.getArity(); i > 0; i--) { + stack.pop(); + } + stack.push(operation); /* Operation.Operator nop = null; switch (op) { case EQ: From 27d7396b1272ee96c7ecc8bf4f1ca1fc18002a97 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 21:57:26 +0200 Subject: [PATCH 51/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index d9c1a1bf..f88bc4b1 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -118,8 +118,7 @@ public void postVisit(Operation operation) throws VisitorException { System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+left + " "+ nop + " " + right+"<<<<<<<<<<<<<<<<<<<<<"); stack.push(nop); - } - } else if (left instanceof IntaVariable || right instanceof IntVariable) { + } else if (left instanceof IntaVariable || right instanceof IntVariable) { if (map.containsKey(left)) { left = map.get(left); } else if (map.containsKey) { From 0c315b89464d404995b2d7f9e59d869c4a5e3ff8 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:01:27 +0200 Subject: [PATCH 52/66] Update ConstantPropagation.java --- src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index f88bc4b1..7a45c39d 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -135,6 +135,7 @@ public void postVisit(Operation operation) throws VisitorException { stack.pop(); } stack.push(operation); + } /* Operation.Operator nop = null; switch (op) { case EQ: From 2482a4bfc5c1063e1208107d0515699c48c70efe Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:05:11 +0200 Subject: [PATCH 53/66] Update ConstantPropagation.java --- .../sun/cs/green/service/simplify/ConstantPropagation.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 7a45c39d..25669fb9 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -104,9 +104,10 @@ public void postVisit(IntVariable variable) { public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); if (stack.size() > 2) { + Expression right = stack.pop(); + Expression left = stack.pop(); if (op == Operation.Operator.EQ) { - Expression right = stack.pop(); - Expression left = stack.pop(); + if (left instanceof IntConstant && right instanceof IntVariable) { map.put((IntVariable) left, (IntConstant) right); if (map.containsKey(left)) { From 9b53157510528efe5e7ecc40f743370c36c61200 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:09:22 +0200 Subject: [PATCH 54/66] Fixed some more erros --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 25669fb9..c0fd4013 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -119,10 +119,10 @@ public void postVisit(Operation operation) throws VisitorException { System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+left + " "+ nop + " " + right+"<<<<<<<<<<<<<<<<<<<<<"); stack.push(nop); - } else if (left instanceof IntaVariable || right instanceof IntVariable) { + } else if (left instanceof IntVariable || right instanceof IntVariable) { if (map.containsKey(left)) { left = map.get(left); - } else if (map.containsKey) { + } else if (map.containsKey(right)) { right = map.get(right); } Operation nop = new Operation(operation.getOperator(), left, right); From 9629484a36f32c4f2b2fb1f4268e8abf87f82d34 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:13:33 +0200 Subject: [PATCH 55/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index c0fd4013..7d134b2d 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -103,7 +103,7 @@ public void postVisit(IntVariable variable) { @Override public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); - if (stack.size() > 2) { + if (stack.size() >= 2) { Expression right = stack.pop(); Expression left = stack.pop(); if (op == Operation.Operator.EQ) { From 14f7b0df9e66bac5c83387a8a375d7dafeb64731 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:19:28 +0200 Subject: [PATCH 56/66] Update ConstantPropagation.java --- .../sun/cs/green/service/simplify/ConstantPropagation.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 7d134b2d..087c50b6 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -110,9 +110,8 @@ public void postVisit(Operation operation) throws VisitorException { if (left instanceof IntConstant && right instanceof IntVariable) { map.put((IntVariable) left, (IntConstant) right); - if (map.containsKey(left)) { - left = map.get(left); - } + } else if (right instanceof IntConstant && left instanceof IntVariable) { + map.put((IntVariable) right, (IntConstant) left); } Operation nop = new Operation(operation.getOperator(), left, right); From f805c9b841c7e6a027cbdbff25a32e2202951008 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:27:45 +0200 Subject: [PATCH 57/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 087c50b6..d579efc7 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -109,9 +109,9 @@ public void postVisit(Operation operation) throws VisitorException { if (op == Operation.Operator.EQ) { if (left instanceof IntConstant && right instanceof IntVariable) { - map.put((IntVariable) left, (IntConstant) right); - } else if (right instanceof IntConstant && left instanceof IntVariable) { map.put((IntVariable) right, (IntConstant) left); + } else if (right instanceof IntConstant && left instanceof IntVariable) { + map.put((IntVariable) left, (IntConstant) right); } Operation nop = new Operation(operation.getOperator(), left, right); From a05c0c752206b2721848db3fd14f2b3a830bee4c Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:31:03 +0200 Subject: [PATCH 58/66] Update ConstantPropagation.java --- .../service/simplify/ConstantPropagation.java | 55 +------------------ 1 file changed, 1 insertion(+), 54 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index d579efc7..c9cd1959 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -108,9 +108,7 @@ public void postVisit(Operation operation) throws VisitorException { Expression left = stack.pop(); if (op == Operation.Operator.EQ) { - if (left instanceof IntConstant && right instanceof IntVariable) { - map.put((IntVariable) right, (IntConstant) left); - } else if (right instanceof IntConstant && left instanceof IntVariable) { + if (right instanceof IntConstant && left instanceof IntVariable) { map.put((IntVariable) left, (IntConstant) right); } @@ -136,57 +134,6 @@ public void postVisit(Operation operation) throws VisitorException { } stack.push(operation); } - /* 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(); - System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+l + " "+ nop + " " + r+"<<<<<<<<<<<<<<<<<<<<<"); - - 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); - }*/ } - } - } From ea56d3e5cbcc88a02cf4c4e9bec01ef8c33c87a5 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:37:31 +0200 Subject: [PATCH 59/66] Update ConstantPropagation.java --- .../service/simplify/ConstantPropagation.java | 31 +++++++++---------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index c9cd1959..b4b77b01 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -30,7 +30,10 @@ public class ConstantPropagation extends BasicService { public ConstantPropagation(Green solver) { super(solver); } - + + /** + * Taken from SATCanonizerService.java + */ @Override public Set processRequest(Instance instance) { @SuppressWarnings("unchecked") @@ -44,7 +47,10 @@ public Set processRequest(Instance instance) { } return result; } - + + /** + * Taken from SATCanonizerService.java + */ @Override public void report(Reporter reporter) { reporter.report(getClass().getSimpleName(), "invocations = " + invocations); @@ -78,12 +84,12 @@ public Expression propagate(Expression expression, private static class OrderingVisitor extends Visitor { - private Map map; + private Map hashmap; private Stack stack; public OrderingVisitor() { stack = new Stack(); - map = new HashMap(); + hashmap = new HashMap(); } public Expression getExpression() { @@ -109,18 +115,16 @@ public void postVisit(Operation operation) throws VisitorException { if (op == Operation.Operator.EQ) { if (right instanceof IntConstant && left instanceof IntVariable) { - map.put((IntVariable) left, (IntConstant) right); + hashmap.put((IntVariable) left, (IntConstant) right); } Operation nop = new Operation(operation.getOperator(), left, right); - System.out.println(">>>>>>>>>>>>>>>>>>>>>>"+left + " "+ nop + " " + right+"<<<<<<<<<<<<<<<<<<<<<"); - stack.push(nop); } else if (left instanceof IntVariable || right instanceof IntVariable) { - if (map.containsKey(left)) { - left = map.get(left); + if (hashmap.containsKey(left)) { + left = hashmap.get(left); } else if (map.containsKey(right)) { - right = map.get(right); + right = hashmap.get(right); } Operation nop = new Operation(operation.getOperator(), left, right); stack.push(nop); @@ -128,12 +132,7 @@ public void postVisit(Operation operation) throws VisitorException { Operation nop = new Operation(operation.getOperator(), left, right); stack.push(nop); } - } else { - for (int i = op.getArity(); i > 0; i--) { - stack.pop(); - } - stack.push(operation); - } + } } } } From 942a3b12c826a8fdb3e317da70c86161c23bc5f9 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 22:40:50 +0200 Subject: [PATCH 60/66] Fixed errors --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index b4b77b01..9d9e3b78 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -123,7 +123,7 @@ public void postVisit(Operation operation) throws VisitorException { } else if (left instanceof IntVariable || right instanceof IntVariable) { if (hashmap.containsKey(left)) { left = hashmap.get(left); - } else if (map.containsKey(right)) { + } else if (hashmap.containsKey(right)) { right = hashmap.get(right); } Operation nop = new Operation(operation.getOperator(), left, right); From 9c56978d4f5daa1f2e7a3c34d6dfdc3c4eba2800 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 23:05:16 +0200 Subject: [PATCH 61/66] Added comments --- .../service/simplify/ConstantPropagation.java | 33 +++++++++---------- 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 9d9e3b78..1843d211 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -55,25 +55,19 @@ public Set processRequest(Instance instance) { public void report(Reporter reporter) { reporter.report(getClass().getSimpleName(), "invocations = " + invocations); } - - public Expression propagate(Expression expression, - Map map) { + + /** + * Based off of the same method in SATCanonizerService.java + */ + public Expression propagate(Expression expression) { try { log.log(Level.FINEST, "Before Propagation: " + expression); invocations++; OrderingVisitor orderingVisitor = new OrderingVisitor(); expression.accept(orderingVisitor); expression = orderingVisitor.getExpression(); - //PropagationVisitor propagationVisitor = new PropagationVisitor(); - //expression.accept(propagationVisitor); - //Expression propagated = propagationVisitor.getExpression(); - //if (propagated != null) { - //propagated = new Renamer(map, - // propagationVisitor.getVariableSet()).rename(propagated); - //} log.log(Level.FINEST, "After Propagation: " + expression); return expression; - //return propagated; } catch (VisitorException x) { log.log(Level.SEVERE, "encountered an exception -- this should not be happening!", @@ -89,7 +83,7 @@ private static class OrderingVisitor extends Visitor { public OrderingVisitor() { stack = new Stack(); - hashmap = new HashMap(); + hashmap = new HashMap(); //Added a hash map to store constants propagated to variables } public Expression getExpression() { @@ -110,17 +104,20 @@ public void postVisit(IntVariable variable) { public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); if (stack.size() >= 2) { - Expression right = stack.pop(); - Expression left = stack.pop(); - if (op == Operation.Operator.EQ) { - - if (right instanceof IntConstant && left instanceof IntVariable) { + Expression right = stack.pop(); //gets right value of operator (variable to which will be assigned) + Expression left = stack.pop(); //gets left value of operator (constant to assign) + if (op == Operation.Operator.EQ) { //checks for == + //if there is a variable to the right of the operator and an integer integer to the left + //then assign the integer value to a key corresponding to the variable + if (right instanceof IntConstant && left instanceof IntVariable) { hashmap.put((IntVariable) left, (IntConstant) right); } - + //form the new operation and push it to the stack Operation nop = new Operation(operation.getOperator(), left, right); stack.push(nop); } else if (left instanceof IntVariable || right instanceof IntVariable) { + // If the the current expression is not of the type above create a new expression and add + // it to the hashmap if (hashmap.containsKey(left)) { left = hashmap.get(left); } else if (hashmap.containsKey(right)) { From 8244804a344ee7300e789fe0da2449707fc0a7a5 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 23:14:08 +0200 Subject: [PATCH 62/66] Update ConstantPropagation.java --- .../green/service/simplify/ConstantPropagation.java | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 1843d211..a575fc96 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -115,9 +115,9 @@ public void postVisit(Operation operation) throws VisitorException { //form the new operation and push it to the stack Operation nop = new Operation(operation.getOperator(), left, right); stack.push(nop); - } else if (left instanceof IntVariable || right instanceof IntVariable) { - // If the the current expression is not of the type above create a new expression and add - // it to the hashmap + } else { + // If the the current expression is not of the type above create a new expression and push + // it to the stack if (hashmap.containsKey(left)) { left = hashmap.get(left); } else if (hashmap.containsKey(right)) { @@ -125,10 +125,7 @@ public void postVisit(Operation operation) throws VisitorException { } Operation nop = new Operation(operation.getOperator(), left, right); stack.push(nop); - } else { - Operation nop = new Operation(operation.getOperator(), left, right); - stack.push(nop); - } + } } } } From db3e57b9c694f9339a79ef41cc86f3a66e9d9c24 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 23:16:00 +0200 Subject: [PATCH 63/66] Update ConstantPropagation.java --- .../ac/sun/cs/green/service/simplify/ConstantPropagation.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index a575fc96..07d949af 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -35,7 +35,8 @@ public ConstantPropagation(Green solver) { * Taken from SATCanonizerService.java */ @Override - public Set processRequest(Instance instance) { + public Set processRequest(Instance instance, + HashMap map) { @SuppressWarnings("unchecked") Set result = (Set) instance.getData(getClass()); if (result == null) { From 7cd261b4de0a9fa16e9ab4067c84a5539576ba43 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Mon, 13 Aug 2018 23:21:02 +0200 Subject: [PATCH 64/66] Update ConstantPropagation.java --- .../sun/cs/green/service/simplify/ConstantPropagation.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 07d949af..64ffa307 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -35,8 +35,7 @@ public ConstantPropagation(Green solver) { * Taken from SATCanonizerService.java */ @Override - public Set processRequest(Instance instance, - HashMap map) { + public Set processRequest(Instance instance) { @SuppressWarnings("unchecked") Set result = (Set) instance.getData(getClass()); if (result == null) { @@ -60,7 +59,8 @@ public void report(Reporter reporter) { /** * Based off of the same method in SATCanonizerService.java */ - public Expression propagate(Expression expression) { + public Expression propagate(Expression expression, + Map map) { try { log.log(Level.FINEST, "Before Propagation: " + expression); invocations++; From 80dc5f4baa7dd7fb786282ad8c457175bf4d47b9 Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 14 Aug 2018 09:38:27 +0200 Subject: [PATCH 65/66] Create SimplificationConstantPropogationTest.java --- ...SimplificationConstantPropogationTest.java | 186 ++++++++++++++++++ 1 file changed, 186 insertions(+) create mode 100644 test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java diff --git a/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java new file mode 100644 index 00000000..c7995ac6 --- /dev/null +++ b/test/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 527a9cfc507b81d47b1a4ce47192db33ddb130bb Mon Sep 17 00:00:00 2001 From: Bernard Wiesner <38321866+wiesnerbernard@users.noreply.github.com> Date: Tue, 14 Aug 2018 10:15:08 +0200 Subject: [PATCH 66/66] Updated commenting --- .../service/simplify/ConstantPropagation.java | 21 ++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java index 64ffa307..583aa77f 100644 --- a/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -58,6 +58,9 @@ public void report(Reporter reporter) { /** * Based off of the same method in SATCanonizerService.java + * @param expression: expression to propagate + * map: hashmap of variables + * @return updated expression */ public Expression propagate(Expression expression, Map map) { @@ -76,7 +79,10 @@ public Expression propagate(Expression expression, } return null; } - + + /** + * Class to handle propagation of constants + */ private static class OrderingVisitor extends Visitor { private Map hashmap; @@ -100,14 +106,19 @@ public void postVisit(IntConstant constant) { public void postVisit(IntVariable variable) { stack.push(variable); } - + + /** + * This method propagates a constant through the expression, replacing all instances of a certain variable + * with a constant value. + * @param operation: the current operator that must be handled + */ @Override public void postVisit(Operation operation) throws VisitorException { Operation.Operator op = operation.getOperator(); if (stack.size() >= 2) { - Expression right = stack.pop(); //gets right value of operator (variable to which will be assigned) - Expression left = stack.pop(); //gets left value of operator (constant to assign) - if (op == Operation.Operator.EQ) { //checks for == + Expression right = stack.pop(); + Expression left = stack.pop(); + if (op == Operation.Operator.EQ) { //checks for '==' //if there is a variable to the right of the operator and an integer integer to the left //then assign the integer value to a key corresponding to the variable if (right instanceof IntConstant && left instanceof IntVariable) {