Add config flag for selecting numeric solver. Integ with Z3

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 @@
 /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;
-  }
-}
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<JvmIdentifiableElement, PrimitiveElement> arrayToMap(Object[] tuple, ArrayList<JvmIdentifiableElement> variablesInOrder) {

                 val res = new HashMap

                 for(var i=0; i<tuple.length; i++) {

@@ -53,7 +58,9 @@ class NumericTranslator {
         

         def NumericProblemSolver selectProblemSolver() {

 //              return new NumericProblemSolver

-                return drealSolver;

+//              add numeric solver decision procedure here

+                if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver

+                return numericSolver;

         }

         

         def delegateIsSatisfiable(Map<PConstraint, Iterable<Object[]>> 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<PQuery> 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<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

         val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>

-        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