diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp index 44102156d..8969e02a9 100644 --- a/src/ast/datatype_decl_plugin2.cpp +++ b/src/ast/datatype_decl_plugin2.cpp @@ -24,6 +24,12 @@ Revision History: namespace datatype { + void accessor::fix_range(sort_ref_vector const& dts) { + if (!m_range) { + m_range = dts[m_index]; + } + } + func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const { unsigned n = ps.size(); SASSERT(n == get_def().params().size()); @@ -285,6 +291,14 @@ namespace datatype { sort_ref_vector ps(m); sorts.push_back(d.instantiate(ps)); } + for (symbol const& s : m_def_block) { + def& d = *m_defs[s]; + for (constructor& c : d) { + for (accessor& a : c) { + // a.fix_range(sorts); + } + } + } if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) { m_manager->raise_exception("datatype is not well-founded"); } diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h index a4a76f346..13e85b47f 100644 --- a/src/ast/datatype_decl_plugin2.h +++ b/src/ast/datatype_decl_plugin2.h @@ -46,17 +46,24 @@ namespace datatype { class accessor { ast_manager& m; symbol m_name; - sort_ref m_domain; sort_ref m_range; + unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed. constructor* m_constructor; public: - accessor(ast_manager& m, symbol const& n): + accessor(ast_manager& m, symbol const& n, sort* range): m(m), m_name(n), - m_domain(m), - m_range(m) + m_range(range, m), + m_index(UINT_MAX) + {} + accessor(ast_manager& m, symbol const& n, unsigned index): + m(m), + m_name(n), + m_range(m), + m_index(index) {} sort* range() const { return m_range; } + void fix_range(sort_ref_vector const& dts); symbol const& name() const { return m_name; } func_decl_ref instantiate(sort_ref_vector const& ps) const; func_decl_ref instantiate(sort* dt) const; @@ -78,6 +85,8 @@ namespace datatype { vector const& accessors() const { return m_accessors; } vector::const_iterator begin() const { return m_accessors.begin(); } vector::const_iterator end() const { return m_accessors.end(); } + vector::iterator begin() { return m_accessors.begin(); } + vector::iterator end() { return m_accessors.end(); } func_decl_ref instantiate(sort_ref_vector const& ps) const; func_decl_ref instantiate(sort* dt) const; void attach(def* d) { m_def = d; } @@ -205,6 +214,8 @@ namespace datatype { vector const& constructors() const { return m_constructors; } vector::const_iterator begin() const { return m_constructors.begin(); } vector::const_iterator end() const { return m_constructors.end(); } + vector::iterator begin() { return m_constructors.begin(); } + vector::iterator end() { return m_constructors.end(); } sort_ref_vector const& params() const { return m_params; } util& u() const { return m_util; } param_size::size* sort_size() { return m_sort_size; } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index b630cdff6..8b29004ab 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -25,6 +25,7 @@ Notes: void arith_rewriter::updt_local_params(params_ref const & _p) { arith_rewriter_params p(_p); m_arith_lhs = p.arith_lhs(); + m_arith_ineq_lhs = p.arith_ineq_lhs; m_gcd_rounding = p.gcd_rounding(); m_elim_to_real = p.elim_to_real(); m_push_to_real = p.push_to_real(); @@ -370,7 +371,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) || (is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ))) return reduce_power(arg1, arg2, kind, result); - br_status st = cancel_monomials(arg1, arg2, true, new_arg1, new_arg2); + br_status st = cancel_monomials(arg1, arg2, m_arith_ineq_lhs || m_arith_lhs, new_arg1, new_arg2); TRACE("mk_le_bug", tout << "st: " << st << " " << new_arg1 << " " << new_arg2 << "\n";); if (st != BR_FAILED) { arg1 = new_arg1; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index f1e4c4396..af9d0e09d 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -49,6 +49,7 @@ public: class arith_rewriter : public poly_rewriter { bool m_arith_lhs; + bool m_arith_ineq_lhs; bool m_gcd_rounding; bool m_elim_to_real; bool m_push_to_real; diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/ast/rewriter/arith_rewriter_params.pyg index 9a6c6c1c0..d40f46917 100644 --- a/src/ast/rewriter/arith_rewriter_params.pyg +++ b/src/ast/rewriter/arith_rewriter_params.pyg @@ -9,6 +9,7 @@ def_module_params(module_name='rewriter', ("sort_sums", BOOL, False, "sort the arguments of + application."), ("gcd_rounding", BOOL, False, "use gcd rounding on integer arithmetic atoms."), ("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."), + ("arith_ineq_lhs", BOOL, False, "rewrite inequalities so that right-hand-side is a constant."), ("elim_to_real", BOOL, False, "eliminate to_real from arithmetic predicates that contain only integers."), ("push_to_real", BOOL, True, "distribute to_real over * and +."), ("expand_eqs", BOOL, False, "expand equalities into two inequalities"), diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 7dca13c07..f37cabde8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -120,7 +120,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector