Check models in parallel (#25)

common.py

@@ -1,4 +1,7 @@
 from typing import Set
 
+def immutable(_self, _name, _value):
+    raise Exception("Model values are immutable")
+
 def set_to_str(x: Set) -> str:
     return "{" + ", ".join((str(xi) for xi in x)) + "}"

logic.py

@@ -1,3 +1,4 @@
+from common import immutable
 from typing import Optional, Set, Tuple
 from functools import lru_cache
 
@@ -6,13 +7,14 @@ class Operation:
         self.symbol = symbol
         self.arity = arity
         self.hashed_value = hash(self.symbol) + self.arity
-        def immutable(self, name, value):
-            raise Exception("Operations are immutable")
         self.__setattr__ = immutable
 
     def __hash__(self):
         return self.hashed_value
 
+    def __eq__(self, x):
+        return self.symbol == x.symbol and self.arity == x.arity
+
     def __call__(self, *args):
         # Ensure the arity is met
         assert len(args) == self.arity

model.py

@@ -2,7 +2,7 @@
 Matrix model semantics and satisfiability of
 a given logic.
 """
-from common import set_to_str
+from common import set_to_str, immutable
 from logic import (
     get_propostional_variables, Logic,
     Operation, PropositionalVariable, Term
@@ -15,13 +15,10 @@ from typing import Dict, List, Optional, Set, Tuple
 
 __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation']
 
-
 class ModelValue:
     def __init__(self, name):
         self.name = name
         self.hashed_value = hash(self.name)
-        def immutable(self, name, value):
-            raise Exception("Model values are immutable")
         self.__setattr__ = immutable
     def __str__(self):
         return self.name
@@ -255,7 +252,7 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction],
                         new_elements.add(element)
 
                     # Optimization: Break out of computation
-                    # early when top or bottom element is foun
+                    # early when forbidden element is found
                     if forbidden_element is not None and element == forbidden_element:
                         forbidden_found = True
                         break
@@ -287,7 +284,7 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction],
                             new_elements.add(element)
 
                         # Optimization: Break out of computation
-                        # early when top or bottom element is foun
+                        # early when forbidden element is found
                         if forbidden_element is not None and element == forbidden_element:
                             forbidden_found = True
                             break

parse_magic.py

@@ -410,7 +410,7 @@ def mvalue_from_index(i: int) -> ModelValue:
     Given an index, return the
     representation of the model value.
     """
-    return ModelValue(f"a{i}")
+    return ModelValue(f"{i}")
 
 def parse_mvalue(x: str) -> ModelValue:
     """

vspursuer.py

@@ -1,10 +1,13 @@
 #!/usr/bin/env python3
+from os import cpu_count
 import argparse
+import multiprocessing
+
 from parse_magic import (
     SourceFile,
     parse_matrices
 )
-from vsp import has_vsp
+from vsp import has_vsp, VSP_Result
 
 if __name__ == "__main__":
     parser = argparse.ArgumentParser(description="VSP Checker")
@@ -22,14 +25,21 @@ if __name__ == "__main__":
     print(f"Parsed {len(solutions)} matrices")
 
     num_has_vsp = 0
-    for i, (model, interpretation) in enumerate(solutions):
-        vsp_result = has_vsp(model, interpretation)
-        print(vsp_result)
+    with multiprocessing.Pool(processes=max(cpu_count() - 2, 1)) as pool:
+        results = [
+            pool.apply_async(has_vsp, (model, interpretation,))
+            for model, interpretation in solutions
+        ]
 
-        if args['verbose'] or vsp_result.has_vsp:
-            print(model)
+        for i, result in enumerate(results):
+            vsp_result: VSP_Result = result.get()
+            print(vsp_result)
 
-        if vsp_result.has_vsp:
-            num_has_vsp += 1
+            if args['verbose'] or vsp_result.has_vsp:
+                model = solutions[i][0]
+                print(model)
+
+            if vsp_result.has_vsp:
+                num_has_vsp += 1
 
     print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP")