bug fix #6934

[hgvk94]

No description provided.

[NikolajBjorner]

I don't understand the rationale for the filter.
If something rewrites and to not(or(not..)) then one version is filtered, the other isn't.

[hgvk94]

I don't understand the rationale for the filter. If something rewrites and to not(or(not..)) then one version is filtered, the other isn't.

The plugin for projection of logical symbols (mbp_basic_tg.cpp) will pick an implicant. The filter is supposed to remove all other literals. If we have a literal l === not(or(not(p))), we first add l as a whole to the term graph. Then, mbp_basic adds p as a literal in the term graph, merges equivalence classes of not(p), or(not(p)) with False and class of l with True. When printing the term graph, the filter hides all classes with re-written terms.

[NikolajBjorner]

I am not sure about the explanation. The core of the question is what the pre/post conditions on these passes are, that are used for correctness. Since x & y = !x || !y by de Morgan, the same formula (same meaning) written in two different ways will pass/fail the filters in different ways. So, the condition is syntactic and seems very brittle. Are you able to capture using assertions the assumptions that are made by this code?

[hgvk94]

The proof is not local. The call to saturate() applies MBP rules such that all these terms have ground represatives. The pre-condition here is that if a term is filtered, it has a ground term in its class. The post condition is that the formula after is MBP(v, fml, mdl) where v are all variables on which MBP rules have been applied.

[NikolajBjorner]

I will take the pull request, but based on the discussion I don't think it is a real fix. Fuzzing is bound to find more bugs this way. It is brittle to have long distance assumptions (regardless of what software), and worse when the assumptions are syntactic.