abstract arithmetic value extraction

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

src/smt/CMakeLists.txt

@@ -13,6 +13,7 @@ z3_add_component(smt
     old_interval.cpp
     qi_queue.cpp
     smt_almost_cg_table.cpp
+    smt_arith_value.cpp
     smt_case_split_queue.cpp
     smt_cg_table.cpp
     smt_checker.cpp

src/smt/smt_arith_value.cpp

@@ -0,0 +1,113 @@
+
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    smt_arith_value.cpp
+
+Abstract:
+
+    Utility to extract arithmetic values from context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-12-08.
+
+Revision History:
+
+--*/
+#pragma once;
+
+#include "smt/smt_arith_value.h"
+#include "smt/theory_lra.h"
+#include "smt/theory_arith.h"
+
+namespace smt {
+
+    arith_value::arith_value(context& ctx): 
+        m_ctx(ctx), m(ctx.get_manager()), a(m) {}
+
+    bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) {
+        if (!m_ctx.e_internalized(e)) return false;
+        expr_ref _lo(m);
+        family_id afid = a.get_family_id();
+        is_strict = false;
+        enode* next = m_ctx.get_enode(e), *n = next;
+        bool found = false;
+        bool is_strict1; 
+        rational lo1;
+        theory* th = m_ctx.get_theory(afid);
+        theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
+        theory_i_arith*  thi = dynamic_cast<theory_i_arith*>(th);
+        theory_lra*      thr = dynamic_cast<theory_lra*>(th);
+        do {
+            if (tha && tha->get_lower(next, _lo) && a.is_numeral(_lo, lo1)) {
+                if (!found || lo1 > lo) lo = lo1;
+                found = true;
+            }
+            else if (thi && thi->get_lower(next, _lo) && a.is_numeral(_lo, lo1)) {
+                if (!found || lo1 > lo) lo = lo1;
+                found = true;
+            }
+            else if (thr && thr->get_lower(next, lo1, is_strict1)) {
+                if (!found || lo1 > lo || (lo == lo1 && is_strict1)) lo = lo1, is_strict = is_strict1;
+                found = true;
+            }
+            next = next->get_next();
+        }
+        while (n != next);
+        return found;
+    }
+
+    bool arith_value::get_up(expr* e, rational& up, bool& is_strict) {
+        if (!m_ctx.e_internalized(e)) return false;
+        expr_ref _up(m);
+        family_id afid = a.get_family_id();
+        is_strict = false;
+        enode* next = m_ctx.get_enode(e), *n = next;
+        bool found = false, is_strict1;
+        rational up1;
+        theory* th = m_ctx.get_theory(afid);
+        theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
+        theory_i_arith*  thi = dynamic_cast<theory_i_arith*>(th);
+        theory_lra*      thr = dynamic_cast<theory_lra*>(th);
+        do {
+            if (tha && tha->get_upper(next, _up) && a.is_numeral(_up, up1)) {
+                if (!found || up1 < up) up = up1;
+                found = true;
+            }
+            else if (thi && thi->get_upper(next, _up) && a.is_numeral(_up, up1)) {
+                if (!found || up1 < up) up = up1;
+                found = true;
+            }
+            else if (thr && thr->get_upper(next, up1, is_strict1)) {
+                if (!found || up1 < up || (up1 == up && is_strict1)) up = up1, is_strict = is_strict1;
+                found = true;
+            }
+            next = next->get_next();
+        }
+        while (n != next);
+        return found;
+    }
+
+    bool arith_value::get_value(expr* e, rational& val) {
+        if (!m_ctx.e_internalized(e)) return false;
+        expr_ref _val(m);
+        enode* next = m_ctx.get_enode(e), *n = next;
+        family_id afid = a.get_family_id();
+        theory* th = m_ctx.get_theory(afid);
+        theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
+        theory_i_arith* thi = dynamic_cast<theory_i_arith*>(th);
+        theory_lra* thr = dynamic_cast<theory_lra*>(th);           
+        do { 
+            e = next->get_owner();
+            if (tha && tha->get_value(next, _val) && a.is_numeral(_val, val)) return true;
+            if (thi && thi->get_value(next, _val) && a.is_numeral(_val, val)) return true;
+            if (thr && thr->get_value(next, val)) return true;
+            next = next->get_next();
+        }
+        while (next != n);
+        return false;
+    }
+};

