Add Current status for z3solver.

btypes_primitives/src/main/python_magicstack_immutable/btypes/BRelation.py

@@ -8,6 +8,9 @@ import immutables
 from functools import reduce
 import random
 
+from z3 import Solver
+from z3 import sat
+from z3 import And
 
 class BRelation:
 
@@ -719,3 +722,16 @@ class BRelation:
                 i = i + 1
         sb += "}"
         return sb
+
+    @staticmethod
+    def fromSolver(solver: 'Solver', listOfVariables) -> 'BRelation':
+        currentSet = []
+
+        while solver.check() == sat:
+            currentTuple = reduce(lambda a, b:  BTuple(solver.model()[a], solver.model()[b]), listOfVariables)
+            currentSet.append(currentTuple)
+            firstCondition = Or(listOfVariables[0] != solver.model()[listOfVariables[0]],
+                                 listOfVariables[1] != solver.model()[listOfVariables[1]])
+            solver.add(reduce(lambda a, b:  Or(a, b != solver.model()[b]), listOfVariables[2:], firstCondition))
+
+        return BRelation(*currentSet)

btypes_primitives/src/main/python_magicstack_immutable/btypes/BSet.py

@@ -5,7 +5,8 @@ from btypes.BStruct import *
 
 import immutables
 from functools import reduce
-
+from z3 import Solver
+from z3 import sat
 
 class BSet:
 
@@ -255,5 +256,15 @@ class BSet:
     def __iter__(self):
         return iter(self.__set)
 
+    @staticmethod
+    def fromSolver(solver: 'Solver', listOfVariables) -> 'BSet':
+        currentSet = []
+        key = [x for x in listOfVariables][0]
+        while solver.check() == sat:
+            currentSet.append(solver.model()[key])
+            solver.add(key != solver.model()[key])
+
+        return BSet(*currentSet)
+
 # Import is at the bottom due to cyclic dependencies
 from btypes.BRelation import *

btypes_primitives/src/main/python_magicstack_immutable/btypes/BZ3.py

+from z3 import Int
+from z3 import ArithRef
+from z3 import BoolRef
+from z3 import And
+
+
+def greater(self, other):
+    return self > other
+
+
+def less(self, other):
+    return self < other
+
+
+def equal(self, other):
+    return self == other
+
+
+def __and(self, other):
+    return And(self, other)
+
+
+setattr(ArithRef, 'greater', greater)
+setattr(ArithRef, 'less', less)
+setattr(ArithRef, 'equal', equal)
+setattr(BoolRef, '_and', __and)

constraint_solver.adoc

