mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2025-12-07 04:30:23 +00:00
118 lines
4.1 KiB
Python
118 lines
4.1 KiB
Python
"""
|
||
Check to see if the model has the variable
|
||
sharing property.
|
||
"""
|
||
from itertools import product
|
||
from typing import Dict, List, Optional, Set, Tuple
|
||
from common import set_to_str
|
||
from model import (
|
||
Model, model_closure, ModelFunction, ModelValue
|
||
)
|
||
|
||
class VSP_Result:
|
||
def __init__(
|
||
self, has_vsp: bool, model_name: Optional[str] = None,
|
||
subalgebra1: Optional[Set[ModelValue]] = None,
|
||
subalgebra2: Optional[Set[ModelValue]] = None):
|
||
self.has_vsp = has_vsp
|
||
self.model_name = model_name
|
||
self.subalgebra1 = subalgebra1
|
||
self.subalgebra2 = subalgebra2
|
||
|
||
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.
|
||
Subalgebra 1: {set_to_str(self.subalgebra1)}
|
||
Subalgebra 2: {set_to_str(self.subalgebra2)}
|
||
"""
|
||
|
||
def has_vsp(model: Model, impfunction: ModelFunction,
|
||
negation_defined: bool) -> VSP_Result:
|
||
"""
|
||
Checks whether a model has the variable
|
||
sharing property.
|
||
"""
|
||
# NOTE: No models with only one designated
|
||
# value satisfies VSP
|
||
if len(model.designated_values) == 1:
|
||
return VSP_Result(False, model.name)
|
||
|
||
assert model.ordering is not None, "Expected ordering table in model"
|
||
|
||
top = model.ordering.top()
|
||
bottom = model.ordering.bottom()
|
||
|
||
# Cache of closures
|
||
C: Dict[ModelValue, Set[ModelValue]] = {}
|
||
|
||
for x in model.designated_values:
|
||
# Discard ({⊥} ∪ A', B) subalgebras
|
||
if bottom is not None and x == bottom:
|
||
continue
|
||
|
||
# Discard ({⊤} ∪ A', B) subalgebras when negation is defined
|
||
if top is not None and negation_defined and x == top:
|
||
continue
|
||
|
||
candidate_ys = [y for y in model.designated_values if impfunction(x, y) not in model.designated_values]
|
||
|
||
if len(candidate_ys) == 0:
|
||
continue
|
||
|
||
carrier_set_left: Set[ModelValue] = model_closure(C.get(x, {x,}), model.logical_operations, bottom)
|
||
C[x] = carrier_set_left
|
||
|
||
# Discard ({⊥} ∪ A', B) subalgebras
|
||
if bottom is not None and bottom in carrier_set_left:
|
||
continue
|
||
|
||
# Discard ({⊤} ∪ A', B) subalgebras when negation is defined
|
||
if top is not None and negation_defined and top in carrier_set_left:
|
||
continue
|
||
|
||
for y in candidate_ys:
|
||
# Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b
|
||
if model.ordering.is_lt(x, y):
|
||
continue
|
||
|
||
# Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined
|
||
if negation_defined and model.ordering.is_lt(y, x):
|
||
continue
|
||
|
||
|
||
# Discard (A, {⊤} ∪ B') subalgebras
|
||
if top is not None and y == top:
|
||
continue
|
||
|
||
# Discard (A, {⊥} ∪ B') subalgebras when negation is defined
|
||
if bottom is not None and negation_defined and y == bottom:
|
||
continue
|
||
|
||
carrier_set_right: Set[ModelValue] = model_closure(C.get(y, {y,}), model.logical_operations, top)
|
||
C[y] = carrier_set_right
|
||
|
||
# Discard (A, {⊤} ∪ B') subalgebras
|
||
if top is not None and top in carrier_set_right:
|
||
continue
|
||
|
||
# Discard (A, {⊥} ∪ B') subalgebras when negation is defined
|
||
if bottom is not None and negation_defined and bottom in carrier_set_right:
|
||
continue
|
||
|
||
# Discard subalgebras that intersect
|
||
if not carrier_set_left.isdisjoint(carrier_set_right):
|
||
continue
|
||
|
||
# Check whether for all pairs in the subalgebra,
|
||
# that implication is falsified.
|
||
falsified = True
|
||
for (x2, y2) in product(carrier_set_left, carrier_set_right):
|
||
if impfunction(x2, y2) in model.designated_values:
|
||
falsified = False
|
||
break
|
||
|
||
if falsified:
|
||
return VSP_Result(True, model.name, carrier_set_left, carrier_set_right)
|
||
|
||
return VSP_Result(False, model.name)
|