From 46635f03018e7d3b71453b9e9ba1f4c192e6202a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Oct 22 2009 16:27:53 +0000 Subject: Initial import into F-11 and F-12 branches. --- diff --git a/.cvsignore b/.cvsignore index e69de29..f76e0d5 100644 --- a/.cvsignore +++ b/.cvsignore @@ -0,0 +1 @@ +cvc3-2.1.tar.gz diff --git a/cvc3-build.patch b/cvc3-build.patch new file mode 100644 index 0000000..58119f3 --- /dev/null +++ b/cvc3-build.patch @@ -0,0 +1,21 @@ +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) diff --git a/cvc3-doc.patch b/cvc3-doc.patch new file mode 100644 index 0000000..646559a --- /dev/null +++ b/cvc3-doc.patch @@ -0,0 +1,666 @@ +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 @@ + + + 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 +- *