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@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<<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@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<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));