aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers')
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql2
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend7
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend2
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend36
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend243
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend109
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend156
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend173
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend16
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend8
15 files changed, 549 insertions, 223 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql
index 8d93cafb..c9581137 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql
@@ -81,5 +81,5 @@ private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type:
81 find supertype(containerType,type); 81 find supertype(containerType,type);
82 TypeDefinition.elements(containerType,element); 82 TypeDefinition.elements(containerType,element);
83 TypeDefinition.elements(uncoveredOccurance,element); 83 TypeDefinition.elements(uncoveredOccurance,element);
84 neg find supertype(uncoveredOccurance,type); 84 neg find supertype(type, uncoveredOccurance);
85} \ No newline at end of file 85} \ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
index 432651af..f6b0b4a5 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
@@ -16,6 +16,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
16import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 16import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
17import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 17import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
18import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 18import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
19import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal
20import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper
21import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
19 22
20class AlloySolver extends LogicReasoner{ 23class AlloySolver extends LogicReasoner{
21 24
@@ -25,7 +28,9 @@ class AlloySolver extends LogicReasoner{
25 x.createInjectorAndDoEMFRegistration 28 x.createInjectorAndDoEMFRegistration
26 } 29 }
27 30
28 val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) 31 val Logic2AlloyLanguageMapper_TypeMapper typeMapper = new Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal//Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes
32
33 val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(typeMapper)
29 val AlloyHandler handler = new AlloyHandler 34 val AlloyHandler handler = new AlloyHandler
30 val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper 35 val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper
31 36
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
index 107aa001..bbee35fc 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -117,7 +117,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
117 for(atom: allAtoms) { 117 for(atom: allAtoms) {
118 val typeName = getName(atom.type) 118 val typeName = getName(atom.type)
119 val atomName = atom.name 119 val atomName = atom.name
120 println(atom.toString + " < - " + typeName) 120 //println(atom.toString + " < - " + typeName)
121 if(typeName == forwardTrace.logicLanguage.name) { 121 if(typeName == forwardTrace.logicLanguage.name) {
122 this.logicLanguage = atom 122 this.logicLanguage = atom
123 } else if(typeName == "Int" || typeName == "seq/Int") { 123 } else if(typeName == "Int" || typeName == "seq/Int") {
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
index 397fb84b..3379ba20 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -123,8 +123,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
123 // 7. Each type is in the intersection of the supertypes 123 // 7. Each type is in the intersection of the supertypes
124 for(type : types.filter[it.supertypes.size>=2]) { 124 for(type : types.filter[it.supertypes.size>=2]) {
125 trace.specification.factDeclarations += createALSFactDeclaration => [ 125 trace.specification.factDeclarations += createALSFactDeclaration => [
126 it.name = support.toIDMultiple("abstract",type.name) 126 it.name = support.toIDMultiple("supertypeIsInIntersection",type.name)
127 it.term = createALSEquals => [ 127 it.term = createALSSubset => [
128 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] 128 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
129 it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| 129 it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|
130 createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) 130 createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
@@ -135,7 +135,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
135 // 8. Each abstract type is equal to the union of the subtypes 135 // 8. Each abstract type is equal to the union of the subtypes
136 for(type : types.filter[isIsAbstract]) { 136 for(type : types.filter[isIsAbstract]) {
137 trace.specification.factDeclarations += createALSFactDeclaration => [ 137 trace.specification.factDeclarations += createALSFactDeclaration => [
138 it.name = support.toIDMultiple("abstract",type.name) 138 it.name = support.toIDMultiple("abstractIsUnion",type.name)
139 it.term = createALSEquals => [ 139 it.term = createALSEquals => [
140 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] 140 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
141 it.rightOperand = support.unfoldPlus(type.subtypes.map[e| 141 it.rightOperand = support.unfoldPlus(type.subtypes.map[e|
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
index e511a961..fd4374f5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
@@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data
11class CanonisedFormulae { 11class CanonisedFormulae {
12 CharSequence viatraCode 12 CharSequence viatraCode
13 Map<Assertion,String> assertion2ConstraintPattern 13 Map<Assertion,String> assertion2ConstraintPattern
14 Map<ConstantDefinition,String> constant2ValuePattern
15 Map<RelationDefinition,String> relation2ValuePattern 14 Map<RelationDefinition,String> relation2ValuePattern
16 Map<FunctionDefinition,String> function2ValuePattern
17} \ No newline at end of file 15} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
index 0af0b36a..182f3a3a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
@@ -5,17 +5,35 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
7import java.util.List 7import java.util.List
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
8 11
9/** 12/**
10 * Translates a set of assertions and definitions to viatra patterns. 13 * Translates a Terms into format
14 * <P(x1,...,xn)> := Bodies(x1,...,xn)
15 * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)>
16 * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)>
17 * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)>
11 */ 18 */
12class FormulaCanoniser { 19class FormulaCanoniser {
13 def canonise( 20// def canonise(
14 List<Assertion> assertions, 21// List<Assertion> assertions,
15 List<RelationDefinition> relations, 22// List<RelationDefinition> relations)
16 List<ConstantDefinition> constants, 23// {
17 List<FunctionDefinition> functions) 24//
18 { 25// }
19 26//
20 } 27//
28// def canoniseToConstraintBlock(Term predicate, List<Variable> variables) {
29// val
30// }
31//
32// def freeVariables(Term t) {
33// val subterms = #[t]+t.eAllContents.toList
34// val variables = subterms.filter(Variable).toSet
35// val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable]
36// val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)]
37// return freeVariables.map
38// }
21} \ No newline at end of file 39} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
new file mode 100644
index 00000000..a421d1fd
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
@@ -0,0 +1,243 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.XExpressionExtractor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
5import org.eclipse.emf.ecore.EAttribute
6import org.eclipse.emf.ecore.EEnumLiteral
7import org.eclipse.emf.ecore.EReference
8import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
9import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
10import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
11import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
12import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
13import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
14import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
15import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
23import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.VariableMapping
24import java.util.List
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
31
32class PConstraintTransformer {
33 val extension RelationDefinitionIndexer relationDefinitionIndexer;
34 val expressionExtractor = new XExpressionExtractor
35 val expressionGenerator = new PExpressionGenerator
36
37 new(RelationDefinitionIndexer relationDefinitionIndexer) {
38 this.relationDefinitionIndexer = relationDefinitionIndexer
39 }
40
41 dispatch def transformConstraint(TypeConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
42 val touple = constraint.variablesTuple
43 if(touple.size == 1) {
44 val inputKey = constraint.equivalentJudgement.inputKey
45 if(inputKey instanceof EClassTransitiveInstancesKey) {
46 return relationDefinitionIndexer.base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
47 constraint.getVariableInTuple(0).canonizeName)
48 } else if(inputKey instanceof EDataTypeInSlotsKey){
49 return '''// type constraint is enforced by construction'''
50 }
51
52 } else if(touple.size == 2){
53 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
54 if(key instanceof EReference) {
55 return base.referRelationByName(
56 key,
57 constraint.getVariableInTuple(0).canonizeName,
58 constraint.getVariableInTuple(1).canonizeName,
59 modality.toMustMay)
60 } else if (key instanceof EAttribute) {
61 return base.referAttributeByName(key,
62 constraint.getVariableInTuple(0).canonizeName,
63 constraint.getVariableInTuple(1).canonizeName,
64 modality.toMustMay)
65 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
66 } else {
67 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
68 }
69 }
70 dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality, List<VariableMapping> variableMapping) {
71 val touple = constraint.variablesTuple
72 if(touple.size == 1) {
73 val inputKey = constraint.equivalentJudgement.inputKey
74 if(inputKey instanceof EClassTransitiveInstancesKey) {
75 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
76 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
77 } else if(inputKey instanceof EDataTypeInSlotsKey){
78 return '''// type constraint is enforced by construction'''
79 }
80
81 } else if(touple.size == 2){
82 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
83 if(key instanceof EReference) {
84 return base.referRelationByName(
85 key,
86 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
87 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
88 modality.toMustMay)
89 } else if (key instanceof EAttribute) {
90 return base.referAttributeByName(key,
91 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
92 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
93 modality.toMustMay)
94 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
95 } else {
96 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
97 }
98 }
99
100 dispatch def transformConstraint(Equality equality, Modality modality, List<VariableMapping> variableMapping) {
101 val a = equality.who
102 val b = equality.withWhom
103 transformEquality(modality.toMustMay, a, b)
104 }
105
106 private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
107 if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
108 else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
109 }
110
111 dispatch def transformConstraint(Inequality inequality, Modality modality, List<VariableMapping> variableMapping) {
112 val a = inequality.who
113 val b = inequality.withWhom
114 if(modality.isCurrent) {
115 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
116 } else if(modality.isMust) {
117 return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
118 } else { // modality.isMay
119 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
120 }
121 }
122
123 dispatch def transformConstraint(NegativePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
124 val params = (0..<pcall.actualParametersTuple.size).map[index |
125 val variable = pcall.actualParametersTuple.get(index) as PVariable
126 return variable.canonizeName
127 ]
128 return referPattern(pcall.referredQuery,params,modality.dual,false,false)
129 }
130
131 dispatch def transformConstraint(PositivePatternCall pcall, Modality modality, List<VariableMapping> variableMapping) {
132 val params = (0..<pcall.variablesTuple.size).map[index |
133 val variable = pcall.variablesTuple.get(index) as PVariable
134 return variable.canonizeName
135 ]
136 return referPattern(pcall.referredQuery,params,modality,true,false)
137 }
138 dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality, List<VariableMapping> variableMapping) {
139 val params = (0..1).map[index |
140 val variable = pcall.getVariableInTuple(index) as PVariable
141 return variable.canonizeName
142 ]
143 return referPattern(pcall.referredQuery,params,modality,true,true)
144 }
145 dispatch def transformConstraint(ExportedParameter e, Modality modality, List<VariableMapping> variableMapping) {
146 return '''// «e.parameterName» is exported'''
147 }
148 dispatch def transformConstraint(ConstantValue c, Modality modality, List<VariableMapping> variableMapping) {
149 val target = c.supplierKey
150
151 var String targetString;
152 var String additionalDefinition;
153 if(target instanceof EEnumLiteral) {
154 targetString = '''const_«target.name»_«target.EEnum.name»'''
155 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
156 } else if(target instanceof Integer) {
157 targetString = '''const_«target»_Integer'''
158 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); IntegerElement.value(«targetString»,«target»);'''
159 } else if(target instanceof Boolean) {
160 targetString = '''const_«target»_Boolean'''
161 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); BooleanElement.value(«targetString»,«target»);'''
162 } else if(target instanceof String) {
163 targetString = '''const_«target»_String'''
164 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); StringElement.value(«targetString»,"«target»");'''
165 } else if(target instanceof Double) {
166 targetString = '''const_«target»_Real'''
167 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
168 } else if(target instanceof Float) {
169 targetString = '''const_«target»_Real'''
170 additionalDefinition = '''PrimitiveElement.valueSet(«targetString»,true); RealElement.value(«targetString»,«target»);'''
171 } else {
172 throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
173 }
174
175 val source = c.variablesTuple
176 var String sourceName
177 if(source.size == 1)
178 sourceName = (source.get(0) as PVariable).canonizeName
179 else throw new UnsupportedOperationException("unknown source")
180 return '''«sourceName» == «targetString»;«additionalDefinition»''';
181 }
182
183 protected def valueVariable(PVariable v) {
184 "value_"+v.canonizeName
185 }
186 protected def valueSetted(PVariable v) {
187 "setted_"+v.canonizeName
188 }
189 def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
190 val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
191 if(m.isMay) {
192 '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpression(typeReference,v,v.valueVariable)» check(!«v.valueSetted»||«v.valueVariable»==«target»));'''
193 } else { // Must or current
194 '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpression(typeReference,v,target)»'''
195 }
196 }
197
198 private def hasValueExpression(List<VariableMapping> variableMapping, PVariable v, String target) {
199 hasValueExpression(
200 variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range,
201 v,
202 target
203 )
204 }
205 private def dispatch hasValueExpression(BoolTypeReference typeReference, PVariable v, String target) '''BooleanElement.value(«v.canonizeName»,«target»);'''
206 private def dispatch hasValueExpression(IntTypeReference typeReference, PVariable v, String target) '''IntegerElement.value(«v.canonizeName»,«target»);'''
207 private def dispatch hasValueExpression(RealTypeReference typeReference, PVariable v, String target) '''RealElement.value(«v.canonizeName»,«target»);'''
208 private def dispatch hasValueExpression(StringTypeReference typeReference, PVariable v, String target) '''StringElement.value(«v.canonizeName»,«target»);'''
209 private def dispatch hasValueExpression(TypeReference typeReference, PVariable v, String target) {
210 throw new UnsupportedOperationException('''Unsupported primitive type reference: «typeReference.class»''')
211 }
212
213 dispatch def transformConstraint(ExpressionEvaluation e, Modality modality, List<VariableMapping> variableMapping) {
214 if(e.outputVariable!==null) {
215 throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
216 } else {
217 val expression = expressionExtractor.extractExpression(e.evaluator)
218 if(modality.isMay) {
219 return '''
220 «FOR variable: e.affectedVariables»
221 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
222 «ENDFOR»
223 check(
224 «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»
225 ||
226 («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»)
227 );
228 '''
229 } else { // Must or Current
230 return '''
231 «FOR variable: e.affectedVariables»
232 PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
233 «ENDFOR»
234 check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»);
235 '''
236 }
237 }
238 }
239
240 dispatch def transformConstraint(PConstraint c, Modality modality, List<VariableMapping> variableMapping) {
241 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
242 }
243} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
new file mode 100644
index 00000000..303c87b9
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -0,0 +1,109 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
2
3import java.util.Map
4import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
5import org.eclipse.xtext.xbase.XBinaryOperation
6import org.eclipse.xtext.xbase.XExpression
7import org.eclipse.xtext.xbase.XFeatureCall
8import org.eclipse.xtext.xbase.XMemberFeatureCall
9import org.eclipse.xtext.xbase.XNumberLiteral
10import org.eclipse.xtext.xbase.XUnaryOperation
11
12class PExpressionGenerator {
13 static val N_Base = "org.eclipse.xtext.xbase.lib."
14
15 static val N_PLUS1 = "operator_plus"
16 static val N_MINUS1 = "operator_minus"
17
18 static val N_MINUS2 = "operator_minus"
19 static val N_PLUS2 = "operator_plus"
20 static val N_POWER = "operator_power"
21 static val N_MULTIPLY = "operator_multiply"
22 static val N_DIVIDE = "operator_divide"
23 static val N_MODULO = "operator_modulo"
24 static val N_LESSTHAN = "operator_lessThan"
25 static val N_LESSEQUALSTHAN = "operator_lessEqualsThan"
26 static val N_GREATERTHAN = "operator_greaterThan"
27 static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan"
28 static val N_EQUALS = "operator_equals"
29 static val N_NOTEQUALS = "operator_notEquals"
30 static val N_EQUALS3 = "operator_tripleEquals"
31 static val N_NOTEQUALS3 = "operator_tripleNotEquals"
32
33 protected def isN(String name, String s) {
34 val res = name.startsWith(N_Base) && name.endsWith(s)
35 //println('''[«res»] «name» ?= «N_Base»*«s»''')
36 return res
37 }
38
39 static val N_POWER2 = "java.lang.Math.pow"
40
41 def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName) {
42 val left = e.leftOperand.translateExpression(valueName)
43 val right = e.rightOperand.translateExpression(valueName)
44 val feature = e.feature.qualifiedName
45 if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''}
46 else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' }
47 else if(feature.isN(N_POWER)) { return '''(«left»^«right»)''' }
48 else if(feature.isN(N_MULTIPLY)) { return '''(«left»*«right»)''' }
49 else if(feature.isN(N_DIVIDE)) { return '''(«left»/«right»)''' }
50 else if(feature.isN(N_MODULO)) { return '''(«left»%«right»)''' }
51 else if(feature.isN(N_LESSTHAN)) { return '''(«left»<«right»)''' }
52 else if(feature.isN(N_LESSEQUALSTHAN)) { return '''(«left»<=«right»)''' }
53 else if(feature.isN(N_GREATERTHAN)) { return '''(«left»>«right»)''' }
54 else if(feature.isN(N_GREATEREQUALTHAN)) { return '''(«left»>=«right»)''' }
55 else if(feature.isN(N_EQUALS)) { return '''(«left»==«right»)''' }
56 else if(feature.isN(N_NOTEQUALS)) { return '''(«left»!=«right»)''' }
57 else if(feature.isN(N_EQUALS3)) { return '''(«left»===«right»)''' }
58 else if(feature.isN(N_NOTEQUALS3)) { return '''(«left»!==«right»)''' }
59 else {
60 println("-> " + e.feature+","+e.class)
61 println("-> " + e.leftOperand)
62 println("-> " + e.rightOperand)
63 println("-> " + e.feature.qualifiedName)
64 throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''')
65 }
66 }
67
68 def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName) {
69 val operand = e.operand.translateExpression(valueName)
70 val feature = e.feature.qualifiedName
71 if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''}
72 else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''}
73 else{
74 println("-> " + e.feature+","+e.class)
75 println("-> " + e.operand)
76 println("-> " + e.feature.qualifiedName)
77 throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''')
78 }
79 }
80
81 def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName) {
82 val transformedArguments = e.actualArguments.map[translateExpression(valueName)]
83 val feature = e.feature.qualifiedName
84 if(feature == N_POWER2) {
85 return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)'''
86 }else {
87 println(e.feature+","+e.class)
88 println(e.actualArguments.join(", "))
89 println(e.feature.qualifiedName)
90 throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''')
91 }
92 }
93
94 def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName) {
95 val featureName = e.feature.qualifiedName
96 val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head
97 if(entryWithName !== null) {
98 return entryWithName.value
99 } else {
100 throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
101 }
102 }
103
104 def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName) '''«l.value»'''
105
106 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName) {
107 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
108 }
109} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
index d4c76bb4..379e334a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend
@@ -170,6 +170,7 @@ class PatternGenerator {
170 ///////////////////////// 170 /////////////////////////
171 // 0.1 Existence 171 // 0.1 Existence
172 ///////////////////////// 172 /////////////////////////
173 /** [[exist(element)]]=1 */
173 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 174 private pattern mustExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
174 find interpretation(problem,interpretation); 175 find interpretation(problem,interpretation);
175 LogicProblem.elements(problem,element); 176 LogicProblem.elements(problem,element);
@@ -178,6 +179,7 @@ class PatternGenerator {
178 PartialInterpretation.newElements(interpretation,element); 179 PartialInterpretation.newElements(interpretation,element);
179 } 180 }
180 181
182 /** [[exist(element)]]>=1/2 */
181 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 183 private pattern mayExist(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
182 find mustExist(problem,interpretation,element); 184 find mustExist(problem,interpretation,element);
183 } or { 185 } or {
@@ -198,57 +200,143 @@ class PatternGenerator {
198 //////////////////////// 200 ////////////////////////
199 // 0.2 Equivalence 201 // 0.2 Equivalence
200 //////////////////////// 202 ////////////////////////
201 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 203 pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement)
204 // For non-primitive type. Boolean types always must equivalent or cannot equivalent
205 {
202 find mayExist(problem,interpretation,a); 206 find mayExist(problem,interpretation,a);
203 find mayExist(problem,interpretation,b); 207 find mayExist(problem,interpretation,b);
204 a == b; 208 a == b;
209 } or {
210 find mayExist(problem,interpretation,a);
211 find mayExist(problem,interpretation,b);
212 IntegerElement(a);
213 IntegerElement(b);
214 PrimitiveElement.valueSet(a,false);
215 } or {
216 find mayExist(problem,interpretation,a);
217 find mayExist(problem,interpretation,b);
218 IntegerElement(a);
219 IntegerElement(b);
220 PrimitiveElement.valueSet(b,false);
221 } or {
222 find mayExist(problem,interpretation,a);
223 find mayExist(problem,interpretation,b);
224 RealElement(a);
225 RealElement(b);
226 PrimitiveElement.valueSet(a,false);
227 } or {
228 find mayExist(problem,interpretation,a);
229 find mayExist(problem,interpretation,b);
230 RealElement(a);
231 RealElement(b);
232 PrimitiveElement.valueSet(b,false);
233 } or {
234 find mayExist(problem,interpretation,a);
235 find mayExist(problem,interpretation,b);
236 RealElement(a);
237 IntegerElement(b);
238 PrimitiveElement.valueSet(a,false);
239 } or {
240 find mayExist(problem,interpretation,a);
241 find mayExist(problem,interpretation,b);
242 RealElement(a);
243 IntegerElement(b);
244 PrimitiveElement.valueSet(b,false);
245 } or {
246 find mayExist(problem,interpretation,a);
247 find mayExist(problem,interpretation,b);
248 IntegerElement(a);
249 RealElement(b);
250 PrimitiveElement.valueSet(a,false);
251 } or {
252 find mayExist(problem,interpretation,a);
253 find mayExist(problem,interpretation,b);
254 IntegerElement(a);
255 RealElement(b);
256 PrimitiveElement.valueSet(b,false);
257 } or {
258 find mayExist(problem,interpretation,a);
259 find mayExist(problem,interpretation,b);
260 StringElement(a);
261 StringElement(b);
262 PrimitiveElement.valueSet(a,false);
263 } or {
264 find mayExist(problem,interpretation,a);
265 find mayExist(problem,interpretation,b);
266 StringElement(a);
267 StringElement(b);
268 PrimitiveElement.valueSet(b,false);
205 } 269 }
270
206 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 271 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
272 // For non-primitive and Boolean primitive type
207 find mustExist(problem,interpretation,a); 273 find mustExist(problem,interpretation,a);
208 find mustExist(problem,interpretation,b); 274 find mustExist(problem,interpretation,b);
209 a == b; 275 a == b;
276 } or {
277 find mustExist(problem,interpretation,a);
278 find mustExist(problem,interpretation,b);
279 PrimitiveElement.valueSet(a,true);
280 PrimitiveElement.valueSet(b,true);
281 IntegerElement.value(a,value);
282 IntegerElement.value(b,value);
283 } or {
284 find mustExist(problem,interpretation,a);
285 find mustExist(problem,interpretation,b);
286 PrimitiveElement.valueSet(a,true);
287 PrimitiveElement.valueSet(b,true);
288 RealElement.value(a,value);
289 RealElement.value(b,value);
290 } or {
291 find mustExist(problem,interpretation,a);
292 find mustExist(problem,interpretation,b);
293 PrimitiveElement.valueSet(a,true);
294 PrimitiveElement.valueSet(b,true);
295 RealElement.value(a,value);
296 IntegerElement.value(b,value);
297 } or {
298 find mustExist(problem,interpretation,a);
299 find mustExist(problem,interpretation,b);
300 PrimitiveElement.valueSet(a,true);
301 PrimitiveElement.valueSet(b,true);
302 IntegerElement.value(a,value);
303 RealElement.value(b,value);
304 } or {
305 find mustExist(problem,interpretation,a);
306 find mustExist(problem,interpretation,b);
307 PrimitiveElement.valueSet(a,true);
308 PrimitiveElement.valueSet(b,true);
309 StringElement.value(a,value);
310 StringElement.value(b,value);
210 } 311 }
211 312
212 ////////////////////////
213 // 0.3 Required Patterns by TypeIndexer
214 ////////////////////////
215 «typeIndexer.requiredQueries»
216
217 ////////// 313 //////////
218 // 1. Problem-Specific Base Indexers 314 // 1. Problem-Specific Base Indexers
219 ////////// 315 //////////
220 // 1.1 Type Indexers 316 // 1.1 Type Indexers
221 ////////// 317 //////////
222 // 1.1.1 primitive Type Indexers 318 // 1.1.1 Required Patterns by TypeIndexer
223 ////////// 319 //////////
224««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 320 «typeIndexer.requiredQueries»
225««« find interpretation(problem,interpretation); 321 //////////
226««« PartialInterpretation.booleanelements(interpretation,element); 322 // 1.1.2 primitive Type Indexers
227««« } 323 //////////
228««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 324 // Currently unused. Refer primitive types as:
229««« find interpretation(problem,interpretation); 325 // > PrimitiveElement(element)
230««« PartialInterpretation.integerelements(interpretation,element); 326 // specific types are referred as:
231««« } or { 327 // > BooleanElement(variableName)
232««« find interpretation(problem,interpretation); 328 // > IntegerElement(variableName)
233««« PartialInterpretation.newIntegers(interpetation,element); 329 // > RealElement(variableName)
234««« } 330 // > StringElement(variableName)
235««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { 331 // And their value as
236««« find interpretation(problem,interpretation); 332 // > BooleanElement.value(variableName,value)
237««« PartialInterpretation.realelements(interpretation,element); 333 // > IntegerElement.value(variableName,value)
238««« } or { 334 // > RealElement.value(variableName,value)
239««« find interpretation(problem,interpretation); 335 // > StringElement.value(variableName,value)
240««« PartialInterpretation.newReals(interpetation,element); 336 // Whether a value is set is defined by:
241««« } 337 // > PrimitiveElement.valueSet(variableName,isFilled);
242««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
243««« find interpretation(problem,interpretation);
244««« PartialInterpretation.stringelements(interpretation,element);
245««« } or {
246««« find interpretation(problem,interpretation);
247««« PartialInterpretation.newStrings(interpetation,element);
248««« }
249
250 ////////// 338 //////////
251 // 1.1.2 domain-specific Type Indexers 339 // 1.1.3 domain-specific Type Indexers
252 ////////// 340 //////////
253 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» 341 «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)»
254 342
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
index 9723373f..bd6e3e6e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend
@@ -5,35 +5,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 5import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality 6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import java.util.Map 7import java.util.Map
8import org.eclipse.emf.ecore.EAttribute
9import org.eclipse.emf.ecore.EEnumLiteral
10import org.eclipse.emf.ecore.EReference
11import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
12import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
13import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey
14import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
15import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 8import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
16import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality
17import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter
18import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality
19import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
20import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure 9import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure
21import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue
22import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall
23import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 10import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
25 11
26import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 12import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
27import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
28 13
29class RelationDefinitionIndexer { 14class RelationDefinitionIndexer {
30 val PatternGenerator base; 15 public val PatternGenerator base;
16 val PConstraintTransformer constraintTransformer;
31 17
32 new(PatternGenerator base) { 18 new(PatternGenerator base) {
33 this.base = base 19 this.base = base
20 this.constraintTransformer = new PConstraintTransformer(this);
34 } 21 }
35 22
36 public def generateRelationDefinitions( 23 def generateRelationDefinitions(
37 LogicProblem problem, 24 LogicProblem problem,
38 Iterable<RelationDefinition> relations, 25 Iterable<RelationDefinition> relations,
39 Map<String,PQuery> fqn2PQuery) { 26 Map<String,PQuery> fqn2PQuery) {
@@ -74,7 +61,7 @@ class RelationDefinitionIndexer {
74 private def relationDefinitionName(RelationDefinition relation, Modality modality) 61 private def relationDefinitionName(RelationDefinition relation, Modality modality)
75 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' 62 '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»'''
76 63
77 private def canonizeName(PVariable v) { 64 def canonizeName(PVariable v) {
78 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' 65 return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»'''
79 } 66 }
80 67
@@ -87,7 +74,7 @@ class RelationDefinitionIndexer {
87 «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ 74 «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{
88 find interpretation(problem,interpretation); 75 find interpretation(problem,interpretation);
89 «FOR constraint : body.constraints» 76 «FOR constraint : body.constraints»
90 «constraint.transformConstraint(modality)» 77 «this.constraintTransformer.transformConstraint(constraint,modality,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
91 «ENDFOR» 78 «ENDFOR»
92 }«ENDFOR» 79 }«ENDFOR»
93 ''' 80 '''
@@ -104,158 +91,14 @@ class RelationDefinitionIndexer {
104 ''' 91 '''
105 } 92 }
106 93
107 private def toMustMay(Modality modality) { 94 def toMustMay(Modality modality) {
108 if(modality == Modality::MAY) return Modality::MAY 95 if(modality == Modality::MAY) return Modality::MAY
109 else return Modality::MUST 96 else return Modality::MUST
110 } 97 }
111 98
112 def public referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' 99 def referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) '''
113 «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»); 100 «IF !positive»neg «ENDIF»find «IF transitive»twoParam_«ENDIF»«modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(«IF !transitive»problem,interpretation,«ENDIF»«variables.join(',')»);
114 ''' 101 '''
115 102
116 private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) {
117 val touple = constraint.variablesTuple
118 if(touple.size == 1) {
119 val inputKey = constraint.equivalentJudgement.inputKey
120 if(inputKey instanceof EClassTransitiveInstancesKey) {
121 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
122 constraint.getVariableInTuple(0).canonizeName)
123 } else if(inputKey instanceof EDataTypeInSlotsKey){
124 return '''// type constraint is enforced by construction'''
125 }
126
127 } else if(touple.size == 2){
128 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
129 if(key instanceof EReference) {
130 return base.referRelationByName(
131 key,
132 constraint.getVariableInTuple(0).canonizeName,
133 constraint.getVariableInTuple(1).canonizeName,
134 modality.toMustMay)
135 } else if (key instanceof EAttribute) {
136 return base.referAttributeByName(key,
137 constraint.getVariableInTuple(0).canonizeName,
138 constraint.getVariableInTuple(1).canonizeName,
139 modality.toMustMay)
140 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
141 } else {
142 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
143 }
144 }
145 private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) {
146 val touple = constraint.variablesTuple
147 if(touple.size == 1) {
148 val inputKey = constraint.equivalentJudgement.inputKey
149 if(inputKey instanceof EClassTransitiveInstancesKey) {
150 return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,
151 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)
152 } else if(inputKey instanceof EDataTypeInSlotsKey){
153 return '''// type constraint is enforced by construction'''
154 }
155
156 } else if(touple.size == 2){
157 val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey
158 if(key instanceof EReference) {
159 return base.referRelationByName(
160 key,
161 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
162 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
163 modality.toMustMay)
164 } else if (key instanceof EAttribute) {
165 return base.referAttributeByName(key,
166 (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,
167 (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,
168 modality.toMustMay)
169 } else throw new UnsupportedOperationException('''unknown key: «key.class»''')
170 } else {
171 throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')
172 }
173 }
174
175 private dispatch def transformConstraint(Equality equality, Modality modality) {
176 val a = equality.who
177 val b = equality.withWhom
178 transformEquality(modality.toMustMay, a, b)
179 }
180
181 private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) {
182 if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
183 else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
184 }
185
186 private dispatch def transformConstraint(Inequality inequality, Modality modality) {
187 val a = inequality.who
188 val b = inequality.withWhom
189 if(modality.isCurrent) {
190 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
191 } else if(modality.isMust) {
192 return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
193 } else { // modality.isMay
194 return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);'''
195 }
196 }
197
198 private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) {
199 val params = (0..<pcall.actualParametersTuple.size).map[index |
200 val variable = pcall.actualParametersTuple.get(index) as PVariable
201 return variable.canonizeName
202 ]
203 return referPattern(pcall.referredQuery,params,modality.dual,false,false)
204 }
205 103
206 private dispatch def transformConstraint(PositivePatternCall pcall, Modality modality) {
207 val params = (0..<pcall.variablesTuple.size).map[index |
208 val variable = pcall.variablesTuple.get(index) as PVariable
209 return variable.canonizeName
210 ]
211 return referPattern(pcall.referredQuery,params,modality,true,false)
212 }
213 private dispatch def transformConstraint(BinaryTransitiveClosure pcall, Modality modality) {
214 val params = (0..1).map[index |
215 val variable = pcall.getVariableInTuple(index) as PVariable
216 return variable.canonizeName
217 ]
218 return referPattern(pcall.referredQuery,params,modality,true,true)
219 }
220 private dispatch def transformConstraint(ExportedParameter e, Modality modality) {
221 return '''// «e.parameterName» is exported'''
222 }
223 private dispatch def transformConstraint(ConstantValue c, Modality modality) {
224 val target = c.supplierKey
225
226 var String targetString;
227 var String additionalDefinition;
228 if(target instanceof EEnumLiteral) {
229 targetString = '''const_«target.name»_«target.EEnum.name»'''
230 additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.EEnum.name»"); //LogicProblem.elements(problem,«targetString»);'''
231 } else if(target instanceof Integer) {
232 targetString = '''const_«target»_Integer'''
233 additionalDefinition = '''IntegerElement.value(«targetString»,«target»);'''
234 } else if(target instanceof Boolean) {
235 targetString = '''const_«target»_Boolean'''
236 additionalDefinition = '''BooleanElement.value(«targetString»,«target»);'''
237 } else if(target instanceof String) {
238 targetString = '''const_«target»_String'''
239 additionalDefinition = '''StringElement.value(«targetString»,"«target»");'''
240 } else if(target instanceof Double) {
241 targetString = '''const_«target»_Number'''
242 additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
243 } else if(target instanceof Float) {
244 targetString = '''const_«target»_Number'''
245 additionalDefinition = '''RealElement.value(«targetString»,"«target»");'''
246 } else {
247 throw new UnsupportedOperationException('''Unknown constant type: «target.class»''')
248 }
249
250 val source = c.variablesTuple
251 var String sourceName
252 if(source.size == 1)
253 sourceName = (source.get(0) as PVariable).canonizeName
254 else throw new UnsupportedOperationException("unknown source")
255 return '''«sourceName» == «targetString»;«additionalDefinition»''';
256 }
257
258 private dispatch def transformConstraint(PConstraint c, Modality modality) {
259 throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''')
260 }
261} \ No newline at end of file 104} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
index d1d57189..41eb75a8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend
@@ -48,5 +48,7 @@ abstract class TypeIndexer {
48 public def dispatch CharSequence referPrimitiveValue(String variableName, String value) { 48 public def dispatch CharSequence referPrimitiveValue(String variableName, String value) {
49 '''StringElement.value(«variableName»,"«value»");''' 49 '''StringElement.value(«variableName»,"«value»");'''
50 } 50 }
51 51 public def CharSequence referPrimitiveFilled(String variableName, boolean isFilled) {
52 '''PrimitiveElement.valueSet(«variableName»,«isFilled»);'''
53 }
52} \ No newline at end of file 54} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
index f7a1ce4f..d37acb6d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
@@ -42,6 +42,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
42import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral 42import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral 43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
44import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation 44import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
45import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
45 46
46@Data class Problem2PartialInterpretationTrace { 47@Data class Problem2PartialInterpretationTrace {
47 Map<TypeDeclaration, PartialComplexTypeInterpretation> type2Interpretation 48 Map<TypeDeclaration, PartialComplexTypeInterpretation> type2Interpretation
@@ -233,7 +234,11 @@ class PartialInterpretationInitialiser {
233 234
234 def private Map<RelationDeclaration, PartialRelationInterpretation> initRelations(PartialInterpretation interpretation, PrimitiveValueTrace trace) { 235 def private Map<RelationDeclaration, PartialRelationInterpretation> initRelations(PartialInterpretation interpretation, PrimitiveValueTrace trace) {
235 val Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap 236 val Map<RelationDeclaration, PartialRelationInterpretation> relation2Interpretation = new HashMap
236 for(relation : interpretation.problem.relations.filter(RelationDeclaration)) { 237 val definedRelationDeclarations = interpretation.problem.relations.filter(RelationDefinition).map[defines]
238 val undefinedRelationDeclarations = interpretation.problem.relations.filter(RelationDeclaration).filter[
239 declared | !definedRelationDeclarations.exists[defined | defined === declared]
240 ]
241 for(relation : undefinedRelationDeclarations) {
237 val partialInterpretation = relation.initialisePartialRelationInterpretation 242 val partialInterpretation = relation.initialisePartialRelationInterpretation
238 interpretation.partialrelationinterpretation += partialInterpretation 243 interpretation.partialrelationinterpretation += partialInterpretation
239 relation2Interpretation.put(relation,partialInterpretation) 244 relation2Interpretation.put(relation,partialInterpretation)
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 6639e5f3..bdc48b8d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
@@ -59,7 +59,6 @@ class ViatraReasoner extends LogicReasoner{
59 val transformationStartTime = System.nanoTime 59 val transformationStartTime = System.nanoTime
60 60
61 61
62
63 val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output 62 val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output
64 if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { 63 if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
65 workspace.writeModel(emptySolution,"init.partialmodel") 64 workspace.writeModel(emptySolution,"init.partialmodel")
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend
new file mode 100644
index 00000000..542289d4
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/GraphvizV8WithMemory.xtend
@@ -0,0 +1,16 @@
1package hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz
2
3import guru.nidi.graphviz.engine.GraphvizV8Engine
4
5class GraphvizV8WithMemory extends GraphvizV8Engine {
6 val int memory;
7 new(int memory) {
8 this.memory = memory
9 //this.
10 }
11
12 override protected jsInitEnv() {
13 println super.jsInitEnv()
14 super.jsInitEnv()
15 }
16}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend
index b067ba7d..6f003f80 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.visualisation/src/hu/bme/mit/inf/dslreasoner/visualisation/pi2graphviz/VisualisationQueque.xtend
@@ -3,15 +3,15 @@ package hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz
3import guru.nidi.graphviz.engine.Format 3import guru.nidi.graphviz.engine.Format
4import guru.nidi.graphviz.engine.Graphviz 4import guru.nidi.graphviz.engine.Graphviz
5import guru.nidi.graphviz.engine.GraphvizEngine 5import guru.nidi.graphviz.engine.GraphvizEngine
6import guru.nidi.graphviz.engine.GraphvizV8Engine
7import guru.nidi.graphviz.model.Graph 6import guru.nidi.graphviz.model.Graph
8import java.io.File 7import java.io.File
9import java.io.IOException 8import java.io.IOException
10import java.util.concurrent.BlockingQueue 9import java.util.concurrent.BlockingQueue
11import java.util.concurrent.CompletableFuture 10import java.util.concurrent.CompletableFuture
12import java.util.concurrent.LinkedBlockingQueue 11import java.util.concurrent.LinkedBlockingQueue
13import org.eclipse.xtend.lib.annotations.Data
14import java.util.function.Consumer 12import java.util.function.Consumer
13import org.eclipse.xtend.lib.annotations.Data
14import guru.nidi.graphviz.engine.GraphvizV8Engine
15 15
16class VisualisationQueque { 16class VisualisationQueque {
17 val BlockingQueue<VisualisationQueueEntry> taskQueue = new LinkedBlockingQueue 17 val BlockingQueue<VisualisationQueueEntry> taskQueue = new LinkedBlockingQueue
@@ -45,7 +45,7 @@ class VisualisationQueque {
45 } else { 45 } else {
46 runnerThread = new Thread(new Runnable() { 46 runnerThread = new Thread(new Runnable() {
47 override run() { 47 override run() {
48 val engine = new GraphvizV8Engine() 48 val engine = new GraphvizV8Engine
49 val nullConsumer = new Consumer<GraphvizEngine>() { 49 val nullConsumer = new Consumer<GraphvizEngine>() {
50 override accept(GraphvizEngine t) {} 50 override accept(GraphvizEngine t) {}
51 } 51 }
@@ -69,7 +69,7 @@ class VisualisationQueque {
69 private def execute(GraphvizEngine engine, Graph document, File targetFile, Format format) { 69 private def execute(GraphvizEngine engine, Graph document, File targetFile, Format format) {
70 Graphviz.useEngine(engine); 70 Graphviz.useEngine(engine);
71 try { 71 try {
72 Graphviz.fromGraph(document).render(format).toFile(targetFile) 72 Graphviz.fromGraph(document).totalMemory(536870912).render(format).toFile(targetFile)
73 return null 73 return null
74 } catch(IOException e){ 74 } catch(IOException e){
75 return e.message 75 return e.message
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-07 22:03:51 +0000