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?

-Chris Gorecki

--~--~---------~--~----~------------~-------~--~----~
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
-~----------~----~----~----~------~----~------~--~---

Reply via email to