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.
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()
I changed the names so that this pruning integrates in the code I developed.