From da44ad7e6f387ccaefe2d705bf6010c2ca04ecfa Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 29 Jun 2018 13:43:23 -0700 Subject: [PATCH] added stubs for get_lower/get_upper required by theory_seq Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 17 +++++++++++++++++ src/smt/theory_lra.h | 2 ++ src/smt/theory_seq.cpp | 35 +++++++++++++++++++++++++---------- 3 files changed, 44 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d9be0e872..06d0730b7 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2611,6 +2611,16 @@ public: } } + bool get_lower(enode* n, expr_ref& r) { + NOT_IMPLEMENTED_YET(); + return false; + } + + bool get_upper(enode* n, expr_ref& r) { + NOT_IMPLEMENTED_YET(); + return false; + } + bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const { SASSERT(v1 != null_theory_var); SASSERT(v2 != null_theory_var); @@ -2980,6 +2990,13 @@ model_value_proc * theory_lra::mk_value(enode * n, model_generator & mg) { bool theory_lra::get_value(enode* n, expr_ref& r) { return m_imp->get_value(n, r); } +bool theory_lra::get_lower(enode* n, expr_ref& r) { + return m_imp->get_lower(n, r); +} +bool theory_lra::get_upper(enode* n, expr_ref& r) { + return m_imp->get_upper(n, r); +} + 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 3398e79d4..074b11ba7 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -78,6 +78,8 @@ namespace smt { model_value_proc * mk_value(enode * n, model_generator & mg) override; 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 validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d5fe54fae..47bc0c13e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -26,6 +26,7 @@ Revision History: #include "smt/smt_model_generator.h" #include "smt/theory_seq.h" #include "smt/theory_arith.h" +#include "smt/theory_lra.h" #include "smt/smt_kernel.h" using namespace smt; @@ -3506,6 +3507,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v) if (tha) return tha->get_value(ctx.get_enode(e), v); theory_i_arith* thi = get_th_arith(ctx, afid, e); if (thi) return thi->get_value(ctx.get_enode(e), v); + theory_lra* thr = get_th_arith(ctx, afid, e); + if (thr) return thr->get_value(ctx.get_enode(e), v); TRACE("seq", tout << "no arithmetic theory\n";); return false; } @@ -3531,25 +3534,37 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const { context& ctx = get_context(); expr_ref e(m_util.str.mk_length(_e), m); expr_ref _lo(m); - theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); - if (tha && !tha->get_lower(ctx.get_enode(e), _lo)) return false; - if (!tha) { - theory_i_arith* thi = get_th_arith(ctx, m_autil.get_family_id(), e); - if (!thi || !thi->get_lower(ctx.get_enode(e), _lo)) return false; + family_id afid = m_autil.get_family_id(); + do { + theory_mi_arith* tha = get_th_arith(ctx, afid, e); + if (tha && tha->get_lower(ctx.get_enode(e), _lo)) break; + theory_i_arith* thi = get_th_arith(ctx, afid, e); + if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break; + theory_lra* thr = get_th_arith(ctx, afid, e); + if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break; + TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";); + return false; } + while (false); return m_autil.is_numeral(_lo, lo) && lo.is_int(); } bool theory_seq::upper_bound(expr* _e, rational& hi) const { context& ctx = get_context(); expr_ref e(m_util.str.mk_length(_e), m); - theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); + family_id afid = m_autil.get_family_id(); expr_ref _hi(m); - if (tha && !tha->get_upper(ctx.get_enode(e), _hi)) return false; - if (!tha) { - theory_i_arith* thi = get_th_arith(ctx, m_autil.get_family_id(), e); - if (!thi || !thi->get_upper(ctx.get_enode(e), _hi)) return false; + do { + theory_mi_arith* tha = get_th_arith(ctx, afid, e); + if (tha && tha->get_upper(ctx.get_enode(e), _hi)) break; + theory_i_arith* thi = get_th_arith(ctx, afid, e); + if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break; + theory_lra* thr = get_th_arith(ctx, afid, e); + if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break; + TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";); + return false; } + while (false); return m_autil.is_numeral(_hi, hi) && hi.is_int(); }