src/smt/smt_arith_value.h

@@ -0,0 +1,37 @@
+
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    smt_arith_value.h
+
+Abstract:
+
+    Utility to extract arithmetic values from context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-12-08.
+
+Revision History:
+
+--*/
+#pragma once;
+
+#include "ast/arith_decl_plugin.h"
+#include "smt/smt_context.h"
+
+
+namespace smt {
+    class arith_value {
+        context& m_ctx;        
+        ast_manager& m;
+        arith_util a;
+    public:
+        arith_value(context& ctx);
+        bool get_lo(expr* e, rational& lo, bool& strict);
+        bool get_up(expr* e, rational& up, bool& strict);
+        bool get_value(expr* e, rational& value);
+    };
+};

src/smt/smt_context.h

@@ -1243,6 +1243,11 @@ namespace smt {
     public:
         bool can_propagate() const;
 
+        // Retrieve arithmetic values. 
+        bool get_arith_lo(expr* e, rational& lo, bool& strict);
+        bool get_arith_up(expr* e, rational& up, bool& strict);
+        bool get_arith_value(expr* e, rational& value);
+
         // -----------------------------------
         //
         // Model checking... (must be improved)

src/smt/theory_jobscheduler.cpp

@@ -14,10 +14,39 @@ Author:
 
 Revision History:
 
+TODO:
+
+- arithmetic interface
+
+- propagation queue:
+  - register theory variables for catching when jobs are bound to resources
+  - register bounds on start times to propagate energy constraints
+  - more general registration mechanism for arithmetic theory.
+- csp_cmds
+  - use predicates for add_ feature set? Closed world.
+    set up environment in one swoop.
+  - interact with opt
+- jobs without resources
+  - complain or add dummy resource? At which level.
+
+Features:
+- properties
+- priority
+  - try mss based from outside
+- job-goal
+   - try optimization based on arithmetic solver.
+   - earliest start, latest start
+- constraint level
+- resource groups
+  - resource groups like a resource
+  - resources bound to resource groups within time intervals
+  - job can require to use K resources from a resource group simultaneously.
+
 --*/
 
 #include "smt/theory_jobscheduler.h"
 #include "smt/smt_context.h"
+#include "smt/smt_arith_value.h"
 
 namespace smt {
 
@@ -79,16 +108,18 @@ namespace smt {
 
     final_check_status theory_jobscheduler::final_check_eh() {
 
-        // ensure that each job starts within an avaialable interval.
-        // ! (end_previous_interval < start(j) < start_of_next_interval)
-
         bool blocked = false;
         for (unsigned r = 0; r < m_resources.size(); ++r) {
             if (constrain_resource_energy(r)) {
                 blocked = true;
             }
         }
-
+        for (unsigned j = 0; j < m_jobs.size(); ++j) {
+            if (constrain_end_time_interval(j, resource(j))) {
+                blocked = true;
+            }
+        }
+        
         if (blocked) return FC_CONTINUE;
         return FC_DONE;
     }
@@ -204,9 +235,56 @@ namespace smt {
      * 
      *  r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0
      */
-    void theory_jobscheduler::propagate_end_time_interval(unsigned j, unsigned r) {
+    bool theory_jobscheduler::constrain_end_time_interval(unsigned j, unsigned r) {
-        // TBD
+        unsigned idx1 = 0, idx2 = 0;
-        // establish maximal intervals around start, such that end time is a linear function of start.
+        time_t s = start(j);
+        if (!resource_available(r, s, idx1)) return false;
+        vector<res_available>& available = m_resources[r].m_available;
+        time_t e = ect(j, r, s);
+        if (!resource_available(r, e, idx2)) return false;
+        time_t start1 = available[idx1].m_start;
+        time_t end1   = available[idx1].m_end;
+        unsigned cap1 = available[idx1].m_loadpct;
+        time_t start2 = available[idx2].m_start;
+        time_t end2   = available[idx2].m_end;
+        unsigned cap2 = available[idx2].m_loadpct;
+        // calculate minimal start1 <= t0 <= s,    such that ect(j, r, t0) >= start2 
+        // calculate maximal s      <= t1 <= end1, such that ect(j, r, t1) <= end2
+        time_t delta1 = (s - start1)*cap1;
+        time_t delta2 = (e - start2)*cap2;
+        time_t t0, t1;
+        if (delta1 <= delta2) {
+            t0 = start1;
+        }
+        else {
+            // solve for t0:
+            // (s - t0)*cap1 = (e - start2)*cap2;
+            t0 = s - (delta2 / cap1); 
+        }
+        delta1 = (end1 - s)*cap1;
+        delta2 = (end2 - e)*cap2;
+        if (delta1 <= delta2) {
+            t1 = end1;
+        }
+        else {
+            // solve for t1:
+            // (t1 - s)*cap1 = (end2 - e)*cap2
+            t1 = s + (delta2 / cap1);
+        }
+
+        time_t delta = ect(j, r, t0) - t0;
+        if (end(j) == start(j) + delta) {
+            return false;
+        }
+        literal_vector lits;
+        lits.push_back(~mk_eq(u.mk_job2resource(j), u.mk_resource(r), false));
+        lits.push_back(~mk_ge_lit(u.mk_start(j), t0));
+        lits.push_back(~mk_le_lit(u.mk_start(j), t1));        
+        expr_ref rhs(a.mk_add(u.mk_start(j), a.mk_int(rational(delta, rational::ui64()))), m);
+        lits.push_back(mk_eq(u.mk_end(j), rhs, false));
+        context& ctx = get_context();
+        ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr);
+        return true;
     }
 
     void theory_jobscheduler::propagate_resource_energy(unsigned r) {
@@ -268,8 +346,10 @@ namespace smt {
             // m_jobs[j].m_start <= m_jobs[max_j].m_start;
             // m_jobs[max_j].m_start <= m_jobs[j].m_end;
             lits.push_back(~mk_eq(u.mk_job2resource(j), u.mk_resource(r), false));
-            lits.push_back(~mk_le(m_jobs[j].m_start, m_jobs[max_j].m_start));
+            if (j != max_j) {
-            lits.push_back(~mk_le(m_jobs[max_j].m_start, m_jobs[max_j].m_end));
+                lits.push_back(~mk_le(m_jobs[j].m_start, m_jobs[max_j].m_start));
+                lits.push_back(~mk_le(m_jobs[max_j].m_start, m_jobs[j].m_end));
+            }
             if (j == last_job) break;
         }
         context& ctx = get_context();
@@ -281,7 +361,6 @@ namespace smt {
             job_info const& ji = m_jobs[j];
             unsigned r = resource(j);
             propagate_end_time(j, r);
-            propagate_end_time_interval(j, r);
         }
         for (unsigned r = 0; r < m_resources.size(); ++r) {
             // TBD: check energy constraints on resources.
@@ -345,13 +424,23 @@ namespace smt {
     }
 
     time_t theory_jobscheduler::est(unsigned j) {
-        NOT_IMPLEMENTED_YET();
+        arith_value av(get_context());
+        rational val;
+        bool is_strict;
+        if (av.get_lo(u.mk_start(j), val, is_strict) && !is_strict && val.is_uint64()) {
+            return val.get_uint64();
+        }
         return 0;
     }
 
     time_t theory_jobscheduler::lst(unsigned j) {
-        NOT_IMPLEMENTED_YET();
+        arith_value av(get_context());
-        return 0;
+        rational val;
+        bool is_strict;
+        if (av.get_up(u.mk_start(j), val, is_strict) && !is_strict && val.is_uint64()) {
+            return val.get_uint64();
+        }
+        return std::numeric_limits<time_t>::max();
     }
 
     time_t theory_jobscheduler::ect(unsigned j) {
@@ -379,9 +468,15 @@ namespace smt {
         return 0;
     }
 
+    void theory_jobscheduler::set_preemptable(unsigned j, bool is_preemptable) {
+        m_jobs.reserve(j + 1);
+        m_jobs[j].m_is_preemptable = is_preemptable;        
+    }
 
-    void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end) {
+    void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end, properties const& ps) {
         SASSERT(get_context().at_base_level());
+        SASSERT(1 <= loadpct && loadpct <= 100);
+        SASSERT(0 < cap);
         m_jobs.reserve(j + 1);
         m_resources.reserve(r + 1);
         job_info& ji = m_jobs[j];
@@ -389,16 +484,17 @@ namespace smt {
             throw default_exception("resource already bound to job");
         }
         ji.m_resource2index.insert(r, ji.m_resources.size());
-        ji.m_resources.push_back(job_resource(r, cap, loadpct, end));
+        ji.m_resources.push_back(job_resource(r, cap, loadpct, end, ps));
         SASSERT(!m_resources[r].m_jobs.contains(j));
         m_resources[r].m_jobs.push_back(j);
     }
 
-    void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end) {
+    void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps) {
         SASSERT(get_context().at_base_level());
+        SASSERT(1 <= max_loadpct && max_loadpct <= 100);
         SASSERT(start <= end);
         m_resources.reserve(r + 1);
-        m_resources[r].m_available.push_back(res_available(max_loadpct, start, end));
+        m_resources[r].m_available.push_back(res_available(max_loadpct, start, end, ps));
     }
 
     /*
@@ -411,7 +507,18 @@ namespace smt {
      * Ensure that the availability slots for each resource is sorted by time.
      */
     void theory_jobscheduler::add_done() {
-        context & ctx = get_context();        
+        context & ctx = get_context();
+        
+        // sort availability intervals
+        for (unsigned r = 0; r < m_resources.size(); ++r) {
+            res_info& ri = m_resources[r];
+            vector<res_available>& available = ri.m_available;
+            res_available::compare cmp;
+            std::sort(available.begin(), available.end(), cmp);
+        }
+
+        expr_ref fml(m);
+
         for (unsigned j = 0; j < m_jobs.size(); ++j) {
             job_info const& ji = m_jobs[j];
             expr_ref_vector disj(m);
@@ -419,38 +526,83 @@ namespace smt {
             if (ji.m_resources.empty()) {
                 throw default_exception("every job should be associated with at least one resource");
             }
-            // resource(j) = r => end(j) <= end(j, r)
+
-            // resource(j) = r => start(j) <= lst(j, r, end(j, r))
+            // start(j) <= end(j)
+            fml = a.mk_le(ji.m_start->get_owner(), ji.m_end->get_owner());
+            ctx.assert_expr(fml);
+
+            time_t start_lb = std::numeric_limits<time_t>::max();
+            time_t end_ub = 0;
             for (job_resource const& jr : ji.m_resources) {
+                // resource(j) = r => end(j) <= end(j, r)
+                // resource(j) = r => start(j) <= lst(j, r, end(j, r))
                 unsigned r = jr.m_resource_id;
                 app_ref res(u.mk_resource(r), m);
                 expr_ref eq(m.mk_eq(job, res), m);
                 expr_ref imp(m.mk_implies(eq, mk_le(ji.m_end, jr.m_end)), m);
                 ctx.assert_expr(imp);
-                imp = m.mk_implies(eq, mk_le(ji.m_start, lst(j, r)));
+                time_t t;
+                if (!lst(j, r, t)) {
+                    imp = m.mk_implies(eq, mk_le(ji.m_start, t));
+                }
+                else {
+                    imp = m.mk_not(eq);
+                }
                 ctx.assert_expr(imp);
                 disj.push_back(eq);
+                res_info const& ri = m_resources[r];
+                start_lb = std::min(start_lb, ri.m_available[0].m_start);
+                end_ub = std::max(end_ub, ri.m_available.back().m_end);
+
             }
             // resource(j) = r1 || ... || resource(j) = r_n
             expr_ref fml = mk_or(disj);
             ctx.assert_expr(fml);
 
-            // start(j) >= 0
+            // start(j) >= start_lb
-            fml = mk_ge(ji.m_start, 0);
+            fml = mk_ge(ji.m_start, start_lb);
             ctx.assert_expr(fml);
 
-            // end(j) <= time_t::max
+            // end(j) <= end_ub
-            // is implied by resource(j) = r => end(j) <= end(j, r)
+            fml = mk_le(ji.m_end, end_ub);
+            ctx.assert_expr(fml);
         }        
         for (unsigned r = 0; r < m_resources.size(); ++r) {
-            vector<res_available>& available = m_resources[r].m_available;
+            res_info& ri = m_resources[r];
-            res_available::compare cmp;
+            vector<res_available>& available = ri.m_available;
-            std::sort(available.begin(), available.end(), cmp);
+            if (available.empty()) continue;
-            for (unsigned i = 0; i < available.size(); ++i) {
+            app_ref res(u.mk_resource(r), m);
-                if (i + 1 < available.size() &&
+            for (unsigned j : ri.m_jobs) {
-                    available[i].m_end > available[i + 1].m_start) {
+                // resource(j) == r => start(j) >= available[0].m_start;
+                app_ref job(u.mk_job(j), m);
+                expr_ref eq(m.mk_eq(job, res), m);
+                expr_ref ge(mk_ge(u.mk_start(j), available[0].m_start), m);
+                expr_ref fml(m.mk_implies(eq, ge), m);
+                ctx.assert_expr(fml);                
+            }
+            for (unsigned i = 0; i + 1 < available.size(); ++i) {
+                if (available[i].m_end > available[i + 1].m_start) {
                     throw default_exception("availability intervals should be disjoint");
                 }
+                for (unsigned j : ri.m_jobs) {
+                    // jobs start within an interval.
+                    // resource(j) == r => start(j) <= available[i].m_end || start(j) >= available[i + 1].m_start;
+                    app_ref job(u.mk_job(j), m);
+                    expr_ref eq(m.mk_eq(job, res), m);
+                    expr_ref ge(mk_ge(u.mk_start(j), available[i + 1].m_start), m);
+                    expr_ref le(mk_le(u.mk_start(j), available[i].m_end), m);
+                    fml = m.mk_implies(eq, m.mk_or(le, ge));
+                    ctx.assert_expr(fml);                
+
+                    // if job is not pre-emptable, start and end have to align within contiguous interval.
+                    // resource(j) == r => end(j) <= available[i].m_end || start(j) >= available[i + 1].m_start
+                    if (!m_jobs[j].m_is_preemptable && available[i].m_end + 1 < available[i+1].m_start) {
+                        le = mk_le(u.mk_end(j), available[i].m_end);
+                        ge = mk_ge(u.mk_start(j), available[i+1].m_start);
+                        fml = m.mk_implies(eq, m.mk_or(le, ge));
+                        ctx.assert_expr(fml);
+                    }
+                }
             }
         }
     }
@@ -473,6 +625,10 @@ namespace smt {
             if (ect(j, r, start(j)) > end(j)) {
                 throw default_exception("job not assigned full capacity");
             }
+            unsigned idx;
+            if (!resource_available(r, start(j), idx)) {
+                throw default_exception("resource is not available at job start time");
+            }
         }
         for (unsigned r = 0; r < m_resources.size(); ++r) {
             // order jobs running on r by start, end-time intervals
@@ -601,7 +757,7 @@ namespace smt {
     /**
      * Compute last start time for job on resource r.
      */
-    time_t theory_jobscheduler::lst(unsigned j, unsigned r) {
+    bool theory_jobscheduler::lst(unsigned j, unsigned r, time_t& start) {
         job_resource const& jr = get_job_resource(j, r);
         vector<res_available>& available = m_resources[r].m_available;
         unsigned j_load_pct = jr.m_loadpct;
@@ -619,10 +775,10 @@ namespace smt {
                 cap -= delta;
             }
             if (cap == 0) {
-                return start;
+                return true;
             }
         }
-        throw default_exception("there is insufficient capacity on the resource to run the job");
+        return false;
     }
     
 };

src/smt/theory_jobscheduler.h

@@ -28,16 +28,20 @@ Revision History:
 namespace smt {
 
     typedef uint64_t time_t;
-
+    
     class theory_jobscheduler : public theory {
+    public:
+        typedef map<symbol, double, symbol_hash_proc, symbol_eq_proc> properties;
+    protected:
 
         struct job_resource {
             unsigned m_resource_id;   // id of resource
             unsigned m_capacity;      // amount of resource to use
             unsigned m_loadpct;       // assuming loadpct
             time_t   m_end;           // must run before
-            job_resource(unsigned r, unsigned cap, unsigned loadpct, time_t end):
+            properties m_properties;
-                m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end) {}
+            job_resource(unsigned r, unsigned cap, unsigned loadpct, time_t end, properties const& ps):
+                m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end), m_properties(ps) {}
         };
 
         struct job_time {
@@ -53,22 +57,25 @@ namespace smt {
         };
 
         struct job_info {
+            bool                 m_is_preemptable; // can job be pre-empted
             vector<job_resource> m_resources; // resources allowed to run job.
             u_map<unsigned>      m_resource2index; // resource to index into vector 
             enode*               m_start;
             enode*               m_end;
             enode*               m_resource;
-            job_info(): m_start(nullptr), m_end(nullptr), m_resource(nullptr) {}
+            job_info(): m_is_preemptable(true), m_start(nullptr), m_end(nullptr), m_resource(nullptr) {}
         };
 
         struct res_available {
-            unsigned m_loadpct;
+            unsigned   m_loadpct;
-            time_t m_start;
+            time_t     m_start;
-            time_t m_end;
+            time_t     m_end;
-            res_available(unsigned load_pct, time_t start, time_t end):
+            properties m_properties;
+            res_available(unsigned load_pct, time_t start, time_t end, properties const& ps):
                 m_loadpct(load_pct),
                 m_start(start),
-                m_end(end)
+                m_end(end),
+                m_properties(ps)
             {}
             struct compare {
                 bool operator()(res_available const& ra1, res_available const& ra2) const {
@@ -135,8 +142,9 @@ namespace smt {
 
     public:
         // set up job/resource global constraints
-        void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end);
+        void set_preemptable(unsigned j, bool is_preemptable);
-        void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end);
+        void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end, properties const& ps);
+        void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps);
         void add_done();
 
         // assignments
@@ -150,7 +158,7 @@ namespace smt {
 
         // derived bounds
         time_t ect(unsigned j, unsigned r, time_t start);
-        time_t lst(unsigned j, unsigned r);
+        bool lst(unsigned j, unsigned r, time_t& t);
         
         time_t solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap);
         time_t solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap);
@@ -165,10 +173,10 @@ namespace smt {
 
         // propagation
         void propagate_end_time(unsigned j, unsigned r);
-        void propagate_end_time_interval(unsigned j, unsigned r);
         void propagate_resource_energy(unsigned r);
 
         // final check constraints
+        bool constrain_end_time_interval(unsigned j, unsigned r);
         bool constrain_resource_energy(unsigned r);
 
         void block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job);

src/smt/theory_lra.cpp

@@ -2658,13 +2658,22 @@ public:
         }
     }
 
-    bool get_value(enode* n, expr_ref& r) {
+    bool get_value(enode* n, rational& val) {
         theory_var v = n->get_th_var(get_id());            
         if (!can_get_bound(v)) return false;
         lp::var_index vi = m_theory_var2var_index[v];
-        rational val;
         if (m_solver->has_value(vi, val)) {
             if (is_int(n) && !val.is_int()) return false;
+            return true;
+        }
+        else {
+            return false;
+        }
+    }    
+
+    bool get_value(enode* n, expr_ref& r) {
+        rational val;
+        if (get_value(n, val)) {
             r = a.mk_numeral(val, is_int(n));
             return true;
         }
@@ -2673,7 +2682,7 @@ public:
         }
     }    
 
-    bool get_lower(enode* n, expr_ref& r) {
+    bool get_lower(enode* n, rational& val, bool& is_strict) {
         theory_var v = n->get_th_var(get_id());
         if (!can_get_bound(v)) {
             TRACE("arith", tout << "cannot get lower for " << v << "\n";);
@@ -2681,29 +2690,36 @@ public:
         }
         lp::var_index vi = m_theory_var2var_index[v];
         lp::constraint_index ci;
-        rational val;
+        return m_solver->has_lower_bound(vi, ci, val, is_strict);
+    }
+
+    bool get_lower(enode* n, expr_ref& r) {
         bool is_strict;
-        if (m_solver->has_lower_bound(vi, ci, val, is_strict)) {
+        rational val;
+        if (get_lower(n, val, is_strict) && !is_strict) {
             r = a.mk_numeral(val, is_int(n));
             return true;
         }
-        TRACE("arith", m_solver->print_constraints(tout << "does not have lower bound " << vi << "\n"););
         return false;
     }
 
-    bool get_upper(enode* n, expr_ref& r) {
+    bool get_upper(enode* n, rational& val, bool& is_strict) {
         theory_var v = n->get_th_var(get_id());
         if (!can_get_bound(v))
             return false;
         lp::var_index vi = m_theory_var2var_index[v];
         lp::constraint_index ci;
-        rational val;
+        return m_solver->has_upper_bound(vi, ci, val, is_strict);
+
+    }
+
+    bool get_upper(enode* n, expr_ref& r) {
         bool is_strict;
-        if (m_solver->has_upper_bound(vi, ci, val, is_strict)) {
+        rational val;
+        if (get_upper(n, val, is_strict) && !is_strict) {
             r = a.mk_numeral(val, is_int(n));
             return true;
         }
-        TRACE("arith", m_solver->print_constraints(tout << "does not have upper bound " << vi << "\n"););
         return false;
     }
 
@@ -3132,6 +3148,9 @@ void theory_lra::init_model(model_generator & m) {
 model_value_proc * theory_lra::mk_value(enode * n, model_generator & mg) {
     return m_imp->mk_value(n, mg);
 }
+bool theory_lra::get_value(enode* n, rational& r) {
+    return m_imp->get_value(n, r);
+}
 bool theory_lra::get_value(enode* n, expr_ref& r) {
     return m_imp->get_value(n, r);
 }
@@ -3141,6 +3160,12 @@ bool theory_lra::get_lower(enode* n, expr_ref& r) {
 bool theory_lra::get_upper(enode* n, expr_ref& r) {
     return m_imp->get_upper(n, r);
 }
+bool theory_lra::get_lower(enode* n, rational& r, bool& is_strict) {
+    return m_imp->get_lower(n, r, is_strict);
+}
+bool theory_lra::get_upper(enode* n, rational& r, bool& is_strict) {
+    return m_imp->get_upper(n, r, is_strict);
+}
 
 bool theory_lra::validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
     return m_imp->validate_eq_in_model(v1, v2, is_true);

src/smt/theory_lra.h

@@ -80,6 +80,9 @@ namespace smt {
         bool get_value(enode* n, expr_ref& r) override;
         bool get_lower(enode* n, expr_ref& r);
         bool get_upper(enode* n, expr_ref& r);
+        bool get_value(enode* n, rational& r);
+        bool get_lower(enode* n, rational& r, bool& is_strict);
+        bool get_upper(enode* n, rational& r, bool& is_strict);
 
         bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;