feat: add --theories option to command line

main.py

@@ -43,6 +43,8 @@ def parse_args():
                         default='fusion_functions', help='name of the output file')
     parser.add_argument('--dot', '-d', action='store_true',
                         help='emit formulas and inverses also to dot files')
+    parser.add_argument('--theories', choices=['bool', 'int', 'real', 'string'], nargs='+',
+                        default=[], help='specify the theories to be used during generation')
     return parser.parse_args()
 
 
@@ -54,6 +56,12 @@ def main(args):
         file_name += '.txt'
 
     operator_types = gen_configuration.get_theories()
+    if args.theories:
+        operator_types = [gen_configuration.option_to_operator_type[option]
+                          for option in args.theories]
+    if args.verbose:
+        print(f"Using theories: {operator_types}")
+
     infix_printer = InfixPrinterVisitor()
     trees = []
     for i in range(args.num_functions):

src/gen/gen_configuration.py

@@ -96,6 +96,14 @@
     "StringOperator": "StringEquality",
 }
 
+# A map from command line options to the internal representation.
+option_to_operator_type: Dict[str, str] = {
+    "bool": "BooleanOperator",
+    "int": "IntegerOperator",
+    "real": "RealOperator",
+    "string": "StringOperator",
+}
+
 
 def get_theories():
     return list(theory_declarations.keys())