From 3b5ae285d908471fede2fc540537130a9df9ecb4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Jan 2023 23:28:36 -0800
Subject: [PATCH] add outline for interval reasoning

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_project.py                    |  2 +-
 src/ast/simplifiers/CMakeLists.txt       |  5 ++-
 src/ast/simplifiers/bound_simplifier.cpp | 55 ++++++++++++++++++++++++
 src/ast/simplifiers/bound_simplifier.h   | 12 +++++-
 4 files changed, 70 insertions(+), 4 deletions(-)

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 20bce7c13..2e0e4e739 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -39,7 +39,7 @@ def init_project_def():
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('model',  ['macros'])
     add_lib('converters', ['model'], 'ast/converters')
-    add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
+    add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'interval', 'converters', 'substitution'], 'ast/simplifiers')
     add_lib('tactic', ['simplifiers'])
     add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])
diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt
index 74c544ffe..cd1b34f8c 100644
--- a/src/ast/simplifiers/CMakeLists.txt
+++ b/src/ast/simplifiers/CMakeLists.txt
@@ -20,9 +20,10 @@ z3_add_component(simplifiers
     solve_context_eqs.cpp
     solve_eqs.cpp
   COMPONENT_DEPENDENCIES
-    euf
-    rewriter
     bit_blaster
+    euf
+    interval
     normal_forms
+    rewriter
     substitution
 )
diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp
index 085537720..cf39c78de 100644
--- a/src/ast/simplifiers/bound_simplifier.cpp
+++ b/src/ast/simplifiers/bound_simplifier.cpp
@@ -297,6 +297,61 @@ bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) {
     return false;
 }
 
+void bound_simplifier::get_bounds(expr* x, scoped_interval& i) {
+    i.m().reset_upper(i);
+    i.m().reset_lower(i);
+    
+    rational n;
+    if (a.is_numeral(x, n)) {
+        i.m().set(i, n.to_mpq());
+        return;
+    }
+
+    if (is_var(x)) {
+        unsigned v = to_var(x);
+        bool strict;
+        if (bp.has_upper(v)) {
+            mpq const& q = bp.upper(v, strict);
+            i_cfg.set_upper_is_open(i, strict);
+            i_cfg.set_upper(i, q);
+        }
+        if (bp.has_lower(v)) {
+            mpq const& q = bp.lower(v, strict);
+            i_cfg.set_lower_is_open(i, strict);
+            i_cfg.set_lower(i, q);
+        }
+    }
+
+    if (a.is_add(x)) {
+        scoped_interval sum_i(i.m());
+        scoped_interval arg_i(i.m());
+        i.m().set(sum_i, mpq(0));
+        for (expr* arg : *to_app(x)) {
+            get_bounds(arg, arg_i);
+            i.m().add(sum_i, arg_i, sum_i);
+        }
+        // TODO: intersect
+        i.m().set(i, sum_i);
+    }
+
+    if (a.is_mul(x)) {
+        scoped_interval mul_i(i.m());
+        scoped_interval arg_i(i.m());
+        i.m().set(mul_i, mpq(1));
+        for (expr* arg : *to_app(x)) {
+            get_bounds(arg, arg_i);
+            i.m().add(mul_i, arg_i, mul_i);
+        }
+        // TODO: intersect
+        i.m().set(i, mul_i);
+    }
+
+    // etc:
+    // import interval from special case code for lower and upper.
+
+    
+    
+}
 
 void bound_simplifier::reset() {
     bp.reset();
diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h
index 826800c51..c7739715e 100644
--- a/src/ast/simplifiers/bound_simplifier.h
+++ b/src/ast/simplifiers/bound_simplifier.h
@@ -23,14 +23,21 @@ Description:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/simplifiers/dependent_expr_state.h"
 #include "ast/simplifiers/bound_propagator.h"
+#include "math/interval/interval.h"
 
 
 class bound_simplifier : public dependent_expr_simplifier {
+    typedef interval_manager<im_default_config> interval_manager;
+    typedef interval_manager::interval interval;
+    typedef _scoped_interval<interval_manager> scoped_interval;
+
     arith_util              a;
     th_rewriter             m_rewriter;
     unsynch_mpq_manager     nm;
     small_object_allocator  m_alloc;
     bound_propagator        bp;
+    im_default_config       i_cfg;
+    interval_manager        i_manager;
     unsigned                m_num_vars = 0;
     ptr_vector<expr>        m_var2expr;
     unsigned_vector         m_expr2var;
@@ -68,6 +75,7 @@ class bound_simplifier : public dependent_expr_simplifier {
 
     bool has_upper(expr* x, rational& n, bool& strict);
     bool has_lower(expr* x, rational& n, bool& strict);
+    void get_bounds(expr* x, scoped_interval&);
 
     // e = x + offset
     bool is_offset(expr* e, expr* x, rational& offset);
@@ -78,7 +86,9 @@ public:
         dependent_expr_simplifier(m, fmls),
         a(m),
         m_rewriter(m),
-        bp(nm, m_alloc, p) {
+        bp(nm, m_alloc, p),
+        i_cfg(nm),
+        i_manager(m.limit(), im_default_config(nm)) {
     }
 
     char const* name() const override { return "bounds-simplifier"; }