]>
Commit | Line | Data |
---|---|---|
1b1c55f5 JR |
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 |