On Jul 15, 2008, at 11:34 AM, Chris Gorecki wrote: > Thank you all for your responses. > >> "Wrap minisat" > > The code already implements a satformat output method which can be > read directly by MiniSat, so this is the route I will most likely be > taking. This would have the added advantage of fully incorporating > MiniSat into Sage. > >>> Btw. shouldn't that be >>> sage: a == b >> not for *formulas*, since say also involve the syntax. > > Currently '==' compares parse trees. Is this the desired behavior?
No, I don't think so. E.g. (a and not a) == (a and not b) is kind of strange. - Robert --~--~---------~--~----~------------~-------~--~----~ To post to this group, send email to [email protected] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/sage-devel URLs: http://www.sagemath.org -~----------~----~----~----~------~----~------~--~---
