rpms/cvc3/devel cvc3-build.patch, NONE, 1.1 cvc3-doc.patch, NONE, 1.1 cvc3-gcc4.patch, NONE, 1.1 cvc3-java.patch, NONE, 1.1 cvc3.spec, NONE, 1.1 import.log, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
Jerry James
jjames at fedoraproject.org
Thu Oct 22 16:25:39 UTC 2009
- Previous message (by thread): [pkgdb] qtcurve-gtk2 had acl change status
- Next message (by thread): rpms/cvc3/F-11 cvc3-build.patch, NONE, 1.1 cvc3-doc.patch, NONE, 1.1 cvc3-gcc4.patch, NONE, 1.1 cvc3-java.patch, NONE, 1.1 cvc3.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
Author: jjames
Update of /cvs/pkgs/rpms/cvc3/devel
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv25899/devel
Modified Files:
.cvsignore sources
Added Files:
cvc3-build.patch cvc3-doc.patch cvc3-gcc4.patch
cvc3-java.patch cvc3.spec import.log
Log Message:
Initial import.
cvc3-build.patch:
Makefile.std | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
--- NEW FILE cvc3-build.patch ---
diff -dur cvc3-2.1.ORIG/Makefile.std cvc3-2.1/Makefile.std
--- cvc3-2.1.ORIG/Makefile.std 2009-09-30 12:54:34.000000000 -0600
+++ cvc3-2.1/Makefile.std 2009-10-15 21:12:35.804289073 -0600
@@ -92,7 +92,7 @@
DEBUG_PLATFORM = -optdbg
else
ifeq ($(OPTIMIZED),1)
- LOCAL_CXXFLAGS = -O2
+ LOCAL_CXXFLAGS =
DEBUG_PLATFORM =
else
LOCAL_CXXFLAGS = -D_CVC3_DEBUG_MODE -g -O0
@@ -177,7 +177,7 @@
BUILD_SHARED_LIB=1
endif
-LOCAL_CXXFLAGS += -Wall $(INCLUDE_DIR)
+LOCAL_CXXFLAGS += $(INCLUDE_DIR)
ifdef EXTRAFLAGS
LOCAL_CXXFLAGS += $(EXTRAFLAGS)
cvc3-doc.patch:
INSTALL | 2
doc/Doxyfile.in | 30 ++++++++++---
src/include/expr.h | 2
src/include/theory_arith3.h | 2
src/include/theory_arith_new.h | 17 ++++---
src/include/theory_arith_old.h | 11 ++---
src/include/vc.h | 12 ++---
src/sat/sat_proof.h | 2
src/theory_arith/theory_arith3.cpp | 2
src/theory_arith/theory_arith_new.cpp | 2
src/theory_arith/theory_arith_old.cpp | 2
src/theory_bitvector/bitvector_theorem_producer.cpp | 44 ++++++++++----------
src/theory_core/theory_core.cpp | 2
src/theory_datatype/theory_datatype.cpp | 16 +++----
src/theory_quant/quant_theorem_producer.cpp | 1
src/theory_quant/theory_quant.cpp | 6 +-
src/vcl/vcl.cpp | 35 ++++++++-------
17 files changed, 103 insertions(+), 85 deletions(-)
--- NEW FILE cvc3-doc.patch ---
diff -dur cvc3-2.1.ORIG/doc/Doxyfile.in cvc3-2.1/doc/Doxyfile.in
--- cvc3-2.1.ORIG/doc/Doxyfile.in 2007-09-12 18:06:50.000000000 -0600
+++ cvc3-2.1/doc/Doxyfile.in 2009-10-19 10:13:12.768107753 -0600
@@ -31,7 +31,7 @@
# This could be handy for archiving the generated documentation or
# if some version control system is used.
-PROJECT_NUMBER =
+PROJECT_NUMBER = 2.1
# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute)
# base path where the generated documentation will be put.
@@ -499,8 +499,7 @@
# excluded from the INPUT source files. This way you can easily exclude a
# subdirectory from a directory tree whose root is specified with the INPUT tag.
-EXCLUDE = devel.dox \
- theory_api.dox
+EXCLUDE = devel.dox
# The EXCLUDE_SYMLINKS tag can be used select whether or not files or
# directories that are symbolic links (a Unix filesystem feature) are excluded
@@ -1042,8 +1041,7 @@
# undefined via #undef or recursively expanded use the := operator
# instead of the = operator.
-PREDEFINED = DEBUG \
- DOXYGEN
+PREDEFINED = DOXYGEN
# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then
# this tag can be used to specify a list of macro names that should be expanded.
@@ -1137,6 +1135,24 @@
HAVE_DOT = @HAVE_DOT@
+# By default doxygen will write a font called FreeSans.ttf to the output
+# directory and reference it in all dot files that doxygen generates. This
+# font does not include all possible unicode characters however, so when you need
+# these (or just want a differently looking font) you can specify the font name
+# using DOT_FONTNAME. You need need to make sure dot is able to find the font,
+# which can be done by putting it in a standard location or by setting the
+# DOTFONTPATH environment variable or by setting DOT_FONTPATH to the directory
+# containing the font.
+
+DOT_FONTNAME = FreeSans
+
+# By default doxygen will tell dot to use the output directory to look for the
+# FreeSans.ttf font (which doxygen will put there itself). If you specify a
+# different font using DOT_FONTNAME you can set the path where dot
+# can find it using this tag.
+
+DOT_FONTPATH = /usr/share/fonts/gnu-free
+
# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen
# will generate a graph for each documented class showing the direct and
# indirect inheritance relations. Setting this tag to YES will force the
@@ -1213,7 +1229,7 @@
# generated by dot. Possible values are png, jpg, or gif
# If left blank png will be used.
-DOT_IMAGE_FORMAT = gif
+DOT_IMAGE_FORMAT = png
# The tag DOT_PATH can be used to specify the path where the dot tool can be
# found. If left blank, it is assumed the dot tool can be found in the path.
@@ -1247,7 +1263,7 @@
# makes dot run faster, but since only newer versions of dot (>1.8.10)
# support this, this feature is disabled by default.
-DOT_MULTI_TARGETS = NO
+DOT_MULTI_TARGETS = YES
# If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will
# generate a legend page explaining the meaning of the various boxes and
diff -dur cvc3-2.1.ORIG/INSTALL cvc3-2.1/INSTALL
--- cvc3-2.1.ORIG/INSTALL 2009-10-15 16:06:18.000000000 -0600
+++ cvc3-2.1/INSTALL 2009-10-19 10:13:59.048162819 -0600
@@ -196,7 +196,7 @@
</pre>
<b>Note:</b> The Java interface depends on the "build type" (e.g.,
-"optimized", "debug) of %CVC3. If you choose to re-configure and
+"optimized", "debug") of %CVC3. If you choose to re-configure and
re-build %CVC3 with a different build type, you must run "make clean"
in the current directory and re-build the interface (cleaning and
rebuilding the entire %CVC3 package will suffice).
diff -dur cvc3-2.1.ORIG/src/include/expr.h cvc3-2.1/src/include/expr.h
--- cvc3-2.1.ORIG/src/include/expr.h 2009-10-04 12:41:29.000000000 -0600
+++ cvc3-2.1/src/include/expr.h 2009-10-19 10:13:37.775165727 -0600
@@ -388,7 +388,7 @@
//! Test if e is an atomic formula
/*! An atomic formula is TRUE or FALSE or an application of a predicate
(possibly 0-ary) which does not properly contain any formula. For
- instance, the formula "x = IF f THEN y ELSE z ENDIF is not an atomic
+ instance, the formula "x = IF f THEN y ELSE z ENDIF" is not an atomic
formula, since it contains the condition "f", which is a formula. */
bool isAtomicFormula() const;
//! An abstract atomic formua is an atomic formula or a quantified formula
diff -dur cvc3-2.1.ORIG/src/include/theory_arith3.h cvc3-2.1/src/include/theory_arith3.h
--- cvc3-2.1.ORIG/src/include/theory_arith3.h 2009-05-29 23:48:15.000000000 -0600
+++ cvc3-2.1/src/include/theory_arith3.h 2009-10-19 10:13:12.769107906 -0600
@@ -337,7 +337,7 @@
* Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
* changes in the future, it will not be used in the ordering.
*
- * @param var the variable
+ * @param variable the variable
* @param max the value to set it to
*/
void fixCurrentMaxCoefficient(Expr variable, Rational max);
diff -dur cvc3-2.1.ORIG/src/include/theory_arith_new.h cvc3-2.1/src/include/theory_arith_new.h
--- cvc3-2.1.ORIG/src/include/theory_arith_new.h 2009-06-29 20:14:48.000000000 -0600
+++ cvc3-2.1/src/include/theory_arith_new.h 2009-10-19 10:13:12.769107906 -0600
@@ -434,7 +434,7 @@
inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
/**
- * Les then or equal comparison operator.
+ * Less than or equal comparison operator.
*/
inline bool operator <= (const EpsRational& r) const {
switch (r.type) {
@@ -459,12 +459,12 @@
}
/**
- * Les then comparison operator.
+ * Less than comparison operator.
*/
inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
/**
- * Bigger then equal comparison operator.
+ * Greater than comparison operator.
*/
inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
@@ -787,6 +787,7 @@
* Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).
*
* @param x_i the variable to assert the bound on
+ * @param c the bound to assert
*/
QueryResult assertUpper(const Expr& x_i, const EpsRational& c, const Theorem& thm);
@@ -794,13 +795,15 @@
* Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).
*
* @param x_i the variable to assert the bound on
+ * @param c the bound to assert
*/
QueryResult assertLower(const Expr& x_i, const EpsRational& c, const Theorem& thm);
/**
- * Asserts a new equality constraint on a variable by asserting both upper and lower bound.
+ * Asserts a new equality constraint on a variable by asserting both upper and lower bounds.
*
* @param x_i the variable to assert the bound on
+ * @param c the the bound to assert
*/
QueryResult assertEqual(const Expr& x_i, const EpsRational& c, const Theorem& thm);
@@ -862,8 +865,8 @@
/**
* Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
- * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separatied to
- * <ul>
+ * explanation clause. The variables in the row of \f$x_i = \sum_x{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to
+ * <ul>
* <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
* <li>\f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
* </ul>
@@ -878,7 +881,7 @@
/**
* Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
- * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separatied to
+ * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to
* <ul>
* <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
* <li>\f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
diff -dur cvc3-2.1.ORIG/src/include/theory_arith_old.h cvc3-2.1/src/include/theory_arith_old.h
--- cvc3-2.1.ORIG/src/include/theory_arith_old.h 2009-09-29 19:50:21.000000000 -0600
+++ cvc3-2.1/src/include/theory_arith_old.h 2009-10-19 10:13:12.771175241 -0600
@@ -364,7 +364,7 @@
* Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
* changes in the future, it will not be used in the ordering.
*
- * @param var the variable
+ * @param variable the variable
* @param max the value to set it to
*/
void fixCurrentMaxCoefficient(Expr variable, Rational max);
@@ -653,7 +653,7 @@
inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
/**
- * Les then or equal comparison operator.
+ * Less than or equal comparison operator.
*/
inline bool operator <= (const EpsRational& r) const {
switch (r.type) {
@@ -678,19 +678,19 @@
}
/**
- * Les then comparison operator.
+ * Less than comparison operator.
*/
inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
/**
- * Bigger then equal comparison operator.
+ * Greater than comparison operator.
*/
inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
/**
* Returns the string representation of the number.
*
- * @param the string representation of the number
+ * @return the string representation of the number
*/
std::string toString() const {
switch (type) {
@@ -846,7 +846,6 @@
* @param x variable x::Difference
* @param y variable y
* @param c rational c
- * @param kind the kind of inequality (LE or LT)
* @param edge_thm the theorem for this edge
*/
void addEdge(const Expr& x, const Expr& y, const Rational& c, const Theorem& edge_thm);
diff -dur cvc3-2.1.ORIG/src/include/vc.h cvc3-2.1/src/include/vc.h
--- cvc3-2.1.ORIG/src/include/vc.h 2009-10-04 12:41:29.000000000 -0600
+++ cvc3-2.1/src/include/vc.h 2009-10-19 10:13:12.772197964 -0600
@@ -28,9 +28,7 @@
#include "formula_value.h"
/*****************************************************************************/
-/*!
- *\defgroup Note Note that this list of modules is very incomplete
- *\brief Note that this list of modules is very incomplete
+/*! Note that this list of modules is very incomplete
*/
/*****************************************************************************/
@@ -750,10 +748,10 @@
//! Set triggers for quantifier instantiation
/*!
- * \param e is the expression for which triggers are being set. \param
- * Each item in triggers is a vector of Expr containing one or more
- * patterns. A pattern is a term or Atomic predicate sub-expression of
- * e. A vector containing more than one pattern is treated as a
+ * \param e the expression for which triggers are being set
+ * \param triggers Each item in triggers is a vector of Expr containing one
+ * or more patterns. A pattern is a term or Atomic predicate sub-expression
+ * of e. A vector containing more than one pattern is treated as a
* multi-trigger. Patterns will be matched in the order they occur in
* the vector.
*/
diff -dur cvc3-2.1.ORIG/src/sat/sat_proof.h cvc3-2.1/src/sat/sat_proof.h
--- cvc3-2.1.ORIG/src/sat/sat_proof.h 2008-04-03 22:18:32.000000000 -0600
+++ cvc3-2.1/src/sat/sat_proof.h 2009-10-19 10:13:12.773204281 -0600
@@ -1,6 +1,6 @@
/*****************************************************************************/
/*!
- *\file minisat_proof.h
+ *\file sat_proof.h
*\brief Sat solver proof representation
*
* Author: Alexander Fuchs
diff -dur cvc3-2.1.ORIG/src/theory_arith/theory_arith3.cpp cvc3-2.1/src/theory_arith/theory_arith3.cpp
--- cvc3-2.1.ORIG/src/theory_arith/theory_arith3.cpp 2009-10-08 16:15:52.000000000 -0600
+++ cvc3-2.1/src/theory_arith/theory_arith3.cpp 2009-10-19 10:13:12.775109510 -0600
@@ -421,7 +421,7 @@
return thm;
}
-/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
+/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
* -# translate e to the form e' = 0
* -# if (e'.isRational()) then {if e' != 0 return false else true}
* -# a for loop checks if all the variables are integers.
diff -dur cvc3-2.1.ORIG/src/theory_arith/theory_arith_new.cpp cvc3-2.1/src/theory_arith/theory_arith_new.cpp
--- cvc3-2.1.ORIG/src/theory_arith/theory_arith_new.cpp 2009-10-08 16:15:52.000000000 -0600
+++ cvc3-2.1/src/theory_arith/theory_arith_new.cpp 2009-10-19 10:13:12.777233052 -0600
@@ -320,7 +320,7 @@
return thm;
}
-/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
+/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
* -# translate e to the form e' = 0
* -# if (e'.isRational()) then {if e' != 0 return false else true}
* -# a for loop checks if all the variables are integers.
diff -dur cvc3-2.1.ORIG/src/theory_arith/theory_arith_old.cpp cvc3-2.1/src/theory_arith/theory_arith_old.cpp
--- cvc3-2.1.ORIG/src/theory_arith/theory_arith_old.cpp 2009-10-08 16:15:52.000000000 -0600
+++ cvc3-2.1/src/theory_arith/theory_arith_old.cpp 2009-10-19 10:13:12.781233049 -0600
@@ -436,7 +436,7 @@
return thm;
}
-/*! Psuedo-code for doSolve. (Input is an equation) (output is a Theorem)
+/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
* -# translate e to the form e' = 0
* -# if (e'.isRational()) then {if e' != 0 return false else true}
* -# a for loop checks if all the variables are integers.
diff -dur cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp
--- cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-15 19:23:59.000000000 -0600
+++ cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-19 10:13:12.785232967 -0600
@@ -479,7 +479,7 @@
//if both MSBs are constants, then we can optimize the output. we
//know precisely the value of the signed comparison in cases where
- //topbit of e0 and e1 are constants. e.g. |-1 at t0 < 0 at t1 is clearly
+ //topbit of e0 and e1 are constants. e.g. |-1\@t0 < 0\@t1 is clearly
//|-TRUE.
//-1 indicates that both topBits are not known to be BVCONSTS
@@ -1009,9 +1009,9 @@
}
-// Input: x: a_0 @ ... @ a_n,
+// Input: x: a_0 \@ ... \@ a_n,
// i: bitposition
-// Output |- BOOLEXTRACT(a_0 @ ... @ a_n, i) <=> BOOLEXTRACT(a_j, k)
+// Output |- BOOLEXTRACT(a_0 \@ ... \@ a_n, i) <=> BOOLEXTRACT(a_j, k)
// where j and k are determined by structure of CONCAT
Theorem BitvectorTheoremProducer::bitExtractConcatenation(const Expr & x,
int i)
@@ -1939,7 +1939,7 @@
}
-//! t<<n = c @ 0bin00...00, takes e == (t<<n)
+//! t<<n = c \@ 0bin00...00, takes e == (t<<n)
Theorem BitvectorTheoremProducer::leftShiftToConcat(const Expr& e) {
if(CHECK_PROOFS) {
// The kids must be constant expressions
@@ -1963,7 +1963,7 @@
return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
}
-//! t<<n = c @ 0bin00...00, takes e == (t<<n)
+//! t<<n = c \@ 0bin00...00, takes e == (t<<n)
Theorem BitvectorTheoremProducer::constWidthLeftShiftToConcat(const Expr& e) {
if(CHECK_PROOFS) {
// The kids must be constant expressions
@@ -1996,7 +1996,7 @@
}
-//! t>>m = 0bin00...00 @ t[bvLength-1:m], takes e == (t>>n)
+//! t>>m = 0bin00...00 \@ t[bvLength-1:m], takes e == (t>>n)
Theorem BitvectorTheoremProducer::rightShiftToConcat(const Expr& e) {
if(CHECK_PROOFS) {
CHECK_SOUND(e.getOpKind() == RIGHTSHIFT && e.arity() == 1,
@@ -2028,7 +2028,7 @@
}
-//! BVSHL(t,c) = t[n-c,0] @ 0bin00...00
+//! BVSHL(t,c) = t[n-c,0] \@ 0bin00...00
Theorem BitvectorTheoremProducer::bvshlToConcat(const Expr& e) {
if(CHECK_PROOFS) {
// The second kid must be a constant expression
@@ -2102,7 +2102,7 @@
}
-//! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]
+//! BVLSHR(t,c) = 0bin00...00 \@ t[n-1,c]
Theorem BitvectorTheoremProducer::bvlshrToConcat(const Expr& e)
{
if(CHECK_PROOFS) {
@@ -2265,7 +2265,7 @@
//! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
-/*! If k = 2^m, return k*t = t at 0...0 */
+/*! If k = 2^m, return k*t = t\@0...0 */
Theorem BitvectorTheoremProducer::constMultToPlus(const Expr& e) {
DebugAssert(false,
"BitvectorTheoremProducer::constMultToPlus: this rule does not work\n");
@@ -2459,7 +2459,7 @@
}
-//! (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat)
+//! (t1 \@ t2)[i:j] = t1[...] \@ t2[...] (push extraction through concat)
Theorem
BitvectorTheoremProducer::extractConcat(const Expr& e) {
TRACE("bitvector rules", "extractConcat(", e, ") {");
@@ -2672,7 +2672,7 @@
}
-//! ~(t1 at ...@tn) = (~t1)@...@(~tn) -- push negation through concat
+//! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat
Theorem
BitvectorTheoremProducer::negConcat(const Expr& e) {
if(CHECK_PROOFS) {
@@ -3190,7 +3190,7 @@
}
-//! c1 at c2@... at cn = c (concatenation of constant bitvectors)
+//! c1\@c2\@...\@cn = c (concatenation of constant bitvectors)
Theorem BitvectorTheoremProducer::concatConst(const Expr& e) {
if(CHECK_PROOFS) {
// The kids must be constant expressions
@@ -3211,7 +3211,7 @@
}
-//! Flatten one level of nested concatenation, e.g.: x@(y at z)@w = x at y@z at w
+//! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w
Theorem
BitvectorTheoremProducer::concatFlatten(const Expr& e) {
if(CHECK_PROOFS) {
@@ -3233,7 +3233,7 @@
}
-//! Merge n-ary concat. of adjacent extractions: x[15:8]@x[7:0] = x[15:0]
+//! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]
Theorem
BitvectorTheoremProducer::concatMergeExtract(const Expr& e) {
if(CHECK_PROOFS) {
@@ -4681,7 +4681,7 @@
}
-// BVMULT(N, a at b, y) = BVPLUS(N, BVMULT(N,b,y), BVMULT(N-n,a,y) @ n-bit-0-string)
+// BVMULT(N, a\@b, y) = BVPLUS(N, BVMULT(N,b,y), BVMULT(N-n,a,y) \@ n-bit-0-string)
// where n = BVSize(b), a != 0, one of a or b is a constant
Theorem BitvectorTheoremProducer::liftConcatBVMult(const Expr& e)
{
@@ -4917,7 +4917,7 @@
}
-// BVPLUS(N, a0, ..., an) = BVPLUS(N-n,a0[N-1:n],...an[N-1:n])@t
+// BVPLUS(N, a0, ..., an) = BVPLUS(N-n,a0[N-1:n],...an[N-1:n])\@t
// where n = BVSize(t), and the sum of the lowest n bits of a0..an is exactly
// equal to t (i.e. no carry)
Theorem BitvectorTheoremProducer::liftConcatBVPlus(const Expr& e)
@@ -5602,9 +5602,9 @@
// Input: t[hi:lo] = rhs
// if t appears as leaf in rhs, then:
-// t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false
+// t[hi:lo] = rhs |- Exists x,y,z. (t = x \@ y i@ z AND y = rhs), solvedForm = false
// else
-// t[hi:lo] = rhs |- Exists x,z. (t = x @ rhs @ z), solvedForm = true
+// t[hi:lo] = rhs |- Exists x,z. (t = x \@ rhs \@ z), solvedForm = true
Theorem BitvectorTheoremProducer::processExtract(const Theorem& e, bool& solvedForm)
{
Expr expr = e.getExpr();
@@ -6075,7 +6075,7 @@
}
-//! BVZEROEXTEND(e, i) = zeroString @ e
+//! BVZEROEXTEND(e, i) = zeroString \@ e
// where zeroString is a string of i zeroes
Theorem BitvectorTheoremProducer::zeroExtendRule(const Expr& e) {
if(CHECK_PROOFS) {
@@ -6103,7 +6103,7 @@
}
-//! BVREPEAT(e, i) = e @ e @ ... @ e
+//! BVREPEAT(e, i) = e \@ e \@ ... \@ e
// where e appears i times on the right
Theorem BitvectorTheoremProducer::repeatRule(const Expr& e) {
if(CHECK_PROOFS) {
@@ -6136,7 +6136,7 @@
}
-//! BVROTL(e, i) = a[n-i-1:0] @ a[n-1:n-i]
+//! BVROTL(e, i) = a[n-i-1:0] \@ a[n-1:n-i]
// where n is the size of e and i is less than n (otherwise i mod n is used)
Theorem BitvectorTheoremProducer::rotlRule(const Expr& e) {
if(CHECK_PROOFS) {
@@ -6167,7 +6167,7 @@
}
-//! BVROTR(e, i) = a[i-1:0] @ a[n-1:i]
+//! BVROTR(e, i) = a[i-1:0] \@ a[n-1:i]
// where n is the size of e and i is less than n (otherwise i mod n is used)
Theorem BitvectorTheoremProducer::rotrRule(const Expr& e) {
if(CHECK_PROOFS) {
diff -dur cvc3-2.1.ORIG/src/theory_core/theory_core.cpp cvc3-2.1/src/theory_core/theory_core.cpp
--- cvc3-2.1.ORIG/src/theory_core/theory_core.cpp 2009-09-30 13:39:06.000000000 -0600
+++ cvc3-2.1/src/theory_core/theory_core.cpp 2009-10-19 10:13:12.788233008 -0600
@@ -3099,7 +3099,7 @@
}
-bool TheoryCore::incomplete(vector<string>& reasons)
+bool TheoryCore::incomplete(std::vector<std::string>& reasons)
{
if(d_incomplete.size() > 0) {
for(CDMap<string,bool>::iterator i=d_incomplete.begin(),
diff -dur cvc3-2.1.ORIG/src/theory_datatype/theory_datatype.cpp cvc3-2.1/src/theory_datatype/theory_datatype.cpp
--- cvc3-2.1.ORIG/src/theory_datatype/theory_datatype.cpp 2009-10-05 20:12:41.000000000 -0600
+++ cvc3-2.1/src/theory_datatype/theory_datatype.cpp 2009-10-19 10:13:12.790252403 -0600
@@ -857,10 +857,10 @@
}
-Expr TheoryDatatype::dataType(const string& name,
- const vector<string>& constructors,
- const vector<vector<string> >& selectors,
- const vector<vector<Expr> >& types)
+Expr TheoryDatatype::dataType(const std::string& name,
+ const std::vector<std::string>& constructors,
+ const std::vector<std::vector<std::string> >& selectors,
+ const std::vector<std::vector<Expr> >& types)
{
vector<string> names;
vector<vector<string> > constructors2;
@@ -876,10 +876,10 @@
// Elements of types are either the expr from an existing type or a string
// naming one of the datatypes being defined
-Expr TheoryDatatype::dataType(const vector<string>& names,
- const vector<vector<string> >& allConstructors,
- const vector<vector<vector<string> > >& allSelectors,
- const vector<vector<vector<Expr> > >& allTypes)
+Expr TheoryDatatype::dataType(const std::vector<std::string>& names,
+ const std::vector<std::vector<std::string> >& allConstructors,
+ const std::vector<std::vector<std::vector<std::string> > >& allSelectors,
+ const std::vector<std::vector<std::vector<Expr> > >& allTypes)
{
vector<Expr> returnTypes;
diff -dur cvc3-2.1.ORIG/src/theory_quant/quant_theorem_producer.cpp cvc3-2.1/src/theory_quant/quant_theorem_producer.cpp
--- cvc3-2.1.ORIG/src/theory_quant/quant_theorem_producer.cpp 2009-10-04 12:41:29.000000000 -0600
+++ cvc3-2.1/src/theory_quant/quant_theorem_producer.cpp 2009-10-19 10:13:12.791296402 -0600
@@ -241,6 +241,7 @@
* subtype predicates for the bound variables of the quanitfied expression.
* \param t1 is the quantifier (a Theorem)
* \param terms are the terms to instantiate.
+ * \param quantLevel the quantification level for the formula
*/
Theorem QuantTheoremProducer::universalInst(const Theorem& t1, const vector<Expr>& terms, int quantLevel){
diff -dur cvc3-2.1.ORIG/src/theory_quant/theory_quant.cpp cvc3-2.1/src/theory_quant/theory_quant.cpp
--- cvc3-2.1.ORIG/src/theory_quant/theory_quant.cpp 2009-10-07 00:24:44.000000000 -0600
+++ cvc3-2.1/src/theory_quant/theory_quant.cpp 2009-10-19 10:13:12.795232784 -0600
@@ -2860,7 +2860,7 @@
}
-void TheoryQuant::setupTriggers(ExprMap<ExprMap<vector<dynTrig>* >*>& trig_maps, const Theorem& thm, size_t univs_id){
+void TheoryQuant::setupTriggers(ExprMap<ExprMap<std::vector<dynTrig>* >*>& trig_maps, const Theorem& thm, size_t univs_id){
// static std::vector<Expr> libQuant;
const Expr& e = thm.getExpr();
@@ -4137,7 +4137,7 @@
}
//match a gterm against all the trigs in d_allmap_trigs
-void TheoryQuant::matchListNew(ExprMap<ExprMap<vector<dynTrig>*>*>& new_trigs,
+void TheoryQuant::matchListNew(ExprMap<ExprMap<std::vector<dynTrig>*>*>& new_trigs,
const CDList<Expr>& glist,
size_t gbegin,
size_t gend){
@@ -7984,7 +7984,7 @@
d_lastEqsUpdatePos.set(d_eqsUpdate.size());
}
-void TheoryQuant::synCheckSat(ExprMap<ExprMap<vector<dynTrig>* >* >& new_trigs, bool fullEffort){
+void TheoryQuant::synCheckSat(ExprMap<ExprMap<std::vector<dynTrig>* >* >& new_trigs, bool fullEffort){
d_allout=false;
diff -dur cvc3-2.1.ORIG/src/vcl/vcl.cpp cvc3-2.1/src/vcl/vcl.cpp
--- cvc3-2.1.ORIG/src/vcl/vcl.cpp 2009-10-15 14:29:30.000000000 -0600
+++ cvc3-2.1/src/vcl/vcl.cpp 2009-10-19 10:13:12.798131491 -0600
@@ -775,8 +775,8 @@
}
-Type VCL::recordType(const vector<string>& fields,
- const vector<Type>& types)
+Type VCL::recordType(const std::vector<std::string>& fields,
+ const std::vector<Type>& types)
{
DebugAssert(fields.size() == types.size(),
"VCL::recordType: number of fields is different \n"
@@ -789,9 +789,10 @@
}
-Type VCL::dataType(const string& name,
- const string& constructor,
- const vector<string>& selectors, const vector<Expr>& types)
+Type VCL::dataType(const std::string& name,
+ const std::string& constructor,
+ const std::vector<std::string>& selectors,
+ const std::vector<Expr>& types)
{
vector<string> constructors;
constructors.push_back(constructor);
@@ -806,10 +807,10 @@
}
-Type VCL::dataType(const string& name,
- const vector<string>& constructors,
- const vector<vector<string> >& selectors,
- const vector<vector<Expr> >& types)
+Type VCL::dataType(const std::string& name,
+ const std::vector<std::string>& constructors,
+ const std::vector<std::vector<std::string> >& selectors,
+ const std::vector<std::vector<Expr> >& types)
{
Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
if(d_dump) {
@@ -819,11 +820,11 @@
}
-void VCL::dataType(const vector<string>& names,
- const vector<vector<string> >& constructors,
- const vector<vector<vector<string> > >& selectors,
- const vector<vector<vector<Expr> > >& types,
- vector<Type>& returnTypes)
+void VCL::dataType(const std::vector<std::string>& names,
+ const std::vector<std::vector<std::string> >& constructors,
+ const std::vector<std::vector<std::vector<std::string> > >& selectors,
+ const std::vector<std::vector<std::vector<Expr> > >& types,
+ std::vector<Type>& returnTypes)
{
Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
if(d_dump) {
@@ -1405,8 +1406,8 @@
}
-Expr VCL::recordExpr(const vector<string>& fields,
- const vector<Expr>& exprs)
+Expr VCL::recordExpr(const std::vector<std::string>& fields,
+ const std::vector<Expr>& exprs)
{
DebugAssert(fields.size() > 0, "VCL::recordExpr()");
DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
@@ -2107,7 +2108,7 @@
}
-bool VCL::incomplete(vector<string>& reasons) {
+bool VCL::incomplete(std::vector<std::string>& reasons) {
// TODO: add to interactive interface
// Return true only after a failed query
return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
cvc3-gcc4.patch:
include/command_line_exception.h | 2 +-
include/memory_manager_context.h | 1 +
include/sound_exception.h | 2 +-
theory_arith/arith_exception.h | 2 +-
theory_bitvector/bitvector_theorem_producer.cpp | 1 +
util/debug.cpp | 1 +
util/rational-gmp.cpp | 1 +
7 files changed, 7 insertions(+), 3 deletions(-)
--- NEW FILE cvc3-gcc4.patch ---
diff -dur cvc3-2.1.ORIG/src/include/command_line_exception.h cvc3-2.1/src/include/command_line_exception.h
--- cvc3-2.1.ORIG/src/include/command_line_exception.h 2006-08-09 15:19:30.000000000 -0600
+++ cvc3-2.1/src/include/command_line_exception.h 2009-10-16 09:34:46.141974605 -0600
@@ -31,7 +31,7 @@
// Constructors
CLException() { }
CLException(const std::string& msg): Exception(msg) { }
- CLException(char* msg): Exception(msg) { }
+ CLException(const char* msg): Exception(msg) { }
// Destructor
virtual ~CLException() { }
// Printing the message
diff -dur cvc3-2.1.ORIG/src/include/memory_manager_context.h cvc3-2.1/src/include/memory_manager_context.h
--- cvc3-2.1.ORIG/src/include/memory_manager_context.h 2009-04-10 14:38:25.000000000 -0600
+++ cvc3-2.1/src/include/memory_manager_context.h 2009-10-16 09:34:46.141974605 -0600
@@ -21,6 +21,7 @@
#ifndef _cvc3__include__memory_manager_context_h
#define _cvc3__include__memory_manager_context_h
+#include <cstdlib>
#include <vector>
#include "memory_manager.h"
diff -dur cvc3-2.1.ORIG/src/include/sound_exception.h cvc3-2.1/src/include/sound_exception.h
--- cvc3-2.1.ORIG/src/include/sound_exception.h 2006-08-09 15:19:30.000000000 -0600
+++ cvc3-2.1/src/include/sound_exception.h 2009-10-16 09:34:46.142839030 -0600
@@ -33,7 +33,7 @@
// Constructors
SoundException() { }
SoundException(const std::string& msg): Exception(msg) { }
- SoundException(char* msg): Exception(msg) { }
+ SoundException(const char* msg): Exception(msg) { }
// Destructor
virtual ~SoundException() { }
virtual std::string toString() const {
diff -dur cvc3-2.1.ORIG/src/theory_arith/arith_exception.h cvc3-2.1/src/theory_arith/arith_exception.h
--- cvc3-2.1.ORIG/src/theory_arith/arith_exception.h 2006-08-09 15:19:31.000000000 -0600
+++ cvc3-2.1/src/theory_arith/arith_exception.h 2009-10-16 09:35:47.378849519 -0600
@@ -35,7 +35,7 @@
// Constructors
ArithException() { }
ArithException(const std::string& msg): Exception(msg) { }
- ArithException(char* msg): Exception(msg) { }
+ ArithException(const char* msg): Exception(msg) { }
// Destructor
virtual ~ArithException() { }
virtual std::string toString() const {
diff -dur cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp
--- cvc3-2.1.ORIG/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-16 09:34:37.696911611 -0600
+++ cvc3-2.1/src/theory_bitvector/bitvector_theorem_producer.cpp 2009-10-16 09:36:54.411809170 -0600
@@ -28,6 +28,7 @@
// This code is trusted
#define _CVC3_TRUSTED_
+#include <cstdio>
#include "bitvector_theorem_producer.h"
#include "common_proof_rules.h"
#include "theory_core.h"
diff -dur cvc3-2.1.ORIG/src/util/debug.cpp cvc3-2.1/src/util/debug.cpp
--- cvc3-2.1.ORIG/src/util/debug.cpp 2009-03-03 10:31:33.000000000 -0700
+++ cvc3-2.1/src/util/debug.cpp 2009-10-16 09:34:46.144161887 -0600
@@ -19,6 +19,7 @@
*/
/*****************************************************************************/
+#include <cstdlib>
#include <fstream>
#include <stdlib.h>
diff -dur cvc3-2.1.ORIG/src/util/rational-gmp.cpp cvc3-2.1/src/util/rational-gmp.cpp
--- cvc3-2.1.ORIG/src/util/rational-gmp.cpp 2008-11-14 13:49:11.000000000 -0700
+++ cvc3-2.1/src/util/rational-gmp.cpp 2009-10-16 09:34:46.145125371 -0600
@@ -24,6 +24,7 @@
#include "compat_hash_set.h"
#include "rational.h"
+#include <climits>
#include <sstream>
#include <gmp.h>
#include <limits.h>
cvc3-java.patch:
include/cvc3/JniUtils.h | 4 ++--
src/cvc3/JniUtils.cpp | 5 ++++-
src/cvc3/ValidityChecker_impl.cpp | 4 ++--
3 files changed, 8 insertions(+), 5 deletions(-)
--- NEW FILE cvc3-java.patch ---
diff -dur cvc3-2.1.ORIG/java/include/cvc3/JniUtils.h cvc3-2.1/java/include/cvc3/JniUtils.h
--- cvc3-2.1.ORIG/java/include/cvc3/JniUtils.h 2008-12-12 15:48:14.000000000 -0700
+++ cvc3-2.1/java/include/cvc3/JniUtils.h 2009-10-19 11:22:57.817991587 -0600
@@ -168,7 +168,7 @@
env->FindClass("java/lang/Object"),
NULL);
- for (int i = 0; i < v.size(); ++i) {
+ for (unsigned int i = 0U; i < v.size(); ++i) {
env->SetObjectArrayElement(jarray, i, embed_copy<T>(env, v[i]));
}
@@ -182,7 +182,7 @@
env->FindClass("java/lang/Object"),
NULL);
- for (int i = 0; i < v.size(); ++i) {
+ for (unsigned int i = 0U; i < v.size(); ++i) {
env->SetObjectArrayElement(jarray, i, embed_const_ref<T>(env, &v[i]));
}
diff -dur cvc3-2.1.ORIG/java/src/cvc3/JniUtils.cpp cvc3-2.1/java/src/cvc3/JniUtils.cpp
--- cvc3-2.1.ORIG/java/src/cvc3/JniUtils.cpp 2008-10-01 12:35:31.000000000 -0600
+++ cvc3-2.1/java/src/cvc3/JniUtils.cpp 2009-10-19 11:22:17.203023038 -0600
@@ -74,6 +74,9 @@
case PRESENTATION_LANG: return toJava(env, "PRESENTATION");
case SMTLIB_LANG: return toJava(env, "SMTLIB");
case LISP_LANG: return toJava(env, "LISP");
+ case AST_LANG: return toJava(env, "AST");
+ case SIMPLIFY_LANG: return toJava(env, "SIMPLIFY");
+ case TPTP_LANG: return toJava(env, "TPTP");
}
DebugAssert(false, "JniUtils::toJava(InputLanguage): unreachable");
@@ -155,7 +158,7 @@
env->FindClass("java/lang/String"),
env->NewStringUTF(""));
- for(int i = 0; i < v.size(); ++i) {
+ for(unsigned int i = 0U; i < v.size(); ++i) {
env->SetObjectArrayElement(jarray, i, toJava(env, v[i]));
}
diff -dur cvc3-2.1.ORIG/java/src/cvc3/ValidityChecker_impl.cpp cvc3-2.1/java/src/cvc3/ValidityChecker_impl.cpp
--- cvc3-2.1.ORIG/java/src/cvc3/ValidityChecker_impl.cpp 2009-09-30 12:54:35.000000000 -0600
+++ cvc3-2.1/java/src/cvc3/ValidityChecker_impl.cpp 2009-10-19 11:22:17.203023038 -0600
@@ -584,11 +584,11 @@
return embed_copy(env, vc->forallExpr(vars, *body));
DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr2
-jobject m ValidityChecker vc cv Expr vars c Expr body cv Expr triggers
+jobject m ValidityChecker vc cv Expr vars c Expr body cvv Expr triggers
return embed_copy(env, vc->forallExpr(vars, *body, triggers));
DEFINITION: Java_cvc3_ValidityChecker_jniSetTriggers
-void m ValidityChecker vc c Expr closure cv Expr triggers
+void m ValidityChecker vc c Expr closure cvv Expr triggers
vc->setTriggers(*closure, triggers);
DEFINITION: Java_cvc3_ValidityChecker_jniExistsExpr
--- NEW FILE cvc3.spec ---
# If the emacs-el package has installed a pkgconfig file, use that to determine
# install locations and Emacs version at build time, otherwise set defaults.
%if %($(pkg-config emacs) ; echo $?)
%define emacs_version 22.1
%define emacs_lispdir %{_datadir}/emacs/site-lisp
%else
%define emacs_version %(pkg-config emacs --modversion)
%define emacs_lispdir %(pkg-config emacs --variable sitepkglispdir)
%endif
# If the xemacs-devel package has installed a pkgconfig file, use that to
# determine install locations and Emacs version at build time, otherwise set
# defaults.
%if %($(pkg-config xemacs) ; echo $?)
%define xemacs_version 21.5
%define xemacs_lispdir %{_datadir}/xemacs/site-packages/lisp
%else
%define xemacs_version %(pkg-config xemacs --modversion)
%define xemacs_lispdir %(pkg-config xemacs --variable sitepkglispdir)
%endif
Name: cvc3
Version: 2.1
Release: 2%{?dist}
Summary: Validity checker of many-sorted first-order formulas with theories
Group: Applications/Engineering
License: BSD
URL: http://www.cs.nyu.edu/acsys/cvc3/
Source: http://www.cs.nyu.edu/acsys/cvc3/download/%{version}/cvc3-%{version}.tar.gz
# Override compiler flag selection so that $RPM_OPT_FLAGS will take effect.
# Submitted upstream June 2008.
Patch0: cvc3-build.patch
# Fix a few problems in the doxygen documentation.
# Submitted upstream June 2008, with an update in August 2008.
Patch1: cvc3-doc.patch
# GCC 4.3+ uses a streamlined header architecture, so more includes are needed.
# This patch was last submitted upstream on 16 Oct 2009.
Patch2: cvc3-gcc4.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
# Fix Java build problems. This patch was last sent upstream on 19 Oct 2009.
Patch3: cvc3-java.patch
BuildRequires: bison, doxygen, emacs, emacs-el, flex, gnu-free-sans-fonts
BuildRequires: gmp-devel, graphviz, java-devel, jpackage-utils, perl, time
BuildRequires: transfig, tex(latex), xemacs, xemacs-devel
Requires: gnu-free-sans-fonts
%description
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in logical
theories and their combination.
CVC3 is the latest offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular, it
builds on the code base of CVC Lite, its most recent predecessor. Its high
level design follows that of the Sammy prover.
CVC3 works with a version of first-order logic with polymorphic types and has
a wide variety of features including:
* several built-in base theories: rational and integer linear arithmetic,
arrays, tuples, records, inductive data types, bit vectors, and equality
over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* a rich C and C++ API for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial purposes (see
license).
For example, if you run 'cvc3 +interactive' and submit:
i, j: INT; ASSERT i = j + 1; QUERY i>j;
it will determine "Valid." If you then ask:
QUERY i<j; COUNTERMODEL;
it will determine "Invalid." and show an example demonstrating when the formula
is not true (e.g., i = 0 and j = -1).
%package devel
Group: Development/Libraries
Summary: Header files for development with CVC3
Requires: %{name} = %{version}-%{release}
%description devel
Header files need to develop with CVC3.
%package doc
Group: Documentation
Summary: API documentation for CVC3
Requires: %{name} = %{version}-%{release}
%description doc
API documentation for CVC3.
%package java
Group: Development/Libraries/Java
Summary: Java interface for CVC3
Requires: %{name} = %{version}-%{release}, java, jpackage-utils
%description java
Java interface for CVC3.
%package emacs
Group: Applications/Engineering
Summary: Compiled Emacs mode for CVC3
Requires: emacs(bin) >= %{emacs_version}
Requires: %{name} = %{version}-%{release}
%description emacs
This package contains the byte compiled CVC3 mode for Emacs.
%package emacs-el
Group: Applications/Engineering
Summary: Elisp source files for the CVC3 Emacs mode
Requires: %{name} = %{version}-%{release}
%description emacs-el
This package contains the source Elisp files for the CVC3 mode for Emacs. You
do not need to install this package to run %{name}. Install the %{name}-emacs
package to use %{name} with Emacs.
%package xemacs
Group: Applications/Engineering
Summary: Compiled XEmacs mode for CVC3
Requires: xemacs(bin) >= %{xemacs_version}
Requires: %{name} = %{version}-%{release}
%description xemacs
This package contains the byte compiled CVC3 mode for XEmacs.
%package xemacs-el
Group: Applications/Engineering
Summary: Elisp source files for the CVC3 XEmacs mode
Requires: %{name} = %{version}-%{release}
%description xemacs-el
This package contains the source Elisp files for the CVC3 mode for XEmacs. You
do not need to install this package to run %{name}. Install the %{name}-xemacs
package to use %{name} with XEmacs.
%prep
%setup -q
%patch0 -p1
%patch1 -p1
%patch2 -p1
%patch3 -p1
# We can't use loadLibrary, since the JNI libaries are not in a standard place
sed -i \
-e "s|loadLibrary(\"cvc3jni\")|load(\"%{_libdir}/%{name}/libcvc3jni.so\")|" \
java/src/cvc3/Embedded.java
%build
%configure --with-build=optimized --enable-dynamic --enable-java \
--with-java-home=/usr/lib/jvm/java
make %{?_smp_mflags}
# Build the documentation
cd doc
make
rm -f html/*.{map,md5}
%install
rm -rf %{buildroot}
mkdir -p %{buildroot}%{_libdir}/%{name}
%makeinstall javadir=%{buildroot}%{_libdir}/%{name}
# Byte compile the CVC3 mode file for Emacs
mkdir -p %{buildroot}%{_datadir}/emacs/site-lisp
cp -p emacs/cvc-mode.el %{buildroot}%{_datadir}/emacs/site-lisp
pushd %{buildroot}%{_datadir}/emacs/site-lisp
emacs --batch --no-site-file -f batch-byte-compile cvc-mode.el
popd
# Byte compile the CVC3 mode file for XEmacs
mkdir -p %{buildroot}%{_datadir}/xemacs/site-packages/lisp
cp -p emacs/cvc-mode.el %{buildroot}%{_datadir}/xemacs/site-packages/lisp
pushd %{buildroot}%{_datadir}/xemacs/site-packages/lisp
xemacs --batch --no-site-file -f batch-byte-compile cvc-mode.el
popd
# Add missing executable bits to the shared libraries
chmod a+x %{buildroot}%{_libdir}/*.so.*
# Move the JNI libraries to the right place
mv %{buildroot}%{_libdir}/libcvc3jni.* %{buildroot}%{_libdir}/%{name}
# FIXME: dot segfaults on building one inheritance graph, leaving a 0-byte file
badfile="doc/html/classHash_1_1hash__table__inherit__graph.png"
if [ -f "$badfile" -a ! -s "$badfile" ] ; then
rm -f "$badfile"
fi
%check
LD_LIBRARY_PATH=`pwd`/lib make regressonly4
%post -p /sbin/ldconfig
%postun -p /sbin/ldconfig
%clean
rm -rf %{buildroot}
%files
%defattr(-,root,root,-)
%doc INSTALL LICENSE PEOPLE README VERSION
%{_bindir}/cvc3
%{_libdir}/libcvc3.so.*
%files devel
%defattr(-,root,root,-)
%{_includedir}/cvc3
%{_libdir}/*.so
%files doc
%defattr(-,root,root,-)
%doc doc/html
%files java
%defattr(-,root,root,-)
%{_libdir}/%{name}
%files emacs
%defattr(-,root,root,-)
%{_datadir}/emacs/site-lisp/*.elc
%files emacs-el
%defattr(-,root,root,-)
%{_datadir}/emacs/site-lisp/*.el
%files xemacs
%defattr(-,root,root,-)
%{_datadir}/xemacs/site-packages/lisp/*.elc
%files xemacs-el
%defattr(-,root,root,-)
%{_datadir}/xemacs/site-packages/lisp/*.el
%changelog
* Mon Oct 19 2009 Jerry James <loganjerry at gmail.com> - 2.1-2
- Fix problems found on review
- Enable the Java interface
* Thu Oct 15 2009 Jerry James <loganjerry at gmail.com> - 2.1-1
- Initial RPM
--- NEW FILE import.log ---
cvc3-2_1-2_fc11:HEAD:cvc3-2.1-2.fc11.src.rpm:1256228722
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/cvc3/devel/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- .cvsignore 22 Oct 2009 04:07:31 -0000 1.1
+++ .cvsignore 22 Oct 2009 16:25:39 -0000 1.2
@@ -0,0 +1 @@
+cvc3-2.1.tar.gz
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/cvc3/devel/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- sources 22 Oct 2009 04:07:31 -0000 1.1
+++ sources 22 Oct 2009 16:25:39 -0000 1.2
@@ -0,0 +1 @@
+d3756ab645f2e8d567217d8be16a4404 cvc3-2.1.tar.gz
- Previous message (by thread): [pkgdb] qtcurve-gtk2 had acl change status
- Next message (by thread): rpms/cvc3/F-11 cvc3-build.patch, NONE, 1.1 cvc3-doc.patch, NONE, 1.1 cvc3-gcc4.patch, NONE, 1.1 cvc3-java.patch, NONE, 1.1 cvc3.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the fedora-extras-commits
mailing list