ersatz creates duplicate clauses

[jwaldmann]

Ersatz had Formula = Set Clause (where "formula" means "CNF" - while actual formulas (DAGs) are represented by the type Bit).

Semantically, this is correct, but I checked that this creates massive performance problems. So I replaced this with Formula = Seq Clause. But now these formulas contains lots of duplicate clauses. (Sometimes, 9 out of 10 clauses are duplicate.) This should not happen, or - I don't understand what is happening. Is there something broken with detecting sharing, so some trees (DAG nodes) are visited more than once?

Minisat can handle duplicate clauses just fine. The motivation for investigation is to reduce ersatz execution time for building the formula, by no re-visiting subtrees (as long as it's easy to detect).

Plan: write graphviz binding to show the DAG. Identify nodes in the DAG by makeStablePointer (just as runBit / generateLiteral do).

[ekmett]

Would using something like a HashSet help to reduce the cost of comparing clauses for ordering?

[jwaldmann]

possibly yes, but I'd rather find out why there are duplicate clauses at all.

[jwaldmann]

Consider this program:

let x1 = not (and ...) -- creates Not (And (...)
    x2 = not x1    -- creates (And (...))
    x3 = not x2    -- creates Not (And (...))

This is due to rule not (Not c) = c (from the original ersatz code https://github.com/ekmett/ersatz/blame/master/src/Ersatz/Bit.hs#L91 ). Nodes for x1 and x3 will be semantically equivalent, but makeStablePointer will not detect this, because we called the Not constructor two times.

But then, this should not be a problem since Not nodes will never allocate a new variable (in runBit).

Still, something similar might happen for And nodes that are de/re-constructed during AIG "simplifications" (introduced by me).

[jwaldmann]

Idea from previous message does not apply. Formula construction is OK, but duplicates were produced when asserting.