Add config flag for selecting numeric solver. Integ with Z3

13 files changed, 10 insertions, 283 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 @@
 /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<String, String> 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<String> validateMetamodel(final EcoreMetamodelDescriptor descriptor) {
-    final LinkedList<String> errors = new LinkedList<String>();
-    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.<EDataType>unmodifiableList(CollectionLiterals.<EDataType>newArrayList(_eInt, _eBoolean, _eString, _eDouble, _eFloat)).contains(dataType);
-  }
-  
-  public void allSupertypesAreIncluded(final List<EClass> classes, final List<String> errors) {
-    for (final EClass c : classes) {
-      EList<EClass> _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<EEnum> enums, final List<EEnumLiteral> literals, final List<String> 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<EClass> classes, final List<EReference> references, final List<String> 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<EClass> classes, final List<EAttribute> attributes, final List<String> 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<EAttribute> attributes, final List<String> 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<String> validateQueryAndMetamodel(final EcoreMetamodelDescriptor metamodel, final Pair<ViatraQuerySetDescriptor, Set<Pattern>> viatra) {
-    final Set<Pattern> patterns = viatra.getValue();
-    List<EClass> _classes = metamodel.getClasses();
-    List<EEnum> _enums = metamodel.getEnums();
-    Iterable<EClassifier> _plus = Iterables.<EClassifier>concat(_classes, _enums);
-    List<EEnumLiteral> _literals = metamodel.getLiterals();
-    Iterable<ENamedElement> _plus_1 = Iterables.<ENamedElement>concat(_plus, _literals);
-    List<EAttribute> _attributes = metamodel.getAttributes();
-    Iterable<ENamedElement> _plus_2 = Iterables.<ENamedElement>concat(_plus_1, _attributes);
-    List<EReference> _references = metamodel.getReferences();
-    final Set<ENamedElement> elementsInMetamodel = IterableExtensions.<ENamedElement>toSet(Iterables.<ENamedElement>concat(_plus_2, _references));
-    final LinkedList<String> errors = new LinkedList<String>();
-    for (final Pattern pattern : patterns) {
-      {
-        final Iterable<ENamedElement> 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<ENamedElement> getReferredNamedElements(final Pattern pattern) {
-    final List<EObject> elements = IteratorExtensions.<EObject>toList(pattern.eAllContents());
-    final Function1<EObject, Iterable<ENamedElement>> _function = (EObject element) -> {
-      final EList<EReference> references = element.eClass().getEAllReferences();
-      final Function1<EReference, Iterable<ENamedElement>> _function_1 = (EReference r) -> {
-        boolean _isMany = r.isMany();
-        if (_isMany) {
-          Object _eGet = element.eGet(r);
-          return Iterables.<ENamedElement>filter(((List<?>) _eGet), ENamedElement.class);
-        } else {
-          final Object value = element.eGet(r);
-          if ((value instanceof ENamedElement)) {
-            return Collections.<ENamedElement>unmodifiableList(CollectionLiterals.<ENamedElement>newArrayList(((ENamedElement)value)));
-          } else {
-            return Collections.<ENamedElement>unmodifiableList(CollectionLiterals.<ENamedElement>newArrayList());
-          }
-        }
-      };
-      return Iterables.<ENamedElement>filter((Iterables.<ENamedElement>concat(ListExtensions.<EReference, Iterable<ENamedElement>>map(references, _function_1))), ENamedElement.class);
-    };
-    return Iterables.<ENamedElement>concat(ListExtensions.<EObject, Iterable<ENamedElement>>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<String> QualifiedName() {
-    return this.converter2;
-  }
-}