Add constraint solving for python with python-constraint (just integer + boolean)

build.gradle

@@ -67,15 +67,15 @@ tasks.withType(JavaExec) {
     if(project.hasProperty('language') && project.hasProperty('big_integer') && project.hasProperty('deferred_set_size') && project.hasProperty('file')) {
         if(!(project.hasProperty('minint') && project.hasProperty('maxint'))) {
             if (project.hasProperty('addition')) {
-                args([language, big_integer, -2147483648, 2147483647, deferred_set_size, project.rootDir.path.toString() + File.separator +  file, addition])
+                args([language, big_integer, -2147483648, 2147483647, deferred_set_size, true, project.rootDir.path.toString() + File.separator +  file, addition])
             } else {
-                args([language, big_integer, -2147483648, 2147483647, deferred_set_size, project.rootDir.path.toString() + File.separator + file])
+                args([language, big_integer, -2147483648, 2147483647, deferred_set_size, true, project.rootDir.path.toString() + File.separator + file])
             }
         } else {
             if (project.hasProperty('addition')) {
-                args([language, big_integer, minint, maxint, deferred_set_size, project.rootDir.path.toString() + File.separator + file, addition])
+                args([language, big_integer, minint, maxint, deferred_set_size, true, project.rootDir.path.toString() + File.separator + file, addition])
             } else {
-                args([language, big_integer, minint, maxint, deferred_set_size, project.rootDir.path.toString() + File.separator + file])
+                args([language, big_integer, minint, maxint, deferred_set_size, true, project.rootDir.path.toString() + File.separator + file])
             }
         }
     }

src/main/java/de/hhu/stups/codegenerator/CodeGenerator.java

@@ -40,7 +40,7 @@ public class CodeGenerator {
 	* Example: gradle run -Planguage = "java" -Pbig_integer="false" -Pminint=-2047 -Pmaxint=2048 -Pdeferred_set_size="10" -Pfile = "Lift.mch"
 	*/
 	public static void main(String[] args) throws URISyntaxException, MalformedURLException, CodeGenerationException {
-		if(args.length < 6 || args.length > 7) {
+		if(args.length < 7 || args.length > 8) {
 			System.err.println("Wrong number of arguments");
 			return;
 		}
@@ -49,15 +49,16 @@ public class CodeGenerator {
 		String minint = args[2];
 		String maxint = args[3];
 		String deferredSetSize = args[4];
+		boolean useConstraintSolving = useConstraintSolving(args[5]);
 		CodeGenerator codeGenerator = new CodeGenerator();
-		Path path = Paths.get(args[5]);
+		Path path = Paths.get(args[6]);
 		checkPath(path);
 		checkIntegerRange(useBigInteger, minint, maxint);
 		String addition = null;
-		if(args.length == 7) {
-			addition = args[6];
+		if(args.length == 8) {
+			addition = args[7];
 		}
-		codeGenerator.generate(path, mode, useBigInteger, minint, maxint, deferredSetSize, true, addition, false);
+		codeGenerator.generate(path, mode, useBigInteger, minint, maxint, deferredSetSize, useConstraintSolving, true, addition, false);
 	}
 
 	/*
@@ -97,6 +98,21 @@ public class CodeGenerator {
 		return useBigInteger;
 	}
 
+	/*
+	 * This functon extracts boolean for using constraint solving from the given string
+	 */
+	private static boolean useConstraintSolving(String constraintOption) {
+		boolean useConstraintSolving;
+		if("true".equals(constraintOption)) {
+			useConstraintSolving = true;
+		} else if("false".equals(constraintOption)) {
+			useConstraintSolving = false;
+		} else {
+			throw new RuntimeException("Wrong argument for choice of constraints");
+		}
+		return useConstraintSolving;
+	}
+
 	private static void checkPath(Path path) {
 		if(path == null) {
 			throw new RuntimeException("File not found");
@@ -118,7 +134,7 @@ public class CodeGenerator {
 	/*
 	* This function generates code from a given path for a machine, the target language and the information whether it is a main machine of a project
 	*/
-	public List<Path> generate(Path path, GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, boolean isMain, String addition, boolean isIncludedMachine) throws CodeGenerationException {
+	public List<Path> generate(Path path, GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, boolean useConstraintSolving, boolean isMain, String addition, boolean isIncludedMachine) throws CodeGenerationException {
 		if(isMain) {
 			paths.clear();
 		}
@@ -128,16 +144,16 @@ public class CodeGenerator {
 		if(addition != null) {
 			additionAsList[additionAsList.length - 1] = addition;
 		}
-		machineReferenceGenerator.generateIncludedMachines(project, pathAsList, mode, useBigInteger, minint, maxint, deferredSetSize);
-		paths.add(writeToFile(path, mode, useBigInteger, minint, maxint, deferredSetSize, project.getMainMachine(), addition != null ? Paths.get(String.join("/",additionAsList)) : null, isIncludedMachine));
+		machineReferenceGenerator.generateIncludedMachines(project, pathAsList, mode, useBigInteger, minint, maxint, deferredSetSize, useConstraintSolving);
+		paths.add(writeToFile(path, mode, useBigInteger, minint, maxint, deferredSetSize, useConstraintSolving, project.getMainMachine(), addition != null ? Paths.get(String.join("/",additionAsList)) : null, isIncludedMachine));
 		return paths;
 	}
 
 	/*
 	* This function generates code for a targeted programming language with creating the belonging file
 	*/
-	private Path writeToFile(Path path, GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, MachineNode node, Path addition, boolean isIncludedMachine) {
-		MachineGenerator generator = new MachineGenerator(mode, useBigInteger, minint, maxint, deferredSetSize, addition, isIncludedMachine);
+	private Path writeToFile(Path path, GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, boolean useConstraintSolving, MachineNode node, Path addition, boolean isIncludedMachine) {
+		MachineGenerator generator = new MachineGenerator(mode, useBigInteger, minint, maxint, deferredSetSize, useConstraintSolving, addition, isIncludedMachine);
 		machineReferenceGenerator.updateNameHandler(generator);
 		machineReferenceGenerator.updateDeclarationGenerator(generator);
 		machineReferenceGenerator.updateRecordStructGenerator(generator);

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

@@ -179,6 +179,7 @@ public class ExpressionGenerator {
         this.identifierGenerator = identifierGenerator;
         this.typeGenerator = typeGenerator;
         this.iterationConstructHandler = iterationConstructHandler;
+        this.iterationConstructHandler.setExpressionGenerator(this);
         this.recordStructGenerator = recordStructGenerator;
     }
 
@@ -800,7 +801,7 @@ public class ExpressionGenerator {
     /*
     * This function generates code for MININT
     */
-    private String generateMinInt() {
+    public String generateMinInt() {
         ST number = currentGroup.getInstanceOf("number");
         TemplateHandler.add(number, "number", minint);
         TemplateHandler.add(number, "useBigInteger", useBigInteger);
@@ -820,7 +821,7 @@ public class ExpressionGenerator {
     /*
     * This function generates code for MAXINT
     */
-    private String generateMaxInt() {
+    public String generateMaxInt() {
         ST number = currentGroup.getInstanceOf("number");
         TemplateHandler.add(number, "number", maxint);
         TemplateHandler.add(number, "useBigInteger", useBigInteger);

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

@@ -123,7 +123,7 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
 
 	private Set<String> infiniteSets;
 
-	public MachineGenerator(GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, Path addition, boolean isIncludedMachine) {
+	public MachineGenerator(GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, boolean useConstraintSolving, Path addition, boolean isIncludedMachine) {
 		this.currentGroup = CodeGeneratorUtils.getGroup(mode);
 		this.useBigInteger = useBigInteger;
 		this.boundedVariablesDepth = new HashMap<>();
@@ -138,7 +138,7 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
 		this.parallelConstructHandler = new ParallelConstructHandler();
 		this.typeGenerator = new TypeGenerator(currentGroup, nameHandler, this);
 		this.importGenerator = new ImportGenerator(currentGroup, nameHandler, useBigInteger);
-		this.iterationConstructHandler = new IterationConstructHandler(currentGroup, this, nameHandler, typeGenerator, importGenerator);
+		this.iterationConstructHandler = new IterationConstructHandler(currentGroup, this, nameHandler, typeGenerator, importGenerator, useConstraintSolving);
 		this.deferredSetAnalyzer = new DeferredSetAnalyzer(Integer.parseInt(deferredSetSize));
 		this.infiniteSetGenerator = new InfiniteSetGenerator(currentGroup, this, nameHandler);
 		this.identifierGenerator = new IdentifierGenerator(currentGroup, this, nameHandler, parallelConstructHandler, declarationGenerator);

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

@@ -29,14 +29,14 @@ public class MachineReferenceGenerator {
     /*
     * This function generates code for all included machines from the given options
     */
-    public void generateIncludedMachines(BProject project, String[] pathAsList, GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize) {
+    public void generateIncludedMachines(BProject project, String[] pathAsList, GeneratorMode mode, boolean useBigInteger, String minint, String maxint, String deferredSetSize, boolean useConstraintSolving) {
         String last = project.getMainMachine().getName();
         for(MachineReferenceNode referenceNode : project.getMainMachine().getMachineReferences()) {
             pathAsList[pathAsList.length - 1] = pathAsList[pathAsList.length - 1].replaceAll(last, referenceNode.getMachineName());
             last = referenceNode.getMachineName();
             Path currentPath = Paths.get(String.join("/", pathAsList));
             if(!codeGenerator.getPaths().contains(currentPath)) {
-                codeGenerator.generate(currentPath, mode, useBigInteger, minint, maxint, deferredSetSize, false, null, true);
+                codeGenerator.generate(currentPath, mode, useBigInteger, minint, maxint, deferredSetSize, useConstraintSolving, false, null, true);
             }
         }
     }

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

@@ -67,6 +67,7 @@ public class PredicateGenerator {
         this.nameHandler = nameHandler;
         this.importGenerator = importGenerator;
         this.iterationConstructHandler = iterationConstructHandler;
+        this.iterationConstructHandler.setPredicateGenerator(this);
         this.infiniteSetGenerator = infiniteSetGenerator;
         this.infiniteSetGenerator.setPredicateGenerator(this);
         this.relationSetGenerator = new RelationSetGenerator(currentGroup, machineGenerator, nameHandler, infiniteSetGenerator);

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

 package de.hhu.stups.codegenerator.generators.iteration;
 
+import de.hhu.stups.codegenerator.generators.ExpressionGenerator;
 import de.hhu.stups.codegenerator.generators.ImportGenerator;
 import de.hhu.stups.codegenerator.generators.MachineGenerator;
+import de.hhu.stups.codegenerator.generators.PredicateGenerator;
 import de.hhu.stups.codegenerator.generators.TypeGenerator;
 import de.hhu.stups.codegenerator.handlers.IterationConstructHandler;
 import de.hhu.stups.codegenerator.handlers.NameHandler;
@@ -85,11 +87,14 @@ public class IterationConstructGenerator implements AbstractVisitor<Void, Void>
 
     private final List<String> allBoundedVariables;
 
+    private final boolean useConstraintSolving;
+
     public IterationConstructGenerator(final IterationConstructHandler iterationConstructHandler, final MachineGenerator machineGenerator, final NameHandler nameHandler, final STGroup group,
-                                       final TypeGenerator typeGenerator, final ImportGenerator importGenerator) {
+                                       final TypeGenerator typeGenerator, final ImportGenerator importGenerator, final ExpressionGenerator expressionGenerator,
+                                       final PredicateGenerator predicateGenerator, final boolean useConstraintSolving) {
         this.iterationConstructHandler = iterationConstructHandler;
         this.iterationPredicateGenerator = new IterationPredicateGenerator(group, machineGenerator, typeGenerator, iterationConstructHandler);
-        this.setComprehensionGenerator = new SetComprehensionGenerator(group, machineGenerator, this, iterationConstructHandler, iterationPredicateGenerator, typeGenerator);
+        this.setComprehensionGenerator = new SetComprehensionGenerator(group, machineGenerator, this, iterationConstructHandler, iterationPredicateGenerator, typeGenerator, expressionGenerator, predicateGenerator);
         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);
@@ -101,6 +106,7 @@ public class IterationConstructGenerator implements AbstractVisitor<Void, Void>
         this.iterationsMapIdentifier = new HashMap<>();
         this.boundedVariables = new ArrayList<>();
         this.allBoundedVariables = new ArrayList<>();
+        this.useConstraintSolving = useConstraintSolving;
     }
 
 
@@ -148,7 +154,11 @@ public class IterationConstructGenerator implements AbstractVisitor<Void, Void>
     */
     @Override
     public Void visitSetComprehensionNode(SetComprehensionNode node, Void expected) {
+        if(!useConstraintSolving) {
             iterationsMapCode.put(node.toString(), setComprehensionGenerator.generateSetComprehension(node));
+        } else {
+            iterationsMapCode.put(node.toString(), setComprehensionGenerator.generateConstraintSet(node));
+        }
         iterationConstructHandler.incrementIterationConstructCounter();
         return null;
     }

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

 package de.hhu.stups.codegenerator.generators.iteration;
 
+import de.hhu.stups.codegenerator.generators.CodeGenerationException;
+import de.hhu.stups.codegenerator.generators.ExpressionGenerator;
 import de.hhu.stups.codegenerator.generators.MachineGenerator;
+import de.hhu.stups.codegenerator.generators.PredicateGenerator;
 import de.hhu.stups.codegenerator.generators.TypeGenerator;
 import de.hhu.stups.codegenerator.handlers.IterationConstructHandler;
 import de.hhu.stups.codegenerator.handlers.TemplateHandler;
@@ -16,6 +19,7 @@ import org.stringtemplate.v4.STGroup;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.List;
+import java.util.stream.Collectors;
 
 /**
  * Created by fabian on 04.03.19.
@@ -34,15 +38,21 @@ public class SetComprehensionGenerator {
 
     private final TypeGenerator typeGenerator;
 
+    private final PredicateGenerator predicateGenerator;
+
+    private final ExpressionGenerator expressionGenerator;
+
     public SetComprehensionGenerator(final STGroup group, final MachineGenerator machineGenerator, final IterationConstructGenerator iterationConstructGenerator,
                                      final IterationConstructHandler iterationConstructHandler, final IterationPredicateGenerator iterationPredicateGenerator,
-                                     final TypeGenerator typeGenerator) {
+                                     final TypeGenerator typeGenerator, final ExpressionGenerator expressionGenerator, final PredicateGenerator predicateGenerator) {
         this.group = group;
         this.machineGenerator = machineGenerator;
         this.iterationConstructGenerator = iterationConstructGenerator;
         this.iterationConstructHandler = iterationConstructHandler;
         this.iterationPredicateGenerator = iterationPredicateGenerator;
         this.typeGenerator = typeGenerator;
+        this.predicateGenerator = predicateGenerator;
+        this.expressionGenerator = expressionGenerator;
     }
 
     /*
@@ -73,6 +83,79 @@ public class SetComprehensionGenerator {
         return result;
     }
 
+    /*
+     * This function generates code for a set comprehension by constraint solving from the belonging AST node
+     */
+    public String generateConstraintSet(SetComprehensionNode node) {
+        machineGenerator.inIterationConstruct(node.getDeclarationList());
+        List<DeclarationNode> declarations = node.getDeclarationList();
+
+        ST template = group.getInstanceOf("constraint_solving");
+
+        List<ST> declarationTemplates = new ArrayList<>();
+        for (DeclarationNode declaration: declarations) {
+            declarationTemplates.add(generateConstraintVariableDeclaration(declaration));
+        }
+
+        int iterationConstructCounter = iterationConstructHandler.getIterationConstructCounter();
+        String identifier = "_cs_set_" + iterationConstructCounter;
+        String problemIdentifier = "_cs_problem_" + 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("variableDeclarations", declarationTemplates);
+        template.add("constraint", generateConstraint((PredicateOperatorNode) node.getPredicateNode(), declarations));
+
+        String result = template.render();
+        iterationConstructGenerator.addGeneration(node.toString(), identifier, declarations, result);
+
+        machineGenerator.leaveIterationConstruct(node.getDeclarationList());
+        return result;
+    }
+
+    public ST generateConstraintVariableDeclaration(DeclarationNode declaration) {
+        ST range = group.getInstanceOf("constraint_type");
+        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);
+                break;
+            default:
+                throw new CodeGenerationException("Type " + declaration.getType().toString() + " not supported for constraint solving!");
+        }
+
+        int iterationConstructCounter = iterationConstructHandler.getIterationConstructCounter();
+        String problemIdentifier = "_cs_problem_" + iterationConstructCounter;
+
+        ST template = group.getInstanceOf("constraint_variable_declaration");
+        template.add("identifier", declaration.getName());
+        template.add("range", range.render());
+        template.add("problemIdentifier", problemIdentifier);
+        return template;
+    }
+
+    public String generateConstraint(PredicateOperatorNode predicate, List<DeclarationNode> declarations) {
+        ST constraint = group.getInstanceOf("constraint");
+
+        int iterationConstructCounter = iterationConstructHandler.getIterationConstructCounter();
+        String problemIdentifier = "_cs_problem_" + 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("constraintFunction", predicateGenerator.visitPredicateOperatorNode(predicate));
+
+        return constraint.render();
+    }
+
     /*
     * This function generates code for the predicate of a set comprehension
     */

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

 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.IterationConstructGenerator;
 import de.hhu.stups.codegenerator.generators.MachineGenerator;
 import de.hhu.stups.codegenerator.generators.TypeGenerator;
@@ -31,8 +33,13 @@ public class IterationConstructHandler {
 
     private final STGroup group;
 
+    private final boolean useConstraintSolving;
+
+    private ExpressionGenerator expressionGenerator;
+    private PredicateGenerator predicateGenerator;
+
     public IterationConstructHandler(final STGroup group, final MachineGenerator machineGenerator, final NameHandler nameHandler,
-                                     final TypeGenerator typeGenerator, final ImportGenerator importGenerator) {
+                                     final TypeGenerator typeGenerator, final ImportGenerator importGenerator, final boolean useConstraintSolving) {
         this.currentIterationConstructGenerator = null;
         this.iterationConstructCounter = 0;
         this.machineGenerator = machineGenerator;
@@ -40,6 +47,7 @@ public class IterationConstructHandler {
         this.typeGenerator = typeGenerator;
         this.importGenerator = importGenerator;
         this.group = group;
+        this.useConstraintSolving = useConstraintSolving;
     }
 
     public void setIterationConstructGenerator(IterationConstructGenerator iterationConstructGenerator) {
@@ -61,7 +69,7 @@ public class IterationConstructHandler {
     * This function returns a new IterationConstructGenerator
     */
     public IterationConstructGenerator getNewIterationConstructGenerator() {
-        return new IterationConstructGenerator(this, machineGenerator, nameHandler, group, typeGenerator, importGenerator);
+        return new IterationConstructGenerator(this, machineGenerator, nameHandler, group, typeGenerator, importGenerator, expressionGenerator, predicateGenerator, useConstraintSolving);
     }
 
     /*
@@ -153,4 +161,12 @@ public class IterationConstructHandler {
     public IterationConstructGenerator getCurrentIterationConstructGenerator() {
         return currentIterationConstructGenerator;
     }
+
+  public void setExpressionGenerator(ExpressionGenerator expressionGenerator) {
+        this.expressionGenerator = expressionGenerator;
+  }
+
+    public void setPredicateGenerator(PredicateGenerator predicateGenerator) {
+        this.predicateGenerator = predicateGenerator;
+    }
 }

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

@@ -15,8 +15,6 @@ from btypes.BUtils import BUtils
 
 class <machine>:
 
-
-
     <sets; separator="\n">
 
     <initialization>
@@ -199,6 +197,38 @@ if(<predicate>).booleanValue():
 <endif>
 >>
 
+constraint_solving(identifier, problemIdentifier, variableDeclarations, constraint, isRelation) ::= <<
+from constraint import Problem
+from functools import reduce
+from btypes.BSet import BSet
+from btypes.BUtils import BUtils
+<problemIdentifier> = Problem()
+<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())
+<endif>
+>>
+
+constraint_variable_declaration(identifier, problemIdentifier, range) ::= <<
+<identifier> = <problemIdentifier>.addVariable("<identifier>", <range>)
+>>
+
+constraint_type(isInteger, minInt, maxInt, isBoolean, isSet) ::= <<
+<if(isInteger)>BSet.interval(<minInt>, <maxInt>).getSet()<elseif(isBoolean)>BUtils.BOOL.getSet()<endif>
+>>
+
+constraint(problemIdentifier, var1, var2, constraintFunction) ::= <<
+<problemIdentifier>.addConstraint(lambda <var1><var2 : {var |, <var>}>: <constraintFunction>, ("<var1>"<var2 : {var |, "<var>"}>))
+>>
+
 lambda(type, identifier, lambda, leftType, rightType) ::= <<
 <identifier> = BRelation()
 <lambda>
@@ -407,11 +437,11 @@ binary(arg1,operator,arg2) ::= <<
 >>
 
 or(arg1, arg2) ::= <<
-<arg1> or <arg2>
+(<arg1> or <arg2>)
 >>
 
 and(arg1, arg2) ::= <<
-<arg1> and <arg2>
+(<arg1> and <arg2>)
 >>
 
 implies(arg1, arg2) ::= <<
@@ -529,8 +559,8 @@ identifier(identifier, rhsOnLhs, fromOtherMachine, otherMachine, isPrivate) ::=
 <if(fromOtherMachine)>self.<otherMachine>._get_<identifier>()<else><if(rhsOnLhs)>_ld_<identifier><else><if(isPrivate)>self.<endif><identifier><endif><endif>
 >>
 
-number(number, useBigInteger) ::= <<
-<if(useBigInteger)>BInteger("<number>")<else>BInteger(<number>)<endif>
+number(number) ::= <<
+BInteger(<number>)
 >>
 
 infinite_predicate(arg, operator) ::= <<

src/test/java/de/hhu/stups/codegenerator/TestC.java

@@ -29,7 +29,7 @@ public class TestC {
         Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
                 .getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
         CodeGenerator codeGenerator = new CodeGenerator();
-        List<Path> cFilePaths = codeGenerator.generate(mchPath, GeneratorMode.C, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, null, false);
+        List<Path> cFilePaths = codeGenerator.generate(mchPath, GeneratorMode.C, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", false,true, null, false);
 
         //cFilePaths.forEach(path -> cleanUp(path.toString()));
     }

src/test/java/de/hhu/stups/codegenerator/TestClojure.java

@@ -25,7 +25,7 @@ public class TestClojure {
         Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
                 .getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
         CodeGenerator codeGenerator = new CodeGenerator();
-        List<Path> cljFilePaths = codeGenerator.generate(mchPath, GeneratorMode.CLJ, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, null, false);
+        List<Path> cljFilePaths = codeGenerator.generate(mchPath, GeneratorMode.CLJ, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", false, true, null, false);
 
         //cljFilePaths.forEach(path -> cleanUp(path.toString()));
     }

src/test/java/de/hhu/stups/codegenerator/cpp/TestCpp.java

@@ -48,7 +48,7 @@ public class TestCpp {
 		Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
 				.getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
 		CodeGenerator codeGenerator = new CodeGenerator();
-		List<Path> cppFilePaths = codeGenerator.generate(mchPath, GeneratorMode.CPP, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, null, false);
+		List<Path> cppFilePaths = codeGenerator.generate(mchPath, GeneratorMode.CPP, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", false,true, null, false);
 
 		Process process = Runtime.getRuntime()
 				.exec("g++ -std=c++14 -O2 -march=native -g -DIMMER_NO_THREAD_SAFETY -c " + cppFilePaths.get(cppFilePaths.size() - 1).toFile().getAbsoluteFile().toString());
@@ -63,7 +63,7 @@ public class TestCpp {
 		Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
 				.getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
 		CodeGenerator codeGenerator = new CodeGenerator();
-		List<Path> cppFilePaths = codeGenerator.generate(mchPath, GeneratorMode.CPP, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, addition, false);
+		List<Path> cppFilePaths = codeGenerator.generate(mchPath, GeneratorMode.CPP, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", false,true, addition, false);
 
 		Runtime runtime = Runtime.getRuntime();
 

src/test/java/de/hhu/stups/codegenerator/java/TestJava.java

@@ -48,7 +48,7 @@ public class TestJava {
 		Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
 				.getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
 		CodeGenerator codeGenerator = new CodeGenerator();
-		List<Path> javaFilePaths = codeGenerator.generate(mchPath, GeneratorMode.JAVA, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, null, false);
+		List<Path> javaFilePaths = codeGenerator.generate(mchPath, GeneratorMode.JAVA, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", false,true, null, false);
 		Process process = Runtime.getRuntime()
 				.exec("javac -classpath btypes_persistent.jar " + String.join(" ", javaFilePaths.stream()
 						.map(path -> path.toFile().getAbsoluteFile().toString())
@@ -71,7 +71,7 @@ public class TestJava {
 		Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
 				.getResource("de/hhu/stups/codegenerator/" + machinePath + ".mch").toURI());
 		CodeGenerator codeGenerator = new CodeGenerator();
-		List<Path> javaFilePaths = codeGenerator.generate(mchPath, GeneratorMode.JAVA, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, addition, false);
+		List<Path> javaFilePaths = codeGenerator.generate(mchPath, GeneratorMode.JAVA, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", false, true, addition, false);
 		Runtime runtime = Runtime.getRuntime();
 		Process compileProcess = runtime.exec("javac -cp btypes_persistent.jar " +
 				String.join(" ", javaFilePaths.stream()

src/test/java/de/hhu/stups/codegenerator/python/TestPython.java

@@ -45,7 +45,7 @@ public class TestPython {
 		Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
 				.getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
 		CodeGenerator codeGenerator = new CodeGenerator();
-		List<Path> pythonFilePaths = codeGenerator.generate(mchPath, GeneratorMode.PY, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, null, false);
+		List<Path> pythonFilePaths = codeGenerator.generate(mchPath, GeneratorMode.PY, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, true, null, false);
 
 		//pythonFilePaths.forEach(path -> cleanUp(path.toString()));
 	}
@@ -55,7 +55,7 @@ public class TestPython {
 		Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
 				.getResource("de/hhu/stups/codegenerator/" + machinePath + ".mch").toURI());
 		CodeGenerator codeGenerator = new CodeGenerator();
-		List<Path> pythonFilePaths = codeGenerator.generate(mchPath, GeneratorMode.PY, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, addition, false);
+		List<Path> pythonFilePaths = codeGenerator.generate(mchPath, GeneratorMode.PY, false, String.valueOf(Integer.MIN_VALUE), String.valueOf(Integer.MAX_VALUE), "10", true, true, addition, false);
 
     Path mainPath = pythonFilePaths.get(pythonFilePaths.size() - 1);
 

src/test/java/de/hhu/stups/codegenerator/python/TestSetComprehension.java

+package de.hhu.stups.codegenerator.python;
+
+import org.junit.Test;
+
+public class TestSetComprehension extends TestPython {
+
+    @Test
+    public void testSetComprehensionInteger() throws Exception {
+        testPython("set_comprehension/SetComprehensionInteger", "SetComprehensionInteger", "SetComprehensionIntegerAddition.stpy", true);
+    }
+
+    @Test
+    public void testSetComprehensionInteger2() throws Exception {
+        testPython("set_comprehension/SetComprehensionInteger2", "SetComprehensionInteger2", "SetComprehensionInteger2Addition.stpy", true);
+    }
+
+    @Test
+    public void testSetComprehensionInteger3() throws Exception {
+        testPython("set_comprehension/SetComprehensionInteger3", "SetComprehensionInteger3", "SetComprehensionInteger3Addition.stpy", true);
+    }
+
+    @Test
+    public void testSetComprehensionBool() throws Exception {
+        testPython("set_comprehension/SetComprehensionBool", "SetComprehensionBool", "SetComprehensionBoolAddition.stpy", true);
+    }
+
+    @Test
+    public void testSetComprehensionBool2() throws Exception {
+        testPython("set_comprehension/SetComprehensionBool2", "SetComprehensionBool2", "SetComprehensionBool2Addition.stpy", true);
+    }
+
+    @Test
+    public void testSetComprehensionExists() throws Exception {
+        testPython("set_comprehension/SetComprehensionExists", "SetComprehensionExists", "SetComprehensionExistsAddition.stpy", true);
+    }
+}

src/test/resources/de/hhu/stups/codegenerator/set_comprehension/SetComprehensionBool.mch

+MACHINE SetComprehensionBool
+
+VARIABLES  x
+
+INVARIANT  x : POW(BOOL*BOOL)
+
+INITIALISATION x := {}
+
+OPERATIONS
+
+	calculate =
+	    x:={a,b|a=TRUE or b=TRUE};
+
+	out <-- getCard = out := card(x);
+	
+	out <-- getSet = out := x
+
+END
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/set_comprehension/SetComprehensionBool.out

+3
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/set_comprehension/SetComprehensionBool2.mch

+MACHINE SetComprehensionBool2
+
+VARIABLES  x
+
+INVARIANT  x : POW(BOOL*BOOL*BOOL*BOOL)
+
+INITIALISATION x := {}
+
+OPERATIONS
+
+	calculate =
+	    x:={a,b,c,d|(a=TRUE or b=TRUE) & (c=TRUE or d=TRUE)};
+
+	out <-- getCard = out := card(x);
+	
+	out <-- getSet = out := x
+
+END
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/set_comprehension/SetComprehensionBool2.out

+9
\ No newline at end of file