move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532

src/ast/rewriter/arith_rewriter.cpp

@@ -23,9 +23,8 @@ Notes:
 #include "ast/ast_pp.h"
 
 seq_util& arith_rewriter_core::seq() {
-    if (!m_seq) {
-        m_seq = alloc(seq_util, m);
-    }
+    if (!m_seq) 
+        m_seq = alloc(seq_util, m);    
     return *m_seq;
 }
 

src/ast/simplifiers/CMakeLists.txt

@@ -1,6 +1,7 @@
 z3_add_component(simplifiers
   SOURCES
     bit_blaster.cpp
+    bound_manager.cpp
     bv_slice.cpp
     card2bv.cpp
     demodulator_simplifier.cpp

src/ast/simplifiers/bound_manager.cpp

@@ -0,0 +1,288 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bound_manager.cpp
+
+Abstract:
+
+    Collect bounds.
+
+Author:
+
+    Leonardo (leonardo) 2011-05-16
+
+Notes:
+
+--*/
+
+#include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_translation.h"
+#include "ast/simplifiers/bound_manager.h"
+
+bound_manager::bound_manager(ast_manager & m):
+    m_util(m),
+    m_bounded_vars(m) {
+}
+
+bound_manager::~bound_manager() {
+    reset();
+}
+
+bound_manager* bound_manager::translate(ast_manager& dst_m) {
+    bound_manager* result = alloc(bound_manager, dst_m);
+    ast_translation tr(m(), dst_m);
+    expr_dependency_translation edtr(tr);
+    for (auto& kv : m_lowers) result->m_lowers.insert(tr(kv.m_key), kv.m_value);
+    for (auto& kv : m_uppers) result->m_uppers.insert(tr(kv.m_key), kv.m_value);
+    for (auto& kv : m_lower_deps) result->m_lower_deps.insert(tr(kv.m_key), edtr(kv.m_value));
+    for (auto& kv : m_upper_deps) result->m_upper_deps.insert(tr(kv.m_key), edtr(kv.m_value));
+    for (expr* e : m_bounded_vars) result->m_bounded_vars.push_back(tr(e));
+    return result;
+}
+
+
+static decl_kind swap_decl(decl_kind k) {
+    switch (k) {
+    case OP_LE: return OP_GE;
+    case OP_LT: return OP_GT;
+    case OP_GE: return OP_LE;
+    case OP_GT: return OP_LT;
+    default:
+        UNREACHABLE();
+        return k;
+    }
+}
+
+decl_kind bound_manager::neg(decl_kind k) {
+    switch (k) {
+    case OP_LE: return OP_GT;
+    case OP_LT: return OP_GE;
+    case OP_GE: return OP_LT;
+    case OP_GT: return OP_LE;
+    default:
+        UNREACHABLE();
+        return k;
+    }
+}
+
+void bound_manager::norm(numeral & n, decl_kind & k) {
+    switch (k) {
+    case OP_LE: return;
+    case OP_GE: return;
+    case OP_LT: 
+        // x < n --> x <= n-1
+        n--;
+        k = OP_LE;
+        return;
+    case OP_GT:
+        // x > n --> x >= n+1
+        n++;
+        k = OP_GE;
+        return;
+    default:
+        return;
+    }
+}
+
+static bool is_lower(decl_kind k) {
+    return k == OP_GT || k == OP_GE;
+}
+
+static bool is_strict(decl_kind k) {
+    return k == OP_LT || k == OP_GT;
+} 
+
+bool bound_manager::is_numeral(expr* v, numeral& n, bool& is_int) {
+    expr* w;
+    if (m_util.is_uminus(v, w) && is_numeral(w, n, is_int)) {
+        n.neg();
+        return true;
+    }
+    return m_util.is_numeral(v, n, is_int);
+}
+
+void bound_manager::operator()(expr * f, expr_dependency * d, proof* p) {
+    if (p)
+        return;
+    TRACE("bound_manager", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
+    expr * v;
+    numeral n;
+    if (is_disjunctive_bound(f, d))
+        return;
+    if (is_equality_bound(f, d))
+        return;
+    bool pos = true;    
+    while (m().is_not(f, f))
+        pos = !pos;
+    if (!is_app(f))
+        return;
+    app * t = to_app(f);
+    if (t->get_family_id() != m_util.get_family_id())
+        return;
+    decl_kind k = t->get_decl_kind();
+    if (k != OP_LE && k != OP_GE && k != OP_LT && k != OP_GT)
+        return;
+    expr * lhs = t->get_arg(0);
+    expr * rhs = t->get_arg(1);
+    bool is_int;
+    if (is_uninterp_const(lhs) && is_numeral(rhs, n, is_int)) {
+        v = lhs;
+    }
+    else if (is_uninterp_const(rhs) && is_numeral(lhs, n, is_int)) {
+        v = rhs;
+        k = swap_decl(k);
+    }
+    else {
+        return;
+    }
+    if (!pos)
+        k = neg(k);
+    if (is_int)
+        norm(n, k);
+    TRACE("bound_manager", tout << "found bound for:\n" << mk_ismt2_pp(v, m()) << "\n";);
+    bool strict = is_strict(k);
+    if (is_lower(k)) {
+        insert_lower(v, strict, n, d);
+    }
+    else {
+        insert_upper(v, strict, n, d);
+    }
+}
+
+void bound_manager::insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d) {
+    limit old;
+    if (m_uppers.find(v, old)) {
+        if (n < old.first || (n == old.first && strict && !old.second)) {
+            // improved bound
+            m_uppers.insert(v, limit(n, strict));
+            if (d)
+                m_upper_deps.insert(v, d);
+        }
+    }
+    else {
+        m_uppers.insert(v, limit(n, strict));
+        if (d)
+            m_upper_deps.insert(v, d);
+        if (!m_lowers.contains(v)) {
+            m_bounded_vars.push_back(v);
+        }
+    }
+}
+
+void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d) {
+    limit old;
+    if (m_lowers.find(v, old)) {
+        if (n > old.first || (n == old.first && strict && !old.second)) {
+            // improved bound
+            m_lowers.insert(v, limit(n, strict));
+            if (d)
+                m_lower_deps.insert(v, d);
+        }
+    }
+    else {
+        m_lowers.insert(v, limit(n, strict));
+        if (d)
+            m_lower_deps.insert(v, d);
+        if (!m_uppers.contains(v)) {
+            m_bounded_vars.push_back(v);
+        }
+    }
+}
+
+bool bound_manager::is_equality_bound(expr * f, expr_dependency * d) {
+    expr* x, *y;
+    if (!m().is_eq(f, x, y)) {
+        return false;
+    }
+    if (!is_uninterp_const(x)) {
+        std::swap(x, y);
+    }
+    numeral n;
+    bool is_int;
+    if (is_uninterp_const(x) && is_numeral(y, n, is_int)) {
+        insert_lower(x, false, n, d);
+        insert_upper(x, false, n, d);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
+    numeral lo, hi, n;
+    if (!m().is_or(f)) return false;
+    unsigned sz = to_app(f)->get_num_args();
+    if (sz == 0) return false;
+    expr * x, * y, * v = nullptr;
+    bool is_int;
+    for (unsigned i = 0; i < sz; ++i) {
+        expr * e = to_app(f)->get_arg(i);
+        if (!m().is_eq(e, x, y)) return false;
+        if (is_uninterp_const(x) && 
+            is_numeral(y, n, is_int) && is_int && 
+            (x == v || v == nullptr)) {
+            if (v == nullptr) { v = x; lo = hi = n; }
+            if (n < lo) lo = n;
+            if (n > hi) hi = n;
+        }
+        else if (is_uninterp_const(y) && 
+                 is_numeral(x, n, is_int) && is_int && 
+                 (y == v || v == nullptr)) {
+            if (v == nullptr) { v = y; lo = hi = n; }
+            if (n < lo) lo = n;
+            if (n > hi) hi = n;
+        }
+        else {
+            return false;
+        }
+    }
+    TRACE("bound_manager", tout << "bounds: " << lo << " " << hi << "\n";);
+    insert_lower(v, false, lo, d);
+    insert_upper(v, false, hi, d);
+    return true;
+}
+
+void bound_manager::reset() {
+    m_bounded_vars.finalize();
+    m_lowers.finalize();
+    m_uppers.finalize();
+    m_lower_deps.finalize();
+    m_upper_deps.finalize();
+}
+
+bool bound_manager::inconsistent() const {
+    for (auto const& [k,v] : m_lowers) {
+        limit const& lim1 = v;
+        limit lim2;        
+        if (m_uppers.find(k, lim2)) {
+            if (lim1.first > lim2.first)
+                return true;            
+            if (lim1.first == lim2.first &&
+                !lim1.second && lim2.second) {
+                return true;
+            }
+        }
+    }
+    return false;
+}
+
+void bound_manager::display(std::ostream & out) const {
+    numeral n; bool strict;
+    for (iterator it = begin(); it != end(); ++it) {
+        expr * v = *it;
+        if (has_lower(v, n, strict))
+            out << n << " " << (strict ? "<" : "<=");
+        else
+            out << "-oo <";
+        out << " " << mk_ismt2_pp(v, m()) << " ";
+        if (has_upper(v, n, strict))
+            out << (strict ? "<" : "<=") << " " << n;
+        else
+            out << "< oo";
+        out << "\n";
+    }
+}

src/ast/simplifiers/bound_manager.h

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bound_manager.h
+
+Abstract:
+
+    Collect bounds.
+
+Author:
+
+    Leonardo (leonardo) 2011-05-16
+
+Notes:
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+#include "ast/arith_decl_plugin.h"
+
+
+class bound_manager {
+public:
+    typedef rational     numeral;
+private:
+    typedef std::pair<numeral, bool> limit;
+    arith_util           m_util;
+    obj_map<expr, limit> m_lowers;
+    obj_map<expr, limit> m_uppers;
+    obj_map<expr, expr_dependency*> m_lower_deps;
+    obj_map<expr, expr_dependency*> m_upper_deps;
+    expr_ref_vector     m_bounded_vars;
+    bool is_disjunctive_bound(expr * f, expr_dependency * d);
+    bool is_equality_bound(expr * f, expr_dependency * d);
+    bool is_numeral(expr* v, rational& n, bool& is_int);
+    void insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d);
+    void insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d);
+public:
+    static decl_kind neg(decl_kind k);
+    static void norm(numeral & n, decl_kind & k);
+
+    bound_manager(ast_manager & m);
+    ~bound_manager();
+    
+    bound_manager* translate(ast_manager& dst_m);
+
+    ast_manager & m() const { return m_util.get_manager(); }
+    
+    void operator()(expr * n, expr_dependency * d, proof* p);
+    
+    bool has_lower(expr * c, numeral & v, bool & strict) const {
+        limit l;
+        if (m_lowers.find(c, l)) {
+            v = l.first;
+            strict = l.second;
+            return true;
+        }
+        return false;
+    }
+
+    bool has_upper(expr * c, numeral & v, bool & strict) const {
+        limit l;
+        if (m_uppers.find(c, l)) {
+            v = l.first;
+            strict = l.second;
+            return true;
+        }
+        return false;
+    }
+
+    expr_dependency * lower_dep(expr * c) const {
+        expr_dependency * d;
+        if (m_lower_deps.find(c, d))
+            return d;
+        return nullptr;
+    }
+
+    expr_dependency * upper_dep(expr * c) const {
+        expr_dependency * d;
+        if (m_upper_deps.find(c, d))
+            return d;
+        return nullptr;
+    }
+
+    bool inconsistent() const;
+    
+    bool has_lower(expr * c) const {
+        return m_lowers.contains(c);
+    }
+
+    bool has_upper(expr * c) const {
+        return m_uppers.contains(c);
+    }
+    
+    typedef ptr_vector<expr>::const_iterator iterator;
+    
+    /**
+       \brief Iterator for all bounded constants.
+    */
+    iterator begin() const { return m_bounded_vars.begin(); }
+    iterator end() const { return m_bounded_vars.end(); }
+    
+    void reset();
+
+    // for debugging purposes
+    void display(std::ostream & out) const;
+};
+

