Improve

src/kind.cpp

@@ -77,7 +77,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     // conversions
     case Kind::EVAL_TO_INT: o << "EVAL_TO_INT"; break;
     case Kind::EVAL_TO_RAT: o << "EVAL_TO_RAT"; break;
-    case Kind::EVAL_TO_BV: o << "EVAL_TO_BV"; break;
+    case Kind::EVAL_TO_BIN: o << "EVAL_TO_BIN"; break;
     case Kind::EVAL_TO_STRING: o << "EVAL_TO_STRING"; break;
     default: o << "UnknownKind(" << unsigned(k) << ")"; break;
   }
@@ -139,7 +139,7 @@ std::string kindToTerm(Kind k)
         // conversions
         case Kind::EVAL_TO_INT: ss << "to_z";break;
         case Kind::EVAL_TO_RAT: ss << "to_q";break;
-        case Kind::EVAL_TO_BV: ss << "to_bv";break;
+        case Kind::EVAL_TO_BIN: ss << "to_bin";break;
         case Kind::EVAL_TO_STRING: ss << "to_str";break;
         default:ss << "[" << k << "]";break;
         }
@@ -217,7 +217,7 @@ bool isLiteralOp(Kind k)
     // conversions
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_TO_RAT:
-    case Kind::EVAL_TO_BV:
+    case Kind::EVAL_TO_BIN:
     case Kind::EVAL_TO_STRING:return true; break;
     default: break;
   }

src/kind.h

@@ -87,7 +87,7 @@ enum class Kind
   // conversions
   EVAL_TO_INT,
   EVAL_TO_RAT,
-  EVAL_TO_BV,
+  EVAL_TO_BIN,
   EVAL_TO_STRING
 };
 

src/literal.cpp

@@ -136,7 +136,7 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
 {
   Assert (k!=Kind::EVAL_IS_EQ && k!=Kind::EVAL_IF_THEN_ELSE && k!=Kind::EVAL_REQUIRES);
   Kind ka = Kind::NONE;
-  if (k!=Kind::EVAL_EXTRACT && k!=Kind::EVAL_TO_BV)
+  if (k!=Kind::EVAL_EXTRACT && k!=Kind::EVAL_TO_BIN)
   {
     ka = allSameKind(args);
     if (ka==Kind::NONE)
@@ -413,7 +413,7 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
         default: break;
       }
       break;
-    case Kind::EVAL_TO_BV:
+    case Kind::EVAL_TO_BIN:
       if (args[0]->d_kind==Kind::NUMERAL && args[0]->d_int.fitsUnsignedInt())
       {
         uint32_t size = args[0]->d_int.toUnsignedInt();

src/state.cpp

@@ -73,7 +73,7 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("is_neg", Kind::EVAL_IS_NEG);
   bindBuiltinEval("to_z", Kind::EVAL_TO_INT);
   bindBuiltinEval("to_q", Kind::EVAL_TO_RAT);
-  bindBuiltinEval("to_bin", Kind::EVAL_TO_BV);
+  bindBuiltinEval("to_bin", Kind::EVAL_TO_BIN);
   bindBuiltinEval("to_str", Kind::EVAL_TO_STRING);
   // strings
   bindBuiltinEval("len", Kind::EVAL_LENGTH);

src/type_checker.cpp

@@ -163,7 +163,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_INT_DIV:
     case Kind::EVAL_INT_MOD:
     case Kind::EVAL_RAT_DIV:
-    case Kind::EVAL_TO_BV:
+    case Kind::EVAL_TO_BIN:
     case Kind::EVAL_FIND:
     case Kind::EVAL_CONS:
       ret = (nargs==2);