diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-29 20:13:52 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-06 15:40:36 -0400 |
commit | 5c42662fe5cea3051341c8292202357e2a5e7dd3 (patch) | |
tree | 94aa636b95c7a81594a3d82f236263c91b0f6d0f /src | |
parent | 0dce010bea47bc6a318eece2bd92ed2305b64c21 (diff) |
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
Diffstat (limited to 'src')
-rwxr-xr-x | src/expr/mkkind | 3 | ||||
-rw-r--r-- | src/parser/parser.h | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 3 |
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()); |