From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 2 Mar 2021 23:22:03 +0000 (-0800)
Subject: Remove non-ASCII characters from source files. (#6039)
X-Git-Tag: cvc5-1.0.0~2167
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80d9eab67e60ae8750165ce18ecd4eebcdc06b44;p=cvc5.git

Remove non-ASCII characters from source files. (#6039)

Make collect_tags.py more robust for non-ASCII characters.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 7a191cd8a..e1c64b750 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3944,7 +3944,7 @@ bool Solver::isValidInteger(const std::string& s) const
 
   if (s[index] == '0' && s.length() > (index + 1))
   {
-    // From SMT-Lib 2.6: A〈numeral〉is the digit 0 or a non-empty sequence of
+    // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
     // digits not starting with 0. So integers like 001, 000 are not allowed
     return false;
   }
diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py
index ea4938d6b..07a6dc18b 100644
--- a/src/base/collect_tags.py
+++ b/src/base/collect_tags.py
@@ -23,7 +23,7 @@ def collect_tags(basedir):
     tags = set()
     for ext in ['.cc', '.cpp', '.g', '.h']:
         for filename in glob.iglob('{}/**/*{}'.format(basedir, ext), recursive=True):
-            content = open(filename).read()
+            content = open(filename, 'rb').read().decode()
             for tag in RE_PAT.finditer(content):
                 tags.add(tag.group(1))
     return sorted(tags)
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 075a50e06..a092a8778 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -18,7 +18,7 @@
  ** described in
  **   Liana Hadarean, An Efficient and Trustworthy Theory Solver for
  **   Bit-vectors in Satisfiability Modulo Theories.
-**   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
+ **   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
  **/
 
 #include "preprocessing/passes/ackermann.h"
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index 08d95927c..cd0d059e4 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -18,7 +18,7 @@
  ** described in
  **   Liana Hadarean, An Efficient and Trustworthy Theory Solver for
  **   Bit-vectors in Satisfiability Modulo Theories.
-**   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
+ **   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
  **/
 
 #include "cvc4_private.h"
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index d57d2a20a..b41af4a76 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -91,7 +91,7 @@ Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
     // If the next one can be merged, try to merge
     bool merged = false;
     if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) {
-      //x[i : j] @ x[j − 1 : k] -> c x[i : k]
+      // x[i : j] @ x[j - 1 : k] -> c x[i : k]
       unsigned nextHigh = utils::getExtractHigh(next);
       unsigned nextLow  = utils::getExtractLow(next);
       if(nextHigh + 1 == currentLow) {
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 9cc8fb773..129d5ce7a 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -184,7 +184,7 @@ Integer Integer::extractBitRange(uint32_t bitCount, uint32_t low) const
 {
   // bitCount = high-low+1
   uint32_t high = low + bitCount - 1;
-  //— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b)
+  //- Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b)
   mpz_class rem, div;
   mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high + 1);
   mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low);