ctx-simplify refcounting issue


It seems like something is wrong with reference counting in ctx_simplify_tactic::imp::m_occs. Right now, when I run the Python program here:


I get the following output:

Or(a, And(Not(b), Not(And(Not(b), c)))) -> [[Or(a, And(Not(b), Not(And(Not(b), c))))]]

meaning, the Not(b) inside the Not(And(...)) is not getting simplified away. In principle, ctx-simplify-tactic should be getting this right, but it turns out this isn't getting simplified because ctx_simplify_tactic::imp::shared() returns false for the 'b' expression. This is despite the fact that 'b' is, infact, shared. After I apply this patch, which ignores m_occs in shared():


the simplification finally works, where the same program produces:

Or(a, And(Not(b), Not(And(Not(b), c)))) -> [[Or(a, And(Not(b), Not(c)))]]
Closed Jun 7, 2013 at 1:32 AM by leodemoura
Fixed in the unstable branch.


leodemoura wrote Jun 7, 2013 at 1:32 AM

The bug was fixed in the unstable branch.

The reference counter was correct. There is only one occurrence of b (as a child of Not), but there are many occurrences of Not(b). The code for handling the Not was ignoring this fact.