brozek/vspursuer
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/matmod.git synced 2026-01-30 07:33:38 +00:00
Code Issues Projects Releases Packages Wiki Activity

Some comment changes

Browse source
This commit is contained in:
Brandon Rozek 2026-01-27 11:23:47 -05:00
parent 07d7b2fdb1
commit f8eca388d4
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
smt.py
View file

@ -230,7 +230,7 @@ class SMTLogicEncoder:
for smt_elem in self.smt_carrier_set for smt_elem in self.smt_carrier_set
} }
# Exclude operation function mappings # Iterate over all logical operations
for model_func in model.logical_operations: for model_func in model.logical_operations:
operation = Operation(model_func.operation_name, model_func.arity) operation = Operation(model_func.operation_name, model_func.arity)
smt_func = self.operation_function_map[operation] smt_func = self.operation_function_map[operation]
@ -239,10 +239,9 @@ class SMTLogicEncoder:
smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs) smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs)
smt_output = model_value_to_smt[output] smt_output = model_value_to_smt[output]
# For future models the input->output mapping may differ # It may be the case that the output of f(input) differs
constraints.append(smt_func(*smt_inputs) != smt_output) constraints.append(smt_func(*smt_inputs) != smt_output)
# Exclude designated value set
for smt_elem in self.smt_carrier_set: for smt_elem in self.smt_carrier_set:
model_val = ModelValue(str(smt_elem)) model_val = ModelValue(str(smt_elem))
is_designated_in_model = model_val in model.designated_values is_designated_in_model = model_val in model.designated_values

2
vsp.py
View file

@ -168,7 +168,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
) )
) )
# x -> y is non-designated # x -> y is non-designated for any x in K1 and y in K2
smt_imp = encoder.model_function_map[impfn] smt_imp = encoder.model_function_map[impfn]
for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set): for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
encoder.solver.add( encoder.solver.add(