diff --git a/.cvsignore b/.cvsignore
index f76e0d5..3ea3757 100644
--- a/.cvsignore
+++ b/.cvsignore
@@ -1 +1 @@
-cvc3-2.1.tar.gz
+cvc3-2.2.tar.gz
diff --git a/cvc3-build.patch b/cvc3-build.patch
index 58119f3..f9d2535 100644
--- a/cvc3-build.patch
+++ b/cvc3-build.patch
@@ -1,6 +1,6 @@
-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
+diff -dur cvc3-2.2.ORIG/Makefile.std cvc3-2.2/Makefile.std
+--- cvc3-2.2.ORIG/Makefile.std 2009-09-30 12:54:34.000000000 -0600
++++ cvc3-2.2/Makefile.std 2009-10-15 21:12:35.804289073 -0600
@@ -92,7 +92,7 @@
DEBUG_PLATFORM = -optdbg
else
diff --git a/cvc3-doc.patch b/cvc3-doc.patch
index 646559a..769ce3c 100644
--- a/cvc3-doc.patch
+++ b/cvc3-doc.patch
@@ -1,12 +1,12 @@
-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
+diff -dur cvc3-2.2.ORIG/doc/Doxyfile.in cvc3-2.2/doc/Doxyfile.in
+--- cvc3-2.2.ORIG/doc/Doxyfile.in 2007-09-11 11:31:56.000000000 -0600
++++ cvc3-2.2/doc/Doxyfile.in 2009-11-19 12:20:02.067998020 -0700
@@ -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
++PROJECT_NUMBER = 2.2
# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute)
# base path where the generated documentation will be put.
@@ -73,594 +73,3 @@ diff -dur cvc3-2.1.ORIG/doc/Doxyfile.in cvc3-2.1/doc/Doxyfile.in
# 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 @@
-
-
- Note: 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
-- *
-+ * 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
-+ *
- * - \f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
- *
- \f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
- *
-@@ -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
- *
- * - \f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
- *
- \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@t0 < 0@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<>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, ) -- translation of k*t to BVPLUS
--/*! If k = 2^m, return k*t = t@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@...@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@c2@...@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@z)@w = x@y@z@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@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& reasons)
-+bool TheoryCore::incomplete(std::vector& reasons)
- {
- if(d_incomplete.size() > 0) {
- for(CDMap::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& constructors,
-- const vector >& selectors,
-- const vector >& types)
-+Expr TheoryDatatype::dataType(const std::string& name,
-+ const std::vector& constructors,
-+ const std::vector >& selectors,
-+ const std::vector >& types)
- {
- vector names;
- vector > 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& names,
-- const vector >& allConstructors,
-- const vector > >& allSelectors,
-- const vector > >& allTypes)
-+Expr TheoryDatatype::dataType(const std::vector& names,
-+ const std::vector >& allConstructors,
-+ const std::vector > >& allSelectors,
-+ const std::vector > >& allTypes)
- {
- vector 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& 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* >*>& trig_maps, const Theorem& thm, size_t univs_id){
-+void TheoryQuant::setupTriggers(ExprMap* >*>& trig_maps, const Theorem& thm, size_t univs_id){
-
- // static std::vector 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*>*>& new_trigs,
-+void TheoryQuant::matchListNew(ExprMap*>*>& new_trigs,
- const CDList& glist,
- size_t gbegin,
- size_t gend){
-@@ -7984,7 +7984,7 @@
- d_lastEqsUpdatePos.set(d_eqsUpdate.size());
- }
-
--void TheoryQuant::synCheckSat(ExprMap* >* >& new_trigs, bool fullEffort){
-+void TheoryQuant::synCheckSat(ExprMap* >* >& 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& fields,
-- const vector& types)
-+Type VCL::recordType(const std::vector& fields,
-+ const std::vector& 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& selectors, const vector& types)
-+Type VCL::dataType(const std::string& name,
-+ const std::string& constructor,
-+ const std::vector& selectors,
-+ const std::vector& types)
- {
- vector constructors;
- constructors.push_back(constructor);
-@@ -806,10 +807,10 @@
- }
-
-
--Type VCL::dataType(const string& name,
-- const vector& constructors,
-- const vector >& selectors,
-- const vector >& types)
-+Type VCL::dataType(const std::string& name,
-+ const std::vector& constructors,
-+ const std::vector >& selectors,
-+ const std::vector >& types)
- {
- Expr res = d_theoryDatatype->dataType(name, constructors, selectors, types);
- if(d_dump) {
-@@ -819,11 +820,11 @@
- }
-
-
--void VCL::dataType(const vector& names,
-- const vector >& constructors,
-- const vector > >& selectors,
-- const vector > >& types,
-- vector& returnTypes)
-+void VCL::dataType(const std::vector& names,
-+ const std::vector >& constructors,
-+ const std::vector > >& selectors,
-+ const std::vector > >& types,
-+ std::vector& returnTypes)
- {
- Expr res = d_theoryDatatype->dataType(names, constructors, selectors, types);
- if(d_dump) {
-@@ -1405,8 +1406,8 @@
- }
-
-
--Expr VCL::recordExpr(const vector& fields,
-- const vector& exprs)
-+Expr VCL::recordExpr(const std::vector& fields,
-+ const std::vector& exprs)
- {
- DebugAssert(fields.size() > 0, "VCL::recordExpr()");
- DebugAssert(fields.size() == exprs.size(),"VCL::recordExpr()");
-@@ -2107,7 +2108,7 @@
- }
-
-
--bool VCL::incomplete(vector& reasons) {
-+bool VCL::incomplete(std::vector& reasons) {
- // TODO: add to interactive interface
- // Return true only after a failed query
- return (d_lastQuery.isNull() && d_theoryCore->incomplete(reasons));
diff --git a/cvc3-gcc4.patch b/cvc3-gcc4.patch
deleted file mode 100644
index cb66593..0000000
--- a/cvc3-gcc4.patch
+++ /dev/null
@@ -1,80 +0,0 @@
-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
- #include
- #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
- #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
- #include
- #include
-
-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
- #include
- #include
- #include
diff --git a/cvc3-java.patch b/cvc3-java.patch
deleted file mode 100644
index 740d4d7..0000000
--- a/cvc3-java.patch
+++ /dev/null
@@ -1,60 +0,0 @@
-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(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(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
diff --git a/cvc3.spec b/cvc3.spec
index df0822f..7122e03 100644
--- a/cvc3.spec
+++ b/cvc3.spec
@@ -1,14 +1,6 @@
-# If the xemacs-devel package has installed a pkgconfig file, use that to
-# determine version at build time, otherwise set a default.
-%if %($(pkg-config xemacs) ; echo $?)
-%define xemacs_version 21.5
-%else
-%define xemacs_version %(pkg-config xemacs --modversion)
-%endif
-
Name: cvc3
-Version: 2.1
-Release: 3%{?dist}
+Version: 2.2
+Release: 1%{?dist}
Summary: Validity checker of many-sorted first-order formulas with theories
Group: Applications/Engineering
@@ -18,15 +10,10 @@ Source: http://www.cs.nyu.edu/acsys/cvc3/download/%{version}/cvc3-%{vers
# 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.
+# This patch is Fedora-specific. Set up doxygen so that the generated
+# documentation meets packaging standards.
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, java-devel, jpackage-utils, perl, time
@@ -114,7 +101,7 @@ package to use %{name} with Emacs.
%package xemacs
Group: Applications/Engineering
Summary: Compiled XEmacs mode for CVC3
-Requires: xemacs(bin) >= %{xemacs_version}
+Requires: xemacs(bin) >= %{_xemacs_version}
Requires: %{name} = %{version}-%{release}
BuildArch: noarch
@@ -136,8 +123,6 @@ package to use %{name} with XEmacs.
%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 \
@@ -226,6 +211,10 @@ rm -rf %{buildroot}
%{_xemacs_sitelispdir}/*.el
%changelog
+* Thu Nov 19 2009 Jerry James - 2.2-1
+- Update to 2.2
+- Drop upstreamed patches (gcc4 and java)
+
* Tue Oct 27 2009 Jerry James - 2.1-3
- Drop the graphviz BR to block generation of huge class graphs
- Use the new (X)Emacs RPM macros to simplify the spec file
diff --git a/sources b/sources
index 07ae57c..92dcff1 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-d3756ab645f2e8d567217d8be16a4404 cvc3-2.1.tar.gz
+fe24b28454977ca035a39c35ad144796 cvc3-2.2.tar.gz