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

Revised algorithm to cache closures

Browse source
This commit is contained in:
Brandon Rozek 2025-11-24 16:52:04 -05:00
parent 2fbdf26274
commit 872e54ec5e
1 changed files with 34 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

91
vsp.py
View file

@ -3,7 +3,7 @@ Check to see if the model has the variable
sharing property. sharing property.
""" """
from itertools import product from itertools import product
from typing import List, Optional, Set, Tuple from typing import Dict, List, Optional, Set, Tuple
from common import set_to_str from common import set_to_str
from model import ( from model import (
Model, model_closure, ModelFunction, ModelValue Model, model_closure, ModelFunction, ModelValue
@ -43,81 +43,46 @@ def has_vsp(model: Model, impfunction: ModelFunction,
top = model.ordering.top() top = model.ordering.top()
bottom = model.ordering.bottom() bottom = model.ordering.bottom()
# Compute I the set of tuples (x, y) where C: Dict[ModelValue, Set[ModelValue]] = {}
# x -> y does not take a designiated value U: Dict[ModelValue, Set[ModelValue]] = {}
I: List[Tuple[ModelValue, ModelValue]] = []
for (x, y) in product(model.designated_values, model.designated_values): for d in model.designated_values:
if impfunction(x, y) not in model.designated_values: C[d] = model_closure({d,}, model.logical_operations, None)
I.append((x, y)) U[d] = {y for y in model.designated_values if impfunction(d, y) in model.designated_values}
# Find the subalgebras which falsify implication for x in model.designated_values:
for xys in I: Xs = C[x]
xi = xys[0]
# Discard ({⊥} ∪ A', B) subalgebras # Discard ({⊥} ∪ A', B) subalgebras
if bottom is not None and xi == bottom: if bottom is not None and bottom in Xs:
continue continue
# Discard ({⊤} ∪ A', B) subalgebras when negation is defined # Discard ({⊤} ∪ A', B) subalgebras when negation is defined
if top is not None and negation_defined and xi == top: if top is not None and negation_defined and top in Xs:
continue continue
yi = xys[1] Ux = U[x]
for y in model.designated_values - Xs - Ux:
Ys = C[y]
# Discard (A, {⊤} ∪ B') subalgebras # Discard (A, {⊤} ∪ B') subalgebras
if top is not None and yi == top: if top is not None and top in Ys:
continue continue
# Discard (A, {⊥} ∪ B') subalgebras when negation is defined # Discard (A, {⊥} ∪ B') subalgebras when negation is defined
if bottom is not None and negation_defined and yi == bottom: if bottom is not None and negation_defined and bottom in Ys:
continue continue
# Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b if not Xs.isdisjoint(Ys):
if model.ordering.is_lt(xi, yi): continue
continue
# Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined falsified = True
if negation_defined and model.ordering.is_lt(yi, xi): for (xi, yi) in product(Xs, Ys):
continue if impfunction(xi, yi) in model.designated_values:
falsified = False
break
# Compute the left closure of the set containing xi under all the operations if falsified:
carrier_set_left: Set[ModelValue] = model_closure({xi,}, model.logical_operations, bottom) return VSP_Result(True, model.name, Xs, Ys)
# 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
# Compute the closure of all operations
# with just the ys
carrier_set_right: Set[ModelValue] = model_closure({yi,}, model.logical_operations, top)
# 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) return VSP_Result(False, model.name)