brozek/vspursuer
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/matmod.git synced 2025-12-13 04:50:25 +00:00
Code Issues Projects Releases Packages Wiki Activity

(#52) Skip model sizes 2-5 and 7 when conjunction, disjunction, and negation are defined

Browse source
This commit is contained in:
Brandon Rozek 2025-12-12 11:38:52 -05:00 • committed by GitHub
commit bf2735023f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 18 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

8
utils/compare_vsp_results.py
View file

@ -56,9 +56,9 @@ if __name__ == "__main__":
extra_models1 = 0 extra_models1 = 0
extra_models2 = 0 extra_models2 = 0
for model, impfunction, negation_defined in solutions1: for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions1:
total_models1 += 1 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: if vsp_result.has_vsp:
good_models1 += 1 good_models1 += 1
@ -83,9 +83,9 @@ if __name__ == "__main__":
# Check through the remaining models in the second set # 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 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: if not vsp_result.has_vsp:
bad_models2 += 1 bad_models2 += 1

6
vsp.py
View file

@ -28,7 +28,7 @@ Subalgebra 2: {set_to_str(self.subalgebra2)}
""" """
def has_vsp(model: Model, impfunction: ModelFunction, def has_vsp(model: Model, impfunction: ModelFunction,
negation_defined: bool) -> VSP_Result: negation_defined: bool, conjunction_disjunction_defined: bool) -> VSP_Result:
""" """
Checks whether a model has the variable Checks whether a model has the variable
sharing property. sharing property.
@ -38,6 +38,10 @@ def has_vsp(model: Model, impfunction: ModelFunction,
if len(model.designated_values) == 1: if len(model.designated_values) == 1:
return VSP_Result(False, model.name) 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" assert model.ordering is not None, "Expected ordering table in model"
top = model.ordering.top() top = model.ordering.top()

17
vspursuer.py
View file

@ -6,7 +6,7 @@ from queue import Empty as QueueEmpty
import argparse import argparse
import multiprocessing as mp import multiprocessing as mp
from logic import Negation, Implication, Operation from logic import Conjunction, Disjunction, Implication, Negation, Operation
from model import Model, ModelFunction from model import Model, ModelFunction
from parse_magic import SourceFile, parse_matrices from parse_magic import SourceFile, parse_matrices
from vsp import has_vsp, VSP_Result 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 # NOTE: Implication must be defined, the rest may not
impfunction = interpretation[Implication] impfunction = interpretation[Implication]
negation_defined = Negation in interpretation 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 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 # NOTE: Memory optimization - Don't return model if it doesn't have VSP
model = model if vsp_result.has_vsp else None model = model if vsp_result.has_vsp else None
return (model, vsp_result) return (model, vsp_result)
@ -61,8 +62,8 @@ def worker_vsp(task_queue: mp.Queue, result_queue: mp.Queue):
# If sentinal value, break # If sentinal value, break
if task is None: if task is None:
break 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) result_queue.put(result)
finally: finally:
# Either an exception occured or the worker finished # Either an exception occured or the worker finished
@ -178,8 +179,8 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
solutions = parse_matrices(SourceFile(data_file)) solutions = parse_matrices(SourceFile(data_file))
solutions = restructure_solutions(solutions, skip_to) 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) print_with_timestamp(vsp_result)
num_tested += 1 num_tested += 1