From 0af00e62dee673c8025bf7a7a5a7e865f1192f12 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Aug 2018 12:42:26 -0700 Subject: [PATCH] abstract arithmetic value extraction Signed-off-by: Nikolaj Bjorner --- src/smt/CMakeLists.txt | 1 + src/smt/smt_arith_value.cpp | 113 ++++++++++++++++ src/smt/smt_arith_value.h | 37 ++++++ src/smt/smt_context.h | 5 + src/smt/theory_jobscheduler.cpp | 224 +++++++++++++++++++++++++++----- src/smt/theory_jobscheduler.h | 34 +++-- src/smt/theory_lra.cpp | 45 +++++-- src/smt/theory_lra.h | 3 + 8 files changed, 405 insertions(+), 57 deletions(-) create mode 100644 src/smt/smt_arith_value.cpp create mode 100644 src/smt/smt_arith_value.h diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 13a00d44e..4b640f8ca 100644 --- a/src/smt/CMakeLists.txt +++ b/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 diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp new file mode 100644 index 000000000..ecf924111 --- /dev/null +++ b/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(th); + theory_i_arith* thi = dynamic_cast(th); + theory_lra* thr = dynamic_cast(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(th); + theory_i_arith* thi = dynamic_cast(th); + theory_lra* thr = dynamic_cast(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(th); + theory_i_arith* thi = dynamic_cast(th); + theory_lra* thr = dynamic_cast(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; + } +}; diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h new file mode 100644 index 000000000..9b0f833ac --- /dev/null +++ b/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); + }; +}; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ff92f6f95..f545f7c6d 100644 --- a/src/smt/smt_context.h +++ b/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) diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index f12193c2e..173d44c52 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/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) { - // TBD - // establish maximal intervals around start, such that end time is a linear function of start. + bool theory_jobscheduler::constrain_end_time_interval(unsigned j, unsigned r) { + unsigned idx1 = 0, idx2 = 0; + time_t s = start(j); + if (!resource_available(r, s, idx1)) return false; + vector& 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)); - lits.push_back(~mk_le(m_jobs[max_j].m_start, m_jobs[max_j].m_end)); + if (j != max_j) { + 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(); - return 0; + arith_value av(get_context()); + 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::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& 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::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 - fml = mk_ge(ji.m_start, 0); + // start(j) >= start_lb + fml = mk_ge(ji.m_start, start_lb); ctx.assert_expr(fml); - // end(j) <= time_t::max - // is implied by resource(j) = r => end(j) <= end(j, r) + // end(j) <= end_ub + fml = mk_le(ji.m_end, end_ub); + ctx.assert_expr(fml); } for (unsigned r = 0; r < m_resources.size(); ++r) { - vector& available = m_resources[r].m_available; - res_available::compare cmp; - std::sort(available.begin(), available.end(), cmp); - for (unsigned i = 0; i < available.size(); ++i) { - if (i + 1 < available.size() && - available[i].m_end > available[i + 1].m_start) { + res_info& ri = m_resources[r]; + vector& available = ri.m_available; + if (available.empty()) continue; + app_ref res(u.mk_resource(r), m); + for (unsigned j : ri.m_jobs) { + // 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& 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; } }; diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index 369cc1955..117303ff7 100644 --- a/src/smt/theory_jobscheduler.h +++ b/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 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): - m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end) {} + properties m_properties; + 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 m_resources; // resources allowed to run job. u_map 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; - time_t m_start; - time_t m_end; - res_available(unsigned load_pct, time_t start, time_t end): + unsigned m_loadpct; + time_t m_start; + time_t m_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 add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end); + void set_preemptable(unsigned j, bool is_preemptable); + 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); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 267412da6..6c66de91d 100644 --- a/src/smt/theory_lra.cpp +++ b/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); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 074b11ba7..811fa1812 100644 --- a/src/smt/theory_lra.h +++ b/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;