build fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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");
             }

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(range, m),
-            m_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<accessor> const& accessors() const { return m_accessors; }
         vector<accessor>::const_iterator begin() const { return m_accessors.begin(); }
         vector<accessor>::const_iterator end() const { return m_accessors.end(); }
+        vector<accessor>::iterator begin() { return m_accessors.begin(); }
+        vector<accessor>::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<constructor> const& constructors() const { return m_constructors; }
         vector<constructor>::const_iterator begin() const { return m_constructors.begin(); }
         vector<constructor>::const_iterator end() const { return m_constructors.end(); }
+        vector<constructor>::iterator begin() { return m_constructors.begin(); }
+        vector<constructor>::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; }

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;

src/ast/rewriter/arith_rewriter.h

@@ -49,6 +49,7 @@ public:
 
 class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     bool m_arith_lhs;
+    bool m_arith_ineq_lhs;
     bool m_gcd_rounding;
     bool m_elim_to_real;
     bool m_push_to_real;

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"),

src/smt/asserted_formulas.cpp

@@ -120,7 +120,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
 void asserted_formulas::set_eliminate_and(bool flag) {
     params_ref p;
     p.set_bool("elim_and", flag);
-//    p.set_bool("arith_lhs", true);
+    p.set_bool("arith_ineq_lhs", true);
     p.set_bool("sort_sums", true);
     p.set_bool("rewrite_patterns", true);
     p.set_bool("expand_eqs", m_params.m_arith_expand_eqs);