mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #1784, fix #1783

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-01 17:31:14 -07:00
parent 77d68409c2
commit 8b08821112
2 changed files with 23 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/ast/datatype_decl_plugin.h
View file

@ -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);
}
};

5
src/smt/theory_lra.cpp
View file

@ -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);
}