+# Entscheidungen bzgl. Constraint Solver
+
+Der Codegenerator b2program unterstützt zur Zeit nur einen Teil der in ProB implementierten Set-Comprehensions.
+Um diese Funktion zu erweitern haben wir den Einsatz eines Constraint-Solvers in Betracht gezogen.
+Constraint-Solver sind Programme, denen man  ein Problem beschreibt und die dann eine / alle mögliche(n) Lösung(en) berechnen.
+
+Zuletzt haben wir b2program um die Programmiersprache Python erweitert.
+Daher haben wir uns entschieden auch mit der Erweiterung um einen Constraint-Solver für Python zu beginnen.
+
+In einer Recherche sind wir auf die folgenden Constraint-Solver gestoßen:
+
+* https://choco-solver.org/[Choco-Solver]
+* https://github.com/xoolive/facile[facile]
+* https://labix.org/python-constraint[python-constraint]
+* https://developers.google.com/optimization/cp/cp_solver[CP-SAT Solver]
+* https://docs.sympy.org/latest/modules/solvers/solvers.html[SymPy]
+
+Im folgenden werden wir Vor- und Nachteile, sowie unsere Vorgehensweise und Probleme mit den einzelnen Constraint-Solvern erläutern.
+
+## Choco-Solver
+Der Choco-Solver ist eine mit IntelliJ IDEA entwickelte Open-Source Bibliothek.
+In der Ursprünglichen Recherche ist der Solver auf Grund vielfältiger Datentypen positiv aufgefallen.
+Nach oberflächlicher Betrachtung ist allerdings aufgefallen, dass nur die Programmiersprache Java unterstützt wird.
+Daher ist der Choco-Solver für Python nicht geeignet.
+Allerdings ist für die Implementierung in Java zu empfehlen diesen genauer zu betrachten.
+
+## facile
+Facile ist einer der ersten Constraint-Solver auf den wir gestoßen sind.
+Er unterstützt laut Dokumentation Gleichungen, Ungleichungen, sowie Funktionen.
+Allerdings gab es bei der Installation Probleme.
+
+Die empfohlene Installation ist die Installation mit pip.
+Diese warf folgende Fehlermeldung:
+
+   ERROR: Could not find a version that satisfies the requirement facile
+   ERROR: No matching distribution found for facile
+
+Nach etwas mehr Recherche stellte sich heraus, dass keine passende Version der Software für mein System bei pip hinterlegt ist.
+
+Die nächste Installationsvariante war die Installation mit easy_install.
+Dabei gab es Probleme, da die setuptools-Bibliothek nicht gefunden wurde.
+Der Import der Bibliothek mit Python funktionierte allerdings.
+Im Verdacht waren fehlende PATH Variablen, falsch installierte Python-Versionen, sowie Probleme mit Nutzerrechten.
+Allerdings konnte ich für dieses Problem leider keine Lösung finden.
+
+Der nächste Ansatz zur Installation war die Installation mit opam.
+Dafür musste zunächst opam istalliert werden.
+Danach konnte mit opam install facile die Bibliothek installiert werden.
+Allerdings habe ich dann erst festgestellt, dass facile nur für python2 geeignet ist.
+Da die in der API verwendete Syntax Python3 kompatibel ist, ist mir dies nicht vorher aufgefalen.
+Daher ist facile für unsere Zwecke nicht geeignet, da b2program Python3 verwendet und auf weitere externe Bibliotheken angewiesen ist.
+
+## python-constraint
+Python-constraint ist der Constraint-Solver, der von PyB, einem B-Interpreter unseres Lehrstuhls, verwendet wird.
+Die Installation mit pip verlief hier problemlos.
+
+Um mit python-constraint eine Problem zu lösen, legt man erst das Problem an.
+Dann fügt dann die Variablen mit einem gegebenen Definitionsbereich pro Variable hinzu.
+Zuletzt fügt man die Bedingungen hinzu und kann sich dann die Lösungen ausgeben lassen.
+Die Syntax dafür sieht wie folgt aus:
+
+....
+from constraint import *
+
+problem = Problem()
+
+problem.addVariable("x", range(-50,50))
+problem.addVariable("y", range(-50,50))
+
+problem.addConstraint(lambda x,y: 0<x and x<y and y<10, ["x", "y"])
+
+problem.getSolutions()
+....
+
+Mit dieser Definition berechnet man die Set-Comprehensions {x,y | 0<x & x<y & y<10} (unter der Einschränkung, dass x und y im Intervall von -50 bis 50 liegen).
+b2program kann solche Set-Comprehensions bisher noch nicht lösen, da alle Variablen am Beginn des Prädikates gebunden werden müssen.
+Die Einschränkung des Definitionsbereichs der Variablen lässt sich über den Typ vornehmen, der bei den entsprechenden DeclarationNodes des ASTs hinterlegt ist
+
+Der Definitionsbereich der Variablen lässt sich als Liste beliebiger Werte angeben.
+Daher lassen sich auch andere Typen als Integer, wie z.B. Boolean definieren.
+
+Allerdings kann der angegebene Definitionsbereich nicht unendlich groß werden.
+Möchte man beispielsweise den Integer-Bereich von -2147483648 bis 2147483647 (Standard Integer Bereich von b2program), so gibt python-constraint nur einen *"MemoryError"* aus.
+
+Betrachtet man also Probleme mit großen Zahlen, so ist python-constraint nicht geeignet.
+Für kleinere Probleme sollte es allerdings gut funktionieren.
+
+## CP-SAT Solver
+Der CP-SAT Solver ist ein Constraint-Solver von Google zur Lösung von Integer Constraints.
+Dieser Solver unterstützt nur Probleme, die durch Integer ausgedrückt werden können.
+Allerdings kann man z.B. Booleans durch 0 und 1 ausdrücken und ggf. auch andere Problemstellungen umformulieren.
+Die Installation erfolgt hier ebenfalls über pip.
+
+Das Anlegen und Lösen eines Problems erfolgt hier ähnlich zu python-constraint.
+Allerdings werden die Variablen hier als separate Variablen deklariert und nicht nur im Problem gespeichert.
+Die Syntax sieht wie folgt aus:
+
+....
+from ortools.sat.python import cp_model
+
+model = cp_model.CpModel()
+
+x = model.NewIntVar(-50, 50, 'x')
+y = model.NewIntVar(-50, 50, 'y')
+
+model.Add(0<x)
+model.Add(x<y)
+model.Add(y<10)
+
+solver = cp_model.CpSolver()
+status = solver.Solve(model)
+
+print("Wert für x: ", solver.Value(x))
+print("Wert für y: ", solver.Value(y))
+....
+
+Dies gibt allerdings nur eine mögliche Lösung aus.
+Wenn man alle Lösungen ausgeben möchte, muss man eine zusätzliche Klasse definieren, die während des Lösungsprozesses alle Lösungen sammelt und dann am Ende ausgeben kann.
+Außerdem müssen die (Un-)Gleichungen jeweils separat hinzugefügt werden und können nicht gesammelt übergeben werden.
+
+Für diesen Solver spricht allerdings, dass er auch mit großen Zahlen arbeiten kann und alle möglichen Lösungen berechnet.
+
+## SymPy
+SymPy ist eine Bibliothek, die symbolischen Umgang mit verschiedenen Typen von Gleichungen ermöglicht.
+Das heißt, dass Gleichungen nach Möglichkeit nicht ausgerechnet, sondern vereinfacht werden.
+Die Ergebnisse werden dann symbolisch dargestellt und können so verwendet werden.
+
+Die Syntax dafür sieht wie folgt aus:
+....
+from sympy import symbols
+from sympy.solvers.inequalities import reduce_rational_inequalities
+x=symbols('x')
+reduce_rational_inequalities([[0<x]], x)
+....
+
+Mit SymPy ist es allerdings schwierig Gleichungen und Ungleichungen, oder mehrere Gleichungen zu kombinieren.
+Daher ist es für unsere Zwecke wahrscheinlich nicht geeignet.
+
+## Fazit
+Von den betrachteten Solvern sind wahrscheinlich python-constraint und CP-SAT Solver die beiden passendsten für unser Problem.
+python-constraint liefert viel Funktionalität, dank der Constraints über lambda-Funktionen, schränkt dafür aber den Zahlenraum stark ein.
+CP-SAT Solver hingegen liefert einen großen Zahlenraum, dafür ist es komplizierter die Constraints zu definieren.
+
+## Nachtrag: Z3 Solver
+Der Z3 Solver stellt viele Funktionen für das Constraint Solving zur Verfügung.
+Darunter fallen Datentypen wie Int, Bool, String und mehr.
+Des weiteren ist es möglich Prädikate wie Exists und ForAll abzufragen.
+Wie auch bei den anderen Constaint Solvern ist es auch hier möglich die Lösungsmenge zu extrahieren.
+Allerdings muss dafür jede Lösung einzeln gesammelt und dann von den möglichen Lösungen ausgeschlossen werden.
+Der Code dafür sieht wie folgt aus:
+
+....
+solutionSet = []
+    while solver.check() == sat:
+        currentTuple = reduce(lambda a, b:  BTuple(solver.model()[a], solver.model()[b]), listOfVariables)
+        solutionSet.append(currentTuple)
+        firstCondition =
+            Or(listOfVariables[0] != solver.model()[listOfVariables[0]],
+               listOfVariables[1] != solver.model()[listOfVariables[1]])
+        solver.add(reduce(lambda a, b:  Or(a, b != solver.model()[b]),
+                          listOfVariables[2:], firstCondition))
+
+....
+
+Dabei müssen die Variablen nachgehalten werden und jeweils einzeln ausgeschlossen werden.
+
+Mit dem Funktionsumfang ist der z3 Solver wahrscheinlich das geeignetste Mittel für unseren Zweck.
+Aus Zeitgründen wurde eine vollständige Implementierung allerdings nicht durchgeführt.
+Um den Solver zu implementieren müssen die B-Predikate zu Z3 Predikaten umgeschrieben werden.
+Wahrscheinlich sollte dafür ein neuer PredicateGenerator geschrieben werden, der dann die entsprechenden Predikate generiert.
+Dies ist allerdings zeitaufwändig.