src/ast/simplifiers/extract_eqs.cpp

@@ -21,6 +21,7 @@ Author:
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/simplifiers/extract_eqs.h"
+#include "ast/simplifiers/bound_manager.h"
 #include "params/tactic_params.hpp"
 
 
@@ -83,6 +84,7 @@ namespace euf {
     class arith_extract_eq : public extract_eq {
         ast_manager&       m;
         arith_util         a;
+        bound_manager      m_bm;
         expr_ref_vector    m_args, m_trail;
         expr_sparse_mark   m_nonzero;
         bool               m_enabled = true;
@@ -107,6 +109,17 @@ namespace euf {
                 solve_eq(orig, u, term, d, eqs);
         }
 
+        void solve_to_real(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            expr* z, *u;
+            rational r;            
+            if (!a.is_to_real(x, z) || !is_uninterp_const(z))
+                return;
+            if (a.is_to_real(y, u)) 
+                eqs.push_back(dependent_eq(orig, to_app(z), expr_ref(u, m), d));
+            else if (a.is_numeral(y, r) && r.is_int())
+                eqs.push_back(dependent_eq(orig, to_app(z), expr_ref(a.mk_int(r), m), d));
+        }
+
         /***
         * Solve
         *    x + Y = Z    -> x = Z - Y
@@ -157,8 +170,8 @@ namespace euf {
                         for (expr* yarg : *to_app(arg)) {
                             ++k;
                             nonzero = k == j || m_nonzero.is_marked(yarg) || (a.is_numeral(yarg, r) && r != 0);                           
-                            if (!nonzero)
-                                break;
+if (!nonzero)
+break;
                         }
                         if (!nonzero)
                             continue;
@@ -222,12 +235,12 @@ namespace euf {
         }
 
         void add_pos(expr* f) {
-            expr* lhs = nullptr, *rhs = nullptr;
+            expr* lhs = nullptr, * rhs = nullptr;
             rational val;
-            if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_neg()) 
-                mark_nonzero(lhs);            
+            if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_neg())
+                mark_nonzero(lhs);
             else if (a.is_ge(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_pos())
-                mark_nonzero(lhs);            
+                mark_nonzero(lhs);
             else if (m.is_not(f, f)) {
                 if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && !val.is_neg())
                     mark_nonzero(lhs);
@@ -242,11 +255,12 @@ namespace euf {
             solve_add(orig, x, y, d, eqs);
             solve_mod(orig, x, y, d, eqs);
             solve_mul(orig, x, y, d, eqs);
+            solve_to_real(orig, x, y, d, eqs);
         }
 
     public:
 
-        arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m), m_trail(m) {}
+        arith_extract_eq(ast_manager& m) : m(m), a(m), m_bm(m), m_args(m), m_trail(m) {}
 
         void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
             if (!m_enabled)
@@ -257,6 +271,18 @@ namespace euf {
                 solve_eq(f, x, y, d, eqs);
                 solve_eq(f, y, x, d, eqs);
             }
+            bool str;
+            rational lo, hi;
+            if (a.is_le(f, x, y) && a.is_numeral(y, hi) && m_bm.has_lower(x, lo, str) && !str && lo == hi) {
+                expr_dependency_ref d2(m);
+                d2 = m.mk_join(d, m_bm.lower_dep(x));
+                if (is_uninterp_const(x)) 
+                    eqs.push_back(dependent_eq(f, to_app(x), expr_ref(y, m), d2));
+                else {
+                    solve_eq(f, x, y, d2, eqs);                
+                    solve_eq(f, y, x, d2, eqs);                
+                }
+            }
         }
 
         void pre_process(dependent_expr_state& fmls) override {
@@ -264,8 +290,13 @@ namespace euf {
                 return;
             m_nonzero.reset();
             m_trail.reset();
-            for (unsigned i = 0; i < fmls.qtail(); ++i) 
-                add_pos(fmls[i].fml());            
+            m_bm.reset();
+            for (unsigned i = 0; i < fmls.qtail(); ++i) {
+                auto [f, p, d] = fmls[i]();
+                add_pos(f);
+                m_bm(f, d, p);
+            }
+
         }