-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Description
Hi! I have to develop an app similar to yours and I found a bug that could affect the usage of the tool. If you provide an unsat level of pruning the tool won't do anything. So when you try checking that if the provided level is sat you should first push the context and then add the bias constraint with prune_level. If it's sat, pop the context and then add again the constraint. It should look something like this:
`else:
self.solver.push()
self.add_ddt_constraints(prune_level)
if self.solver.check() == sat:
self.solver.pop()
self.prune_level = prune_level
self.add_ddt_constraints(prune_level)
else:
print(
"The provided pruning lever results in an unsat system! Searching for optimal pruning level..."
)
print()
self.solver.pop()
self.init_differential_characteristic_solver(-1)`
I changed the names so that this pruning integrates in the code I developed.
Metadata
Metadata
Assignees
Labels
No labels