diff --git a/model.py b/model.py index 807f1ec..41483f9 100644 --- a/model.py +++ b/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)} """ diff --git a/utils/compare_vsp_results.py b/utils/compare_vsp_results.py index 82c587d..aa16aa5 100644 --- a/utils/compare_vsp_results.py +++ b/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 diff --git a/vsp.py b/vsp.py index ee87657..5ea2ae9 100644 --- a/vsp.py +++ b/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"""Model {self.model_name} has the variable sharing property. + return f"Matrix {self.model_name} does not have 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) diff --git a/vspursuer.py b/vspursuer.py index d9d9e53..67e73fa 100755 --- a/vspursuer.py +++ b/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 - result = has_vsp_plus_model(model, impfunction, negation_defined) + (model, impfunction, negation_defined, conjunction_disjunction_defined) = task + 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: - model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined) + for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions: + 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__":