ASP Generate Gencay

This commit is contained in:
JanUlrich 2018-07-04 12:29:02 +02:00
parent 3dfbddf693
commit 1f8421db27
7 changed files with 11054 additions and 12 deletions

View File

@ -21,6 +21,7 @@ public class ASPUnify {
programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/step4.lp")); programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/step4.lp"));
programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/subst.lp")); programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/subst.lp"));
programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/unifikation.lp")); programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/unifikation.lp"));
programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/complete/cartesian.lp"));
} }
public ASPUnify(List<File> inputFiles){ public ASPUnify(List<File> inputFiles){
@ -37,7 +38,7 @@ public class ASPUnify {
commands.add(pathToClingo); commands.add(pathToClingo);
//commands.add("--outf=2"); //use JSON-Output //commands.add("--outf=2"); //use JSON-Output
commands.add("--outf=1"); //use Text-Output commands.add("--outf=1"); //use Text-Output
commands.add("-n 0"); //Compute all models commands.add("-n 1"); //Compute n models
for(File file : input){ for(File file : input){
commands.add(file.getPath()); commands.add(file.getPath());
} }

View File

@ -1,5 +1,7 @@
package de.dhbwstuttgart.sat.asp.model; package de.dhbwstuttgart.sat.asp.model;
import de.dhbwstuttgart.typeinference.constraints.Pair;
public enum ASPGencayRule { public enum ASPGencayRule {
ASP_PAIR_EQUALS_NAME("equals"), ASP_PAIR_EQUALS_NAME("equals"),
ASP_PAIR_SMALLER_NAME("sub"), ASP_PAIR_SMALLER_NAME("sub"),
@ -7,10 +9,13 @@ public enum ASPGencayRule {
ASP_PARAMLIST_NAME("paramEq"), ASP_PARAMLIST_NAME("paramEq"),
ASP_FC_PARAMLIST_NAME("param"), ASP_FC_PARAMLIST_NAME("param"),
ASP_PARAMLIST_END_POINTER("null"), ASP_PARAMLIST_END_POINTER("null"),
ASP_PARAMLIST_END_RULE_EQ("endParamEq"),
ASP_PARAMLIST_END_RULE_FC("endParam"),
ASP_TYPE("typeEq"), ASP_TYPE("typeEq"),
ASP_FCTYPE("type"), ASP_FCTYPE("type"),
ASP_TYPE_VAR("var"), ASP_TYPE_VAR("var"),
ASP_GENERIC_VAR("pph"), ASP_GENERIC_VAR("pph"),
ASP_WILDCARD("wildcard"),
ASP_PARAMLIST_ORDER("paramOrder"); ASP_PARAMLIST_ORDER("paramOrder");
private final String text; private final String text;

View File

@ -130,6 +130,11 @@ public class ASPGencayFactory implements TypeVisitor<String> {
stmt = makeStatement(paramname, p, type, stmt = makeStatement(paramname, p, type,
ASPGencayRule.ASP_PARAMLIST_END_POINTER.toString()); ASPGencayRule.ASP_PARAMLIST_END_POINTER.toString());
} }
if(!it.hasNext()){ //Falls es der letzte Pointer ist
String endRule = isFCType?ASPGencayRule.ASP_PARAMLIST_END_RULE_FC.toString():ASPGencayRule.ASP_PARAMLIST_END_RULE_EQ.toString();
writer.add(makeStatement(endRule, p,
ASPGencayRule.ASP_PARAMLIST_END_POINTER.toString()));
}
p = nextP; p = nextP;
writer.add(stmt); writer.add(stmt);
} }
@ -143,11 +148,9 @@ public class ASPGencayFactory implements TypeVisitor<String> {
String pointer = ASPStringConverter.toConstant(NameGenerator.makeNewName()); String pointer = ASPStringConverter.toConstant(NameGenerator.makeNewName());
currentFCTypePointer = pointer; currentFCTypePointer = pointer;
String paramPointer = ASPGencayRule.ASP_PARAMLIST_END_POINTER.toString(); String paramPointer = ASPGencayRule.ASP_PARAMLIST_END_POINTER.toString();
if(refType.getParaList().size() == 1 ){ if(refType.getParaList().size() == 1 && (refType.getParaList().get(0) instanceof TypePlaceholder)){
if(refType.getParaList().get(0) instanceof TypePlaceholder){
TypePlaceholder typePlaceholder = (TypePlaceholder) refType.getParaList().get(0); TypePlaceholder typePlaceholder = (TypePlaceholder) refType.getParaList().get(0);
paramPointer = typePlaceholder.acceptTV(this); paramPointer = typePlaceholder.acceptTV(this);
}
}else{ }else{
List<String> params = null; List<String> params = null;
params = generateParameter(refType); params = generateParameter(refType);
@ -194,6 +197,8 @@ public class ASPGencayFactory implements TypeVisitor<String> {
ret.addAll(generateParameter((RefType) param)); ret.addAll(generateParameter((RefType) param));
}else if(param instanceof TypePlaceholder){ }else if(param instanceof TypePlaceholder){
ret.add(param.acceptTV(this)); ret.add(param.acceptTV(this));
}else if(param instanceof WildcardType){
ret.add(param.acceptTV(this));
}else throw new NotImplementedException(); }else throw new NotImplementedException();
} }
return ret; return ret;
@ -201,7 +206,10 @@ public class ASPGencayFactory implements TypeVisitor<String> {
@Override @Override
public String visit(SuperWildcardType superWildcardType) { public String visit(SuperWildcardType superWildcardType) {
throw new NotImplementedException(); String pointer = ASPStringConverter.toConstant(NameGenerator.makeNewName());
writer.add(makeStatement(ASPGencayRule.ASP_WILDCARD.toString(),
pointer, "super", superWildcardType.getInnerType().acceptTV(this)));
return pointer;
} }
@Override @Override
@ -222,7 +230,10 @@ public class ASPGencayFactory implements TypeVisitor<String> {
@Override @Override
public String visit(ExtendsWildcardType extendsWildcardType) { public String visit(ExtendsWildcardType extendsWildcardType) {
throw new NotImplementedException(); String pointer = ASPStringConverter.toConstant(NameGenerator.makeNewName());
writer.add(makeStatement(ASPGencayRule.ASP_WILDCARD.toString(),
pointer, "extends", extendsWildcardType.getInnerType().acceptTV(this)));
return pointer;
} }
@Override @Override

View File

@ -1,5 +1,6 @@
package de.dhbwstuttgart.sat.asp.writer; package de.dhbwstuttgart.sat.asp.writer;
import java.util.ArrayList;
import java.util.Collection; import java.util.Collection;
import java.util.HashSet; import java.util.HashSet;
import java.util.List; import java.util.List;

View File

@ -69,6 +69,40 @@ public class GeneratorTest extends UnifyWithoutWildcards{
System.out.println(resultSet); System.out.println(resultSet);
} }
@Test
public void example5() throws ClassNotFoundException { //Das Beispiel aus dem Paper
ConstraintSet<Pair> 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<RefTypeOrTPHOrWildcardOrGeneric> list1 = Arrays.asList(tphA);
List<RefTypeOrTPHOrWildcardOrGeneric> 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));
RefType integer = new RefType(new JavaClassName(Integer.class.getName()), new ArrayList<>(), new NullToken());
List<RefTypeOrTPHOrWildcardOrGeneric> list3 = Arrays.asList(integer);
List<RefTypeOrTPHOrWildcardOrGeneric> list4 = Arrays.asList(tphA);
RefType abstractList = new RefType(new JavaClassName(AbstractList.class.getName()), list3, new NullToken());
RefType list = new RefType(new JavaClassName(List.class.getName()), list4, new NullToken());
testSet.addUndConstraint(new Pair(abstractList, list, PairOperator.SMALLERDOT));
Set<ClassOrInterface> fc = new HashSet<>();
fc.add(ASTFactory.createClass(Stack.class));
fc.add(ASTFactory.createClass(Vector.class));
fc.add(ASTFactory.createClass(AbstractList.class));
fc.add(ASTFactory.createClass(List.class));
fc.add(ASTFactory.createClass(Integer.class));
fc.add(ASTFactory.createClass(Number.class));
String resultSet = ASPGencayFactory.generateASP(testSet, fc);
System.out.println(resultSet);
}
private Collection<ClassOrInterface> getFC() { private Collection<ClassOrInterface> getFC() {
Set<ClassOrInterface> ret = new HashSet<>(); Set<ClassOrInterface> ret = new HashSet<>();
ret.add(ASTFactory.createClass(Matrix.class)); ret.add(ASTFactory.createClass(Matrix.class));

View File

@ -1,13 +1,27 @@
import java.util.Vector; import java.util.Vector;
import java.util.ArrayList;
import java.lang.Object; import java.lang.Object;
class MyVector{ class MyVector{
id(x){ id(x){
Object i; Object i;
x.elementAt(i); ///*
x.elementAt(i); x.add(i);
x.elementAt(i); x.add(i);
return x.elementAt(i); x.add(i);
x.add(i);
x.add(i);
x.add(i);
x.add(i);
x.add(i);
x.add(i);
x.add(i);
x.add(i);
x.add(i);
//*/
//TODO: Allein die Constraints aus diesem Stmt verursachen 5000 mögliche Lösungen. Warum?
x.add(i);
return x;
} }
} }

10976
test/logFiles/log Normal file

File diff suppressed because it is too large Load Diff