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<symbol> 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() {