mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #2120 fix #2122

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-03 17:15:38 +01:00
parent 9fde9fe3a2
commit 0acc042bf7
3 changed files with 51 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/polynomial/algebraic_numbers.cpp
View file

@ -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);

2
src/math/polynomial/upolynomial.cpp
View file

@ -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))

93
src/parsers/smt2/smt2parser.cpp
View file

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