cvc3-doxygen.patch

   1 --- src/theory_bitvector/bitvector_proof_rules.h.orig   2009-10-15 19:12:02.000000000 -0600
   2 +++ src/theory_bitvector/bitvector_proof_rules.h        2011-09-06 11:09:44.567370638 -0600
   3 @@ -540,14 +540,14 @@ namespace CVC3 {
   4                                        std::vector<Theorem>& output_bits) = 0;
   5
   6      /**
   7 -     * Rewrite x_1 \vee x_2 \vee \ldots \vee x_n = 0 into
   8 -     * x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0.
   9 +     * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into
  10 +     * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].
  11       */
  12      virtual Theorem zeroBVOR(const Expr& orEqZero) = 0;
  13
  14      /**
  15 -     * Rewrite x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n into
  16 -     * x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n.
  17 +     * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into
  18 +     * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].
  19       */
  20      virtual Theorem oneBVAND(const Expr& andEqOne) = 0;
  21
  22 --- src/theory_bitvector/bitvector_theorem_producer.h.orig      2009-10-15 19:12:03.000000000 -0600
  23 +++ src/theory_bitvector/bitvector_theorem_producer.h   2011-09-06 11:11:29.751366334 -0600
  24 @@ -577,7 +577,7 @@ namespace CVC3 {
  25
  26      /**
  27       * Rewrite x/y to
  28 -     * \exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m & 0 <= m < y)
  29 +     * \f[\exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m \wedge 0 <= m < y)\f]
  30       */
  31      virtual Theorem bvUDivTheorem(const Expr& divExpr);
  32
  33 @@ -629,14 +629,14 @@ namespace CVC3 {
  34      virtual Theorem bvSModRewrite(const Expr& sModExpr);
  35
  36      /**
  37 -     * Rewrite x_1 \vee x_2 \vee \ldots \vee x_n = 0 into
  38 -     * x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0.
  39 +     * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into
  40 +     * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].
  41       */
  42      virtual Theorem zeroBVOR(const Expr& orEqZero);
  43
  44      /**
  45 -     * Rewrite x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n into
  46 -     * x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n.
  47 +     * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into
  48 +     * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].
  49       */
  50      virtual Theorem oneBVAND(const Expr& andEqOne);
  51