|
|
72c7f33 |
--- src/theory_bitvector/bitvector_proof_rules.h.orig 2009-10-15 19:12:02.000000000 -0600
|
|
|
72c7f33 |
+++ src/theory_bitvector/bitvector_proof_rules.h 2011-09-06 11:09:44.567370638 -0600
|
|
|
72c7f33 |
@@ -540,14 +540,14 @@ namespace CVC3 {
|
|
|
72c7f33 |
std::vector<Theorem>& output_bits) = 0;
|
|
|
72c7f33 |
|
|
|
72c7f33 |
/**
|
|
|
72c7f33 |
- * Rewrite x_1 \vee x_2 \vee \ldots \vee x_n = 0 into
|
|
|
72c7f33 |
- * x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0.
|
|
|
72c7f33 |
+ * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into
|
|
|
72c7f33 |
+ * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].
|
|
|
72c7f33 |
*/
|
|
|
72c7f33 |
virtual Theorem zeroBVOR(const Expr& orEqZero) = 0;
|
|
|
72c7f33 |
|
|
|
72c7f33 |
/**
|
|
|
72c7f33 |
- * Rewrite x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n into
|
|
|
72c7f33 |
- * x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n.
|
|
|
72c7f33 |
+ * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into
|
|
|
72c7f33 |
+ * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].
|
|
|
72c7f33 |
*/
|
|
|
72c7f33 |
virtual Theorem oneBVAND(const Expr& andEqOne) = 0;
|
|
|
72c7f33 |
|
|
|
72c7f33 |
--- src/theory_bitvector/bitvector_theorem_producer.h.orig 2009-10-15 19:12:03.000000000 -0600
|
|
|
72c7f33 |
+++ src/theory_bitvector/bitvector_theorem_producer.h 2011-09-06 11:11:29.751366334 -0600
|
|
|
72c7f33 |
@@ -577,7 +577,7 @@ namespace CVC3 {
|
|
|
72c7f33 |
|
|
|
72c7f33 |
/**
|
|
|
72c7f33 |
* Rewrite x/y to
|
|
|
72c7f33 |
- * \exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m & 0 <= m < y)
|
|
|
72c7f33 |
+ * \f[\exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m \wedge 0 <= m < y)\f]
|
|
|
72c7f33 |
*/
|
|
|
72c7f33 |
virtual Theorem bvUDivTheorem(const Expr& divExpr);
|
|
|
72c7f33 |
|
|
|
72c7f33 |
@@ -629,14 +629,14 @@ namespace CVC3 {
|
|
|
72c7f33 |
virtual Theorem bvSModRewrite(const Expr& sModExpr);
|
|
|
72c7f33 |
|
|
|
72c7f33 |
/**
|
|
|
72c7f33 |
- * Rewrite x_1 \vee x_2 \vee \ldots \vee x_n = 0 into
|
|
|
72c7f33 |
- * x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0.
|
|
|
72c7f33 |
+ * Rewrite \f[x_1 \vee x_2 \vee \ldots \vee x_n = 0\f] into
|
|
|
72c7f33 |
+ * \f[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\f].
|
|
|
72c7f33 |
*/
|
|
|
72c7f33 |
virtual Theorem zeroBVOR(const Expr& orEqZero);
|
|
|
72c7f33 |
|
|
|
72c7f33 |
/**
|
|
|
72c7f33 |
- * Rewrite x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n into
|
|
|
72c7f33 |
- * x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n.
|
|
|
72c7f33 |
+ * Rewrite \f[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\f] into
|
|
|
72c7f33 |
+ * \f[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\f].
|
|
|
72c7f33 |
*/
|
|
|
72c7f33 |
virtual Theorem oneBVAND(const Expr& andEqOne);
|
|
|
72c7f33 |
|