Merge branch 'main' into feat/46

model.py

@@ -129,6 +129,12 @@ class OrderTable:
 
         candidates = X.intersection(Y)
 
+        if not candidates:
+            return None
+
+        if len(candidates) == 1:
+            return next(iter(candidates))
+
         # Grab all elements greater than each of the candidates
         candidate_ge_maps = (self.ge_map[candidate] for candidate in candidates)
         common_ge_values = reduce(set.intersection, candidate_ge_maps)
@@ -147,6 +153,12 @@ class OrderTable:
 
         candidates = X.intersection(Y)
 
+        if not candidates:
+            return None
+
+        if len(candidates) == 1:
+            return next(iter(candidates))
+
         # Grab all elements smaller than each of the candidates
         candidate_le_maps = (self.le_map[candidate] for candidate in candidates)
         common_le_values = reduce(set.intersection, candidate_le_maps)
@@ -209,7 +221,7 @@ class Model:
 
     def __str__(self):
         result = ("=" * 25) + f"""
-Model Name: {self.name}
+Matrix Name: {self.name}
 Carrier Set: {set_to_str(self.carrier_set)}
 Designated Values: {set_to_str(self.designated_values)}
 """

utils/compare_vsp_results.py

@@ -56,9 +56,9 @@ if __name__ == "__main__":
     extra_models1 = 0
     extra_models2 = 0
 
-    for model, impfunction, negation_defined in solutions1:
+    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions1:
         total_models1 += 1
-        vsp_result = has_vsp(model, impfunction, negation_defined)
+        vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
 
         if vsp_result.has_vsp:
             good_models1 += 1
@@ -83,9 +83,9 @@ if __name__ == "__main__":
 
 
     # Check through the remaining models in the second set
-    for model, impfunction, negation_defined in solutions2:
+    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions2:
         total_models2 += 1
-        vsp_result = has_vsp(model, impfunction, negation_defined)
+        vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
 
         if not vsp_result.has_vsp:
             bad_models2 += 1

vsp.py

@@ -29,14 +29,14 @@ class VSP_Result:
 
     def __str__(self):
         if not self.has_vsp:
-            return f"Model {self.model_name} does not have the variable sharing property."
+            return f"Matrix {self.model_name} does not have the variable sharing property."
-        return f"""Model {self.model_name} has the variable sharing property.
+        return f"""Matrix {self.model_name} has the variable sharing property.
 Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
 def has_vsp_magical(model: Model, impfunction: ModelFunction,
-            negation_defined: bool) -> VSP_Result:
+            negation_defined: bool, conjunction_disjunction_defined: bool) -> VSP_Result:
     """
     Checks whether a MaGIC model has the variable
     sharing property.
@@ -46,6 +46,10 @@ def has_vsp_magical(model: Model, impfunction: ModelFunction,
     if len(model.designated_values) == 1:
         return VSP_Result(False, model.name)
 
+    if len(model.carrier_set) in [2,3,4,5,7] \
+        and conjunction_disjunction_defined and negation_defined:
+        return VSP_Result(False, model.name)
+
     assert model.ordering is not None, "Expected ordering table in model"
 
     top = model.ordering.top()
@@ -190,9 +194,9 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
 
 
 def has_vsp(model: Model, impfunction: ModelFunction,
-            negation_defined: bool) -> VSP_Result:
+            negation_defined: bool, conjunction_disjunction_defined: bool) -> VSP_Result:
     if model.is_magical:
-        return has_vsp_magical(model, impfunction, negation_defined)
+        return has_vsp_magical(model, impfunction, negation_defined, conjunction_disjunction_defined)
 
     return has_vsp_smt(model)
 

vspursuer.py

@@ -6,7 +6,7 @@ from queue import Empty as QueueEmpty
 import argparse
 import multiprocessing as mp
 
-from logic import Negation, Implication, Operation
+from logic import Conjunction, Disjunction, Implication, Negation, Operation
 from model import Model, ModelFunction
 from parse_magic import SourceFile, parse_matrices
 from vsp import has_vsp, VSP_Result
@@ -36,13 +36,14 @@ def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, Model
         # NOTE: Implication must be defined, the rest may not
         impfunction = interpretation[Implication]
         negation_defined = Negation in interpretation
-        yield (model, impfunction, negation_defined)
+        conjunction_disjunction_defined = (Conjunction in interpretation) and (Disjunction in interpretation)
+        yield (model, impfunction, negation_defined, conjunction_disjunction_defined)
 
-def has_vsp_plus_model(model, impfunction, negation_defined) -> Tuple[Optional[Model], VSP_Result]:
+def has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined) -> Tuple[Optional[Model], VSP_Result]:
     """
     Wrapper which also stores the models along with its vsp result
     """
-    vsp_result = has_vsp(model, impfunction, negation_defined)
+    vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
     # NOTE: Memory optimization - Don't return model if it doesn't have VSP
     model = model if vsp_result.has_vsp else None
     return (model, vsp_result)
@@ -61,8 +62,8 @@ def worker_vsp(task_queue: mp.Queue, result_queue: mp.Queue):
             # If sentinal value, break
             if task is None:
                 break
-            (model, impfunction, negation_defined) = task
+            (model, impfunction, negation_defined, conjunction_disjunction_defined) = task
-            result = has_vsp_plus_model(model, impfunction, negation_defined)
+            result = has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined)
             result_queue.put(result)
     finally:
         # Either an exception occured or the worker finished
@@ -168,7 +169,7 @@ def multi_process_runner(num_cpu: int, data_file_path: str, skip_to: Optional[st
         if vsp_result.has_vsp:
             num_has_vsp += 1
 
-    print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP")
+    print_with_timestamp(f"Tested {num_tested} matrices, {num_has_vsp} of which satisfy VSP")
 
 def single_process_runner(data_file_path: str, skip_to: Optional[str]):
     num_tested = 0
@@ -178,8 +179,8 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
     solutions = parse_matrices(SourceFile(data_file))
     solutions = restructure_solutions(solutions, skip_to)
 
-    for model, impfunction, negation_defined in solutions:
+    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions:
-        model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined)
+        model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined)
         print_with_timestamp(vsp_result)
         num_tested += 1
 
@@ -189,7 +190,7 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
         if vsp_result.has_vsp:
             num_has_vsp += 1
 
-    print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP")
+    print_with_timestamp(f"Tested {num_tested} matrices, {num_has_vsp} of which satisfy VSP")
 
 
 if __name__ == "__main__":