From 0acc042bf77860dbd9d7d42d6ac4fdae8afb7ca8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Feb 2019 17:15:38 +0100 Subject: [PATCH] fix #2120 fix #2122 Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/algebraic_numbers.cpp | 11 ++- src/math/polynomial/upolynomial.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 93 ++++++++++------------- 3 files changed, 51 insertions(+), 55 deletions(-) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 17360f35b..25a1985a7 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -561,7 +561,9 @@ namespace algebraic_numbers { }; void sort_roots(numeral_vector & r) { - std::sort(r.begin(), r.end(), lt_proc(m_wrapper)); + if (m_limit.inc()) { + std::sort(r.begin(), r.end(), lt_proc(m_wrapper)); + } } void isolate_roots(scoped_upoly const & up, numeral_vector & roots) { @@ -1750,8 +1752,7 @@ namespace algebraic_numbers { // then they MUST BE DIFFERENT. // Thus, if we keep refining the interval of a and b, // eventually they will not overlap - while (true) { - checkpoint(); + while (m_limit.inc()) { refine(a); refine(b); m_compare_refine++; @@ -1764,6 +1765,9 @@ namespace algebraic_numbers { } } + if (!m_limit.inc()) + return 0; + // make sure that intervals of a and b have the same magnitude int a_m = magnitude(a_lower, a_upper); int b_m = magnitude(b_lower, b_upper); @@ -1810,6 +1814,7 @@ namespace algebraic_numbers { // V == 0 --> a = b // if (V < 0) == (p_b(b_lower) < 0) then b > a else b < a // + m_compare_sturm++; upolynomial::scoped_upolynomial_sequence seq(upm()); upm().sturm_tarski_seq(cell_a->m_p_sz, cell_a->m_p, cell_b->m_p_sz, cell_b->m_p, seq); diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index f300dc4ab..65dbf91f4 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -2517,7 +2517,7 @@ namespace upolynomial { // Keep expanding the Sturm sequence starting at seq void manager::sturm_seq_core(upolynomial_sequence & seq) { scoped_numeral_vector r(m()); - while (true) { + while (m_limit.inc()) { unsigned sz = seq.size(); srem(seq.size(sz-2), seq.coeffs(sz-2), seq.size(sz-1), seq.coeffs(sz-1), r); if (is_zero(r)) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 64f9c36fd..bf1e25e57 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1371,11 +1371,11 @@ namespace smt2 { else { while (!curr_is_rparen()) { m_env.begin_scope(); + check_lparen_next("invalid pattern binding, '(' expected"); unsigned num_bindings = m_num_bindings; parse_match_pattern(srt); patterns.push_back(expr_stack().back()); expr_stack().pop_back(); - check_lparen_next("invalid pattern binding, '(' expected"); parse_expr(); cases.push_back(expr_stack().back()); expr_stack().pop_back(); @@ -1474,22 +1474,29 @@ namespace smt2 { * _ * x */ - - bool parse_constructor_pattern(sort * srt) { - if (!curr_is_lparen()) { - return false; - } - next(); + + void parse_match_pattern(sort * srt) { + symbol C; svector vars; expr_ref_vector args(m()); - symbol C(check_identifier_next("constructor symbol expected")); - while (!curr_is_rparen()) { - symbol v(check_identifier_next("variable symbol expected")); - if (v != m_underscore && vars.contains(v)) { - throw parser_exception("unexpected repeated variable in pattern expression"); - } - vars.push_back(v); - } + + if (curr_is_identifier()) { + C = curr_id(); + } + else if (curr_is_lparen()) { + next(); + C = check_identifier_next("constructor symbol expected"); + while (!curr_is_rparen()) { + symbol v(check_identifier_next("variable symbol expected")); + if (v != m_underscore && vars.contains(v)) { + throw parser_exception("unexpected repeated variable in pattern expression"); + } + vars.push_back(v); + } + } + else { + throw parser_exception("expecting a constructor, _, variable or constructor application"); + } next(); // now have C, vars @@ -1498,10 +1505,28 @@ namespace smt2 { // store expression in expr_stack(). // ensure that bound variables are adjusted to vars - func_decl* f = m_ctx.find_func_decl(C, 0, nullptr, vars.size(), nullptr, srt); - if (!f) { + func_decl* f = nullptr; + try { + f = m_ctx.find_func_decl(C, 0, nullptr, vars.size(), nullptr, srt); + } + catch (cmd_exception &) { + if (!args.empty()) { + throw; + } + } + + if (!f && !args.empty()) { throw parser_exception("expecting a constructor that has been declared"); } + if (!f) { + m_num_bindings++; + var * v = m().mk_var(0, srt); + if (C != m_underscore) { + m_env.insert(C, local(v, m_num_bindings)); + } + expr_stack().push_back(v); + return; + } if (!dtutil().is_constructor(f)) { throw parser_exception("expecting a constructor"); } @@ -1517,40 +1542,6 @@ namespace smt2 { } } expr_stack().push_back(m().mk_app(f, args.size(), args.c_ptr())); - return true; - } - - void parse_match_pattern(sort* srt) { - if (parse_constructor_pattern(srt)) { - // done - } - else if (curr_id() == m_underscore) { - // we have a wild-card. - // store dummy variable in expr_stack() - next(); - var* v = m().mk_var(0, srt); - expr_stack().push_back(v); - } - else { - symbol xC(check_identifier_next("constructor symbol or variable expected")); - // check if xC is a constructor, otherwise make it a variable - // of sort srt. - try { - func_decl* f = m_ctx.find_func_decl(xC, 0, nullptr, 0, nullptr, srt); - if (!dtutil().is_constructor(f)) { - throw parser_exception("expecting a constructor, got a previously declared function"); - } - if (f->get_arity() > 0) { - throw parser_exception("constructor expects arguments, but no arguments were supplied in pattern"); - } - expr_stack().push_back(m().mk_const(f)); - } - catch (cmd_exception &) { - var* v = m().mk_var(0, srt); - expr_stack().push_back(v); - m_env.insert(xC, local(v, m_num_bindings++)); - } - } } symbol parse_indexed_identifier_core() {