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 7a191cd8ab8a3c984c7453ab311ebfa384103226..e1c64b75078f1d642f719c441cc6a053fe15c4cb 100644 (file)
--- 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 ea4938d6b3fb8c1b505c4d103c7227873d94cb81..07a6dc18bc6bd413cb84301ef60c83eb527a5b71 100644 (file)
--- 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 075a50e0699b7978b9e9521da599b061da407dd7..a092a877890fbc408e7b113918e5119ff6d8c8a8 100644 (file)
--- 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 08d95927c3cf774764399b8555d30ae1e114e114..cd0d059e43af691e9b867fac9abb312db5e1c959 100644 (file)
--- 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 d57d2a20ab8cf0fe2d109b2936af1469280f3868..b41af4a76307767a81b518f0181514c703bdf719 100644 (file)
--- 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 9cc8fb77357cc8b5425ee3c2eac5b6f3da6236c6..129d5ce7adf671c1b250a942f206ac13822acf30 100644 (file)
--- 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);