From 8b08821112c9307341f4711a9d4a1df9bf998b35 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Aug 2018 17:31:14 -0700
Subject: [PATCH] fix #1784, fix #1783
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/datatype_decl_plugin.h | 26 +++++++++++++++++++-------
src/smt/theory_lra.cpp | 5 ++++-
2 files changed, 23 insertions(+), 8 deletions(-)
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 17602efcf..fc98c97e7 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -134,13 +134,25 @@ namespace datatype {
~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
- sort_size s1 = m_arg1->eval(S);
- sort_size s2 = m_arg2->eval(S);
- if (s1.is_infinite()) return s1;
- if (s2.is_infinite()) return s2;
- if (s1.is_very_big()) return s1;
- if (s2.is_very_big()) return s2;
- rational r = rational(s1.size(), rational::ui64()) + rational(s2.size(), rational::ui64());
+ rational r(0);
+ ptr_vector<size> todo;
+ todo.push_back(m_arg1);
+ todo.push_back(m_arg2);
+ while (!todo.empty()) {
+ size* s = todo.back();
+ todo.pop_back();
+ plus* p = dynamic_cast<plus*>(s);
+ if (p) {
+ todo.push_back(p->m_arg1);
+ todo.push_back(p->m_arg2);
+ }
+ else {
+ sort_size sz = s->eval(S);
+ if (sz.is_infinite()) return sz;
+ if (sz.is_very_big()) return sz;
+ r += rational(sz.size(), rational::ui64());
+ }
+ }
return sort_size(r);
}
};
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a49e0e4bb..267412da6 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2805,7 +2805,9 @@ public:
TRACE("arith", display(tout << st << " v" << v << "\n"););
switch (st) {
case lp::lp_status::OPTIMAL: {
- inf_rational val(term_max.x, term_max.y);
+ init_variable_values();
+ inf_rational val = get_value(v);
+ // inf_rational val(term_max.x, term_max.y);
blocker = mk_gt(v);
return inf_eps(rational::zero(), val);
}
@@ -2851,6 +2853,7 @@ public:
}
theory_var add_objective(app* term) {
+ TRACE("opt", tout << expr_ref(term, m) << "\n";);
return internalize_def(term);
}