diff --git a/btypes_primitives/src/main/python_magicstack_immutable/btypes/BRelation.py b/btypes_primitives/src/main/python_magicstack_immutable/btypes/BRelation.py
index 92f791a052941ca7304d6195014ace814741dee5..1b894ec5604443d733959122d6b12e3884461814 100644
--- a/btypes_primitives/src/main/python_magicstack_immutable/btypes/BRelation.py
+++ b/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)
diff --git a/btypes_primitives/src/main/python_magicstack_immutable/btypes/BSet.py b/btypes_primitives/src/main/python_magicstack_immutable/btypes/BSet.py
index cd0ed7551a87b507d3c3f9b79b4c2aec4cd2bd1b..66a7ec48c36e3e884b7bd32d7ea038ae472a00b7 100644
--- a/btypes_primitives/src/main/python_magicstack_immutable/btypes/BSet.py
+++ b/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 *
diff --git a/btypes_primitives/src/main/python_magicstack_immutable/btypes/BZ3.py b/btypes_primitives/src/main/python_magicstack_immutable/btypes/BZ3.py
new file mode 100644
index 0000000000000000000000000000000000000000..3e31f7532eaa896d69f18104f0eecac2de553d2b
--- /dev/null
+++ b/btypes_primitives/src/main/python_magicstack_immutable/btypes/BZ3.py
@@ -0,0 +1,26 @@
+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)
diff --git a/constraint_solver.adoc b/constraint_solver.adoc
new file mode 100644
index 0000000000000000000000000000000000000000..478f44cdf3848ddc5fa14978242c230d2228b1ac
--- /dev/null
+++ b/constraint_solver.adoc
@@ -0,0 +1,171 @@
+# 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.
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
index 9ee3f00a4adf99b48d96e0e61c04491bb60bdc03..116a92dc46b77b58fd2e1ee10e6ba8a0fae93861 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
+++ b/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);
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/OperatorGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/OperatorGenerator.java
index c002f2acc6d31977f080f2d1147bce6223034d6d..e74c32b6703f335c1f9bc469706a82a56c5c42e5 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/OperatorGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/OperatorGenerator.java
@@ -1,6 +1,7 @@
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("");
}
/*
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/iteration/ConstraintSolverPredicateGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/iteration/ConstraintSolverPredicateGenerator.java
new file mode 100644
index 0000000000000000000000000000000000000000..345ae5b789bd1e6a0dd5d194f14ac46015a9a182
--- /dev/null
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/iteration/ConstraintSolverPredicateGenerator.java
@@ -0,0 +1,105 @@
+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;
+ }
+}
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/iteration/IterationConstructGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/iteration/IterationConstructGenerator.java
index 508fc28ff40a6656287a3d588cc4c987f3a16ce4..36b87c7f3a7c65ec889ba2b9dd70e3e5d1718b0a 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/iteration/IterationConstructGenerator.java
+++ b/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);
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/iteration/SetComprehensionGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/iteration/SetComprehensionGenerator.java
index cd35e520b5ef541b32512e8d1a41e94632cd318b..fc0dfd3038023d49dd66d87c5bedf9f2ee3b2008 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/iteration/SetComprehensionGenerator.java
+++ b/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();
diff --git a/src/main/java/de/hhu/stups/codegenerator/handlers/IterationConstructHandler.java b/src/main/java/de/hhu/stups/codegenerator/handlers/IterationConstructHandler.java
index 7ea631b876bf4b28174c96e6be1ddaa4ffe28fe4..a6468c20c0af6bf9bbb8f51508511636d91accd6 100644
--- a/src/main/java/de/hhu/stups/codegenerator/handlers/IterationConstructHandler.java
+++ b/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);
}
/*
@@ -162,11 +165,16 @@ public class IterationConstructHandler {
return currentIterationConstructGenerator;
}
- public void setExpressionGenerator(ExpressionGenerator expressionGenerator) {
+ public void setExpressionGenerator(ExpressionGenerator expressionGenerator) {
this.expressionGenerator = expressionGenerator;
- }
+ }
public void setPredicateGenerator(PredicateGenerator predicateGenerator) {
this.predicateGenerator = predicateGenerator;
}
+
+ public void setConstraintSolverPredicateGenerator(ConstraintSolverPredicateGenerator constraintSolverPredicateGenerator) {
+ this.constraintSolverPredicateGenerator = constraintSolverPredicateGenerator;
+ }
+
}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/PythonTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/PythonTemplate.stg
index 6b3a772cdc5e2b44b0f80a9d9fad698776a3af24..201ccb81752af449a799e5a98087df4493a13b55 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/PythonTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/PythonTemplate.stg
@@ -192,41 +192,38 @@ set_comprehension_predicate(otherIterationConstructs, set, element, emptyPredica
<if(emptyPredicate)>
<set> = <set>.union(<if(isRelation)>BRelation<else>BSet<endif>(<element>))
<else>
-if(<predicate>).booleanValue():
+if (<predicate>).booleanValue():
<set> = <set>.union(<if(isRelation)>BRelation<else>BSet<endif>(<element>))
<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) ::= <<