[Bug 555161] Review Request: csisat - Tool for LA+EUF Interpolation

[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=555161

--- Comment #1 from David A. Wheeler <dwheeler at dwheeler.com> 2010-01-17 21:43:30 EST ---
I've started looking over the .spec file, here are some initial comments...

# FIXME: %%{?_smp_mflags} doesn't work
 Should the "FIXME" really be there?  I'd just state that "smp_mflags"
 doesn't work, and move on; smp_mflags doesn't work for LOTS of package builds.

# Make sure we don't use the bundled version of picosat
rm -fr picosat-632
 I suggest changing "picosat-632" to "picosat-*"; that way,
 updates to the package are less likely to unintentionally re-include this.

# Get rid of inappropriate executable bits
chmod a-x L* R* T*
 This is mysterious to readers, and could easily go wrong on future versions.
 I strongly recommend changing this to:
chmod a-x *.txt
 which fixes the same files, but for a far more obvious reason :-).

The one-line summary "Tool for LA+EUF Interpolation" is incomprehensible
for the uninitiated; can we make that clearer?
I'll have to admit that I can't think of an easy way to make the short
one clearer.

The multi-line description needs to be clearer and note the acronyms. I.E.,
"of rational linear arithmetic (LA) and equality with uninterpreted function
(EUF) symbols...." (since the acronyms are used in the summary).
And frankly, a less-forbidding description would be good.
What's an "interpolator"?  What does this do, WITHOUT using specialized terms?
E.G.,
 This reads a set of mathematical formulas that may combine variables,
addition, multiplication, comparisons (<,>, etc.), as well as boolean
expressions (and, or, not).  It determines if it is possible to set the
variables to values so that the set of formulas are all simultaneously
true (if it can, then the set of formulas is "satisfiable").

Unfortunately, since "picosat-devel" isn't in the Fedora repository, I can't
easily use a koji build to test this :-(.

The ReadMe.txt file says that "The PicoSAT integration is experimental"; I
presume that the default csi_dpll is proprietary, correct?  If that's right,
then I guess this is what we need to do.

I used rpmlint, and got no warnings or errors (good!):
  rpmlint csisat.spec ../RPMS/i586/csisat-* ../SRPMS/csisat-1.2-1.fc11.src.rpm 
 3 packages and 1 specfiles checked; 0 errors, 0 warnings.

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