You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Reporting progress: while investigating #33, I changed the implementation of choose_conj with its naive implementation ; thus impacting make_conj and conjunction.
This makes for identical results (and better speed) in all benchmark cases, except for (x <-> (p ∨ ¬p)) ∧ (y <-> (q ∨ ¬q)) ∧ ¬(p ∧ q) which times out.
The issue is in conjunction ; seemingly highly inefficient in that case.
Counterintuitively, it seems to make more calls to Provable_dec.
We'll see if the solution above fixes this issue too.
Try to replace
make_conj
withAnd
(and similarly for disjunction and implication) to see if it makes the benchmarks worseThe text was updated successfully, but these errors were encountered: