From 5c42662fe5cea3051341c8292202357e2a5e7dd3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 29 May 2014 20:13:52 -0400 Subject: 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 --- src/parser/parser.h | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/parser/parser.h') 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; } -- cgit v1.2.3