src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java

@@ -4,6 +4,7 @@ import de.hhu.stups.codegenerator.CodeGeneratorUtils;
 import de.hhu.stups.codegenerator.GeneratorMode;
 import de.hhu.stups.codegenerator.analyzers.DeferredSetAnalyzer;
 import de.hhu.stups.codegenerator.analyzers.RecordStructAnalyzer;
+import de.hhu.stups.codegenerator.generators.iteration.ConstraintSolverPredicateGenerator;
 import de.hhu.stups.codegenerator.handlers.IterationConstructHandler;
 import de.hhu.stups.codegenerator.handlers.NameHandler;
 import de.hhu.stups.codegenerator.handlers.ParallelConstructHandler;
@@ -87,6 +88,8 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
 
 	private final PredicateGenerator predicateGenerator;
 
+	private final ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator;
+
 	private final LambdaFunctionGenerator lambdaFunctionGenerator;
 
 	private final SubstitutionGenerator substitutionGenerator;
@@ -153,7 +156,8 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
 																expressionGenerator, predicateGenerator, identifierGenerator, iterationConstructHandler,
 																parallelConstructHandler, recordStructGenerator, declarationGenerator, lambdaFunctionGenerator,
 																infiniteSetGenerator);
-		this.operatorGenerator = new OperatorGenerator(predicateGenerator, expressionGenerator);
+		this.constraintSolverPredicateGenerator = new ConstraintSolverPredicateGenerator(this, iterationConstructHandler);
+		this.operatorGenerator = new OperatorGenerator(predicateGenerator, expressionGenerator, constraintSolverPredicateGenerator);
 		this.operationGenerator = new OperationGenerator(currentGroup, this, substitutionGenerator, declarationGenerator, identifierGenerator, nameHandler,
 															typeGenerator, recordStructGenerator);
 

