mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

fix #2910

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-01 14:31:13 -08:00
parent a9d22d7409
commit 321329d77c
4 changed files with 13 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -2284,6 +2284,7 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
<< " for function " << mk_pp(f,*this) << " for function " << mk_pp(f,*this)
<< " supplied sort is " << " supplied sort is "
<< mk_pp(actual_sort, *this); << mk_pp(actual_sort, *this);
SASSERT(false);
throw ast_exception(buffer.str()); throw ast_exception(buffer.str());
} }
} }

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

@ -2034,7 +2034,8 @@ namespace smt2 {
process_last_symbol(fr); process_last_symbol(fr);
TRACE("consume_attributes", tout << "pop_attr_expr_frame, expr_stack.size(): " << expr_stack().size() << "\n";); TRACE("consume_attributes", tout << "pop_attr_expr_frame, expr_stack.size(): " << expr_stack().size() << "\n";);
// the resultant expression is already on the top of the stack. // the resultant expression is already on the top of the stack.
SASSERT(expr_stack().size() == fr->m_expr_spos + 1); if (expr_stack().size() != fr->m_expr_spos + 1)
throw parser_exception("invalid expression");
m_stack.deallocate(fr); m_stack.deallocate(fr);
m_num_expr_frames--; m_num_expr_frames--;
} }

2
src/smt/theory_arith.h
View file

@ -1000,7 +1000,7 @@ namespace smt {
bool is_mixed_real_integer(row const & r) const; bool is_mixed_real_integer(row const & r) const;
bool is_integer(row const & r) const; bool is_integer(row const & r) const;
typedef std::pair<rational, expr *> coeff_expr; typedef std::pair<rational, expr *> coeff_expr;
void get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & vars); bool get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & vars);
expr * p2expr(sbuffer<coeff_expr> & p); expr * p2expr(sbuffer<coeff_expr> & p);
expr * power(expr * var, unsigned power); expr * power(expr * var, unsigned power);
expr * mk_nary_mul(unsigned sz, expr * const * args, bool is_int); expr * mk_nary_mul(unsigned sz, expr * const * args, bool is_int);

16
src/smt/theory_arith_nl.h
View file

@ -1209,7 +1209,7 @@ void theory_arith<Ext>::display_coeff_exprs(std::ostream & out, sbuffer<coeff_ex
occurrences is also stored. occurrences is also stored.
*/ */
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & varinfo) { bool theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & varinfo) {
context & ctx = get_context(); context & ctx = get_context();
varinfo.reset(); varinfo.reset();
m_var2num_occs.reset(); m_var2num_occs.reset();
@ -1222,10 +1222,8 @@ void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
m_var2num_occs.insert(VAR, occs); \ m_var2num_occs.insert(VAR, occs); \
} }
typename sbuffer<coeff_expr>::const_iterator it = p.begin(); for (auto const& ce : p) {
typename sbuffer<coeff_expr>::const_iterator end = p.end(); expr * m = ce.second;
for (; it != end; ++it) {
expr * m = it->second;
if (is_pure_monomial(m)) { if (is_pure_monomial(m)) {
unsigned num_vars = get_num_vars_in_monomial(m); unsigned num_vars = get_num_vars_in_monomial(m);
for (unsigned i = 0; i < num_vars; i++) { for (unsigned i = 0; i < num_vars; i++) {
@ -1242,6 +1240,7 @@ void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
else { else {
TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";); TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
UNREACHABLE(); UNREACHABLE();
return false;
} }
} }
@ -1250,6 +1249,7 @@ void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
if (vn.m_value > 1) if (vn.m_value > 1)
varinfo.push_back(var_num_occs(vn.m_key, vn.m_value)); varinfo.push_back(var_num_occs(vn.m_key, vn.m_value));
} }
return true;
} }
/** /**
@ -1519,7 +1519,8 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
TRACE("non_linear", tout << "p.size: " << p.size() << "\n";); TRACE("non_linear", tout << "p.size: " << p.size() << "\n";);
if (var == nullptr) { if (var == nullptr) {
sbuffer<var_num_occs> varinfo; sbuffer<var_num_occs> varinfo;
get_polynomial_info(p, varinfo); if (!get_polynomial_info(p, varinfo))
return nullptr;
if (varinfo.empty()) if (varinfo.empty())
return p2expr(p); return p2expr(p);
sbuffer<var_num_occs>::const_iterator it = varinfo.begin(); sbuffer<var_num_occs>::const_iterator it = varinfo.begin();
@ -1608,7 +1609,8 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_cross_nested_consistent(sbuffer<coeff_expr> & p) { bool theory_arith<Ext>::is_cross_nested_consistent(sbuffer<coeff_expr> & p) {
sbuffer<var_num_occs> varinfo; sbuffer<var_num_occs> varinfo;
get_polynomial_info(p, varinfo); if (!get_polynomial_info(p, varinfo))
return true;
if (varinfo.empty()) if (varinfo.empty())
return true; return true;
std::stable_sort(varinfo.begin(), varinfo.end(), var_num_occs_lt()); std::stable_sort(varinfo.begin(), varinfo.end(), var_num_occs_lt());