diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 6cddb6038..3edb26818 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -30,6 +30,10 @@ Version 4.2 - Z3 by default switches to an incremental solver when a Solver object is used to solve many queries. In the this version, we switch back to the tactic framework if the incremental solver returns "unknown". +- Allow negative numerals in the SMT 2.0 frontend. That is, Z3 SMT 2.0 parser now accepts numerals such as "-2". It is not needed to encode them as "(- 2)" anymore. + The parser still accepts -foo as a symbol. That is, it is *not* a shorthand for (- foo). + This feature is disabled when SMTLIB2_COMPLIANT=true is set in the command line. + - Now, Z3 can be compiled inside cygwin using gcc. - Fixed bug in the unsat core generation. diff --git a/lib/cmd_context.h b/lib/cmd_context.h index 8bc1e242e..381abce1c 100644 --- a/lib/cmd_context.h +++ b/lib/cmd_context.h @@ -246,6 +246,7 @@ protected: public: cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); ~cmd_context(); + bool is_smtlib2_compliant() const { return m_params.m_smtlib2_compliant; } void set_logic(symbol const & s); bool has_logic() const { return m_logic != symbol::null; } symbol const & get_logic() const { return m_logic; } diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp index 85b73e362..4439d571f 100644 --- a/lib/pdr_dl_interface.cpp +++ b/lib/pdr_dl_interface.cpp @@ -186,7 +186,7 @@ void dl_interface::collect_params(param_descrs& p) { p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"); p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); - p.insert(":flexible-trace", CPK_BOOL, "PDR: (default true) allow PDR generate long counter-examples by extending candidate trace within search area"); + p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area"); PRIVATE_PARAMS(p.insert(":use-farkas-model", CPK_BOOL, "PDR: (default false) enable using Farkas generalization through model propagation");); PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions");); PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");); diff --git a/lib/smt2parser.cpp b/lib/smt2parser.cpp index 70f984de7..da5bd0e88 100644 --- a/lib/smt2parser.cpp +++ b/lib/smt2parser.cpp @@ -2353,7 +2353,7 @@ namespace smt2 { public: parser(cmd_context & ctx, std::istream & is, bool interactive): m_ctx(ctx), - m_scanner(is, interactive), + m_scanner(ctx, is, interactive), m_curr(scanner::NULL_TOKEN), m_curr_cmd(0), m_num_bindings(0), diff --git a/lib/smt2scanner.cpp b/lib/smt2scanner.cpp index b2780356c..0546fe914 100644 --- a/lib/smt2scanner.cpp +++ b/lib/smt2scanner.cpp @@ -87,17 +87,12 @@ namespace smt2 { next(); } } - - scanner::token scanner::read_symbol() { - SASSERT(m_normalized[static_cast(curr())] == 'a' || curr() == ':'); - m_string.reset(); - m_string.push_back(curr()); - next(); - + + scanner::token scanner::read_symbol_core() { while (true) { char c = curr(); char n = m_normalized[static_cast(c)]; - if (n == 'a' || n == '0') { + if (n == 'a' || n == '0' || n == '-') { m_string.push_back(c); next(); } @@ -110,6 +105,14 @@ namespace smt2 { } } + scanner::token scanner::read_symbol() { + SASSERT(m_normalized[static_cast(curr())] == 'a' || curr() == ':' || curr() == '-'); + m_string.reset(); + m_string.push_back(curr()); + next(); + read_symbol_core(); + } + scanner::token scanner::read_number() { SASSERT('0' <= curr() && curr() <= '9'); rational q(1); @@ -140,6 +143,22 @@ namespace smt2 { TRACE("scanner", tout << "new number: " << m_number << "\n";); return is_float ? FLOAT_TOKEN : INT_TOKEN; } + + scanner::token scanner::read_signed_number() { + SASSERT(curr() == '-'); + next(); + if ('0' <= curr() && curr() <= '9') { + scanner::token r = read_number(); + m_number.neg(); + return r; + } + else { + // it is a symbol. + m_string.reset(); + m_string.push_back('-'); + return read_symbol_core(); + } + } scanner::token scanner::read_string() { SASSERT(curr() == '\"'); @@ -222,7 +241,8 @@ namespace smt2 { } } - scanner::scanner(std::istream& stream, bool interactive): + scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive): + m_ctx(ctx), m_interactive(interactive), m_spos(0), m_curr(0), // avoid Valgrind warning @@ -259,7 +279,7 @@ namespace smt2 { m_normalized[static_cast('&')] = 'a'; m_normalized[static_cast('*')] = 'a'; m_normalized[static_cast('_')] = 'a'; - m_normalized[static_cast('-')] = 'a'; + m_normalized[static_cast('-')] = '-'; m_normalized[static_cast('+')] = 'a'; m_normalized[static_cast('=')] = 'a'; m_normalized[static_cast('<')] = 'a'; @@ -304,6 +324,11 @@ namespace smt2 { return read_number(); case '#': return read_bv_literal(); + case '-': + if (m_ctx.is_smtlib2_compliant()) + return read_symbol(); + else + return read_signed_number(); case -1: return EOF_TOKEN; default: { diff --git a/lib/smt2scanner.h b/lib/smt2scanner.h index d504ba3e7..015f05fa1 100644 --- a/lib/smt2scanner.h +++ b/lib/smt2scanner.h @@ -31,6 +31,7 @@ namespace smt2 { class scanner { private: + cmd_context & m_ctx; bool m_interactive; int m_spos; // position in the current line of the stream char m_curr; // current char; @@ -73,7 +74,7 @@ namespace smt2 { EOF_TOKEN }; - scanner(std::istream& stream, bool interactive = false); + scanner(cmd_context & ctx, std::istream& stream, bool interactive = false); ~scanner() {} @@ -85,10 +86,12 @@ namespace smt2 { char const * get_string() const { return m_string.begin(); } token scan(); + token read_symbol_core(); token read_symbol(); token read_quoted_symbol(); void read_comment(); token read_number(); + token read_signed_number(); token read_string(); token read_bv_literal();