diff --git a/green/.classpath b/.classpath similarity index 91% rename from green/.classpath rename to .classpath index 6be54f10..02791d30 100644 --- a/green/.classpath +++ b/.classpath @@ -2,15 +2,15 @@ - - - - - - - + + + + + + + diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..81f26b6c --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +/bin/ +.classpath +.project + diff --git a/green/.project b/.project similarity index 95% rename from green/.project rename to .project index f4ea30c4..df575bd9 100644 --- a/green/.project +++ b/.project @@ -1,17 +1,17 @@ - - - green - - - - - - org.eclipse.jdt.core.javabuilder - - - - - - org.eclipse.jdt.core.javanature - - + + + green + + + + + + org.eclipse.jdt.core.javabuilder + + + + + + org.eclipse.jdt.core.javanature + + diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 00000000..df9d4762 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,14 @@ + +sudo: required + +language: java + +services: + - docker + + +before_install: + - docker build -t green . + +script: + - docker run green /bin/sh -c "ant;ant test -v" \ No newline at end of file diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 00000000..c9231b3c --- /dev/null +++ b/Dockerfile @@ -0,0 +1,37 @@ +FROM openjdk:8 + +MAINTAINER Phillip van Heerden + +# Update the system +RUN apt update -y +RUN apt upgrade -y + +# Install ant, libgomp1 (GCC OpenMP support library), vim, patchelf, and tmux. +# These should be available on the NARGA machines. +RUN apt install ant -y +RUN apt install vim -y +RUN apt install tmux -y +RUN apt install patchelf -y +RUN apt install libgomp1 + +# Clone down the GreenSolver repository +RUN git clone https://github.com/FloraJuliane/green + +# Download and extract Z3 +RUN mkdir z3 +WORKDIR z3 +RUN wget https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-ubuntu-16.04.zip +RUN unzip z3-4.7.1-x64-ubuntu-16.04.zip + +# Fix the link time error with libz3java.so +WORKDIR /z3/z3-4.7.1-x64-ubuntu-16.04/bin +RUN patchelf --set-rpath '.:$ORIGIN' libz3java.so + +# Make the z3 path a bit easier for sed +WORKDIR /z3/ +RUN mv z3-4.7.1-x64-ubuntu-16.04/ z3/ + +# Update the build.properties file with the new z3 paths +WORKDIR /green/ +RUN sed -i '16s/.*/z3path = \/z3\/z3\/bin\/z3/' build.properties +RUN sed -i '17s/.*/z3lib = \/z3\/z3\/bin/' build.properties diff --git a/README.md b/README.md new file mode 100644 index 00000000..898a3d0c --- /dev/null +++ b/README.md @@ -0,0 +1,8 @@ +[![Build Status](https://travis-ci.org/FloraJuliane/green.svg?branch=master)](https://travis-ci.org/FloraJuliane/green.svg?branch=master) + +Notes: + +The first step is to update "build.properties" with your local +settings. You do not need to set z3 and latte, but in that case +some unit tests won't run. + diff --git a/green/build.properties b/build.properties similarity index 100% rename from green/build.properties rename to build.properties diff --git a/green/build.xml b/build.xml similarity index 96% rename from green/build.xml rename to build.xml index 0c29bed8..aa146fe6 100644 --- a/green/build.xml +++ b/build.xml @@ -95,8 +95,8 @@ - - + + diff --git a/green/.travis.yml b/green/.travis.yml deleted file mode 100644 index 97f7ae1d..00000000 --- a/green/.travis.yml +++ /dev/null @@ -1,2 +0,0 @@ -language: java -script: ant build diff --git a/green/README.txt b/green/README.txt deleted file mode 100644 index 9ef36125..00000000 --- a/green/README.txt +++ /dev/null @@ -1,10 +0,0 @@ -====================================================================== -Green -====================================================================== - -Notes: - -(1) The first step is to update "build.properties" with your local - settings. You do not need to set z3 and latte, but in that case - some unit tests won't run. - \ No newline at end of file diff --git a/greenserver/.classpath b/greenserver/.classpath deleted file mode 100644 index f9faca31..00000000 --- a/greenserver/.classpath +++ /dev/null @@ -1,8 +0,0 @@ - - - - - - - - diff --git a/greenserver/.project b/greenserver/.project deleted file mode 100644 index e2b4dbca..00000000 --- a/greenserver/.project +++ /dev/null @@ -1,17 +0,0 @@ - - - greenserver - - - - - - org.eclipse.jdt.core.javabuilder - - - - - - org.eclipse.jdt.core.javanature - - diff --git a/greenserver/.settings/org.eclipse.jdt.core.prefs b/greenserver/.settings/org.eclipse.jdt.core.prefs deleted file mode 100644 index 8000cd6c..00000000 --- a/greenserver/.settings/org.eclipse.jdt.core.prefs +++ /dev/null @@ -1,11 +0,0 @@ -eclipse.preferences.version=1 -org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled -org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.6 -org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve -org.eclipse.jdt.core.compiler.compliance=1.6 -org.eclipse.jdt.core.compiler.debug.lineNumber=generate -org.eclipse.jdt.core.compiler.debug.localVariable=generate -org.eclipse.jdt.core.compiler.debug.sourceFile=generate -org.eclipse.jdt.core.compiler.problem.assertIdentifier=error -org.eclipse.jdt.core.compiler.problem.enumIdentifier=error -org.eclipse.jdt.core.compiler.source=1.6 diff --git a/greenserver/C/client/Makefile b/greenserver/C/client/Makefile deleted file mode 100644 index 5fb89163..00000000 --- a/greenserver/C/client/Makefile +++ /dev/null @@ -1,61 +0,0 @@ -#=============================================================================== -# Makefile -#=============================================================================== - -#------------------------------------------------------------------------------- -# We start with the configuration file. -#------------------------------------------------------------------------------- - -CC = gcc -LD = gcc -CFLAGS = -O3 -W -Wall -LDFLAGS = - -#------------------------------------------------------------------------------- -# Main target -#------------------------------------------------------------------------------- - -PROGS = testgreen testgreenklee quitgreen - -all : $(PROGS) - -#------------------------------------------------------------------------------- -# High-level rules -#------------------------------------------------------------------------------- - -testgreen : testgreen.o green.o - -testgreen.o : testgreen.c - -testgreenklee : testgreenklee.o green.o - -testgreenklee.o : testgreenklee.c - -quitgreen : quitgreen.o green.o - -quitgreen.o : quitgreen.c - -green.o : green.c green.h - -#------------------------------------------------------------------------------- -# Low-level rules -#------------------------------------------------------------------------------- - -% : %.o - $(LD) $(LDFLAGS) $^ -o $@ - -%.o : %.c - $(CC) $(CFLAGS) -c $< -o $@ - - - -#------------------------------------------------------------------------------- -# Cleaning up. -#------------------------------------------------------------------------------- - -clean : - rm -f core *.o $(PROGS) - -#=============================================================================== -# End of Makefile -#=============================================================================== diff --git a/greenserver/C/client/green.c b/greenserver/C/client/green.c deleted file mode 100644 index a4b0e7be..00000000 --- a/greenserver/C/client/green.c +++ /dev/null @@ -1,93 +0,0 @@ -/*------------------------------------------------------------------------------ - * green.c - * - * Client for the GreenServer running in Java. - * Jaco Geldenhuys - * 6 June 2013 - *----------------------------------------------------------------------------*/ - -#include -#include -#include -#include -#include -#include -#include "green.h" - -/** - * The size of the query result buffer. - */ - -#define GREEN_BUFSIZE (32) - -/** - * The socket connection to the server. - */ - -int green_socket; - -/** - * Error reporting routine. - */ - -void report_and_die(char* message) { - fprintf(stderr, "ERROR: %s\n", message); - exit(-1); -} - -/** - * Initialize the Green client. This amounts to connecting to the server. If - * the parameter is the server port. For now we assume that the server is - * running on the local machine, but this might change in the future. - */ - -void green_initialize(int port) { - struct sockaddr_in server; /* Green server address */ - - /* Create a reliable, stream socket using TCP */ - if ((green_socket = socket(PF_INET, SOCK_STREAM, IPPROTO_TCP)) < 0) { - report_and_die("socket() failed"); - } - - /* Construct the server address structure */ - memset(&server, 0, sizeof(server)); /* Zero out structure */ - server.sin_family = AF_INET; /* Internet address family */ - server.sin_addr.s_addr = inet_addr("127.0.0.1"); /* Server IP address */ - server.sin_port = htons(port); /* Server port */ - - /* Establish the connection to the echo server */ - if (connect(green_socket, (struct sockaddr *) &server, sizeof(server)) < 0) { - report_and_die("connect() failed"); - } -} - -void green_shutdown() { - if (send(green_socket, "CLOSE\n", 5, 0) != 5) { - // do nothing - } - close(green_socket); - exit(0); -} - -int green_issat(char* query) { - int query_len; - int bytes_rcvd; - char buf[GREEN_BUFSIZE]; - - query_len = strlen(query); - - if (send(green_socket, query, query_len, 0) != query_len) { - report_and_die("send() sent a different number of bytes than expected"); - } - - if ((bytes_rcvd = recv(green_socket, buf, GREEN_BUFSIZE - 1, 0)) <= 0) { - report_and_die("recv() failed or connection closed prematurely"); - } - - return (buf[0] != '0'); -} - -/*------------------------------------------------------------------------------ - * End of green.c - *----------------------------------------------------------------------------*/ - diff --git a/greenserver/C/client/green.h b/greenserver/C/client/green.h deleted file mode 100644 index edb31afe..00000000 --- a/greenserver/C/client/green.h +++ /dev/null @@ -1,22 +0,0 @@ -/*------------------------------------------------------------------------------ - * green.h - * - * C header file for the GreenServer client. - * Jaco Geldenhuys - * 6 June 2013 - *----------------------------------------------------------------------------*/ - -#ifndef GREEN_H -#define GREEN_H - -void green_initialize(); -void green_shutdown(); - -int green_issat(char* query); - -#endif - -/*------------------------------------------------------------------------------ - * End of green.h - *----------------------------------------------------------------------------*/ - diff --git a/greenserver/C/client/quitgreen.c b/greenserver/C/client/quitgreen.c deleted file mode 100644 index 8d379bf1..00000000 --- a/greenserver/C/client/quitgreen.c +++ /dev/null @@ -1,22 +0,0 @@ -/*------------------------------------------------------------------------------ - * quitgreen.c - * - * Tell the Green server to shut down. - * Jaco Geldenhuys - * 6 June 2013 - *----------------------------------------------------------------------------*/ - -#include -#include "green.h" - -int main() { - green_initialize(9408); - green_issat("QUIT\n"); - green_shutdown(); - return 0; -} - -/*------------------------------------------------------------------------------ - * End of quitgreen.c - *----------------------------------------------------------------------------*/ - diff --git a/greenserver/C/client/testgreen.c b/greenserver/C/client/testgreen.c deleted file mode 100644 index 1875e63c..00000000 --- a/greenserver/C/client/testgreen.c +++ /dev/null @@ -1,28 +0,0 @@ -/*------------------------------------------------------------------------------ - * testgreen.c - * - * Test program for the Green client. - * Jaco Geldenhuys - * 6 June 2013 - *----------------------------------------------------------------------------*/ - -#include -#include "green.h" - -void issat(char* query) { - int answer = green_issat(query); - printf("QUERY: \"%s\"\nANSWER: %d\n\n", query, answer); -} - -int main() { - green_initialize(9408); - issat("piet\n"); - issat("pompies\n"); - green_shutdown(); - return 0; -} - -/*------------------------------------------------------------------------------ - * End of testgreen.c - *----------------------------------------------------------------------------*/ - diff --git a/greenserver/C/client/testgreenklee.c b/greenserver/C/client/testgreenklee.c deleted file mode 100644 index e4ecc031..00000000 --- a/greenserver/C/client/testgreenklee.c +++ /dev/null @@ -1,29 +0,0 @@ -/*------------------------------------------------------------------------------ - * testgreenklee.c - * - * Test program for the Green client with actual Klee constraints. - * Jaco Geldenhuys - * 6 June 2013 - *----------------------------------------------------------------------------*/ - -#include -#include "green.h" - -void issat(char* query) { - int answer = green_issat(query); - printf("QUERY: \"%s\"\nANSWER: %d\n\n", query, answer); -} - -int main() { - green_initialize(9408); - issat("array a[4] : w32 -> w8 = symbolic (query [(Eq false (Eq 0 N0:(ReadLSB w32 0 a))) (Eq false (Slt N0 0))] false)\n"); - issat("array a[4] : w32 -> w8 = symbolic (query [(Eq false (Eq 0 N0:(ReadLSB w32 0 a))) (Slt N0 0)] false)\n"); - issat("array a[4] : w32 -> w8 = symbolic (query [(Eq 0 (ReadLSB w32 0 a))] false)\n"); - green_shutdown(); - return 0; -} - -/*------------------------------------------------------------------------------ - * End of testgreenklee.c - *----------------------------------------------------------------------------*/ - diff --git a/greenserver/build.xml b/greenserver/build.xml deleted file mode 100644 index 7b4eddac..00000000 --- a/greenserver/build.xml +++ /dev/null @@ -1,117 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/greenserver/lib/green.jar b/greenserver/lib/green.jar deleted file mode 100644 index 599edfdf..00000000 Binary files a/greenserver/lib/green.jar and /dev/null differ diff --git a/greenserver/src/za/ac/sun/cs/green/server/GreenServer.java b/greenserver/src/za/ac/sun/cs/green/server/GreenServer.java deleted file mode 100644 index 63ca0cd5..00000000 --- a/greenserver/src/za/ac/sun/cs/green/server/GreenServer.java +++ /dev/null @@ -1,110 +0,0 @@ -package za.ac.sun.cs.green.server; - -import java.io.BufferedReader; -import java.io.IOException; -import java.io.InputStreamReader; -import java.io.PrintStream; -import java.net.ServerSocket; -import java.net.Socket; -import java.util.logging.Level; -import java.util.logging.Logger; - -import za.ac.sun.cs.green.Green; -import za.ac.sun.cs.green.Instance; - -public class GreenServer { - - private static Green green = null; - - private static Logger log = null; - - public static void main(String[] args) { - green = new Green("greenserver"); - log = green.getLog(); - ServerSocket serverSocket = null; - Socket clientSocket = null; - BufferedReader input = null; - PrintStream output = null; - try { - serverSocket = new ServerSocket(9408); - boolean isRunning = true; - while (isRunning) { - log.info("Waiting for a client to connect..."); - clientSocket = serverSocket.accept(); - log.info("Connected: " + clientSocket.getInetAddress() + ":" + clientSocket.getLocalPort()); - input = new BufferedReader(new InputStreamReader(clientSocket.getInputStream())); - output = new PrintStream(clientSocket.getOutputStream()); - while (clientSocket.isConnected()) { - String query = input.readLine(); - if ((query == null) || query.equals("QUIT")) { - isRunning = false; - log.info("Closing the client connection and shutting down"); - output.print("OK"); - output.close(); - try { - input.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "input.close() failed", x); - } - try { - clientSocket.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "clientSocket.close() failed", x); - } - break; - } - if (query.equals("CLOSE")) { - log.info("Closing the client connection"); - output.print("OK"); - output.close(); - try { - input.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "input.close() failed", x); - } - try { - clientSocket.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "clientSocket.close() failed", x); - } - break; - } - output.print(process(query)); - } - } - } catch (IOException x) { - log.log(Level.SEVERE, x.getMessage(), x); -// } catch (KleeParseException x) { -// log.log(Level.SEVERE, x.getMessage(), x); - } finally { - output.close(); - try { - input.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "input.close() failed", x); - } - try { - clientSocket.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "clientSocket.close() failed", x); - } - try { - serverSocket.close(); - } catch (IOException x) { - log.log(Level.SEVERE, "serverSocket.close() failed", x); - } - } - } - - private static char[] process(String query) { - log.info("QUERY: " + query); - Instance i = new Instance(green, null, /* TODO CHANGE! */null); - Boolean r = (Boolean) i.request("sat"); - if ((r != null) && r) { - return new char[] { '1' }; - } else { - return new char[] { '0' }; - } - } - -} diff --git a/green/lib/apfloat.jar b/lib/apfloat.jar similarity index 100% rename from green/lib/apfloat.jar rename to lib/apfloat.jar diff --git a/green/lib/choco-solver-2.1.3.jar b/lib/choco-solver-2.1.3.jar similarity index 100% rename from green/lib/choco-solver-2.1.3.jar rename to lib/choco-solver-2.1.3.jar diff --git a/green/lib/choco-solver-3.3.1.jar b/lib/choco-solver-3.3.1.jar similarity index 100% rename from green/lib/choco-solver-3.3.1.jar rename to lib/choco-solver-3.3.1.jar diff --git a/green/lib/com.microsoft.z3.jar b/lib/com.microsoft.z3.jar similarity index 100% rename from green/lib/com.microsoft.z3.jar rename to lib/com.microsoft.z3.jar diff --git a/green/lib/com.microsoft.z3.jar0 b/lib/com.microsoft.z3.jar0 similarity index 100% rename from green/lib/com.microsoft.z3.jar0 rename to lib/com.microsoft.z3.jar0 diff --git a/green/lib/commons-exec-1.2.jar b/lib/commons-exec-1.2.jar similarity index 100% rename from green/lib/commons-exec-1.2.jar rename to lib/commons-exec-1.2.jar diff --git a/green/lib/jedis-2.0.0.jar b/lib/jedis-2.0.0.jar similarity index 100% rename from green/lib/jedis-2.0.0.jar rename to lib/jedis-2.0.0.jar diff --git a/green/lib/junit_4.8.2.jar b/lib/junit_4.8.2.jar similarity index 100% rename from green/lib/junit_4.8.2.jar rename to lib/junit_4.8.2.jar diff --git a/green/lib/libcvc3.jar b/lib/libcvc3.jar similarity index 100% rename from green/lib/libcvc3.jar rename to lib/libcvc3.jar diff --git a/green/lib/libz3.dylib b/lib/libz3.dylib similarity index 100% rename from green/lib/libz3.dylib rename to lib/libz3.dylib diff --git a/green/lib/libz3java.dylib b/lib/libz3java.dylib similarity index 100% rename from green/lib/libz3java.dylib rename to lib/libz3java.dylib diff --git a/green/lib/org.hamcrest.core_1.1.0.jar b/lib/org.hamcrest.core_1.1.0.jar similarity index 100% rename from green/lib/org.hamcrest.core_1.1.0.jar rename to lib/org.hamcrest.core_1.1.0.jar diff --git a/green/lib/slf4j-api-1.7.12.jar b/lib/slf4j-api-1.7.12.jar similarity index 100% rename from green/lib/slf4j-api-1.7.12.jar rename to lib/slf4j-api-1.7.12.jar diff --git a/green/lib/slf4j-simple-1.7.12.jar b/lib/slf4j-simple-1.7.12.jar similarity index 100% rename from green/lib/slf4j-simple-1.7.12.jar rename to lib/slf4j-simple-1.7.12.jar diff --git a/green/lib/trove-3.1a1.jar b/lib/trove-3.1a1.jar similarity index 100% rename from green/lib/trove-3.1a1.jar rename to lib/trove-3.1a1.jar diff --git a/green/src/za/ac/sun/cs/green/Green.java b/src/za/ac/sun/cs/green/Green.java similarity index 100% rename from green/src/za/ac/sun/cs/green/Green.java rename to src/za/ac/sun/cs/green/Green.java diff --git a/green/src/za/ac/sun/cs/green/Instance.java b/src/za/ac/sun/cs/green/Instance.java similarity index 100% rename from green/src/za/ac/sun/cs/green/Instance.java rename to src/za/ac/sun/cs/green/Instance.java diff --git a/green/src/za/ac/sun/cs/green/Service.java b/src/za/ac/sun/cs/green/Service.java similarity index 100% rename from green/src/za/ac/sun/cs/green/Service.java rename to src/za/ac/sun/cs/green/Service.java diff --git a/green/src/za/ac/sun/cs/green/expr/Constant.java b/src/za/ac/sun/cs/green/expr/Constant.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/Constant.java rename to src/za/ac/sun/cs/green/expr/Constant.java diff --git a/green/src/za/ac/sun/cs/green/expr/Expression.java b/src/za/ac/sun/cs/green/expr/Expression.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/Expression.java rename to src/za/ac/sun/cs/green/expr/Expression.java diff --git a/green/src/za/ac/sun/cs/green/expr/IntConstant.java b/src/za/ac/sun/cs/green/expr/IntConstant.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/IntConstant.java rename to src/za/ac/sun/cs/green/expr/IntConstant.java diff --git a/green/src/za/ac/sun/cs/green/expr/IntVariable.java b/src/za/ac/sun/cs/green/expr/IntVariable.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/IntVariable.java rename to src/za/ac/sun/cs/green/expr/IntVariable.java diff --git a/green/src/za/ac/sun/cs/green/expr/Operation.java b/src/za/ac/sun/cs/green/expr/Operation.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/Operation.java rename to src/za/ac/sun/cs/green/expr/Operation.java diff --git a/green/src/za/ac/sun/cs/green/expr/RealConstant.java b/src/za/ac/sun/cs/green/expr/RealConstant.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/RealConstant.java rename to src/za/ac/sun/cs/green/expr/RealConstant.java diff --git a/green/src/za/ac/sun/cs/green/expr/RealVariable.java b/src/za/ac/sun/cs/green/expr/RealVariable.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/RealVariable.java rename to src/za/ac/sun/cs/green/expr/RealVariable.java diff --git a/green/src/za/ac/sun/cs/green/expr/StringConstant.java b/src/za/ac/sun/cs/green/expr/StringConstant.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/StringConstant.java rename to src/za/ac/sun/cs/green/expr/StringConstant.java diff --git a/green/src/za/ac/sun/cs/green/expr/StringVariable.java b/src/za/ac/sun/cs/green/expr/StringVariable.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/StringVariable.java rename to src/za/ac/sun/cs/green/expr/StringVariable.java diff --git a/green/src/za/ac/sun/cs/green/expr/Variable.java b/src/za/ac/sun/cs/green/expr/Variable.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/Variable.java rename to src/za/ac/sun/cs/green/expr/Variable.java diff --git a/green/src/za/ac/sun/cs/green/expr/Visitor.java b/src/za/ac/sun/cs/green/expr/Visitor.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/Visitor.java rename to src/za/ac/sun/cs/green/expr/Visitor.java diff --git a/green/src/za/ac/sun/cs/green/expr/VisitorException.java b/src/za/ac/sun/cs/green/expr/VisitorException.java similarity index 100% rename from green/src/za/ac/sun/cs/green/expr/VisitorException.java rename to src/za/ac/sun/cs/green/expr/VisitorException.java diff --git a/green/src/za/ac/sun/cs/green/log/GreenFormatter.java b/src/za/ac/sun/cs/green/log/GreenFormatter.java similarity index 100% rename from green/src/za/ac/sun/cs/green/log/GreenFormatter.java rename to src/za/ac/sun/cs/green/log/GreenFormatter.java diff --git a/green/src/za/ac/sun/cs/green/log/GreenHandler.java b/src/za/ac/sun/cs/green/log/GreenHandler.java similarity index 100% rename from green/src/za/ac/sun/cs/green/log/GreenHandler.java rename to src/za/ac/sun/cs/green/log/GreenHandler.java diff --git a/green/src/za/ac/sun/cs/green/parser/klee/ParseException.java b/src/za/ac/sun/cs/green/parser/klee/ParseException.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/klee/ParseException.java rename to src/za/ac/sun/cs/green/parser/klee/ParseException.java diff --git a/green/src/za/ac/sun/cs/green/parser/klee/Parser.java b/src/za/ac/sun/cs/green/parser/klee/Parser.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/klee/Parser.java rename to src/za/ac/sun/cs/green/parser/klee/Parser.java diff --git a/green/src/za/ac/sun/cs/green/parser/klee/Scanner.java b/src/za/ac/sun/cs/green/parser/klee/Scanner.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/klee/Scanner.java rename to src/za/ac/sun/cs/green/parser/klee/Scanner.java diff --git a/green/src/za/ac/sun/cs/green/parser/klee/Token.java b/src/za/ac/sun/cs/green/parser/klee/Token.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/klee/Token.java rename to src/za/ac/sun/cs/green/parser/klee/Token.java diff --git a/green/src/za/ac/sun/cs/green/parser/smtlib2/Keyword0.java b/src/za/ac/sun/cs/green/parser/smtlib2/Keyword0.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/smtlib2/Keyword0.java rename to src/za/ac/sun/cs/green/parser/smtlib2/Keyword0.java diff --git a/green/src/za/ac/sun/cs/green/parser/smtlib2/ParseException.java b/src/za/ac/sun/cs/green/parser/smtlib2/ParseException.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/smtlib2/ParseException.java rename to src/za/ac/sun/cs/green/parser/smtlib2/ParseException.java diff --git a/green/src/za/ac/sun/cs/green/parser/smtlib2/Parser0.java b/src/za/ac/sun/cs/green/parser/smtlib2/Parser0.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/smtlib2/Parser0.java rename to src/za/ac/sun/cs/green/parser/smtlib2/Parser0.java diff --git a/green/src/za/ac/sun/cs/green/parser/smtlib2/Scanner0.java b/src/za/ac/sun/cs/green/parser/smtlib2/Scanner0.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/smtlib2/Scanner0.java rename to src/za/ac/sun/cs/green/parser/smtlib2/Scanner0.java diff --git a/green/src/za/ac/sun/cs/green/parser/smtlib2/Token0.java b/src/za/ac/sun/cs/green/parser/smtlib2/Token0.java similarity index 100% rename from green/src/za/ac/sun/cs/green/parser/smtlib2/Token0.java rename to src/za/ac/sun/cs/green/parser/smtlib2/Token0.java diff --git a/green/src/za/ac/sun/cs/green/service/BasicService.java b/src/za/ac/sun/cs/green/service/BasicService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/BasicService.java rename to src/za/ac/sun/cs/green/service/BasicService.java diff --git a/green/src/za/ac/sun/cs/green/service/CountService.java b/src/za/ac/sun/cs/green/service/CountService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/CountService.java rename to src/za/ac/sun/cs/green/service/CountService.java diff --git a/green/src/za/ac/sun/cs/green/service/ModelService.java b/src/za/ac/sun/cs/green/service/ModelService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/ModelService.java rename to src/za/ac/sun/cs/green/service/ModelService.java diff --git a/green/src/za/ac/sun/cs/green/service/SATService.java b/src/za/ac/sun/cs/green/service/SATService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/SATService.java rename to src/za/ac/sun/cs/green/service/SATService.java diff --git a/green/src/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.java b/src/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.java rename to src/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.java diff --git a/green/src/za/ac/sun/cs/green/service/bounder/BounderService.java b/src/za/ac/sun/cs/green/service/bounder/BounderService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/bounder/BounderService.java rename to src/za/ac/sun/cs/green/service/bounder/BounderService.java diff --git a/green/src/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.java b/src/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.java rename to src/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.java diff --git a/green/src/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.java b/src/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.java rename to src/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.java diff --git a/green/src/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.java b/src/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.java rename to src/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.java diff --git a/green/src/za/ac/sun/cs/green/service/choco/ChocoTranslator.java b/src/za/ac/sun/cs/green/service/choco/ChocoTranslator.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco/ChocoTranslator.java rename to src/za/ac/sun/cs/green/service/choco/ChocoTranslator.java diff --git a/green/src/za/ac/sun/cs/green/service/choco/ModelChocoService.java b/src/za/ac/sun/cs/green/service/choco/ModelChocoService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco/ModelChocoService.java rename to src/za/ac/sun/cs/green/service/choco/ModelChocoService.java diff --git a/green/src/za/ac/sun/cs/green/service/choco/SATChocoService.java b/src/za/ac/sun/cs/green/service/choco/SATChocoService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco/SATChocoService.java rename to src/za/ac/sun/cs/green/service/choco/SATChocoService.java diff --git a/green/src/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.java b/src/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.java rename to src/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.java diff --git a/green/src/za/ac/sun/cs/green/service/choco3/Choco3Translator.java b/src/za/ac/sun/cs/green/service/choco3/Choco3Translator.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco3/Choco3Translator.java rename to src/za/ac/sun/cs/green/service/choco3/Choco3Translator.java diff --git a/green/src/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.java b/src/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.java rename to src/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.java diff --git a/green/src/za/ac/sun/cs/green/service/choco3/SATChoco3Service.java b/src/za/ac/sun/cs/green/service/choco3/SATChoco3Service.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco3/SATChoco3Service.java rename to src/za/ac/sun/cs/green/service/choco3/SATChoco3Service.java diff --git a/green/src/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.java b/src/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.java rename to src/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.java diff --git a/green/src/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.java b/src/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.java rename to src/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.java diff --git a/green/src/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.java b/src/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.java rename to src/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.java diff --git a/green/src/za/ac/sun/cs/green/service/factorizer/FactorExpression.java b/src/za/ac/sun/cs/green/service/factorizer/FactorExpression.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/factorizer/FactorExpression.java rename to src/za/ac/sun/cs/green/service/factorizer/FactorExpression.java diff --git a/green/src/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.java b/src/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.java rename to src/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.java diff --git a/green/src/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.java b/src/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.java rename to src/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.java diff --git a/green/src/za/ac/sun/cs/green/service/latte/CountLattEService.java b/src/za/ac/sun/cs/green/service/latte/CountLattEService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/latte/CountLattEService.java rename to src/za/ac/sun/cs/green/service/latte/CountLattEService.java diff --git a/green/src/za/ac/sun/cs/green/service/renamer/RenamerService.java b/src/za/ac/sun/cs/green/service/renamer/RenamerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/renamer/RenamerService.java rename to src/za/ac/sun/cs/green/service/renamer/RenamerService.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..04e0d023 --- /dev/null +++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropagation.java @@ -0,0 +1,644 @@ +package za.ac.sun.cs.green.service.simplify; + +import java.util.Collections; +import java.util.HashMap; +import java.util.Map; +import java.util.Set; +import java.util.SortedMap; +import java.util.SortedSet; +import java.util.Stack; +import java.util.TreeMap; +import java.util.TreeSet; +import java.util.logging.Level; + +import za.ac.sun.cs.green.Instance; +import za.ac.sun.cs.green.Green; +import za.ac.sun.cs.green.expr.Expression; +import za.ac.sun.cs.green.service.BasicService; +import za.ac.sun.cs.green.util.Reporter; +import za.ac.sun.cs.green.expr.Constant; +import za.ac.sun.cs.green.expr.IntConstant; +import za.ac.sun.cs.green.expr.IntVariable; +import za.ac.sun.cs.green.expr.Operation; +import za.ac.sun.cs.green.expr.Variable; +import za.ac.sun.cs.green.expr.Visitor; +import za.ac.sun.cs.green.expr.VisitorException; + +public class ConstantPropagation extends BasicService { + + /** + * Number of times the slicer has been invoked. + */ + private int invocations = 0; + + public ConstantPropagation(Green solver) { + super(solver); + } + + @Override + public Set processRequest(Instance instance) { + @SuppressWarnings("unchecked") + Set result = (Set) instance.getData(getClass()); + if (result == null) { + final Map map = new HashMap(); + final Expression e = canonize(instance.getFullExpression(), map); + final Instance i = new Instance(getSolver(), instance.getSource(), null, e); + result = Collections.singleton(i); + instance.setData(getClass(), result); + } + return result; + } + + @Override + public void report(Reporter reporter) { + reporter.report(getClass().getSimpleName(), "invocations = " + invocations); + } + + public Expression canonize(Expression expression, Map map) { + try { + log.log(Level.FINEST, "Before Canonization: " + expression); + invocations++; + OrderingVisitor orderingVisitor = new OrderingVisitor(); + expression.accept(orderingVisitor); + expression = orderingVisitor.getExpression(); + log.log(Level.FINEST, "After Propagation: " + expression); +// CanonizationVisitor canonizationVisitor = new CanonizationVisitor(); +// expression.accept(canonizationVisitor); +// Expression canonized = canonizationVisitor.getExpression(); +// log.log(Level.FINEST, "After Canonization: " + canonized); + return expression; + } catch (VisitorException x) { + log.log(Level.SEVERE, "encountered an exception -- this should not be happening!", x); + } + return null; + } + + private static class OrderingVisitor extends Visitor { + + private Stack stack; + private Map variableMap = new HashMap(); + + 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.LT; + break; + case LE: + nop = Operation.Operator.LE; + break; + case GT: + nop = Operation.Operator.GT; + break; + case GE: + nop = Operation.Operator.GE; + break; + default: + break; + } + if (nop != null) { + Expression r = stack.pop(); + Expression l = stack.pop(); + + if ((l instanceof IntVariable) && (r instanceof IntConstant) && (nop == Operation.Operator.EQ)) { + if (!variableMap.containsKey(l)) + variableMap.put(l, r); + } else if ((r instanceof IntVariable) && (l instanceof IntConstant) && (nop == Operation.Operator.EQ)) { + if (!variableMap.containsKey(l)) + variableMap.put(r, l); + } + + 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) && (nop != Operation.Operator.EQ)) { + if (variableMap.containsKey(r)) { + stack.push(new Operation(nop, variableMap.get(r), r)); + } + } else if ((l instanceof IntVariable) && (r instanceof IntConstant) && (nop != Operation.Operator.EQ)) { + if (variableMap.containsKey(l)) { + stack.push(new Operation(nop, variableMap.get(l), r )); + } + } else if ((r instanceof IntVariable) && (l instanceof IntConstant)) { + stack.push(new Operation(nop, l, r)); + } else { + stack.push(new Operation(nop, l, r)); + } + } else if (op.getArity() == 2) { + Expression r = stack.pop(); + Expression l = stack.pop(); + + if (variableMap.containsKey(r)) { + stack.push(new Operation(op, l, variableMap.get(r))); + } else if (variableMap.containsKey(l)) { + stack.push(new Operation(op, variableMap.get(l), r)); + } else { + stack.push(new Operation(op, l, r)); + } + } else { + for (int i = op.getArity(); i > 0; i--) { + stack.pop(); + } + stack.push(operation); + } + } + + } + + private static class CanonizationVisitor extends Visitor { + + private Stack stack; + + private SortedSet conjuncts; + + private SortedSet variableSet; + + private Map lowerBounds; + + private Map upperBounds; + + private IntVariable boundVariable; + + private Integer bound; + + private int boundCoeff; + + private boolean unsatisfiable; + + private boolean linearInteger; + + public CanonizationVisitor() { + stack = new Stack(); + conjuncts = new TreeSet(); + variableSet = new TreeSet(); + unsatisfiable = false; + linearInteger = true; + } + + public SortedSet getVariableSet() { + return variableSet; + } + + public Expression getExpression() { + if (!linearInteger) { + return null; + } else if (unsatisfiable) { + return Operation.FALSE; + } else { + if (!stack.isEmpty()) { + Expression x = stack.pop(); + if (x.equals(Operation.FALSE)) { + return Operation.FALSE; + } else if (!x.equals(Operation.TRUE)) { + conjuncts.add(x); + } + } + SortedSet newConjuncts = processBounds(); + // new TreeSet(); + Expression c = null; + for (Expression e : newConjuncts) { + if (e.equals(Operation.FALSE)) { + return Operation.FALSE; + } else if (e instanceof Operation) { + Operation o = (Operation) e; + if (o.getOperator() == Operation.Operator.GT) { + e = new Operation(Operation.Operator.LT, scale(-1, o.getOperand(0)), o.getOperand(1)); + } else if (o.getOperator() == Operation.Operator.GE) { + e = new Operation(Operation.Operator.LE, scale(-1, o.getOperand(0)), o.getOperand(1)); + } + o = (Operation) e; + if (o.getOperator() == Operation.Operator.GT) { + e = new Operation(Operation.Operator.GE, merge(o.getOperand(0), new IntConstant(-1)), + o.getOperand(1)); + } else if (o.getOperator() == Operation.Operator.LT) { + e = new Operation(Operation.Operator.LE, merge(o.getOperand(0), new IntConstant(1)), + o.getOperand(1)); + } + } + if (c == null) { + c = e; + } else { + c = new Operation(Operation.Operator.AND, c, e); + } + } + return (c == null) ? Operation.TRUE : c; + } + } + + private SortedSet processBounds() { + return conjuncts; + } + + @SuppressWarnings("unused") + private void extractBound(Expression e) throws VisitorException { + if (e instanceof Operation) { + Operation o = (Operation) e; + Expression lhs = o.getOperand(0); + Operation.Operator op = o.getOperator(); + if (isBound(lhs)) { + switch (op) { + case EQ: + lowerBounds.put(boundVariable, bound * boundCoeff); + upperBounds.put(boundVariable, bound * boundCoeff); + break; + case LT: + if (boundCoeff == 1) { + upperBounds.put(boundVariable, bound * -1 - 1); + } else { + lowerBounds.put(boundVariable, bound + 1); + } + break; + case LE: + if (boundCoeff == 1) { + upperBounds.put(boundVariable, bound * -1); + } else { + lowerBounds.put(boundVariable, bound); + } + break; + case GT: + if (boundCoeff == 1) { + lowerBounds.put(boundVariable, bound * -1 + 1); + } else { + upperBounds.put(boundVariable, bound - 1); + } + break; + case GE: + if (boundCoeff == 1) { + lowerBounds.put(boundVariable, bound * -1); + } else { + upperBounds.put(boundVariable, bound); + } + break; + default: + break; + } + } + } + } + + private boolean isBound(Expression lhs) { + if (!(lhs instanceof Operation)) { + return false; + } + Operation o = (Operation) lhs; + if (o.getOperator() == Operation.Operator.MUL) { + if (!(o.getOperand(0) instanceof IntConstant)) { + return false; + } + if (!(o.getOperand(1) instanceof IntVariable)) { + return false; + } + boundVariable = (IntVariable) o.getOperand(1); + bound = 0; + if ((((IntConstant) o.getOperand(0)).getValue() == 1) + || (((IntConstant) o.getOperand(0)).getValue() == -1)) { + boundCoeff = ((IntConstant) o.getOperand(0)).getValue(); + return true; + } else { + return false; + } + } else if (o.getOperator() == Operation.Operator.ADD) { + if (!(o.getOperand(1) instanceof IntConstant)) { + return false; + } + bound = ((IntConstant) o.getOperand(1)).getValue(); + if (!(o.getOperand(0) instanceof Operation)) { + return false; + } + Operation p = (Operation) o.getOperand(0); + if (!(p.getOperand(0) instanceof IntConstant)) { + return false; + } + if (!(p.getOperand(1) instanceof IntVariable)) { + return false; + } + boundVariable = (IntVariable) p.getOperand(1); + if ((((IntConstant) p.getOperand(0)).getValue() == 1) + || (((IntConstant) p.getOperand(0)).getValue() == -1)) { + boundCoeff = ((IntConstant) p.getOperand(0)).getValue(); + return true; + } else { + return false; + } + } else { + return false; + } + } + + @Override + public void postVisit(Constant constant) { + if (linearInteger && !unsatisfiable) { + if (constant instanceof IntConstant) { + stack.push(constant); + } else { + stack.clear(); + linearInteger = false; + } + } + } + + @Override + public void postVisit(Variable variable) { + if (linearInteger && !unsatisfiable) { + if (variable instanceof IntVariable) { + variableSet.add((IntVariable) variable); + stack.push(new Operation(Operation.Operator.MUL, Operation.ONE, variable)); + } else { + stack.clear(); + linearInteger = false; + } + } + } + + @Override + public void postVisit(Operation operation) throws VisitorException { + if (!linearInteger || unsatisfiable) { + return; + } + Operation.Operator op = operation.getOperator(); + switch (op) { + case AND: + if (!stack.isEmpty()) { + Expression x = stack.pop(); + if (!x.equals(Operation.TRUE)) { + conjuncts.add(x); + } + } + if (!stack.isEmpty()) { + Expression x = stack.pop(); + if (!x.equals(Operation.TRUE)) { + conjuncts.add(x); + } + } + break; + case EQ: + case NE: + case LT: + case LE: + case GT: + case GE: + if (!stack.isEmpty()) { + Expression e = merge(scale(-1, stack.pop()), stack.pop()); + if (e instanceof IntConstant) { + int v = ((IntConstant) e).getValue(); + boolean b = true; + if (op == Operation.Operator.EQ) { + b = v == 0; + } else if (op == Operation.Operator.NE) { + b = v != 0; + } else if (op == Operation.Operator.LT) { + b = v < 0; + } else if (op == Operation.Operator.LE) { + b = v <= 0; + } else if (op == Operation.Operator.GT) { + b = v > 0; + } else if (op == Operation.Operator.GE) { + b = v >= 0; + } + if (b) { + stack.push(Operation.TRUE); + } else { + stack.push(Operation.FALSE); + // unsatisfiable = true; + } + } else { + stack.push(new Operation(op, e, Operation.ZERO)); + } + } + break; + case ADD: + stack.push(merge(stack.pop(), stack.pop())); + break; + case SUB: + stack.push(merge(scale(-1, stack.pop()), stack.pop())); + break; + case MUL: + if (stack.size() >= 2) { + Expression r = stack.pop(); + Expression l = stack.pop(); + if ((l instanceof IntConstant) && (r instanceof IntConstant)) { + int li = ((IntConstant) l).getValue(); + int ri = ((IntConstant) r).getValue(); + stack.push(new IntConstant(li * ri)); + } else if (l instanceof IntConstant) { + int li = ((IntConstant) l).getValue(); + stack.push(scale(li, r)); + } else if (r instanceof IntConstant) { + int ri = ((IntConstant) r).getValue(); + stack.push(scale(ri, l)); + } else { + stack.clear(); + linearInteger = false; + } + } + break; + case NOT: + if (!stack.isEmpty()) { + Expression e = stack.pop(); + if (e.equals(Operation.TRUE)) { + e = Operation.FALSE; + } else if (e.equals(Operation.FALSE)) { + e = Operation.TRUE; + } else if (e instanceof Operation) { + Operation o = (Operation) e; + switch (o.getOperator()) { + case NOT: + e = o.getOperand(0); + break; + case EQ: + e = new Operation(Operation.Operator.NE, o.getOperand(0), o.getOperand(1)); + break; + case NE: + e = new Operation(Operation.Operator.EQ, o.getOperand(0), o.getOperand(1)); + break; + case GE: + e = new Operation(Operation.Operator.LT, o.getOperand(0), o.getOperand(1)); + break; + case GT: + e = new Operation(Operation.Operator.LE, o.getOperand(0), o.getOperand(1)); + break; + case LE: + e = new Operation(Operation.Operator.GT, o.getOperand(0), o.getOperand(1)); + break; + case LT: + e = new Operation(Operation.Operator.GE, o.getOperand(0), o.getOperand(1)); + break; + default: + break; + } + } else { + // We just drop the NOT?? + } + stack.push(e); + } else { + // We just drop the NOT?? + } + break; + default: + break; + } + } + + private Expression merge(Expression left, Expression right) { + Operation l = null; + Operation r = null; + int s = 0; + if (left instanceof IntConstant) { + s = ((IntConstant) left).getValue(); + } else { + if (hasRightConstant(left)) { + s = getRightConstant(left); + l = getLeftOperation(left); + } else { + l = (Operation) left; + } + } + if (right instanceof IntConstant) { + s += ((IntConstant) right).getValue(); + } else { + if (hasRightConstant(right)) { + s += getRightConstant(right); + r = getLeftOperation(right); + } else { + r = (Operation) right; + } + } + SortedMap coefficients = new TreeMap(); + IntConstant c; + Variable v; + Integer k; + + // Collect the coefficients of l + if (l != null) { + while (l.getOperator() == Operation.Operator.ADD) { + Operation o = (Operation) l.getOperand(1); + assert (o.getOperator() == Operation.Operator.MUL); + c = (IntConstant) o.getOperand(0); + v = (IntVariable) o.getOperand(1); + coefficients.put(v, c.getValue()); + l = (Operation) l.getOperand(0); + } + assert (l.getOperator() == Operation.Operator.MUL); + c = (IntConstant) l.getOperand(0); + v = (IntVariable) l.getOperand(1); + coefficients.put(v, c.getValue()); + } + + // Collect the coefficients of r + if (r != null) { + while (r.getOperator() == Operation.Operator.ADD) { + Operation o = (Operation) r.getOperand(1); + assert (o.getOperator() == Operation.Operator.MUL); + c = (IntConstant) o.getOperand(0); + v = (IntVariable) o.getOperand(1); + k = coefficients.get(v); + if (k == null) { + coefficients.put(v, c.getValue()); + } else { + coefficients.put(v, c.getValue() + k); + } + r = (Operation) r.getOperand(0); + } + assert (r.getOperator() == Operation.Operator.MUL); + c = (IntConstant) r.getOperand(0); + v = (IntVariable) r.getOperand(1); + k = coefficients.get(v); + if (k == null) { + coefficients.put(v, c.getValue()); + } else { + coefficients.put(v, c.getValue() + k); + } + } + + Expression lr = null; + for (Map.Entry e : coefficients.entrySet()) { + int coef = e.getValue(); + if (coef != 0) { + Operation term = new Operation(Operation.Operator.MUL, new IntConstant(coef), e.getKey()); + if (lr == null) { + lr = term; + } else { + lr = new Operation(Operation.Operator.ADD, lr, term); + } + } + } + if ((lr == null) || (lr instanceof IntConstant)) { + return new IntConstant(s); + } else if (s == 0) { + return lr; + } else { + return new Operation(Operation.Operator.ADD, lr, new IntConstant(s)); + } + } + + private boolean hasRightConstant(Expression expression) { + return isAddition(expression) && (getRightExpression(expression) instanceof IntConstant); + } + + private int getRightConstant(Expression expression) { + return ((IntConstant) getRightExpression(expression)).getValue(); + } + + private Expression getLeftExpression(Expression expression) { + return ((Operation) expression).getOperand(0); + } + + private Expression getRightExpression(Expression expression) { + return ((Operation) expression).getOperand(1); + } + + private Operation getLeftOperation(Expression expression) { + return (Operation) getLeftExpression(expression); + } + + private boolean isAddition(Expression expression) { + return ((Operation) expression).getOperator() == Operation.Operator.ADD; + } + + private Expression scale(int factor, Expression expression) { + if (factor == 0) { + return Operation.ZERO; + } + if (expression instanceof IntConstant) { + return new IntConstant(factor * ((IntConstant) expression).getValue()); + } else if (expression instanceof IntVariable) { + return expression; + } else { + assert (expression instanceof Operation); + Operation o = (Operation) expression; + Operation.Operator p = o.getOperator(); + Expression l = scale(factor, o.getOperand(0)); + Expression r = scale(factor, o.getOperand(1)); + return new Operation(p, l, r); + } + } + + } + +} diff --git a/green/src/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.java b/src/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.java rename to src/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.java diff --git a/green/src/za/ac/sun/cs/green/service/slicer/SATSlicerService.java b/src/za/ac/sun/cs/green/service/slicer/SATSlicerService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/slicer/SATSlicerService.java rename to src/za/ac/sun/cs/green/service/slicer/SATSlicerService.java diff --git a/green/src/za/ac/sun/cs/green/service/slicer/Slicer.java b/src/za/ac/sun/cs/green/service/slicer/Slicer.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/slicer/Slicer.java rename to src/za/ac/sun/cs/green/service/slicer/Slicer.java diff --git a/green/src/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.java b/src/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.java rename to src/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.java diff --git a/green/src/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.java b/src/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.java rename to src/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.java diff --git a/green/src/za/ac/sun/cs/green/service/z3/SATZ3JavaService.java b/src/za/ac/sun/cs/green/service/z3/SATZ3JavaService.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/z3/SATZ3JavaService.java rename to src/za/ac/sun/cs/green/service/z3/SATZ3JavaService.java diff --git a/green/src/za/ac/sun/cs/green/service/z3/SATZ3Service.java b/src/za/ac/sun/cs/green/service/z3/SATZ3Service.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/z3/SATZ3Service.java rename to src/za/ac/sun/cs/green/service/z3/SATZ3Service.java diff --git a/green/src/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.java b/src/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.java rename to src/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.java diff --git a/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java b/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java similarity index 100% rename from green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java rename to src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java diff --git a/green/src/za/ac/sun/cs/green/store/BasicStore.java b/src/za/ac/sun/cs/green/store/BasicStore.java similarity index 100% rename from green/src/za/ac/sun/cs/green/store/BasicStore.java rename to src/za/ac/sun/cs/green/store/BasicStore.java diff --git a/green/src/za/ac/sun/cs/green/store/NullStore.java b/src/za/ac/sun/cs/green/store/NullStore.java similarity index 100% rename from green/src/za/ac/sun/cs/green/store/NullStore.java rename to src/za/ac/sun/cs/green/store/NullStore.java diff --git a/green/src/za/ac/sun/cs/green/store/Store.java b/src/za/ac/sun/cs/green/store/Store.java similarity index 100% rename from green/src/za/ac/sun/cs/green/store/Store.java rename to src/za/ac/sun/cs/green/store/Store.java diff --git a/green/src/za/ac/sun/cs/green/store/redis/RedisStore.java b/src/za/ac/sun/cs/green/store/redis/RedisStore.java similarity index 100% rename from green/src/za/ac/sun/cs/green/store/redis/RedisStore.java rename to src/za/ac/sun/cs/green/store/redis/RedisStore.java diff --git a/green/src/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.java b/src/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.java similarity index 100% rename from green/src/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.java rename to src/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.java diff --git a/green/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java b/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java similarity index 100% rename from green/src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java rename to src/za/ac/sun/cs/green/taskmanager/SerialTaskManager.java diff --git a/green/src/za/ac/sun/cs/green/taskmanager/TaskManager.java b/src/za/ac/sun/cs/green/taskmanager/TaskManager.java similarity index 100% rename from green/src/za/ac/sun/cs/green/taskmanager/TaskManager.java rename to src/za/ac/sun/cs/green/taskmanager/TaskManager.java diff --git a/green/src/za/ac/sun/cs/green/util/Base64.java b/src/za/ac/sun/cs/green/util/Base64.java similarity index 100% rename from green/src/za/ac/sun/cs/green/util/Base64.java rename to src/za/ac/sun/cs/green/util/Base64.java diff --git a/green/src/za/ac/sun/cs/green/util/Configuration.java b/src/za/ac/sun/cs/green/util/Configuration.java similarity index 100% rename from green/src/za/ac/sun/cs/green/util/Configuration.java rename to src/za/ac/sun/cs/green/util/Configuration.java diff --git a/green/src/za/ac/sun/cs/green/util/Misc.java b/src/za/ac/sun/cs/green/util/Misc.java similarity index 100% rename from green/src/za/ac/sun/cs/green/util/Misc.java rename to src/za/ac/sun/cs/green/util/Misc.java diff --git a/green/src/za/ac/sun/cs/green/util/Reporter.java b/src/za/ac/sun/cs/green/util/Reporter.java similarity index 100% rename from green/src/za/ac/sun/cs/green/util/Reporter.java rename to src/za/ac/sun/cs/green/util/Reporter.java diff --git a/green/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java similarity index 72% rename from green/test/za/ac/sun/cs/green/EntireSuite.java rename to test/za/ac/sun/cs/green/EntireSuite.java index 31b27ca0..98e7c3fa 100644 --- a/green/test/za/ac/sun/cs/green/EntireSuite.java +++ b/test/za/ac/sun/cs/green/EntireSuite.java @@ -16,41 +16,15 @@ import com.microsoft.z3.Context; import cvc3.ValidityChecker; -import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Parser0Test; -import za.ac.sun.cs.green.parser.smtlib2.SMTLIB2Scanner0Test; -import za.ac.sun.cs.green.service.bounder.BounderTest; import za.ac.sun.cs.green.service.canonizer.SATCanonizerTest; -import za.ac.sun.cs.green.service.choco.SATChocoTest; -import za.ac.sun.cs.green.service.cvc3.SATCVC3Test; -import za.ac.sun.cs.green.service.factorizer.SATFactorizerTest; -import za.ac.sun.cs.green.service.latte.CountLattETest; -import za.ac.sun.cs.green.service.latte.CountLattEWithBounderTest; -import za.ac.sun.cs.green.service.slicer.ParallelSATSlicerTest; -import za.ac.sun.cs.green.service.slicer.SATSlicerTest; -import za.ac.sun.cs.green.service.z3.SATZ3JavaTest; +import za.ac.sun.cs.green.service.simplify.ConstantPropagationTest; import za.ac.sun.cs.green.service.z3.SATZ3Test; -import za.ac.sun.cs.green.util.ParallelSATTest; -import za.ac.sun.cs.green.util.SetServiceTest; -import za.ac.sun.cs.green.util.SetTaskManagerTest; @RunWith(Suite.class) @Suite.SuiteClasses({ - SetTaskManagerTest.class, - SetServiceTest.class, - SATSlicerTest.class, SATCanonizerTest.class, - SATChocoTest.class, - SATCVC3Test.class, - ParallelSATSlicerTest.class, - ParallelSATTest.class, SATZ3Test.class, - SATFactorizerTest.class, - CountLattETest.class, - CountLattEWithBounderTest.class, - BounderTest.class, - SMTLIB2Scanner0Test.class, - SMTLIB2Parser0Test.class, - SATZ3JavaTest.class + ConstantPropagationTest.class }) public class EntireSuite { @@ -67,7 +41,7 @@ public class EntireSuite { public static final boolean HAS_Z3; - public static final boolean HAS_Z3JAVA; + public static final boolean HAS_Z3JAVA = false; static { String latte = null, z3 = null, barvinok = null; @@ -87,10 +61,11 @@ public class EntireSuite { LATTE_PATH = latte; BARVINOK_PATH = barvinok; Z3_PATH = z3; - //HAS_CVC3 = checkCVC3Presence(); - //HAS_LATTE = checkLattEPresence(); HAS_Z3 = checkZ3Presence(); - HAS_Z3JAVA = checkZ3JavaPresence(); + if (!HAS_Z3) { + System.out.println("Z3 Not Available, no tests for it will be executed"); + } + } private static boolean checkCVC3Presence() { diff --git a/test/za/ac/sun/cs/green/misc/FactorizerCNFTest.java b/test/za/ac/sun/cs/green/misc/FactorizerCNFTest.java new file mode 100644 index 00000000..3512eda7 --- /dev/null +++ b/test/za/ac/sun/cs/green/misc/FactorizerCNFTest.java @@ -0,0 +1,167 @@ +package za.ac.sun.cs.green.misc; + +import static org.junit.Assert.*; + +import java.util.Arrays; +import java.util.Properties; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; + +import org.junit.AfterClass; +import org.junit.Assume; +import org.junit.BeforeClass; +import org.junit.Test; + +import za.ac.sun.cs.green.EntireSuite; +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.service.sink.FactorSinkService; +import za.ac.sun.cs.green.util.Configuration; + +public class FactorizerCNFTest { + + 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","(factor sink)"); + props.setProperty("green.service.sat.factor", + "za.ac.sun.cs.green.service.factorizer.SATFactorizerService"); + props.setProperty("green.service.sat.sink", "za.ac.sun.cs.green.service.sink.FactorSinkService"); + Configuration config = new Configuration(solver, props); + config.configure(); + } + + @AfterClass + public static void report() { + if (solver != null) { + solver.report(); + } + } + + private boolean finalCheck(String[] expected, Instance factor) { + String[] expectedReplaced = new String[expected.length]; + for (int i=0; i s2 = new TreeSet(Arrays.asList(s0.split("&&"))); + SortedSet s3 = new TreeSet(Arrays.asList(expectedReplaced)); + return s2.equals(s3); + } + + private void finalCheck(String[][] expected, Set factors) { + assertEquals(expected.length, factors.size()); + for (Instance i : factors) { + boolean found = false; + for (String[] e : expected) { + if (finalCheck(e, i)) { + found = true; + break; + } + } + if (!found) { + System.out.println("Not found: " + i.getExpression()); + } + assertTrue(found); + } + } + + private void check(Expression expression, String[]... expected) { + Instance i = new Instance(solver, null, expression); + Expression e = i.getExpression(); + assertTrue(e.equals(expression)); + assertEquals(expression.toString(), e.toString()); + Object result = i.request("sat"); + assertEquals(null, result); + Object f0 = i.getData(FactorSinkService.class); + assertTrue(f0 instanceof Set); + @SuppressWarnings("unchecked") + Set f = (Set) f0; + finalCheck(expected, f); + } + + private Operation BOOL(IntVariable v) { + return new Operation(Operation.Operator.NE, v, Operation.ZERO); + } + + /* (v1 or v2) and (v3 or v4) */ + + @Test + public void test1() { + Operation v1 = BOOL(new IntVariable("a1", 0, 1)); + Operation v2 = BOOL(new IntVariable("a2", 0, 1)); + Operation v3 = BOOL(new IntVariable("a3", 0, 1)); + Operation v4 = BOOL(new IntVariable("a4", 0, 1)); + + + Operation c1 = new Operation(Operation.Operator.OR, v1, v2); + Operation c2 = new Operation(Operation.Operator.OR, v3, v4); + + Operation all = new Operation(Operation.Operator.AND, c1, c2); + + check(all,new String[] { "(a1!=0)||(a2!=0)" }, new String[] { "(a3!=0)||(a4!=0)" }); + + } + + @Test + public void test01() { + Operation v1 = BOOL(new IntVariable("a1", 0, 1)); + Operation v2 = BOOL(new IntVariable("a2", 0, 1)); + Operation v3 = BOOL(new IntVariable("a3", 0, 1)); + Operation v4 = BOOL(new IntVariable("a4", 0, 1)); + + Operation c1 = new Operation(Operation.Operator.OR, v1, v2); + Operation c2 = new Operation(Operation.Operator.OR, c1, v3); + + Operation all = new Operation(Operation.Operator.AND, c2, v4); + + check(all,new String[] { "((a1!=0)||(a2!=0))||(a3!=0)" }, new String[] { "a4!=0" }); + } + + + @Test + public void test2() { + Operation v1 = BOOL(new IntVariable("a1", 0, 1)); + Operation v2 = BOOL(new IntVariable("a2", 0, 1)); + Operation v3 = BOOL(new IntVariable("a3", 0, 1)); + Operation v4 = BOOL(new IntVariable("a4", 0, 1)); + + + Operation c1 = new Operation(Operation.Operator.OR, v1, v2); + Operation c2 = new Operation(Operation.Operator.OR, v2, v4); + + Operation all = new Operation(Operation.Operator.AND, c1, c2); + + check(all,new String[] { "((a1!=0)||(a2!=0))", "((a2!=0)||(a4!=0))" }); + } + + @Test + public void test3() { + Operation v1 = BOOL(new IntVariable("a1", 0, 1)); + Operation v2 = BOOL(new IntVariable("a2", 0, 1)); + Operation v3 = BOOL(new IntVariable("a3", 0, 1)); + Operation v4 = BOOL(new IntVariable("a4", 0, 1)); + Operation v5 = BOOL(new IntVariable("a5", 0, 1)); + Operation v6 = BOOL(new IntVariable("a6", 0, 1)); + + Operation c1 = new Operation(Operation.Operator.OR, v1, v2); + Operation c2 = new Operation(Operation.Operator.OR, v3, v4); + Operation c3 = new Operation(Operation.Operator.OR, v5, v6); + + Operation all1 = new Operation(Operation.Operator.AND, c1, c2); + + Operation all = new Operation(Operation.Operator.AND, all1, c3); + check(all,new String[] { "(a1!=0)||(a2!=0)" }, new String[] { "(a3!=0)||(a4!=0)"}, new String[] { "(a5!=0)||(a6!=0)" }); + } + + +} diff --git a/green/test/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.java b/test/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.java rename to test/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.java diff --git a/green/test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.java b/test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.java similarity index 100% rename from green/test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.java rename to test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.java diff --git a/green/test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.java b/test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.java similarity index 100% rename from green/test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.java rename to test/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.java diff --git a/green/test/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.java b/test/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.java rename to test/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.java diff --git a/green/test/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.java b/test/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.java rename to test/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.java diff --git a/green/test/za/ac/sun/cs/green/service/bounder/BounderTest.java b/test/za/ac/sun/cs/green/service/bounder/BounderTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/bounder/BounderTest.java rename to test/za/ac/sun/cs/green/service/bounder/BounderTest.java diff --git a/green/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java similarity index 87% rename from green/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java rename to test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java index 8f506820..f2d35fb6 100644 --- a/green/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java +++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java @@ -304,46 +304,4 @@ public void test20() { check(o3, "(2<=2)&&(aa<2)", "1*v+-1<=0"); } - @Test - public void test21() { - IntVariable x1 = new IntVariable("x1", 0, 99); - IntVariable x2 = new IntVariable("x2", 0, 99); - IntVariable x3 = new IntVariable("x3", 0, 99); - IntVariable x4 = new IntVariable("x4", 0, 99); - IntVariable x5 = new IntVariable("x5", 0, 99); - - IntConstant c1 = new IntConstant(1); - IntConstant c0 = new IntConstant(0); - - Operation x2eq1 = new Operation(Operation.Operator.EQ, x2, c1); - Operation x1eq1 = new Operation(Operation.Operator.EQ, x1, c1); - Operation c0eqc0 = new Operation(Operation.Operator.EQ, c0, c0); - Operation o4a = new Operation(Operation.Operator.AND, x1eq1, c0eqc0); - Operation o4b = new Operation(Operation.Operator.AND, x2eq1, o4a); - - Operation o1a = new Operation(Operation.Operator.EQ, x3, c1); - Operation o1 = new Operation(Operation.Operator.NOT, o1a); - - Operation o2a = new Operation(Operation.Operator.EQ, x5, x5); - Operation o2 = new Operation(Operation.Operator.LE, x4, x5); - Operation o3 = new Operation(Operation.Operator.NE, x4, x5); - Operation o3a = new Operation(Operation.Operator.AND, o3, o4b); - - Operation o4 = new Operation(Operation.Operator.AND, o2, o3a); - - Operation o5 = new Operation(Operation.Operator.AND, o2a, o4); - Operation o6 = new Operation(Operation.Operator.AND, o1, o5); - check(o6, "(!(x3==1))&&((x5==x5)&&((x4<=x5)&&((x4!=x5)&&((x2==1)&&((x1==1)&&(0==0))))))", "1*v+-1<=0"); - } - - @Test - public void test23() { - IntVariable x5 = new IntVariable("x5", 0, 99); - IntConstant c1 = new IntConstant(1); - IntConstant c0 = new IntConstant(0); - Operation o2b = new Operation(Operation.Operator.NE, x5, x5); - Operation o2a = new Operation(Operation.Operator.NOT, o2b); - check(o2a, "!(x5!=x5)", "0==0"); - } - } diff --git a/green/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.java rename to test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.java diff --git a/green/test/za/ac/sun/cs/green/service/choco/ModelChocoTest.java b/test/za/ac/sun/cs/green/service/choco/ModelChocoTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/choco/ModelChocoTest.java rename to test/za/ac/sun/cs/green/service/choco/ModelChocoTest.java diff --git a/green/test/za/ac/sun/cs/green/service/choco/SATChocoTest.java b/test/za/ac/sun/cs/green/service/choco/SATChocoTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/choco/SATChocoTest.java rename to test/za/ac/sun/cs/green/service/choco/SATChocoTest.java diff --git a/green/test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.java b/test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.java rename to test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.java diff --git a/green/test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.java b/test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.java rename to test/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.java diff --git a/green/test/za/ac/sun/cs/green/service/choco3/SATChoco3Test.java b/test/za/ac/sun/cs/green/service/choco3/SATChoco3Test.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/choco3/SATChoco3Test.java rename to test/za/ac/sun/cs/green/service/choco3/SATChoco3Test.java diff --git a/green/test/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.java b/test/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.java rename to test/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.java diff --git a/green/test/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.java b/test/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.java rename to test/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.java diff --git a/green/test/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.java b/test/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.java rename to test/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.java diff --git a/green/test/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.java b/test/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.java rename to test/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.java diff --git a/green/test/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.java b/test/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.java rename to test/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.java diff --git a/green/test/za/ac/sun/cs/green/service/latte/CountLattETest.java b/test/za/ac/sun/cs/green/service/latte/CountLattETest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/latte/CountLattETest.java rename to test/za/ac/sun/cs/green/service/latte/CountLattETest.java diff --git a/green/test/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.java b/test/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.java rename to test/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.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..2dc2c122 --- /dev/null +++ b/test/za/ac/sun/cs/green/service/simplify/ConstantPropagationTest.java @@ -0,0 +1,201 @@ +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 ConstantPropagationTest { + + public static Green solver; + + @BeforeClass + public static void initialize() { + solver = new Green(); + Properties props = new Properties(); + props.setProperty("green.services", "sat"); + props.setProperty("green.service.sat", "(simplify sink)"); + //props.setProperty("green.service.sat", "(canonize sink)"); + props.setProperty("green.service.sat.simplify", + "za.ac.sun.cs.green.service.simplify.ConstantPropagation"); + //props.setProperty("green.service.sat.canonize", + // "za.ac.sun.cs.green.service.canonizer.SATCanonizerService"); + + props.setProperty("green.service.sat.sink", + "za.ac.sun.cs.green.service.sink.SinkService"); + Configuration config = new Configuration(solver, props); + config.configure(); + } + + 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); // (String name, Integer lowerBound, Integer upperBound) + 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)"); + } + +// @Test +// public void test00() { +// IntVariable x = new IntVariable("x", 0, 99); +// IntVariable y = new IntVariable("y", 0, 99); +// IntVariable z = new IntVariable("z", 0, 99); +// IntConstant c = new IntConstant(1); +// IntConstant c10 = new IntConstant(10); +// IntConstant c3 = new IntConstant(3); +// Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : x = 1 +// Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : (x + y) +// Operation o3 = new Operation(Operation.Operator.EQ, o2, c10); // o3 : x+y = 10 +// Operation o4 = new Operation(Operation.Operator.AND, o1, o3); // o4 : x = 1 && (x+y) = 10 +// check(o4, "(x==1)&&(y==9)"); +// } + + /*@Test + public void test01() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c2 = new IntConstant(10); + IntConstant c3 = new IntConstant(2); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : (x = 1) + Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : x + y + Operation o3 = new Operation(Operation.Operator.LT, o2, c2); // o3 : (x+y) < 10 + Operation oi = new Operation(Operation.Operator.SUB, y, c); // oi : y-1 + Operation o4 = new Operation(Operation.Operator.EQ, oi, c3); // o4 : y-1 = 2 + Operation o5 = new Operation(Operation.Operator.AND, o1, o3); // o5 : (x = 1) && (x+y < 10) + Operation o = new Operation(Operation.Operator.AND, o5, o4); // o = (x = 1) && (x+y < 10) && (y-1 = 2) + // (x = 1) && (x+y < 10) && (y-1 = 2) + check(o, "(x==1)&&(y==3)"); + } + + @Test + public void test02() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o = new Operation(Operation.Operator.LT, c1, c2); + check(o, "0==0"); + } + + @Test + public void test03() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o = new Operation(Operation.Operator.GT, c1, c2); + check(o, "0==1"); + } + + @Test + public void test04() { + IntConstant c1 = new IntConstant(4); + IntConstant c2 = new IntConstant(10); + Operation o1 = new Operation(Operation.Operator.LT, c1, c2); + Operation o2 = new Operation(Operation.Operator.GT, c1, c2); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + check(o, "0==1"); + } + + + + + @Test + public void test05() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntConstant c = new IntConstant(1); + IntConstant c2 = new IntConstant(10); + IntConstant c3 = new IntConstant(2); + Operation o1 = new Operation(Operation.Operator.EQ, c, x); + Operation o2 = new Operation(Operation.Operator.ADD, x, y); + Operation o3 = new Operation(Operation.Operator.LT, o2, c2); + Operation oi = new Operation(Operation.Operator.SUB, y, c); + Operation o4 = new Operation(Operation.Operator.EQ, c3, oi); + Operation o5 = new Operation(Operation.Operator.AND, o1, o3); + Operation o = new Operation(Operation.Operator.AND, o5, o4); + check(o, "(1==x)&&(3==y)"); + } + + @Test + public void test06() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntVariable z = new IntVariable("z", 0 , 99); + IntConstant c = new IntConstant(1); + Operation o1 = new Operation(Operation.Operator.EQ, x, y); + Operation o2 = new Operation(Operation.Operator.EQ, y, z); + Operation o3 = new Operation(Operation.Operator.EQ, z, c); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + o = new Operation(Operation.Operator.AND, o, o3); + check(o, "(x==1)&&((y==1)&&(z==1))"); + } +/* + @Test + public void test07() { + IntVariable x = new IntVariable("x", 0, 99); + IntVariable y = new IntVariable("y", 0, 99); + IntVariable z = new IntVariable("z", 0 , 99); + IntConstant c = new IntConstant(2); + IntConstant c1 = new IntConstant(4); + Operation o1 = new Operation(Operation.Operator.MUL, x, y); + Operation o2 = new Operation(Operation.Operator.EQ, z, o1); // z = x * y + Operation o3 = new Operation(Operation.Operator.EQ, x, c); // x = 2 + Operation o4 = new Operation(Operation.Operator.ADD, y, x); + Operation o5 = new Operation(Operation.Operator.EQ, o4, c1); // x+y = 4 + + Operation o = new Operation(Operation.Operator.AND, o2, o3); // z = x * y && x = 2 + o = new Operation(Operation.Operator.AND, o, o5); // z = x * y && x = 2 && x+y = 4 + check(o, "(z==4)&&((x==2)&&(y==2))"); + } + + @Test + public void test08() { + IntVariable x = new IntVariable("x", 0, 99); + IntConstant c = new IntConstant(2); + IntConstant c1 = new IntConstant(4); + Operation o1 = new Operation(Operation.Operator.EQ, x, c); + Operation o2 = new Operation(Operation.Operator.EQ, x, c1); + Operation o = new Operation(Operation.Operator.AND, o1, o2); + + check(o, "0==1"); + } + + + +*/ + +} diff --git a/green/test/za/ac/sun/cs/green/service/sink/FactorSinkService.java b/test/za/ac/sun/cs/green/service/sink/FactorSinkService.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/sink/FactorSinkService.java rename to test/za/ac/sun/cs/green/service/sink/FactorSinkService.java diff --git a/green/test/za/ac/sun/cs/green/service/sink/SinkService.java b/test/za/ac/sun/cs/green/service/sink/SinkService.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/sink/SinkService.java rename to test/za/ac/sun/cs/green/service/sink/SinkService.java diff --git a/green/test/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.java b/test/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.java rename to test/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.java diff --git a/green/test/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.java b/test/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.java rename to test/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.java diff --git a/green/test/za/ac/sun/cs/green/service/slicer/SATSlicerTest.java b/test/za/ac/sun/cs/green/service/slicer/SATSlicerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/slicer/SATSlicerTest.java rename to test/za/ac/sun/cs/green/service/slicer/SATSlicerTest.java diff --git a/green/test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.java b/test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.java rename to test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.java diff --git a/green/test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.java b/test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.java rename to test/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.java diff --git a/green/test/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.java b/test/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.java rename to test/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.java diff --git a/green/test/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.java b/test/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.java rename to test/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.java diff --git a/green/test/za/ac/sun/cs/green/service/z3/SATZ3Test.java b/test/za/ac/sun/cs/green/service/z3/SATZ3Test.java similarity index 100% rename from green/test/za/ac/sun/cs/green/service/z3/SATZ3Test.java rename to test/za/ac/sun/cs/green/service/z3/SATZ3Test.java diff --git a/green/test/za/ac/sun/cs/green/util/DummyTaskManager.java b/test/za/ac/sun/cs/green/util/DummyTaskManager.java similarity index 100% rename from green/test/za/ac/sun/cs/green/util/DummyTaskManager.java rename to test/za/ac/sun/cs/green/util/DummyTaskManager.java diff --git a/green/test/za/ac/sun/cs/green/util/NullLogger.java b/test/za/ac/sun/cs/green/util/NullLogger.java similarity index 100% rename from green/test/za/ac/sun/cs/green/util/NullLogger.java rename to test/za/ac/sun/cs/green/util/NullLogger.java diff --git a/green/test/za/ac/sun/cs/green/util/ParallelSATTest.java b/test/za/ac/sun/cs/green/util/ParallelSATTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/util/ParallelSATTest.java rename to test/za/ac/sun/cs/green/util/ParallelSATTest.java diff --git a/green/test/za/ac/sun/cs/green/util/SetServiceTest.java b/test/za/ac/sun/cs/green/util/SetServiceTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/util/SetServiceTest.java rename to test/za/ac/sun/cs/green/util/SetServiceTest.java diff --git a/green/test/za/ac/sun/cs/green/util/SetTaskManagerTest.java b/test/za/ac/sun/cs/green/util/SetTaskManagerTest.java similarity index 100% rename from green/test/za/ac/sun/cs/green/util/SetTaskManagerTest.java rename to test/za/ac/sun/cs/green/util/SetTaskManagerTest.java