src/main/java/de/hhu/stups/codegenerator/generators/OperatorGenerator.java

 package de.hhu.stups.codegenerator.generators;
 
 
+import de.hhu.stups.codegenerator.generators.iteration.ConstraintSolverPredicateGenerator;
 import de.hhu.stups.codegenerator.handlers.TemplateHandler;
 import de.prob.parser.ast.nodes.expression.ExpressionOperatorNode;
 import de.prob.parser.ast.nodes.predicate.PredicateOperatorNode;
@@ -36,11 +37,13 @@ public class OperatorGenerator {
 
     private final ExpressionGenerator expressionGenerator;
 
-    public OperatorGenerator(final PredicateGenerator predicateGenerator, final ExpressionGenerator expressionGenerator) {
+    public OperatorGenerator(final PredicateGenerator predicateGenerator, final ExpressionGenerator expressionGenerator,
+                             final ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator) {
         this.predicateGenerator = predicateGenerator;
         this.predicateGenerator.setOperatorGenerator(this);
         this.expressionGenerator = expressionGenerator;
         this.expressionGenerator.setOperatorGenerator(this);
+        constraintSolverPredicateGenerator.setOperatorGenerator(this);
     }
 
     /*
@@ -63,7 +66,7 @@ public class OperatorGenerator {
                 }
                 return template.render();
             });
-        return result.isPresent() ? result.get() : "";
+        return result.orElse("");
     }
 
     /*

src/main/java/de/hhu/stups/codegenerator/generators/iteration/ConstraintSolverPredicateGenerator.java

+package de.hhu.stups.codegenerator.generators.iteration;
+
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+import java.util.stream.Collectors;
+import de.hhu.stups.codegenerator.generators.MachineGenerator;
+import de.hhu.stups.codegenerator.generators.OperatorGenerator;
+import de.hhu.stups.codegenerator.handlers.IterationConstructHandler;
+import de.prob.parser.ast.nodes.expression.ExpressionOperatorNode;
+import de.prob.parser.ast.nodes.predicate.IdentifierPredicateNode;
+import de.prob.parser.ast.nodes.predicate.IfPredicateNode;
+import de.prob.parser.ast.nodes.predicate.LetPredicateNode;
+import de.prob.parser.ast.nodes.predicate.PredicateOperatorNode;
+import de.prob.parser.ast.nodes.predicate.PredicateOperatorWithExprArgsNode;
+import de.prob.parser.ast.nodes.predicate.QuantifiedPredicateNode;
+import de.prob.parser.ast.visitors.generic.ParametrisedPredicateVisitor;
+
+public class ConstraintSolverPredicateGenerator implements ParametrisedPredicateVisitor<String, Void> {
+
+  /*
+   * Hard-coded lists for identifying the type of the operators for predicates
+   */
+  private static final List<PredicateOperatorNode.PredicateOperator> BINARY_PREDICATE_OPERATORS =
+      Arrays.asList(PredicateOperatorNode.PredicateOperator.AND, PredicateOperatorNode.PredicateOperator.OR,
+          PredicateOperatorNode.PredicateOperator.IMPLIES, PredicateOperatorNode.PredicateOperator.EQUIVALENCE);
+
+  private static final List<PredicateOperatorNode.PredicateOperator> UNARY_PREDICATE_OPERATORS =
+      Collections.singletonList(PredicateOperatorNode.PredicateOperator.NOT);
+
+  private static final List<PredicateOperatorNode.PredicateOperator> PREDICATE_BOOLEANS =
+      Arrays.asList(PredicateOperatorNode.PredicateOperator.TRUE, PredicateOperatorNode.PredicateOperator.FALSE);
+
+  private static final List<ExpressionOperatorNode.ExpressionOperator> POWER_SET_EXPRESSIONS =
+      Arrays.asList(ExpressionOperatorNode.ExpressionOperator.POW, ExpressionOperatorNode.ExpressionOperator.POW1, ExpressionOperatorNode.ExpressionOperator.FIN, ExpressionOperatorNode.ExpressionOperator.FIN1);
+
+
+
+  private final MachineGenerator machineGenerator;
+  private OperatorGenerator operatorGenerator;
+
+  public ConstraintSolverPredicateGenerator(MachineGenerator machineGenerator,
+                                            IterationConstructHandler iterationConstructHandler) {
+    this.machineGenerator = machineGenerator;
+    iterationConstructHandler.setConstraintSolverPredicateGenerator(this);
+  }
+
+  @Override
+  public String visitIdentifierPredicateNode(IdentifierPredicateNode node, Void expected) {
+    throw new RuntimeException("Given node is not implemented: " + node.getClass());
+  }
+
+  @Override
+  public String visitPredicateOperatorNode(PredicateOperatorNode node, Void expected) {
+    List<String> expressionList = node.getPredicateArguments().stream()
+        .map(expr -> machineGenerator.visitPredicateNode(expr, null))
+        .collect(Collectors.toList());
+    return generatePredicate(node, expressionList);
+  }
+
+  @Override
+  public String visitPredicateOperatorWithExprArgs(PredicateOperatorWithExprArgsNode node, Void expected) {
+    List<String> expressionList = node.getExpressionNodes().stream()
+        .map(expr -> machineGenerator.visitExprNode(expr, null))
+        .collect(Collectors.toList());
+    return operatorGenerator.generateBinary(node::getOperator, expressionList);
+  }
+
+  @Override
+  public String visitQuantifiedPredicateNode(QuantifiedPredicateNode node, Void expected) {
+    //TODO
+    throw new RuntimeException("Given node is not implemented: " + node.getClass());
+  }
+
+  @Override
+  public String visitLetPredicateNode(LetPredicateNode node, Void expected) {
+    //TODO
+    throw new RuntimeException("Given node is not implemented: " + node.getClass());
+  }
+
+  @Override
+  public String visitIfPredicateNode(IfPredicateNode node, Void expected) {
+    //TODO
+    throw new RuntimeException("Given node is not implemented: " + node.getClass());
+  }
+
+  /*
+   * This function generates code for a predicate with the given AST node and the list of expressions within the predicate.
+   */
+  public String generatePredicate(PredicateOperatorNode node, List<String> expressionList) {
+    PredicateOperatorNode.PredicateOperator operator = node.getOperator();
+    if(BINARY_PREDICATE_OPERATORS.contains(operator)) {
+      return operatorGenerator.generateBinary(() -> operator, expressionList);
+    } else if(UNARY_PREDICATE_OPERATORS.contains(operator)) {
+      return "";//generateUnaryPredicate(operator, expressionList);
+    } else if(PREDICATE_BOOLEANS.contains(operator)) {
+      return "";//generateBoolean(operator);
+    }
+    throw new RuntimeException("Given operator is not implemented: " + node.getOperator());
+  }
+
+  public void setOperatorGenerator(OperatorGenerator operatorGenerator) {
+    this.operatorGenerator = operatorGenerator;
+  }
+}

src/main/java/de/hhu/stups/codegenerator/generators/iteration/IterationConstructGenerator.java

@@ -91,10 +91,11 @@ public class IterationConstructGenerator implements AbstractVisitor<Void, Void>
 
     public IterationConstructGenerator(final IterationConstructHandler iterationConstructHandler, final MachineGenerator machineGenerator, final NameHandler nameHandler, final STGroup group,
                                        final TypeGenerator typeGenerator, final ImportGenerator importGenerator, final ExpressionGenerator expressionGenerator,
-                                       final PredicateGenerator predicateGenerator, final boolean useConstraintSolving) {
+                                       final PredicateGenerator predicateGenerator, final boolean useConstraintSolving,
+                                       final ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator) {
         this.iterationConstructHandler = iterationConstructHandler;
         this.iterationPredicateGenerator = new IterationPredicateGenerator(group, machineGenerator, typeGenerator, iterationConstructHandler);
-        this.setComprehensionGenerator = new SetComprehensionGenerator(group, machineGenerator, this, iterationConstructHandler, iterationPredicateGenerator, typeGenerator, expressionGenerator, predicateGenerator);
+        this.setComprehensionGenerator = new SetComprehensionGenerator(group, machineGenerator, this, iterationConstructHandler, iterationPredicateGenerator, typeGenerator, expressionGenerator, predicateGenerator, constraintSolverPredicateGenerator);
         this.lambdaGenerator = new LambdaGenerator(group, machineGenerator, this, iterationConstructHandler, iterationPredicateGenerator, typeGenerator);
         this.quantifiedPredicateGenerator = new QuantifiedPredicateGenerator(group, machineGenerator, this, iterationConstructHandler, iterationPredicateGenerator);
         this.quantifiedExpressionGenerator = new QuantifiedExpressionGenerator(group, machineGenerator, nameHandler, typeGenerator, this, iterationConstructHandler, iterationPredicateGenerator);

src/main/java/de/hhu/stups/codegenerator/generators/iteration/SetComprehensionGenerator.java

@@ -42,9 +42,12 @@ public class SetComprehensionGenerator {
 
     private final ExpressionGenerator expressionGenerator;
 
+    private final ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator;
+
     public SetComprehensionGenerator(final STGroup group, final MachineGenerator machineGenerator, final IterationConstructGenerator iterationConstructGenerator,
                                      final IterationConstructHandler iterationConstructHandler, final IterationPredicateGenerator iterationPredicateGenerator,
-                                     final TypeGenerator typeGenerator, final ExpressionGenerator expressionGenerator, final PredicateGenerator predicateGenerator) {
+                                     final TypeGenerator typeGenerator, final ExpressionGenerator expressionGenerator, final PredicateGenerator predicateGenerator,
+                                     final ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator) {
         this.group = group;
         this.machineGenerator = machineGenerator;
         this.iterationConstructGenerator = iterationConstructGenerator;
@@ -53,6 +56,7 @@ public class SetComprehensionGenerator {
         this.typeGenerator = typeGenerator;
         this.predicateGenerator = predicateGenerator;
         this.expressionGenerator = expressionGenerator;
+        this.constraintSolverPredicateGenerator = constraintSolverPredicateGenerator;
     }
 
     /*
@@ -99,14 +103,14 @@ public class SetComprehensionGenerator {
 
         int iterationConstructCounter = iterationConstructHandler.getIterationConstructCounter();
         String identifier = "_cs_set_" + iterationConstructCounter;
-        String problemIdentifier = "_cs_problem_" + iterationConstructCounter;
+        String solverIdentifier = "_cs_solver_" + iterationConstructCounter;
 
         boolean isRelation = node.getDeclarationList().size() > 1;
         //generateBody(template, enumerationTemplates, otherConstructs, identifier, isRelation, predicate, declarations, type);
 
         template.add("identifier", identifier);
         template.add("isRelation", isRelation);
-        template.add("problemIdentifier", problemIdentifier);
+        template.add("solverIdentifier", solverIdentifier);
         template.add("variableDeclarations", declarationTemplates);
         template.add("constraint", generateConstraint((PredicateOperatorNode) node.getPredicateNode(), declarations));
 
@@ -122,8 +126,6 @@ public class SetComprehensionGenerator {
         switch (declaration.getType().toString()){
             case "INTEGER":
                 range.add("isInteger", true);
-                range.add("minInt", expressionGenerator.generateMinInt());
-                range.add("maxInt", expressionGenerator.generateMaxInt());
                 break;
             case "BOOL":
                 range.add("isBoolean", true);
@@ -133,12 +135,11 @@ public class SetComprehensionGenerator {
         }
 
         int iterationConstructCounter = iterationConstructHandler.getIterationConstructCounter();
-        String problemIdentifier = "_cs_problem_" + iterationConstructCounter;
+        String solverIdentifier = "_cs_solver_" + iterationConstructCounter;
 
         ST template = group.getInstanceOf("constraint_variable_declaration");
         template.add("identifier", declaration.getName());
-        template.add("range", range.render());
-        template.add("problemIdentifier", problemIdentifier);
+        template.add("type", range.render());
         return template;
     }
 
@@ -146,11 +147,9 @@ public class SetComprehensionGenerator {
         ST constraint = group.getInstanceOf("constraint");
 
         int iterationConstructCounter = iterationConstructHandler.getIterationConstructCounter();
-        String problemIdentifier = "_cs_problem_" + iterationConstructCounter;
+        String solverIdentifier = "_cs_solver_" + iterationConstructCounter;
 
-        constraint.add("problemIdentifier", problemIdentifier);
-        constraint.add("var1", declarations.get(0).getName());
-        constraint.add("var2",declarations.subList(1,declarations.size()).stream().map(DeclarationNode::getName).collect(Collectors.toList()));
+        constraint.add("solverIdentifier", solverIdentifier);
         constraint.add("constraintFunction", predicateGenerator.visitPredicateOperatorNode(predicate));
 
         return constraint.render();

src/main/java/de/hhu/stups/codegenerator/handlers/IterationConstructHandler.java

@@ -3,6 +3,7 @@ package de.hhu.stups.codegenerator.handlers;
 import de.hhu.stups.codegenerator.generators.ExpressionGenerator;
 import de.hhu.stups.codegenerator.generators.ImportGenerator;
 import de.hhu.stups.codegenerator.generators.PredicateGenerator;
+import de.hhu.stups.codegenerator.generators.iteration.ConstraintSolverPredicateGenerator;
 import de.hhu.stups.codegenerator.generators.iteration.IterationConstructGenerator;
 import de.hhu.stups.codegenerator.generators.MachineGenerator;
 import de.hhu.stups.codegenerator.generators.TypeGenerator;
@@ -37,9 +38,11 @@ public class IterationConstructHandler {
 
     private ExpressionGenerator expressionGenerator;
     private PredicateGenerator predicateGenerator;
+    private ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator;
 
     public IterationConstructHandler(final STGroup group, final MachineGenerator machineGenerator, final NameHandler nameHandler,
-                                     final TypeGenerator typeGenerator, final ImportGenerator importGenerator, final boolean useConstraintSolving) {
+                                     final TypeGenerator typeGenerator, final ImportGenerator importGenerator,
+                                     final boolean useConstraintSolving) {
         this.currentIterationConstructGenerator = null;
         this.iterationConstructCounter = 0;
         this.machineGenerator = machineGenerator;
@@ -69,7 +72,7 @@ public class IterationConstructHandler {
     * This function returns a new IterationConstructGenerator
     */
     public IterationConstructGenerator getNewIterationConstructGenerator() {
-        return new IterationConstructGenerator(this, machineGenerator, nameHandler, group, typeGenerator, importGenerator, expressionGenerator, predicateGenerator, useConstraintSolving);
+        return new IterationConstructGenerator(this, machineGenerator, nameHandler, group, typeGenerator, importGenerator, expressionGenerator, predicateGenerator, useConstraintSolving, constraintSolverPredicateGenerator);
     }
 
     /*
@@ -169,4 +172,9 @@ public class IterationConstructHandler {
     public void setPredicateGenerator(PredicateGenerator predicateGenerator) {
         this.predicateGenerator = predicateGenerator;
     }
+
+    public void setConstraintSolverPredicateGenerator(ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator) {
+        this.constraintSolverPredicateGenerator = constraintSolverPredicateGenerator;
+    }
+
 }

src/main/resources/de/hhu/stups/codegenerator/PythonTemplate.stg

@@ -197,36 +197,33 @@ if(<predicate>).booleanValue():
 <endif>
 >>
 
-constraint_solving(identifier, problemIdentifier, variableDeclarations, constraint, isRelation) ::= <<
-from constraint import Problem
+constraint_solving(identifier, solverIdentifier, variableDeclarations, constraint, isRelation) ::= <<
+from z3 import Solver
+from btypes.BZ3 import Int
+from z3 import Bool
 from functools import reduce
 from btypes.BSet import BSet
 from btypes.BUtils import BUtils
-<problemIdentifier> = Problem()
+<solverIdentifier> = Solver()
+listOfVariables = []
 <variableDeclarations; separator="\n">
 <constraint>
-<identifier> = <problemIdentifier>.getSolutions()
-<if(isRelation)><identifier> = reduce(lambda a,e: a.union(BRelation(reduce(lambda b,f: BTuple(b,f),
-                                                                       list(e.values())[2:],
-                                                                       BTuple(list(e.values())[0],list(e.values())[1])))),
-                      <identifier>,
-                      BRelation())
-<else><identifier> = reduce(lambda a,e: a.union(BSet(e.values())),
-                            <identifier>,
-                            BSet())
+<if(isRelation)><identifier> = BRelation.fromSolver(<solverIdentifier>, listOfVariables)
+<else> <identifier> = BSet.fromSolver(<solverIdentifier>, listOfVariables)
 <endif>
 >>
 
-constraint_variable_declaration(identifier, problemIdentifier, range) ::= <<
-<identifier> = <problemIdentifier>.addVariable("<identifier>", <range>)
+constraint_variable_declaration(identifier, type) ::= <<
+<identifier> = <type>('<identifier>')
+listOfVariables.append(<identifier>)
 >>
 
-constraint_type(isInteger, minInt, maxInt, isBoolean, isSet) ::= <<
-<if(isInteger)>BSet.interval(<minInt>, <maxInt>).getSet()<elseif(isBoolean)>BUtils.BOOL.getSet()<endif>
+constraint_type(isInteger, isBoolean, isSet) ::= <<
+<if(isInteger)>Int<elseif(isBoolean)>Bool<endif>
 >>
 
-constraint(problemIdentifier, var1, var2, constraintFunction) ::= <<
-<problemIdentifier>.addConstraint(lambda <var1><var2 : {var |, <var>}>: <constraintFunction>, ("<var1>"<var2 : {var |, "<var>"}>))
+constraint(solverIdentifier, constraintFunction) ::= <<
+<solverIdentifier>.add(<constraintFunction>)
 >>
 
 lambda(type, identifier, lambda, leftType, rightType) ::= <<
@@ -441,7 +438,7 @@ or(arg1, arg2) ::= <<
 >>
 
 and(arg1, arg2) ::= <<
-(<arg1> and <arg2>)
+(<arg1>._and(<arg2>))
 >>
 
 implies(arg1, arg2) ::= <<