Skip to content

Commit

Permalink
Merge branch 'master' into domspec_heuristics
Browse files Browse the repository at this point in the history
# Conflicts:
#	src/main/java/at/ac/tuwien/kr/alpha/Main.java
#	src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java
#	src/test/java/at/ac/tuwien/kr/alpha/api/AlphaTest.java
  • Loading branch information
rtaupe committed Feb 19, 2020
2 parents e413e3d + d2f7b40 commit 2b8141e
Show file tree
Hide file tree
Showing 14 changed files with 574 additions and 62 deletions.
34 changes: 23 additions & 11 deletions build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,11 @@ repositories {
/* The following configuration directive is a work-around for a fault in the Gradle
* ANTLR plugin. It would require both antlr4 and antlr4-runtime at compile time and
* at run time, which unnecessarily bloats our JARs. Only antlr4-runtime is needed.
* We therefore remove this extension of antlr dependenIterablecies being compile dependencies
* We therefore remove this extension of antlr dependencies being compile dependencies
* and reintroduce them on our own.
*/
configurations {
compile {
implementation {
extendsFrom = extendsFrom.findAll { it != configurations.antlr }
}
}
Expand All @@ -37,15 +37,17 @@ dependencies {
antlr group: 'org.antlr', name: 'antlr4', version: "${antlrVersion}"

// Re-introduce antlr4-runtime as compile dependency.
compile group: 'org.antlr', name: 'antlr4-runtime', version: "${antlrVersion}"
implementation group: 'org.antlr', name: 'antlr4-runtime', version: "${antlrVersion}"

compile group: 'ch.qos.logback', name: 'logback-classic', version: '1.1.7'
compile group: 'commons-cli', name: 'commons-cli', version: '1.3.1'
compile group: 'org.apache.commons', name: 'commons-collections4', version: '4.1'
compile group: 'org.apache.commons', name: 'commons-lang3', version: '3.6'
compile group: 'org.reflections', name: 'reflections', version: '0.9.11'
implementation group: 'ch.qos.logback', name: 'logback-classic', version: '1.1.7'
implementation group: 'commons-cli', name: 'commons-cli', version: '1.3.1'
implementation group: 'org.apache.commons', name: 'commons-collections4', version: '4.1'
implementation group: 'org.apache.commons', name: 'commons-lang3', version: '3.6'
implementation group: 'org.reflections', name: 'reflections', version: '0.9.11'
implementation group: 'org.apache.poi', name: 'poi', version: '4.1.1'
implementation group: 'org.apache.poi', name: 'poi-ooxml', version: '4.1.1'

testCompile group: 'junit', name: 'junit', version: '4.12'
testImplementation group: 'junit', name: 'junit', version: '4.12'
}

tasks.withType(AntlrTask) {
Expand Down Expand Up @@ -81,10 +83,20 @@ task bundledJar(type: Jar) {
}

from {
configurations.compile.collect { it.isDirectory() ? it : zipTree(it) }
configurations.compileClasspath.collect { it.isDirectory() ? it : zipTree(it) }
}

archiveName = "${project.name}-bundled.jar"
archiveFileName = "${project.name}-bundled.jar"

/*
* In order to make sure we don't overwrite NOTICE and LICENSE files coming from dependency
* jars with each other, number them while copying
*/
int i = 1
rename { name -> (name.equals("NOTICE.txt") || name.equals("NOTICE")) ? "NOTICE." + (i++) + ".txt" : null }

int j = 1
rename { name -> (name.equals("LICENSE.txt") || name.equals("LICENSE")) ? "LICENSE." + (j++) + ".txt" : null }

with jar
}
Expand Down
59 changes: 59 additions & 0 deletions src/main/java/at/ac/tuwien/kr/alpha/AnswerSetToXlsxWriter.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
package at.ac.tuwien.kr.alpha;

import at.ac.tuwien.kr.alpha.api.mapper.AnswerSetToObjectMapper;
import at.ac.tuwien.kr.alpha.api.mapper.impl.AnswerSetToWorkbookMapper;
import at.ac.tuwien.kr.alpha.common.AnswerSet;
import org.apache.poi.ss.usermodel.Cell;
import org.apache.poi.ss.usermodel.Row;
import org.apache.poi.ss.usermodel.Sheet;
import org.apache.poi.ss.usermodel.Workbook;
import org.apache.poi.xssf.usermodel.XSSFWorkbook;

import java.io.IOException;
import java.io.OutputStream;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.nio.file.StandardOpenOption;
import java.util.function.BiConsumer;

public class AnswerSetToXlsxWriter implements BiConsumer<Integer, AnswerSet> {

private String targetBasePath;
private AnswerSetToObjectMapper<Workbook> answerSetMapper;

public AnswerSetToXlsxWriter(String targetBasePath) {
this.targetBasePath = targetBasePath;
this.answerSetMapper = new AnswerSetToWorkbookMapper();
}

@Override
public void accept(Integer num, AnswerSet as) {
try {
Path outputPath = Paths.get(this.targetBasePath + "." + num + ".xlsx");
OutputStream os = Files.newOutputStream(outputPath, StandardOpenOption.CREATE, StandardOpenOption.WRITE, StandardOpenOption.TRUNCATE_EXISTING);
Workbook wb = this.answerSetMapper.mapFromAnswerSet(as);
wb.write(os);
wb.close();
os.close();
System.out.println("Answer set written to file " + outputPath.toString());
} catch (IOException ex) {
System.err.println("Failed writing answer set as xlsx file! (" + ex.getMessage() + ")");
}
}

public static void writeUnsatInfo(Path path) throws IOException {
Workbook workbook = new XSSFWorkbook();
// first, create a worksheet for 0-arity predicates
Sheet sheet = workbook.createSheet("Unsatisfiable");
Row row = sheet.createRow(0);
Cell cell = row.createCell(0);
cell.setCellValue("Input is unsatisfiable - No answer sets!");
sheet.autoSizeColumn(0);
OutputStream os = Files.newOutputStream(path, StandardOpenOption.CREATE, StandardOpenOption.WRITE, StandardOpenOption.TRUNCATE_EXISTING);
workbook.write(os);
workbook.close();
os.close();
}

}
27 changes: 25 additions & 2 deletions src/main/java/at/ac/tuwien/kr/alpha/Main.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/**
* Copyright (c) 2016-2019, the Alpha Team.
* Copyright (c) 2016-2020, the Alpha Team.
* All rights reserved.
*
* Additional changes made by Siemens.
Expand Down Expand Up @@ -27,6 +27,7 @@
*/
package at.ac.tuwien.kr.alpha;

import at.ac.tuwien.kr.alpha.api.Alpha;
import at.ac.tuwien.kr.alpha.common.AnswerSet;
import at.ac.tuwien.kr.alpha.common.Program;
import at.ac.tuwien.kr.alpha.config.AlphaConfig;
Expand All @@ -41,7 +42,9 @@

import java.io.FileNotFoundException;
import java.io.IOException;
import java.nio.file.Paths;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.function.BiConsumer;
import java.util.stream.Collectors;
import java.util.stream.Stream;

Expand Down Expand Up @@ -97,9 +100,29 @@ private static void computeAndConsumeAnswerSets(Alpha alpha, InputConfig inputCf

if (!alpha.getConfig().isQuiet()) {
AtomicInteger counter = new AtomicInteger(0);
stream.forEach(as -> System.out.println("Answer set " + counter.incrementAndGet() + ":" + System.lineSeparator() + as.toString()));
final BiConsumer<Integer, AnswerSet> answerSetHandler;
BiConsumer<Integer, AnswerSet> stdoutPrinter = (n, as) -> {
System.out.println("Answer set " + Integer.toString(n) + ":" + System.lineSeparator() + as.toString());
};
if (inputCfg.isWriteAnswerSetsAsXlsx()) {
BiConsumer<Integer, AnswerSet> xlsxWriter = new AnswerSetToXlsxWriter(inputCfg.getAnswerSetFileOutputPath());
answerSetHandler = stdoutPrinter.andThen(xlsxWriter);
} else {
answerSetHandler = stdoutPrinter;
}
stream.forEach(as -> {
int cnt = counter.incrementAndGet();
answerSetHandler.accept(cnt, as);
});
if (counter.get() == 0) {
System.out.println("UNSATISFIABLE");
if (inputCfg.isWriteAnswerSetsAsXlsx()) {
try {
AnswerSetToXlsxWriter.writeUnsatInfo(Paths.get(inputCfg.getAnswerSetFileOutputPath() + ".UNSAT.xlsx"));
} catch (IOException ex) {
System.err.println("Failed writing unsat file!");
}
}
} else {
System.out.println("SATISFIABLE");
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,9 @@
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/
package at.ac.tuwien.kr.alpha;
package at.ac.tuwien.kr.alpha.api;

import at.ac.tuwien.kr.alpha.Util;
import at.ac.tuwien.kr.alpha.common.AnswerSet;
import at.ac.tuwien.kr.alpha.common.AtomStore;
import at.ac.tuwien.kr.alpha.common.AtomStoreImpl;
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
/**
* Copyright (c) 2020, the Alpha Team.
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* 1) Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* 2) Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/
package at.ac.tuwien.kr.alpha.api.mapper;

import at.ac.tuwien.kr.alpha.common.AnswerSet;

/**
* Copyright (c) 2020, the Alpha Team.
*
* Interface definition for an adapter that maps from an {@link AnswerSet} to an instance of the implementation's generic type T.
*
* @param <T> the type to which to map answer sets
*/
public interface AnswerSetToObjectMapper<T> {

T mapFromAnswerSet(AnswerSet answerSet);

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
/**
* Copyright (c) 2020, the Alpha Team.
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* 1) Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* 2) Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*/
package at.ac.tuwien.kr.alpha.api.mapper.impl;

import at.ac.tuwien.kr.alpha.api.mapper.AnswerSetToObjectMapper;
import at.ac.tuwien.kr.alpha.common.AnswerSet;
import at.ac.tuwien.kr.alpha.common.Predicate;
import at.ac.tuwien.kr.alpha.common.atoms.Atom;
import at.ac.tuwien.kr.alpha.common.terms.Term;
import org.apache.poi.ss.usermodel.Cell;
import org.apache.poi.ss.usermodel.CellStyle;
import org.apache.poi.ss.usermodel.FillPatternType;
import org.apache.poi.ss.usermodel.Font;
import org.apache.poi.ss.usermodel.IndexedColors;
import org.apache.poi.ss.usermodel.Row;
import org.apache.poi.ss.usermodel.Sheet;
import org.apache.poi.ss.usermodel.Workbook;
import org.apache.poi.xssf.usermodel.XSSFWorkbook;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.util.List;

/**
* Implementation of {@link AnswerSetToObjectMapper} that generates an office open xml workbook ("excel file") from a given answer set.
*
* Copyright (c) 2020, the Alpha Team.
*/
public class AnswerSetToWorkbookMapper implements AnswerSetToObjectMapper<Workbook> {

private static final Logger LOGGER = LoggerFactory.getLogger(AnswerSetToWorkbookMapper.class);

/**
* Creates an xlsx workbook containing all the atoms from the given {@link AnswerSet} with one sheet per predicate. All predicates with arity 0 are listed
* in a special sheet called "flags". Caution, potential resource leak: note that the returned workbook needs to be closed by the caller once it has been
* processed (written to file etc).
*/
@Override
public Workbook mapFromAnswerSet(AnswerSet answerSet) {
LOGGER.debug("Start mapping answer set to workbook");
Workbook workbook = new XSSFWorkbook();
// create cell style for header cells
CellStyle headerStyle = this.createHeaderStyle(workbook);

// first, create a worksheet for 0-arity predicates
Sheet flags = this.createSheetWithHeader(workbook, headerStyle, "Flags", "Flags");
Sheet currentPredicateSheet;
String[] headerContent;
for (Predicate pred : answerSet.getPredicates()) {
if (pred.getArity() == 0) {
this.writeAtomToSheet(flags, answerSet.getPredicateInstances(pred).first());
} else {
headerContent = new String[pred.getArity()];
for (int i = 0; i < headerContent.length; i++) {
headerContent[i] = "Attribute " + Integer.toString(i + 1);
}
currentPredicateSheet = this.createSheetWithHeader(workbook, headerStyle, pred.getName() + "_" + pred.getArity(), headerContent);
for (Atom atom : answerSet.getPredicateInstances(pred)) {
this.writeAtomToSheet(currentPredicateSheet, atom);
}
}
}
return workbook;
}

private void writeAtomToSheet(Sheet sheet, Atom atom) {
int rownum = -1;
if (sheet.getLastRowNum() == 0 && sheet.getRow(0) == null) {
// sheet is empty, start at row zero
rownum = 0;
} else {
rownum = sheet.getLastRowNum() + 1;
}
Row atomRow = sheet.createRow(rownum);
List<Term> terms = atom.getTerms();
Cell currCell;
if (terms.isEmpty()) {
// 0-arity atom
currCell = atomRow.createCell(0);
currCell.setCellValue(atom.getPredicate().getName());
sheet.autoSizeColumn(0);
} else {
for (int i = 0; i < terms.size(); i++) {
currCell = atomRow.createCell(i);
currCell.setCellValue(terms.get(i).toString());
sheet.autoSizeColumn(i);
}
}
}

private CellStyle createHeaderStyle(Workbook workbook) {
CellStyle headerStyle = workbook.createCellStyle();
Font headerFont = workbook.createFont();
headerFont.setFontHeightInPoints((short) 11);
headerFont.setBold(true); // (short) 0x74c4f2
headerStyle.setFont(headerFont);
headerStyle.setFillPattern(FillPatternType.SOLID_FOREGROUND);
headerStyle.setFillForegroundColor(IndexedColors.GREY_25_PERCENT.getIndex());
return headerStyle;
}

private Sheet createSheetWithHeader(Workbook wb, CellStyle headerStyle, String sheetName, String... headerContent) {
Sheet retVal = wb.createSheet(sheetName);
Row headerRow = retVal.createRow(0);
Cell cell;
for (int i = 0; i < headerContent.length; i++) {
cell = headerRow.createCell(i);
cell.setCellStyle(headerStyle);
cell.setCellValue(headerContent[i]);
}
return retVal;
}

}
Loading

0 comments on commit 2b8141e

Please sign in to comment.