[Bug 529404] Review Request: cvc3 - Validity checker of many-sorted first-order formulas with theories

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


https://bugzilla.redhat.com/show_bug.cgi?id=529404





--- Comment #5 from David A. Wheeler <dwheeler at dwheeler.com>  2009-10-19 18:10:45 EDT ---
The changes all sound great.  I'll start reviewing soon.  Regarding your
questions/comments...

* "I am not going to touch the useless rule warnings generated by bison, as I'm
not certain I can do so without damaging the grammar files.  We should report
this upstream and see if they can fix it, though."

Fair enough.  It may just be a misleading error message.  I think reporting it
upstream is the right solution.

* "I initially added the %check section that you suggested.  However, when I
enabled Java support, %check stopped working because it couldn't find the JAR
files.  There's probably an easy fix for that, but I haven't had time to pursue
it yet."

Okay.  Don't worry about it; %check is optional.  I *like* having %check
sections, and I encourage them, but I have no leg to stand on for *requiring*
them.  If you want to try further, you might be able to use "make regressonly4"
instead of "make regress4" in the %check section.

* "The minisat code does appear to be related somehow to that in the minisat2
package, but it differs signficantly.  The minisat2 package supplies only a
binary, not a library, so I couldn't link with it in any case.  Even if it did
supply a library, I am uncertain of the significance of the differences between
the two code bases.  How do you suggest I proceed on this point?"

As you noted earlier, the minisat code in cvc3 has a copyright date of 2006,
but the minisat2 has a date of 2005, and there are many differences in what's
there.  In addition, the CVC3 minisat does not include lots of code that is in
minisat2.

I think that is clear evidence that what we have here is an internal fork and
serious modification of minisat, for purpose of implementing CVC3.  I think we
should encourage the CVC3 author and minisat2 authors to converge in the
future, if it makes sense for them to do so.  But for the moment, I think we
should package as it is... there's absolutely no evidence that this fork will
ever heal, or even that it SHOULD.  Fedora already packages other forks that
are more egregious (xemacs vs. emacs)... in this case, it's not even clear that
there SHOULD be a merger.

I'll go review the updated spec; thanks for doing this!!

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.