summaryrefslogtreecommitdiff
path: root/src/util/bitvector.h
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2012-04-04 02:02:06 +0000
committerLiana Hadarean <lianahady@gmail.com>2012-04-04 02:02:06 +0000
commit52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch)
tree040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/util/bitvector.h
parent4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff)
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally * added more bv regressions
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r--src/util/bitvector.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 7429ac8c9..512f23136 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -337,9 +337,9 @@ public:
}
/**
- Returns k is the integer is equal to 2^k and zero
+ Returns k is the integer is equal to 2^{k-1} and zero
otherwise
- @return k if the integer is equal to 2^k and zero otherwise
+ @return k if the integer is equal to 2^{k-1} and zero otherwise
*/
unsigned isPow2() {
return d_value.isPow2();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback