Open StephanGocht opened 4 years ago
Actually this is an issue, because one could delete all constraints from the formula and then log every solution existing, after which one can derive contradiction. While, this is technically correct (clearly we found all solutions) it is not clear that this is what we want as this also allows to log non solutions.
The readme clarifies now that v
is only checking against the current database.
Currently it is possible to log the same solution multiple times by adding the solution and then deleting the according constraint. Or to log non solutions by deleting clauses from the original formula. If we just want to verify that all solutions are found, then this is not an issue. If we want to verify a specific solution count then this needs to be forbidden.