From fc9b1a6bb1ab751cd109edd0b5b52e7993971997 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Mon, 28 May 2018 15:51:40 +0200 Subject: [PATCH] =?UTF-8?q?Beginnen=20mit=20ASP=20Generator=20f=C3=BCr=20U?= =?UTF-8?q?nify=20WITH=20wildcards?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/de/dhbwstuttgart/core/JavaTXCompiler.java | 5 +- .../sat/asp/ASPUnifyWithoutWildcards.java | 55 +++++++++++++++++++ src/de/dhbwstuttgart/sat/asp/Clingo.java | 10 +--- .../sat/asp/writer/ASPFactory.java | 4 +- .../syntaxtree/factory/ASTFactory.java | 1 + test/asp/ClingoTest.java | 6 +- test/asp/UnifyWithoutWildcards.java | 4 +- test/asp/gencay/GeneratorTest.java | 38 ++++++++++--- test/javFiles/Generics.jav | 1 + 9 files changed, 96 insertions(+), 28 deletions(-) create mode 100644 src/de/dhbwstuttgart/sat/asp/ASPUnifyWithoutWildcards.java diff --git a/src/de/dhbwstuttgart/core/JavaTXCompiler.java b/src/de/dhbwstuttgart/core/JavaTXCompiler.java index eb1d1db7..106411f6 100644 --- a/src/de/dhbwstuttgart/core/JavaTXCompiler.java +++ b/src/de/dhbwstuttgart/core/JavaTXCompiler.java @@ -7,8 +7,7 @@ import de.dhbwstuttgart.parser.scope.GenericsRegistry; import de.dhbwstuttgart.parser.SyntaxTreeGenerator.SyntaxTreeGenerator; import de.dhbwstuttgart.parser.antlr.Java8Parser.CompilationUnitContext; import de.dhbwstuttgart.parser.scope.JavaClassName; -import de.dhbwstuttgart.parser.scope.JavaClassRegistry; -import de.dhbwstuttgart.sat.asp.Clingo; +import de.dhbwstuttgart.sat.asp.ASPUnifyWithoutWildcards; import de.dhbwstuttgart.sat.asp.parser.ASPParser; import de.dhbwstuttgart.sat.asp.writer.ASPFactory; import de.dhbwstuttgart.syntaxtree.ClassOrInterface; @@ -149,7 +148,7 @@ public class JavaTXCompiler { PrintWriter writer = new PrintWriter(tempDirectory + "test.lp", "UTF-8"); writer.println(content); writer.close(); - Clingo clingo = new Clingo(Arrays.asList(new File(tempDirectory + "test.lp"))); + ASPUnifyWithoutWildcards clingo = new ASPUnifyWithoutWildcards(Arrays.asList(new File(tempDirectory + "test.lp"))); String result = clingo.runClingo(); System.out.println(result); ResultSet resultSet = ASPParser.parse(result, getInvolvedTPHS(cons)); diff --git a/src/de/dhbwstuttgart/sat/asp/ASPUnifyWithoutWildcards.java b/src/de/dhbwstuttgart/sat/asp/ASPUnifyWithoutWildcards.java new file mode 100644 index 00000000..392670ae --- /dev/null +++ b/src/de/dhbwstuttgart/sat/asp/ASPUnifyWithoutWildcards.java @@ -0,0 +1,55 @@ +package de.dhbwstuttgart.sat.asp; + + +import org.apache.commons.io.IOUtils; + +import java.io.File; +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; +import java.nio.charset.StandardCharsets; +import java.util.ArrayList; +import java.util.List; +import java.util.stream.Collectors; + +public class ASPUnifyWithoutWildcards { + private final List input; + private static final List programFiles = new ArrayList<>(); + static{ + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/basis.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/finiteclosure.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/subst.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/reduce.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/unify.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/result.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/adapt.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/cartesian.lp")); + } + + public ASPUnifyWithoutWildcards(List inputFiles){ + this.input = inputFiles; + } + + /* + TODO: Clingo per Java Wrapper https://stackoverflow.com/questions/3356200/using-java-to-wrap-over-c + */ + public String runClingo() throws IOException, InterruptedException { + String pathToClingo = + "/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/clingo-5.2.1-linux-x86_64/clingo"; + List commands = new ArrayList<>(); + commands.add(pathToClingo); + //commands.add("--outf=2"); //use JSON-Output + commands.add("--outf=1"); //use Text-Output + commands.add("-n 0"); //Compute all models + for(File file : input){ + commands.add(file.getPath()); + } + commands.addAll(programFiles.stream().map(f->f.getPath()).collect(Collectors.toList())); + + Process clingo = new ProcessBuilder( commands.toArray(new String[0])).start(); + InputStream output = clingo.getInputStream(); + clingo.waitFor(); + String result = IOUtils.toString(output, StandardCharsets.UTF_8); + return result; + } +} diff --git a/src/de/dhbwstuttgart/sat/asp/Clingo.java b/src/de/dhbwstuttgart/sat/asp/Clingo.java index 78cb694e..d4fdcc4b 100644 --- a/src/de/dhbwstuttgart/sat/asp/Clingo.java +++ b/src/de/dhbwstuttgart/sat/asp/Clingo.java @@ -6,7 +6,6 @@ import org.apache.commons.io.IOUtils; import java.io.File; import java.io.IOException; import java.io.InputStream; -import java.io.OutputStream; import java.nio.charset.StandardCharsets; import java.util.ArrayList; import java.util.List; @@ -16,14 +15,7 @@ public class Clingo { private final List input; private static final List programFiles = new ArrayList<>(); static{ - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/basis.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/finiteclosure.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/subst.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/reduce.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/unify.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/result.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/adapt.lp")); - programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/cartesian.lp")); + } public Clingo(List inputFiles){ diff --git a/src/de/dhbwstuttgart/sat/asp/writer/ASPFactory.java b/src/de/dhbwstuttgart/sat/asp/writer/ASPFactory.java index aafb8166..da37be1a 100644 --- a/src/de/dhbwstuttgart/sat/asp/writer/ASPFactory.java +++ b/src/de/dhbwstuttgart/sat/asp/writer/ASPFactory.java @@ -133,6 +133,7 @@ public class ASPFactory implements TypeVisitor{ } protected String convertParameterlist(List pointers){ + //TODO: Hier an die neue Datenstruktur anpassen String pointer = ASPStringConverter.toConstant(NameGenerator.makeNewName()); Iterator it = pointers.iterator(); String p = pointer; @@ -164,7 +165,8 @@ public class ASPFactory implements TypeVisitor{ } String typeName = ASPStringConverter.toConstant(refType.getName()); String ruleName = isFCType?ASPRule.ASP_FCTYPE.toString():ASPRule.ASP_TYPE.toString(); - ASPStatement stmt = makeStatement(ruleName, pointer, typeName, convertParameterlist(params)); + convertParameterlist(params); + ASPStatement stmt = makeStatement(ruleName, pointer, typeName, Integer.toString(params.size())); writer.add(stmt); return pointer; } diff --git a/src/de/dhbwstuttgart/syntaxtree/factory/ASTFactory.java b/src/de/dhbwstuttgart/syntaxtree/factory/ASTFactory.java index 52921c5d..c5954996 100644 --- a/src/de/dhbwstuttgart/syntaxtree/factory/ASTFactory.java +++ b/src/de/dhbwstuttgart/syntaxtree/factory/ASTFactory.java @@ -89,6 +89,7 @@ public class ASTFactory { } private static Field createField(java.lang.reflect.Field field, JavaClassName jreClass) { + //TODO: Hier auch GenericRefType generieren: return new Field(field.getName(), createType(field.getType(), jreClass, null), field.getModifiers(), new NullToken()); } diff --git a/test/asp/ClingoTest.java b/test/asp/ClingoTest.java index 90635bde..ade2029b 100644 --- a/test/asp/ClingoTest.java +++ b/test/asp/ClingoTest.java @@ -1,9 +1,9 @@ package asp; import de.dhbwstuttgart.parser.NullToken; +import de.dhbwstuttgart.sat.asp.ASPUnifyWithoutWildcards; import de.dhbwstuttgart.sat.asp.parser.ASPParser; import de.dhbwstuttgart.sat.asp.writer.ASPFactory; -import de.dhbwstuttgart.sat.asp.Clingo; import de.dhbwstuttgart.syntaxtree.ClassOrInterface; import de.dhbwstuttgart.syntaxtree.factory.ASTFactory; import de.dhbwstuttgart.syntaxtree.type.RefTypeOrTPHOrWildcardOrGeneric; @@ -14,8 +14,6 @@ import de.dhbwstuttgart.typeinference.result.ResultSet; import de.dhbwstuttgart.typeinference.unify.model.PairOperator; import org.junit.Test; -import javax.json.Json; -import javax.json.JsonObject; import java.io.*; import java.util.*; @@ -31,7 +29,7 @@ public class ClingoTest { writer.println(content); writer.close(); - Clingo clingo = new Clingo(Arrays.asList(new File(tempDirectory + "test.lp"))); + ASPUnifyWithoutWildcards clingo = new ASPUnifyWithoutWildcards(Arrays.asList(new File(tempDirectory + "test.lp"))); String result = clingo.runClingo(); System.out.println(result); ResultSet resultSet = ASPParser.parse(result, Arrays.asList(testType)); diff --git a/test/asp/UnifyWithoutWildcards.java b/test/asp/UnifyWithoutWildcards.java index d425261b..3493b745 100644 --- a/test/asp/UnifyWithoutWildcards.java +++ b/test/asp/UnifyWithoutWildcards.java @@ -2,7 +2,7 @@ package asp; import de.dhbwstuttgart.parser.NullToken; import de.dhbwstuttgart.parser.scope.JavaClassName; -import de.dhbwstuttgart.sat.asp.Clingo; +import de.dhbwstuttgart.sat.asp.ASPUnifyWithoutWildcards; import de.dhbwstuttgart.sat.asp.parser.ASPParser; import de.dhbwstuttgart.sat.asp.writer.ASPFactory; import de.dhbwstuttgart.syntaxtree.ClassOrInterface; @@ -123,7 +123,7 @@ public class UnifyWithoutWildcards { PrintWriter writer = new PrintWriter(tempDirectory + "test.lp", "UTF-8"); writer.println(content); writer.close(); - Clingo clingo = new Clingo(Arrays.asList(new File(tempDirectory + "test.lp"))); + ASPUnifyWithoutWildcards clingo = new ASPUnifyWithoutWildcards(Arrays.asList(new File(tempDirectory + "test.lp"))); String result = clingo.runClingo(); System.out.println(result); ResultSet resultSet = ASPParser.parse(result, getInvolvedTPHS(toTest)); diff --git a/test/asp/gencay/GeneratorTest.java b/test/asp/gencay/GeneratorTest.java index 2c9fc46f..20ac7905 100644 --- a/test/asp/gencay/GeneratorTest.java +++ b/test/asp/gencay/GeneratorTest.java @@ -3,27 +3,22 @@ package asp.gencay; import asp.UnifyWithoutWildcards; import de.dhbwstuttgart.parser.NullToken; import de.dhbwstuttgart.parser.scope.JavaClassName; -import de.dhbwstuttgart.sat.asp.Clingo; -import de.dhbwstuttgart.sat.asp.parser.ASPParser; -import de.dhbwstuttgart.sat.asp.writer.ASPFactory; import de.dhbwstuttgart.sat.asp.writer.ASPGencayFactory; import de.dhbwstuttgart.syntaxtree.ClassOrInterface; import de.dhbwstuttgart.syntaxtree.factory.ASTFactory; +import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType; import de.dhbwstuttgart.syntaxtree.type.RefType; import de.dhbwstuttgart.syntaxtree.type.RefTypeOrTPHOrWildcardOrGeneric; import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder; -import de.dhbwstuttgart.syntaxtree.visual.ResultSetPrinter; import de.dhbwstuttgart.typeinference.constraints.ConstraintSet; import de.dhbwstuttgart.typeinference.constraints.Pair; -import de.dhbwstuttgart.typeinference.result.ResultSet; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.WildcardType; import org.junit.Test; -import java.io.File; -import java.io.IOException; -import java.io.PrintWriter; +import java.lang.reflect.Type; import java.util.*; -import java.util.concurrent.ArrayBlockingQueue; public class GeneratorTest extends UnifyWithoutWildcards{ @Test @@ -51,9 +46,34 @@ public class GeneratorTest extends UnifyWithoutWildcards{ System.out.println(resultSet); } + @Test + public void wildcardExample() throws ClassNotFoundException { //Das Beispiel aus dem Paper + ConstraintSet testSet = new ConstraintSet<>(); + + TypePlaceholder tphA = TypePlaceholder.fresh(new NullToken()); + RefType number = new RefType(new JavaClassName(Number.class.getName()), new ArrayList<>(), new NullToken()); + ExtendsWildcardType extendsNumber = new ExtendsWildcardType(number, new NullToken()); + List list1 = Arrays.asList(tphA); + List list2 = Arrays.asList(extendsNumber); + RefType stack = new RefType(new JavaClassName(Stack.class.getName()), list1, new NullToken()); + RefType vector = new RefType(new JavaClassName(Vector.class.getName()), list2, new NullToken()); + testSet.addUndConstraint(new Pair(stack, vector, PairOperator.SMALLERDOT)); + + + Set fc = new HashSet<>(); + fc.add(ASTFactory.createClass(Stack.class)); + fc.add(ASTFactory.createClass(AbstractList.class)); + fc.add(ASTFactory.createClass(Integer.class)); + + String resultSet = ASPGencayFactory.generateASP(testSet, fc); + System.out.println(resultSet); + } + private Collection getFC() { Set ret = new HashSet<>(); ret.add(ASTFactory.createClass(Matrix.class)); + ret.add(ASTFactory.createClass(Stack.class)); + ret.add(ASTFactory.createClass(AbstractList.class)); //ret.add(ASTFactory.createObjectClass()); //ret.add(ASTFactory.createClass(java.util.List.class)); return ret; diff --git a/test/javFiles/Generics.jav b/test/javFiles/Generics.jav index c76b40aa..dd7b4eba 100644 --- a/test/javFiles/Generics.jav +++ b/test/javFiles/Generics.jav @@ -1,3 +1,4 @@ +import java.lang.String; class Generics { // A mt1(A a, B b){