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

1 files changed, 4 insertions, 0 deletions

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; }