diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1b06435a3..eb65d74cc 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -18,16 +18,16 @@ Notes: --*/ +#include "util/uint_set.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/ast_util.h" -#include "util/uint_set.h" -#include "math/automata/automaton.h" #include "ast/well_sorted.h" #include "ast/rewriter/var_subst.h" #include "ast/rewriter/bool_rewriter.h" +#include "math/automata/automaton.h" #include "math/automata/symbolic_automata_def.h" @@ -810,6 +810,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu result = m_util.str.mk_concat(_len, as.c_ptr() + offset); return BR_DONE; } + if (i == as.size()) { + result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset); + return BR_DONE; + } } if (offset == 0) { return BR_FAILED; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 81783c85c..eaa60d4df 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -667,6 +667,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons match_right_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k_seq); info.set_right_associative(true); + info.set_left_associative(true); return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); } diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index a368c9507..4f7a6ab8c 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -5810,6 +5810,7 @@ namespace polynomial { ps = coeff(B, x, d-1); if (!is_zero(ps)) S.push_back(ps); + SASSERT(d >= e); unsigned delta = d - e; if (delta > 1) { // C <- S_e @@ -5932,8 +5933,8 @@ namespace polynomial { void psc_chain(polynomial const * A, polynomial const * B, var x, polynomial_ref_vector & S) { // psc_chain1(A, B, x, S); - // psc_chain2(A, B, x, S); - // psc_chain_classic(A, B, x, S); + //psc_chain2(A, B, x, S); + //psc_chain_classic(A, B, x, S); psc_chain_optimized(A, B, x, S); } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 3ed62cb81..0cafb4ac1 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -312,6 +312,7 @@ namespace nlsat { polynomial_ref lc(m_pm); polynomial_ref reduct(m_pm); while (true) { + TRACE("nlsat_explain", tout << "elim vanishing x" << x << " k:" << k << " " << p << "\n";); if (is_const(p)) return; if (k == 0) { @@ -320,9 +321,22 @@ namespace nlsat { SASSERT(x != null_var); k = degree(p, x); } - if (m_pm.nonzero_const_coeff(p, x, k)) +#if 0 + anum const & x_val = m_assignment.value(x); + if (m_am.is_zero(x_val)) { + // add_zero_assumption(lc); + lc = m_pm.coeff(p, x, k, reduct); + k--; + p = reduct; + continue; + } +#endif + if (m_pm.nonzero_const_coeff(p, x, k)) { + TRACE("nlsat_explain", tout << "nonzero const x" << x << "\n";); return; // lc is a nonzero constant + } lc = m_pm.coeff(p, x, k, reduct); + TRACE("nlsat_explain", tout << "lc: " << lc << " reduct: " << reduct << "\n";); if (!is_zero(lc)) { if (sign(lc) != polynomial::sign_zero) return; @@ -630,7 +644,7 @@ namespace nlsat { for (unsigned i = 0; i < sz; i++) { s = S.get(i); - TRACE("nlsat_explain", tout << "processing psc(" << i << ")\n"; display(tout, s); tout << "\n";); + TRACE("nlsat_explain", display(tout << "processing psc(" << i << ")\n", s) << "\n";); if (is_zero(s)) { TRACE("nlsat_explain", tout << "skipping psc is the zero polynomial\n";); continue; diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 65acaeec8..816047f49 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -19,6 +19,7 @@ Revision History: #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/well_sorted.h" +#include "ast/array_decl_plugin.h" #include "ast/used_symbols.h" #include "ast/for_each_expr.h" #include "ast/rewriter/var_subst.h" @@ -119,19 +120,23 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { \brief Replace uninterpreted constants occurring in fi->get_else() by their interpretations. */ -void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs) { - if (fi->is_partial()) - return; - expr * fi_else = fi->get_else(); - TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m) << "\n";); +void proto_model::cleanup_func_interp(expr_ref_vector& trail, func_interp * fi, func_decl_set & found_aux_fs) { + if (!fi->is_partial()) { + expr * fi_else = fi->get_else(); + fi->set_else(cleanup_expr(trail, fi_else, found_aux_fs)); + } +} +expr* proto_model::cleanup_expr(expr_ref_vector& trail, expr* fi_else, func_decl_set& found_aux_fs) { + TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m) << "\n";); + trail.reset(); obj_map cache; - expr_ref_vector trail(m); ptr_buffer todo; ptr_buffer args; todo.push_back(fi_else); - expr * a; + expr_ref new_t(m); + while (!todo.empty()) { a = todo.back(); if (is_uninterp_const(a)) { @@ -168,8 +173,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au TRACE("model_bug", tout << f->get_name() << "\n";); found_aux_fs.insert(f); } - expr_ref new_t(m); - new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr()); + new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr()); if (t != new_t.get()) trail.push_back(new_t); todo.pop_back(); @@ -177,7 +181,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au break; } default: - SASSERT(a != 0); + SASSERT(a != nullptr); cache.insert(a, a); todo.pop_back(); break; @@ -187,17 +191,14 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au VERIFY(cache.find(fi_else, a)); - fi->set_else(a); + return a; } void proto_model::remove_aux_decls_not_in_set(ptr_vector & decls, func_decl_set const & s) { - unsigned sz = decls.size(); unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - func_decl * f = decls[i]; + for (func_decl* f : decls) { if (!m_aux_decls.contains(f) || s.contains(f)) { - decls[j] = f; - j++; + decls[j++] = f; } } decls.shrink(j); @@ -211,12 +212,21 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector & decls, fun void proto_model::cleanup() { TRACE("model_bug", model_v2_pp(tout, *this);); func_decl_set found_aux_fs; + expr_ref_vector trail(m); for (auto const& kv : m_finterp) { TRACE("model_bug", tout << kv.m_key->get_name() << "\n";); func_interp * fi = kv.m_value; - cleanup_func_interp(fi, found_aux_fs); + cleanup_func_interp(trail, fi, found_aux_fs); } - + for (unsigned i = 0; i < m_const_decls.size(); ++i) { + func_decl* d = m_const_decls[i]; + expr* e = m_interp[d]; + expr* r = cleanup_expr(trail, e, found_aux_fs); + if (e != r) { + register_decl(d, r); + } + } + // TRACE("model_bug", model_v2_pp(tout, *this);); // remove auxiliary declarations that are not used. if (found_aux_fs.size() != m_aux_decls.size()) { remove_aux_decls_not_in_set(m_decls, found_aux_fs); @@ -224,12 +234,13 @@ void proto_model::cleanup() { for (func_decl* faux : m_aux_decls) { if (!found_aux_fs.contains(faux)) { - TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";); + TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << " " << faux->get_ref_count() << "\n";); unregister_decl(faux); } } m_aux_decls.swap(found_aux_fs); } + TRACE("model_bug", model_v2_pp(tout, *this);); } value_factory * proto_model::get_factory(family_id fid) { diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index 587ddc510..ee8fc7adf 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -55,8 +55,8 @@ class proto_model : public model_core { // Invariant: m_const_decls subset m_decls void remove_aux_decls_not_in_set(ptr_vector & decls, func_decl_set const & s); - void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs); - + void cleanup_func_interp(expr_ref_vector& trail, func_interp * fi, func_decl_set & found_aux_fs); + expr* cleanup_expr(expr_ref_vector& trail, expr* fi_else, func_decl_set& found_aux_fs); public: proto_model(ast_manager & m, params_ref const & p = params_ref());