mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2025-07-29 20:52:01 +00:00
Removed a useless optimization and added one when negation is defined
This commit is contained in:
parent
01204a9551
commit
cd084812cc
1 changed files with 3 additions and 8 deletions
11
vsp.py
11
vsp.py
|
@ -78,16 +78,11 @@ def quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined) ->
|
||||||
# skip this pair
|
# skip this pair
|
||||||
if top is not None and top in ys:
|
if top is not None and top in ys:
|
||||||
return True
|
return True
|
||||||
|
if negation_defined and bottom is not None and bottom in ys:
|
||||||
|
return True
|
||||||
if bottom is not None and bottom in xs:
|
if bottom is not None and bottom in xs:
|
||||||
return True
|
return True
|
||||||
|
if negation_defined and top is not None and top in xs:
|
||||||
# If a subalgebra doesn't have at least one
|
|
||||||
# designated value, move onto the next pair.
|
|
||||||
# Depends on no intersection between xs and ys
|
|
||||||
if xs.isdisjoint(model.designated_values):
|
|
||||||
return True
|
|
||||||
|
|
||||||
if ys.isdisjoint(model.designated_values):
|
|
||||||
return True
|
return True
|
||||||
|
|
||||||
# If the two subalgebras intersect, move
|
# If the two subalgebras intersect, move
|
||||||
|
|
Loading…
Add table
Reference in a new issue