Adding a 'deep' parameter to pl_true seems a better idea. We wouldn't want to break backwards compatibility for users who may have written code assuming the former input/output combos of pl_true. But yes, the modification you suggest to pl_true does seem a good idea to me. About the idea of using a Semantic Tableau, we should probably stick to using a traditional SAT solver for the logic module (Since users looking to use a SAT solver usually need it to return a model, or atleast expect it to). However, what we _can_ do is use the tableau method for the Assumptions system (maybe) - or anywhere else in the core, where a model is not essential. @asmeurer, do you think we should implement that? @Soumya, you could probably run a few tests and check out the timing results. But before that, you may want to get your current pipeline-PRs merged. I guess there are 2-3 of them?
-- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sympy. For more options, visit https://groups.google.com/groups/opt_out.
