From f5afda733ffdf4f52da932e03919c20b99bf7fa6 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 15 Dec 2020 13:18:17 -0500 Subject: Add config flag for selecting numeric solver. Integ with Z3 --- .../.gitignore | 2 +- .../application/execution/SolverLoader.xtend | 9 ++ .../bme/mit/inf/dslreasoner/application/.gitignore | 2 - .../dslreasoner/application/execution/.gitignore | 9 -- .../application/execution/util/.gitignore | 3 - .../dslreasoner/application/generator/.gitignore | 1 - .../inf/dslreasoner/application/linking/.gitignore | 2 - .../inf/dslreasoner/application/scoping/.gitignore | 1 - .../dslreasoner/application/validation/.gitignore | 3 - .../application/validation/MetamodelValidator.java | 157 --------------------- .../validation/QueryAndMetamodelValidator.java | 86 ----------- .../application/valueconverter/.gitignore | 2 - ...licationConfigurationValueConverterService.java | 16 --- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 3 +- .../viatra2logic/NumericTranslator.xtend | 13 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 7 +- .../reasoner/ViatraReasonerConfiguration.xtend | 6 + .../viatrasolver/reasoner/dse/NumericSolver.xtend | 18 ++- .../inputs/familytreeGen.vsconfig | 4 +- 19 files changed, 50 insertions(+), 294 deletions(-) delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/execution/util/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/generator/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/linking/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/scoping/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/MetamodelValidator.java delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/validation/QueryAndMetamodelValidator.java delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/.gitignore delete mode 100644 Application/hu.bme.mit.inf.dslreasoner.application/xtend-gen/hu/bme/mit/inf/dslreasoner/application/valueconverter/ApplicationConfigurationValueConverterService.java 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 @@ /bin/ -/xtend-gen/* \ No newline at end of file +/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 import org.eclipse.xtext.EcoreUtil2 import org.eclipse.xtext.xbase.lib.Functions.Function1 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection class SolverLoader { def loadSolver(Solver solver, Map config) { @@ -139,6 +140,14 @@ class SolverLoader { val stringValue = config.get("fitness-objectCreationCosts") c.calculateObjectCreationCosts = Boolean.parseBoolean(stringValue) } + if (config.containsKey("numeric-solver")) { + val stringValue = config.get("numeric-solver") + c.numericSolverSelection = switch (stringValue) { + case "dreal": NumericSolverSelection.DREAL + case "z3": NumericSolverSelection.Z3 + default: throw new IllegalArgumentException("Unknown numeric solver selection: " + stringValue) + } + } if (config.containsKey("scopePropagator")) { val stringValue = config.get("scopePropagator") 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 @@ -/.ApplicationConfigurationStandaloneSetup.java._trace -/.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 @@ -/.GenerationTaskExecutor.java._trace -/.NullWorkspace.java._trace -/.MetamodelLoader.java._trace -/.ModelLoader.java._trace -/.QueryLoader.java._trace -/.ScopeLoader.java._trace -/.ScriptConsole.java._trace -/.ScriptExecutor.java._trace -/.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 @@ -/.MyModule.java._trace -/.ApplicationConfigurationParser.java._trace -/.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 @@ -/.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 @@ -/.ApplicationConfigurationLinkingService.java._trace -/.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 @@ -/.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 @@ -/.MetamodelValidator.java._trace -/.ApplicationConfigurationValidator.java._trace -/.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 @@ -package hu.bme.mit.inf.dslreasoner.application.validation; - -import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; -import java.util.Collections; -import java.util.LinkedList; -import java.util.List; -import org.eclipse.emf.common.util.EList; -import org.eclipse.emf.ecore.EAttribute; -import org.eclipse.emf.ecore.EClass; -import org.eclipse.emf.ecore.EDataType; -import org.eclipse.emf.ecore.EEnum; -import org.eclipse.emf.ecore.EEnumLiteral; -import org.eclipse.emf.ecore.EReference; -import org.eclipse.emf.ecore.EcorePackage; -import org.eclipse.xtend2.lib.StringConcatenation; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Extension; - -@SuppressWarnings("all") -public class MetamodelValidator { - public LinkedList validateMetamodel(final EcoreMetamodelDescriptor descriptor) { - final LinkedList errors = new LinkedList(); - this.allSupertypesAreIncluded(descriptor.getClasses(), errors); - this.allEnumTypesareIncluded(descriptor.getEnums(), descriptor.getLiterals(), errors); - this.referenceEndpointsAreIncluded(descriptor.getClasses(), descriptor.getReferences(), errors); - this.attributeSourcePontIsIncluded(descriptor.getClasses(), descriptor.getAttributes(), errors); - this.attributeTargetIsSupported(descriptor.getAttributes(), errors); - return errors; - } - - private boolean supportedEDataType(final EDataType dataType) { - @Extension - final EcorePackage l = EcorePackage.eINSTANCE; - EDataType _eInt = l.getEInt(); - EDataType _eBoolean = l.getEBoolean(); - EDataType _eString = l.getEString(); - EDataType _eDouble = l.getEDouble(); - EDataType _eFloat = l.getEFloat(); - return Collections.unmodifiableList(CollectionLiterals.newArrayList(_eInt, _eBoolean, _eString, _eDouble, _eFloat)).contains(dataType); - } - - public void allSupertypesAreIncluded(final List classes, final List errors) { - for (final EClass c : classes) { - EList _eSuperTypes = c.getESuperTypes(); - for (final EClass s : _eSuperTypes) { - boolean _contains = classes.contains(s); - boolean _not = (!_contains); - if (_not) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Metamodel contains \""); - String _name = c.getName(); - _builder.append(_name); - _builder.append("\" but not contains its supertype \""); - String _name_1 = s.getName(); - _builder.append(_name_1); - _builder.append("\"!"); - errors.add(_builder.toString()); - } - } - } - } - - public void allEnumTypesareIncluded(final List enums, final List literals, final List errors) { - for (final EEnumLiteral l : literals) { - boolean _contains = enums.contains(l.getEEnum()); - boolean _not = (!_contains); - if (_not) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Metamodel contains literal \""); - String _name = l.getName(); - _builder.append(_name); - _builder.append("\" but does not contains enum \""); - String _name_1 = l.getEEnum().getName(); - _builder.append(_name_1); - _builder.append("\"!"); - errors.add(_builder.toString()); - } - } - } - - public void referenceEndpointsAreIncluded(final List classes, final List references, final List errors) { - for (final EReference reference : references) { - { - final EClass src = reference.getEContainingClass(); - boolean _contains = classes.contains(src); - boolean _not = (!_contains); - if (_not) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Metamodel contains reference \""); - String _name = reference.getName(); - _builder.append(_name); - _builder.append("\" but does not contains its source type \""); - String _name_1 = src.getName(); - _builder.append(_name_1); - _builder.append("\"!"); - errors.add(_builder.toString()); - } - final EClass trg = reference.getEReferenceType(); - boolean _contains_1 = classes.contains(trg); - boolean _not_1 = (!_contains_1); - if (_not_1) { - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("Metamodel contains reference \""); - String _name_2 = reference.getName(); - _builder_1.append(_name_2); - _builder_1.append("\" but does not contains its target type \""); - String _name_3 = trg.getName(); - _builder_1.append(_name_3); - _builder_1.append("\"!"); - errors.add(_builder_1.toString()); - } - } - } - } - - public void attributeSourcePontIsIncluded(final List classes, final List attributes, final List errors) { - for (final EAttribute attribute : attributes) { - { - final Class src = attribute.getContainerClass(); - boolean _contains = classes.contains(src); - boolean _not = (!_contains); - if (_not) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Metamodel contains attribute \""); - String _name = attribute.getName(); - _builder.append(_name); - _builder.append("\" but does not contains its source type \""); - String _name_1 = src.getName(); - _builder.append(_name_1); - _builder.append("\"!"); - errors.add(_builder.toString()); - } - } - } - } - - public void attributeTargetIsSupported(final List attributes, final List errors) { - for (final EAttribute attribute : attributes) { - { - final EDataType trg = attribute.getEAttributeType(); - boolean _supportedEDataType = this.supportedEDataType(trg); - boolean _not = (!_supportedEDataType); - if (_not) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Metamodels contains attribute \""); - String _name = attribute.getName(); - _builder.append(_name); - _builder.append("\" with unsupported type \""); - String _name_1 = trg.getName(); - _builder.append(_name_1); - _builder.append("\"!"); - errors.add(_builder.toString()); - } - } - } - } -} 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 @@ -package hu.bme.mit.inf.dslreasoner.application.validation; - -import com.google.common.collect.Iterables; -import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; -import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; -import java.util.Collections; -import java.util.LinkedList; -import java.util.List; -import java.util.Set; -import org.eclipse.emf.common.util.EList; -import org.eclipse.emf.ecore.EAttribute; -import org.eclipse.emf.ecore.EClass; -import org.eclipse.emf.ecore.EClassifier; -import org.eclipse.emf.ecore.EEnum; -import org.eclipse.emf.ecore.EEnumLiteral; -import org.eclipse.emf.ecore.ENamedElement; -import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.EReference; -import org.eclipse.viatra.query.patternlanguage.emf.vql.Pattern; -import org.eclipse.xtend2.lib.StringConcatenation; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.IteratorExtensions; -import org.eclipse.xtext.xbase.lib.ListExtensions; -import org.eclipse.xtext.xbase.lib.Pair; - -@SuppressWarnings("all") -public class QueryAndMetamodelValidator { - public LinkedList validateQueryAndMetamodel(final EcoreMetamodelDescriptor metamodel, final Pair> viatra) { - final Set patterns = viatra.getValue(); - List _classes = metamodel.getClasses(); - List _enums = metamodel.getEnums(); - Iterable _plus = Iterables.concat(_classes, _enums); - List _literals = metamodel.getLiterals(); - Iterable _plus_1 = Iterables.concat(_plus, _literals); - List _attributes = metamodel.getAttributes(); - Iterable _plus_2 = Iterables.concat(_plus_1, _attributes); - List _references = metamodel.getReferences(); - final Set elementsInMetamodel = IterableExtensions.toSet(Iterables.concat(_plus_2, _references)); - final LinkedList errors = new LinkedList(); - for (final Pattern pattern : patterns) { - { - final Iterable elements = this.getReferredNamedElements(pattern); - for (final ENamedElement element : elements) { - boolean _contains = elementsInMetamodel.contains(element); - boolean _not = (!_contains); - if (_not) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Pattern \""); - String _name = pattern.getName(); - _builder.append(_name); - _builder.append("\" refers to an element \""); - _builder.append(element); - _builder.append("\" that is not included to the selected metamodel!"); - errors.add(_builder.toString()); - } - } - } - } - return errors; - } - - public Iterable getReferredNamedElements(final Pattern pattern) { - final List elements = IteratorExtensions.toList(pattern.eAllContents()); - final Function1> _function = (EObject element) -> { - final EList references = element.eClass().getEAllReferences(); - final Function1> _function_1 = (EReference r) -> { - boolean _isMany = r.isMany(); - if (_isMany) { - Object _eGet = element.eGet(r); - return Iterables.filter(((List) _eGet), ENamedElement.class); - } else { - final Object value = element.eGet(r); - if ((value instanceof ENamedElement)) { - return Collections.unmodifiableList(CollectionLiterals.newArrayList(((ENamedElement)value))); - } else { - return Collections.unmodifiableList(CollectionLiterals.newArrayList()); - } - } - }; - return Iterables.filter((Iterables.concat(ListExtensions.>map(references, _function_1))), ENamedElement.class); - }; - return Iterables.concat(ListExtensions.>map(elements, _function)); - } -} 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 @@ -/.ApplicationConfigurationValueConverterService.java._trace -/.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 @@ -package hu.bme.mit.inf.dslreasoner.application.valueconverter; - -import hu.bme.mit.inf.dslreasoner.application.valueconverter.QualifiedNameValueConverter; -import org.eclipse.xtext.common.services.DefaultTerminalConverters; -import org.eclipse.xtext.conversion.IValueConverter; -import org.eclipse.xtext.conversion.ValueConverter; - -@SuppressWarnings("all") -public class ApplicationConfigurationValueConverterService extends DefaultTerminalConverters { - private final QualifiedNameValueConverter converter2 = new QualifiedNameValueConverter(); - - @ValueConverter(rule = "QualifiedName") - public IValueConverter QualifiedName() { - return this.converter2; - } -} 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 { var NumericProblemSolver _numericSolver = null //new NumericProblemSolver def getNumericSolver() { if(_numericSolver === null) { - _numericSolver = (new NumericTranslator).selectProblemSolver + // it seems like this getter has no use + _numericSolver = (new NumericTranslator(null)).selectProblemSolver } return _numericSolver } 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 class NumericTranslator { private XExpressionExtractor extractor = new XExpressionExtractor(); - private NumericDrealProblemSolver drealSolver = new NumericDrealProblemSolver(); + private NumericProblemSolver numericSolver; long formingProblemTime=0; long solvingProblemTime=0; @@ -28,6 +28,11 @@ class NumericTranslator { o1.simpleName.compareTo(o2.simpleName) } } + + new(NumericProblemSolver numericProblemSolver){ + this.numericSolver = numericProblemSolver + } + def Map arrayToMap(Object[] tuple, ArrayList variablesInOrder) { val res = new HashMap for(var i=0; i> matches) { @@ -81,5 +88,5 @@ class NumericTranslator { def getFormingProblemTime() {formingProblemTime} def getSolvingProblemTime() {solvingProblemTime} def getFormingSolutionTime() {formingSolutionTime} - def getDrealSolver(){return drealSolver} + def getNumericSolver(){numericSolver} } \ 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 import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel import org.eclipse.viatra.dse.solutionstore.SolutionStore import org.eclipse.viatra.dse.statecode.IStateCoderFactory +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver class ViatraReasoner extends LogicReasoner { val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() @@ -109,7 +110,7 @@ class ViatraReasoner extends LogicReasoner { new SolutionStore(numberOfRequiredSolutions) } solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) - val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) + val numericSolver = new NumericSolver(method, viatraConfig, false) val solutionSaver = method.solutionSaver solutionSaver.numericSolver = numericSolver val solutionCopier = solutionSaver.solutionCopier @@ -165,7 +166,9 @@ class ViatraReasoner extends LogicReasoner { viatraConfig.progressMonitor.workedSearchFinished //dreal teardown - numericSolver.numericDrealSolver.teardown() + if (viatraConfig.numericSolverSelection == NumericSolverSelection.DREAL){ + (numericSolver.numericSolverSelection as NumericDrealProblemSolver).teardown() + } // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches 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 { LARGER_IS_BETTER } +enum NumericSolverSelection { + DREAL, + Z3 +} + class ViatraReasonerConfiguration extends LogicSolverConfiguration { // public var Iterable existingQueries public var nameNewElements = false @@ -70,6 +75,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 public var calculateObjectCreationCosts = false + public var numericSolverSelection = NumericSolverSelection.DREAL //currently defaulted to DREAL public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( 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 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator +import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation @@ -8,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration import java.math.BigDecimal import java.util.HashMap import java.util.LinkedHashMap @@ -25,7 +29,7 @@ class NumericSolver { var ThreadContext threadContext val constraint2MustUnitPropagationPrecondition = new HashMap> val constraint2CurrentUnitPropagationPrecondition = new HashMap> - NumericTranslator t = new NumericTranslator + NumericTranslator t val boolean intermediateConsistencyCheck val boolean caching; @@ -36,12 +40,18 @@ class NumericSolver { var int numberOfSolverCalls = 0 var int numberOfCachedSolverCalls = 0 - new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { + new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { this.method = method - this.intermediateConsistencyCheck = intermediateConsistencyCheck + this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks + this.t = new NumericTranslator(createNumericTranslator(config.numericSolverSelection)) this.caching = caching } + def createNumericTranslator(NumericSolverSelection solverSelection) { + if (solverSelection == NumericSolverSelection.DREAL) return new NumericDrealProblemSolver + if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver + } + def init(ThreadContext context) { // This makes the NumericSolver single-threaded, // but that's not a problem, because we only use the solver on a single thread anyways. @@ -68,7 +78,7 @@ class NumericSolver { def getSolverFormingProblem(){this.t.formingProblemTime} def getSolverSolvingProblem(){this.t.solvingProblemTime} def getSolverSolution(){this.t.formingSolutionTime} - def getNumericDrealSolver(){this.t.drealSolver} + def getNumericSolverSelection(){this.t.numericSolver} def boolean maySatisfiable() { 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 { config = { runtime = 10000, - log-level = normal + log-level = normal, + "numeric-solver" = "dreal", + "scopePropagator" = "typeHierarchy" } runs = 1 -- cgit v1.2.3-54-g00ecf