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

Added check for falsification rules in satisfiable function

Browse source
This commit is contained in:
Brandon Rozek 2025-12-12 18:21:29 -05:00
parent a5fb1b92bb
commit 84f1c1fd36
1 changed files with 33 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

34
model.py
View file

@ -266,9 +266,9 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode
pvars = tuple(get_propostional_variables(tuple(logic.rules))) pvars = tuple(get_propostional_variables(tuple(logic.rules)))
mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set)) mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set))
for mapping in mappings:
# Make sure that the model satisfies each of the rules
for rule in logic.rules: for rule in logic.rules:
# The rule most hold for all valuations
for mapping in mappings:
# The check only applies if the premises are designated # The check only applies if the premises are designated
premise_met = True premise_met = True
premise_ts: Set[ModelValue] = set() premise_ts: Set[ModelValue] = set()
@ -291,6 +291,36 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode
if consequent_t not in model.designated_values: if consequent_t not in model.designated_values:
return False return False
for rule in logic.falsifies:
# We must find one mapping where this does not hold
counterexample_found = False
for mapping in mappings:
# The check only applies if the premises are designated
premise_met = True
premise_ts: Set[ModelValue] = set()
for premise in rule.premises:
premise_t = evaluate_term(premise, mapping, interpretation)
# As soon as one premise is not designated,
# move to the next rule.
if premise_t not in model.designated_values:
premise_met = False
break
# If designated, keep track of the evaluated term
premise_ts.add(premise_t)
if not premise_met:
continue
# With the premises designated, make sure the consequent is not designated
consequent_t = evaluate_term(rule.conclusion, mapping, interpretation)
if consequent_t not in model.designated_values:
counterexample_found = True
break
if not counterexample_found:
return False
return True return True