diff options
19 files changed, 50 insertions, 294 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/.gitignore index 1a9ea807..3197db31 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/.gitignore +++ b/Application/hu.bme.mit.inf.dslreasoner.application/.gitignore | |||
@@ -1,2 +1,2 @@ | |||
1 | /bin/ | 1 | /bin/ |
2 | /xtend-gen/* \ No newline at end of file | 2 | /xtend-gen/ \ No newline at end of file |
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index fd50ad51..bb21f8ee 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend | |||
@@ -29,6 +29,7 @@ import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel | |||
29 | import org.eclipse.xtext.EcoreUtil2 | 29 | import org.eclipse.xtext.EcoreUtil2 |
30 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 30 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | 31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver |
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | ||
32 | 33 | ||
33 | class SolverLoader { | 34 | class SolverLoader { |
34 | def loadSolver(Solver solver, Map<String, String> config) { | 35 | def loadSolver(Solver solver, Map<String, String> config) { |
@@ -139,6 +140,14 @@ class SolverLoader { | |||
139 | val stringValue = config.get("fitness-objectCreationCosts") | 140 | val stringValue = config.get("fitness-objectCreationCosts") |
140 | c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) | 141 | c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) |
141 | } | 142 | } |
143 | if (config.containsKey("numeric-solver")) { | ||
144 | val stringValue = config.get("numeric-solver") | ||
145 | c.numericSolverSelection = switch (stringValue) { | ||
146 | case "dreal": NumericSolverSelection.DREAL | ||
147 | case "z3": NumericSolverSelection.Z3 | ||
148 | default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue) | ||
149 | } | ||
150 | } | ||
142 | if (config.containsKey("scopePropagator")) { | 151 | if (config.containsKey("scopePropagator")) { |
143 | val stringValue = config.get("scopePropagator") | 152 | val stringValue = config.get("scopePropagator") |
144 | c.scopePropagatorStrategy = switch (stringValue) { | 153 | c.scopePropagatorStrategy = switch (stringValue) { |
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/.gitignore deleted file mode 100644 index bca5f28f..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/.gitignore +++ /dev/null | |||
@@ -1,2 +0,0 @@ | |||
1 | /.ApplicationConfigurationStandaloneSetup.java._trace | ||
2 | /.ApplicationConfigurationRuntimeModule.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/.gitignore deleted file mode 100644 index 5c89fb5b..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/.gitignore +++ /dev/null | |||
@@ -1,9 +0,0 @@ | |||
1 | /.GenerationTaskExecutor.java._trace | ||
2 | /.NullWorkspace.java._trace | ||
3 | /.MetamodelLoader.java._trace | ||
4 | /.ModelLoader.java._trace | ||
5 | /.QueryLoader.java._trace | ||
6 | /.ScopeLoader.java._trace | ||
7 | /.ScriptConsole.java._trace | ||
8 | /.ScriptExecutor.java._trace | ||
9 | /.SolverLoader.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/util/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/util/.gitignore deleted file mode 100644 index df803ce6..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/util/.gitignore +++ /dev/null | |||
@@ -1,3 +0,0 @@ | |||
1 | /.MyModule.java._trace | ||
2 | /.ApplicationConfigurationParser.java._trace | ||
3 | /.VQLParser.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/generator/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/generator/.gitignore deleted file mode 100644 index 412c1356..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/generator/.gitignore +++ /dev/null | |||
@@ -1 +0,0 @@ | |||
1 | /.ApplicationConfigurationGenerator.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/linking/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/linking/.gitignore deleted file mode 100644 index 94eaff7d..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/linking/.gitignore +++ /dev/null | |||
@@ -1,2 +0,0 @@ | |||
1 | /.ApplicationConfigurationLinkingService.java._trace | ||
2 | /.PreloadedMetamodelProvider.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/scoping/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/scoping/.gitignore deleted file mode 100644 index 9fe94100..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/scoping/.gitignore +++ /dev/null | |||
@@ -1 +0,0 @@ | |||
1 | /.ApplicationConfigurationScopeProvider.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/.gitignore deleted file mode 100644 index 7caadb6b..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/.gitignore +++ /dev/null | |||
@@ -1,3 +0,0 @@ | |||
1 | /.MetamodelValidator.java._trace | ||
2 | /.ApplicationConfigurationValidator.java._trace | ||
3 | /.QueryAndMetamodelValidator.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.java b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.java deleted file mode 100644 index 872814b8..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.java +++ /dev/null | |||
@@ -1,157 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.application.validation; | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; | ||
4 | import java.util.Collections; | ||
5 | import java.util.LinkedList; | ||
6 | import java.util.List; | ||
7 | import org.eclipse.emf.common.util.EList; | ||
8 | import org.eclipse.emf.ecore.EAttribute; | ||
9 | import org.eclipse.emf.ecore.EClass; | ||
10 | import org.eclipse.emf.ecore.EDataType; | ||
11 | import org.eclipse.emf.ecore.EEnum; | ||
12 | import org.eclipse.emf.ecore.EEnumLiteral; | ||
13 | import org.eclipse.emf.ecore.EReference; | ||
14 | import org.eclipse.emf.ecore.EcorePackage; | ||
15 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
16 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
17 | import org.eclipse.xtext.xbase.lib.Extension; | ||
18 | |||
19 | @SuppressWarnings("all") | ||
20 | public class MetamodelValidator { | ||
21 | public LinkedList<String> validateMetamodel(final EcoreMetamodelDescriptor descriptor) { | ||
22 | final LinkedList<String> errors = new LinkedList<String>(); | ||
23 | this.allSupertypesAreIncluded(descriptor.getClasses(), errors); | ||
24 | this.allEnumTypesareIncluded(descriptor.getEnums(), descriptor.getLiterals(), errors); | ||
25 | this.referenceEndpointsAreIncluded(descriptor.getClasses(), descriptor.getReferences(), errors); | ||
26 | this.attributeSourcePontIsIncluded(descriptor.getClasses(), descriptor.getAttributes(), errors); | ||
27 | this.attributeTargetIsSupported(descriptor.getAttributes(), errors); | ||
28 | return errors; | ||
29 | } | ||
30 | |||
31 | private boolean supportedEDataType(final EDataType dataType) { | ||
32 | @Extension | ||
33 | final EcorePackage l = EcorePackage.eINSTANCE; | ||
34 | EDataType _eInt = l.getEInt(); | ||
35 | EDataType _eBoolean = l.getEBoolean(); | ||
36 | EDataType _eString = l.getEString(); | ||
37 | EDataType _eDouble = l.getEDouble(); | ||
38 | EDataType _eFloat = l.getEFloat(); | ||
39 | return Collections.<EDataType>unmodifiableList(CollectionLiterals.<EDataType>newArrayList(_eInt, _eBoolean, _eString, _eDouble, _eFloat)).contains(dataType); | ||
40 | } | ||
41 | |||
42 | public void allSupertypesAreIncluded(final List<EClass> classes, final List<String> errors) { | ||
43 | for (final EClass c : classes) { | ||
44 | EList<EClass> _eSuperTypes = c.getESuperTypes(); | ||
45 | for (final EClass s : _eSuperTypes) { | ||
46 | boolean _contains = classes.contains(s); | ||
47 | boolean _not = (!_contains); | ||
48 | if (_not) { | ||
49 | StringConcatenation _builder = new StringConcatenation(); | ||
50 | _builder.append("Metamodel contains \""); | ||
51 | String _name = c.getName(); | ||
52 | _builder.append(_name); | ||
53 | _builder.append("\" but not contains its supertype \""); | ||
54 | String _name_1 = s.getName(); | ||
55 | _builder.append(_name_1); | ||
56 | _builder.append("\"!"); | ||
57 | errors.add(_builder.toString()); | ||
58 | } | ||
59 | } | ||
60 | } | ||
61 | } | ||
62 | |||
63 | public void allEnumTypesareIncluded(final List<EEnum> enums, final List<EEnumLiteral> literals, final List<String> errors) { | ||
64 | for (final EEnumLiteral l : literals) { | ||
65 | boolean _contains = enums.contains(l.getEEnum()); | ||
66 | boolean _not = (!_contains); | ||
67 | if (_not) { | ||
68 | StringConcatenation _builder = new StringConcatenation(); | ||
69 | _builder.append("Metamodel contains literal \""); | ||
70 | String _name = l.getName(); | ||
71 | _builder.append(_name); | ||
72 | _builder.append("\" but does not contains enum \""); | ||
73 | String _name_1 = l.getEEnum().getName(); | ||
74 | _builder.append(_name_1); | ||
75 | _builder.append("\"!"); | ||
76 | errors.add(_builder.toString()); | ||
77 | } | ||
78 | } | ||
79 | } | ||
80 | |||
81 | public void referenceEndpointsAreIncluded(final List<EClass> classes, final List<EReference> references, final List<String> errors) { | ||
82 | for (final EReference reference : references) { | ||
83 | { | ||
84 | final EClass src = reference.getEContainingClass(); | ||
85 | boolean _contains = classes.contains(src); | ||
86 | boolean _not = (!_contains); | ||
87 | if (_not) { | ||
88 | StringConcatenation _builder = new StringConcatenation(); | ||
89 | _builder.append("Metamodel contains reference \""); | ||
90 | String _name = reference.getName(); | ||
91 | _builder.append(_name); | ||
92 | _builder.append("\" but does not contains its source type \""); | ||
93 | String _name_1 = src.getName(); | ||
94 | _builder.append(_name_1); | ||
95 | _builder.append("\"!"); | ||
96 | errors.add(_builder.toString()); | ||
97 | } | ||
98 | final EClass trg = reference.getEReferenceType(); | ||
99 | boolean _contains_1 = classes.contains(trg); | ||
100 | boolean _not_1 = (!_contains_1); | ||
101 | if (_not_1) { | ||
102 | StringConcatenation _builder_1 = new StringConcatenation(); | ||
103 | _builder_1.append("Metamodel contains reference \""); | ||
104 | String _name_2 = reference.getName(); | ||
105 | _builder_1.append(_name_2); | ||
106 | _builder_1.append("\" but does not contains its target type \""); | ||
107 | String _name_3 = trg.getName(); | ||
108 | _builder_1.append(_name_3); | ||
109 | _builder_1.append("\"!"); | ||
110 | errors.add(_builder_1.toString()); | ||
111 | } | ||
112 | } | ||
113 | } | ||
114 | } | ||
115 | |||
116 | public void attributeSourcePontIsIncluded(final List<EClass> classes, final List<EAttribute> attributes, final List<String> errors) { | ||
117 | for (final EAttribute attribute : attributes) { | ||
118 | { | ||
119 | final Class<?> src = attribute.getContainerClass(); | ||
120 | boolean _contains = classes.contains(src); | ||
121 | boolean _not = (!_contains); | ||
122 | if (_not) { | ||
123 | StringConcatenation _builder = new StringConcatenation(); | ||
124 | _builder.append("Metamodel contains attribute \""); | ||
125 | String _name = attribute.getName(); | ||
126 | _builder.append(_name); | ||
127 | _builder.append("\" but does not contains its source type \""); | ||
128 | String _name_1 = src.getName(); | ||
129 | _builder.append(_name_1); | ||
130 | _builder.append("\"!"); | ||
131 | errors.add(_builder.toString()); | ||
132 | } | ||
133 | } | ||
134 | } | ||
135 | } | ||
136 | |||
137 | public void attributeTargetIsSupported(final List<EAttribute> attributes, final List<String> errors) { | ||
138 | for (final EAttribute attribute : attributes) { | ||
139 | { | ||
140 | final EDataType trg = attribute.getEAttributeType(); | ||
141 | boolean _supportedEDataType = this.supportedEDataType(trg); | ||
142 | boolean _not = (!_supportedEDataType); | ||
143 | if (_not) { | ||
144 | StringConcatenation _builder = new StringConcatenation(); | ||
145 | _builder.append("Metamodels contains attribute \""); | ||
146 | String _name = attribute.getName(); | ||
147 | _builder.append(_name); | ||
148 | _builder.append("\" with unsupported type \""); | ||
149 | String _name_1 = trg.getName(); | ||
150 | _builder.append(_name_1); | ||
151 | _builder.append("\"!"); | ||
152 | errors.add(_builder.toString()); | ||
153 | } | ||
154 | } | ||
155 | } | ||
156 | } | ||
157 | } | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.java b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.java deleted file mode 100644 index 0b5b8f03..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.java +++ /dev/null | |||
@@ -1,86 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.application.validation; | ||
2 | |||
3 | import com.google.common.collect.Iterables; | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; | ||
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; | ||
6 | import java.util.Collections; | ||
7 | import java.util.LinkedList; | ||
8 | import java.util.List; | ||
9 | import java.util.Set; | ||
10 | import org.eclipse.emf.common.util.EList; | ||
11 | import org.eclipse.emf.ecore.EAttribute; | ||
12 | import org.eclipse.emf.ecore.EClass; | ||
13 | import org.eclipse.emf.ecore.EClassifier; | ||
14 | import org.eclipse.emf.ecore.EEnum; | ||
15 | import org.eclipse.emf.ecore.EEnumLiteral; | ||
16 | import org.eclipse.emf.ecore.ENamedElement; | ||
17 | import org.eclipse.emf.ecore.EObject; | ||
18 | import org.eclipse.emf.ecore.EReference; | ||
19 | import org.eclipse.viatra.query.patternlanguage.emf.vql.Pattern; | ||
20 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
21 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
22 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
23 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
24 | import org.eclipse.xtext.xbase.lib.IteratorExtensions; | ||
25 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
26 | import org.eclipse.xtext.xbase.lib.Pair; | ||
27 | |||
28 | @SuppressWarnings("all") | ||
29 | public class QueryAndMetamodelValidator { | ||
30 | public LinkedList<String> validateQueryAndMetamodel(final EcoreMetamodelDescriptor metamodel, final Pair<ViatraQuerySetDescriptor, Set<Pattern>> viatra) { | ||
31 | final Set<Pattern> patterns = viatra.getValue(); | ||
32 | List<EClass> _classes = metamodel.getClasses(); | ||
33 | List<EEnum> _enums = metamodel.getEnums(); | ||
34 | Iterable<EClassifier> _plus = Iterables.<EClassifier>concat(_classes, _enums); | ||
35 | List<EEnumLiteral> _literals = metamodel.getLiterals(); | ||
36 | Iterable<ENamedElement> _plus_1 = Iterables.<ENamedElement>concat(_plus, _literals); | ||
37 | List<EAttribute> _attributes = metamodel.getAttributes(); | ||
38 | Iterable<ENamedElement> _plus_2 = Iterables.<ENamedElement>concat(_plus_1, _attributes); | ||
39 | List<EReference> _references = metamodel.getReferences(); | ||
40 | final Set<ENamedElement> elementsInMetamodel = IterableExtensions.<ENamedElement>toSet(Iterables.<ENamedElement>concat(_plus_2, _references)); | ||
41 | final LinkedList<String> errors = new LinkedList<String>(); | ||
42 | for (final Pattern pattern : patterns) { | ||
43 | { | ||
44 | final Iterable<ENamedElement> elements = this.getReferredNamedElements(pattern); | ||
45 | for (final ENamedElement element : elements) { | ||
46 | boolean _contains = elementsInMetamodel.contains(element); | ||
47 | boolean _not = (!_contains); | ||
48 | if (_not) { | ||
49 | StringConcatenation _builder = new StringConcatenation(); | ||
50 | _builder.append("Pattern \""); | ||
51 | String _name = pattern.getName(); | ||
52 | _builder.append(_name); | ||
53 | _builder.append("\" refers to an element \""); | ||
54 | _builder.append(element); | ||
55 | _builder.append("\" that is not included to the selected metamodel!"); | ||
56 | errors.add(_builder.toString()); | ||
57 | } | ||
58 | } | ||
59 | } | ||
60 | } | ||
61 | return errors; | ||
62 | } | ||
63 | |||
64 | public Iterable<ENamedElement> getReferredNamedElements(final Pattern pattern) { | ||
65 | final List<EObject> elements = IteratorExtensions.<EObject>toList(pattern.eAllContents()); | ||
66 | final Function1<EObject, Iterable<ENamedElement>> _function = (EObject element) -> { | ||
67 | final EList<EReference> references = element.eClass().getEAllReferences(); | ||
68 | final Function1<EReference, Iterable<ENamedElement>> _function_1 = (EReference r) -> { | ||
69 | boolean _isMany = r.isMany(); | ||
70 | if (_isMany) { | ||
71 | Object _eGet = element.eGet(r); | ||
72 | return Iterables.<ENamedElement>filter(((List<?>) _eGet), ENamedElement.class); | ||
73 | } else { | ||
74 | final Object value = element.eGet(r); | ||
75 | if ((value instanceof ENamedElement)) { | ||
76 | return Collections.<ENamedElement>unmodifiableList(CollectionLiterals.<ENamedElement>newArrayList(((ENamedElement)value))); | ||
77 | } else { | ||
78 | return Collections.<ENamedElement>unmodifiableList(CollectionLiterals.<ENamedElement>newArrayList()); | ||
79 | } | ||
80 | } | ||
81 | }; | ||
82 | return Iterables.<ENamedElement>filter((Iterables.<ENamedElement>concat(ListExtensions.<EReference, Iterable<ENamedElement>>map(references, _function_1))), ENamedElement.class); | ||
83 | }; | ||
84 | return Iterables.<ENamedElement>concat(ListExtensions.<EObject, Iterable<ENamedElement>>map(elements, _function)); | ||
85 | } | ||
86 | } | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/.gitignore b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/.gitignore deleted file mode 100644 index 23da1346..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/.gitignore +++ /dev/null | |||
@@ -1,2 +0,0 @@ | |||
1 | /.ApplicationConfigurationValueConverterService.java._trace | ||
2 | /.QualifiedNameValueConverter.java._trace | ||
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.java b/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.java deleted file mode 100644 index 59a09906..00000000 --- a/Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.java +++ /dev/null | |||
@@ -1,16 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.application.valueconverter; | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.application.valueconverter.QualifiedNameValueConverter; | ||
4 | import org.eclipse.xtext.common.services.DefaultTerminalConverters; | ||
5 | import org.eclipse.xtext.conversion.IValueConverter; | ||
6 | import org.eclipse.xtext.conversion.ValueConverter; | ||
7 | |||
8 | @SuppressWarnings("all") | ||
9 | public class ApplicationConfigurationValueConverterService extends DefaultTerminalConverters { | ||
10 | private final QualifiedNameValueConverter converter2 = new QualifiedNameValueConverter(); | ||
11 | |||
12 | @ValueConverter(rule = "QualifiedName") | ||
13 | public IValueConverter<String> QualifiedName() { | ||
14 | return this.converter2; | ||
15 | } | ||
16 | } | ||
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index b9942a17..1b68fed2 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend | |||
@@ -17,7 +17,8 @@ class ExpressionEvaluation2Logic { | |||
17 | var NumericProblemSolver _numericSolver = null //new NumericProblemSolver | 17 | var NumericProblemSolver _numericSolver = null //new NumericProblemSolver |
18 | def getNumericSolver() { | 18 | def getNumericSolver() { |
19 | if(_numericSolver === null) { | 19 | if(_numericSolver === null) { |
20 | _numericSolver = (new NumericTranslator).selectProblemSolver | 20 | // it seems like this getter has no use |
21 | _numericSolver = (new NumericTranslator(null)).selectProblemSolver | ||
21 | } | 22 | } |
22 | return _numericSolver | 23 | return _numericSolver |
23 | } | 24 | } |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend index 22ea41bf..3d3f2f4a 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | |||
@@ -16,7 +16,7 @@ import org.eclipse.xtext.xbase.XFeatureCall | |||
16 | class NumericTranslator { | 16 | class NumericTranslator { |
17 | 17 | ||
18 | private XExpressionExtractor extractor = new XExpressionExtractor(); | 18 | private XExpressionExtractor extractor = new XExpressionExtractor(); |
19 | private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver(); | 19 | private NumericProblemSolver numericSolver; |
20 | 20 | ||
21 | long formingProblemTime=0; | 21 | long formingProblemTime=0; |
22 | long solvingProblemTime=0; | 22 | long solvingProblemTime=0; |
@@ -28,6 +28,11 @@ class NumericTranslator { | |||
28 | o1.simpleName.compareTo(o2.simpleName) | 28 | o1.simpleName.compareTo(o2.simpleName) |
29 | } | 29 | } |
30 | } | 30 | } |
31 | |||
32 | new(NumericProblemSolver numericProblemSolver){ | ||
33 | this.numericSolver = numericProblemSolver | ||
34 | } | ||
35 | |||
31 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { | 36 | def Map<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) { |
32 | val res = new HashMap | 37 | val res = new HashMap |
33 | for(var i=0; i<tuple.length; i++) { | 38 | for(var i=0; i<tuple.length; i++) { |
@@ -53,7 +58,9 @@ class NumericTranslator { | |||
53 | 58 | ||
54 | def NumericProblemSolver selectProblemSolver() { | 59 | def NumericProblemSolver selectProblemSolver() { |
55 | // return new NumericProblemSolver | 60 | // return new NumericProblemSolver |
56 | return drealSolver; | 61 | // add numeric solver decision procedure here |
62 | if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver | ||
63 | return numericSolver; | ||
57 | } | 64 | } |
58 | 65 | ||
59 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { | 66 | def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> matches) { |
@@ -81,5 +88,5 @@ class NumericTranslator { | |||
81 | def getFormingProblemTime() {formingProblemTime} | 88 | def getFormingProblemTime() {formingProblemTime} |
82 | def getSolvingProblemTime() {solvingProblemTime} | 89 | def getSolvingProblemTime() {solvingProblemTime} |
83 | def getFormingSolutionTime() {formingSolutionTime} | 90 | def getFormingSolutionTime() {formingSolutionTime} |
84 | def getDrealSolver(){return drealSolver} | 91 | def getNumericSolver(){numericSolver} |
85 | } \ No newline at end of file | 92 | } \ No newline at end of file |
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 1f902b90..144e5e6f 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 | |||
@@ -38,6 +38,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer | |||
38 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | 38 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel |
39 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 39 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
40 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 40 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
41 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | ||
41 | 42 | ||
42 | class ViatraReasoner extends LogicReasoner { | 43 | class ViatraReasoner extends LogicReasoner { |
43 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 44 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
@@ -109,7 +110,7 @@ class ViatraReasoner extends LogicReasoner { | |||
109 | new SolutionStore(numberOfRequiredSolutions) | 110 | new SolutionStore(numberOfRequiredSolutions) |
110 | } | 111 | } |
111 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | 112 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) |
112 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) | 113 | val numericSolver = new NumericSolver(method, viatraConfig, false) |
113 | val solutionSaver = method.solutionSaver | 114 | val solutionSaver = method.solutionSaver |
114 | solutionSaver.numericSolver = numericSolver | 115 | solutionSaver.numericSolver = numericSolver |
115 | val solutionCopier = solutionSaver.solutionCopier | 116 | val solutionCopier = solutionSaver.solutionCopier |
@@ -165,7 +166,9 @@ class ViatraReasoner extends LogicReasoner { | |||
165 | viatraConfig.progressMonitor.workedSearchFinished | 166 | viatraConfig.progressMonitor.workedSearchFinished |
166 | 167 | ||
167 | //dreal teardown | 168 | //dreal teardown |
168 | numericSolver.numericDrealSolver.teardown() | 169 | if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ |
170 | (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() | ||
171 | } | ||
169 | 172 | ||
170 | // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches | 173 | // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches |
171 | val statistics = createStatistics => [ | 174 | val statistics = createStatistics => [ |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index fbe6da9d..ebfd5d81 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
@@ -33,6 +33,11 @@ enum PunishSizeStrategy { | |||
33 | LARGER_IS_BETTER | 33 | LARGER_IS_BETTER |
34 | } | 34 | } |
35 | 35 | ||
36 | enum NumericSolverSelection { | ||
37 | DREAL, | ||
38 | Z3 | ||
39 | } | ||
40 | |||
36 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { | 41 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { |
37 | // public var Iterable<PQuery> existingQueries | 42 | // public var Iterable<PQuery> existingQueries |
38 | public var nameNewElements = false | 43 | public var nameNewElements = false |
@@ -70,6 +75,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
70 | public var nonContainmentWeight = 1 | 75 | public var nonContainmentWeight = 1 |
71 | public var unfinishedWFWeight = 1 | 76 | public var unfinishedWFWeight = 1 |
72 | public var calculateObjectCreationCosts = false | 77 | public var calculateObjectCreationCosts = false |
78 | public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL | ||
73 | 79 | ||
74 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | 80 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( |
75 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 81 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 0e789671..4b0ea544 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -1,6 +1,8 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
@@ -8,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
11 | import java.math.BigDecimal | 15 | import java.math.BigDecimal |
12 | import java.util.HashMap | 16 | import java.util.HashMap |
13 | import java.util.LinkedHashMap | 17 | import java.util.LinkedHashMap |
@@ -25,7 +29,7 @@ class NumericSolver { | |||
25 | var ThreadContext threadContext | 29 | var ThreadContext threadContext |
26 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 30 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
27 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 31 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
28 | NumericTranslator t = new NumericTranslator | 32 | NumericTranslator t |
29 | 33 | ||
30 | val boolean intermediateConsistencyCheck | 34 | val boolean intermediateConsistencyCheck |
31 | val boolean caching; | 35 | val boolean caching; |
@@ -36,12 +40,18 @@ class NumericSolver { | |||
36 | var int numberOfSolverCalls = 0 | 40 | var int numberOfSolverCalls = 0 |
37 | var int numberOfCachedSolverCalls = 0 | 41 | var int numberOfCachedSolverCalls = 0 |
38 | 42 | ||
39 | new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { | 43 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { |
40 | this.method = method | 44 | this.method = method |
41 | this.intermediateConsistencyCheck = intermediateConsistencyCheck | 45 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks |
46 | this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) | ||
42 | this.caching = caching | 47 | this.caching = caching |
43 | } | 48 | } |
44 | 49 | ||
50 | def createNumericTranslator(NumericSolverSelection solverSelection) { | ||
51 | if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver | ||
52 | if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver | ||
53 | } | ||
54 | |||
45 | def init(ThreadContext context) { | 55 | def init(ThreadContext context) { |
46 | // This makes the NumericSolver single-threaded, | 56 | // This makes the NumericSolver single-threaded, |
47 | // but that's not a problem, because we only use the solver on a single thread anyways. | 57 | // but that's not a problem, because we only use the solver on a single thread anyways. |
@@ -68,7 +78,7 @@ class NumericSolver { | |||
68 | def getSolverFormingProblem(){this.t.formingProblemTime} | 78 | def getSolverFormingProblem(){this.t.formingProblemTime} |
69 | def getSolverSolvingProblem(){this.t.solvingProblemTime} | 79 | def getSolverSolvingProblem(){this.t.solvingProblemTime} |
70 | def getSolverSolution(){this.t.formingSolutionTime} | 80 | def getSolverSolution(){this.t.formingSolutionTime} |
71 | def getNumericDrealSolver(){this.t.drealSolver} | 81 | def getNumericSolverSelection(){this.t.numericSolver} |
72 | 82 | ||
73 | def boolean maySatisfiable() { | 83 | def boolean maySatisfiable() { |
74 | if(intermediateConsistencyCheck) { | 84 | if(intermediateConsistencyCheck) { |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig index bf0f9dbe..b2a6b64a 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig | |||
@@ -12,7 +12,9 @@ generate { | |||
12 | 12 | ||
13 | config = { | 13 | config = { |
14 | runtime = 10000, | 14 | runtime = 10000, |
15 | log-level = normal | 15 | log-level = normal, |
16 | "numeric-solver" = "dreal", | ||
17 | "scopePropagator" = "typeHierarchy" | ||
16 | } | 18 | } |
17 | 19 | ||
18 | runs = 1 | 20 | runs = 1 |