Sets translate, and other short fixes

- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine

4 files changed, 9 insertions, 3 deletions

diff --git a/src/expr/mkkind b/src/expr/mkkind
index 987feafac..d54aa3a83 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -333,8 +333,9 @@ function register_kind {
   r=$1
   nc=$2
   comment=$3
+  register_kind_counter=$[register_kind_counter+1]
 
-  kind_decls="${kind_decls}  $r, /**< $comment */
+  kind_decls="${kind_decls}  $r, /**< $comment ($register_kind_counter) */
 "
   kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
 "
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 3f5e66492..2f30460d2 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -272,6 +272,10 @@ public:
   void disallowIncludeFile() { d_canIncludeFile = false; }
   bool canIncludeFile() const { return d_canIncludeFile; }
 
+  /** Expose the functionality from SMT/SMT2 parsers, while making
+      implementation optional by returning false by default. */
+  virtual bool logicIsSet() { return false; }
+
   void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; }
   const std::string& getForcedLogic() const { return d_forcedLogic; }
   bool logicIsForced() const { return d_logicIsForced; }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8201c9b7c..8e5a9dae4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -713,7 +713,7 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
 
 // SMT-LIB quoting for symbols
 static std::string quoteSymbol(std::string s) {
-  if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@%^&*_-+=<>.?/") == std::string::npos) {
+  if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") == std::string::npos) {
     // simple unquoted symbol
     return s;
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9ac1e9db..33496ac3b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3444,7 +3444,8 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   Trace("smt") << "--- model-post expected " << expectedType << endl;
 
   // type-check the result we got
-  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType));
+  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType),
+         "Run with -t smt for details.");
 
   // ensure it's a constant
   Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());