mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

making ddl work with objectives

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-15 11:10:03 -07:00
parent f82f7f83b9
commit 90bd02b5f7
1 changed files with 26 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_dense_diff_logic_def.h
View file

@ -826,6 +826,7 @@ namespace smt {
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
} }
// TBD: code is common to both sparse and dense difference logic solvers.
template<typename Ext> template<typename Ext>
bool theory_dense_diff_logic<Ext>::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) { bool theory_dense_diff_logic<Ext>::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) {
@ -855,8 +856,20 @@ namespace smt {
return false; return false;
} }
else { else {
enode * e = get_context().mk_enode(to_app(n), false, false, true); context& ctx = get_context();
theory_var v = mk_var(e); enode * e = 0;
theory_var v = 0;
if (ctx.e_internalized(n)) {
e = ctx.get_enode(to_app(n));
}
else {
e = ctx.mk_enode(to_app(n), false, false, true);
}
v = e->get_th_var(get_id());
if (v == null_theory_var) {
v = mk_var(e);
}
objective.push_back(std::make_pair(v, m)); objective.push_back(std::make_pair(v, m));
} }
return true; return true;
@ -864,7 +877,6 @@ namespace smt {
template<typename Ext> template<typename Ext>
inf_eps_rational<inf_rational> theory_dense_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) { inf_eps_rational<inf_rational> theory_dense_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) {
return inf_eps();
typedef simplex::simplex<simplex::mpq_ext> Simplex; typedef simplex::simplex<simplex::mpq_ext> Simplex;
Simplex S; Simplex S;
ast_manager& m = get_manager(); ast_manager& m = get_manager();
@ -872,10 +884,10 @@ namespace smt {
IF_VERBOSE(1, IF_VERBOSE(1,
for (unsigned i = 0; i < objective.size(); ++i) { for (unsigned i = 0; i < objective.size(); ++i) {
verbose_stream() << "Coefficient " << objective[i].second verbose_stream() << objective[i].second
<< " of theory_var " << objective[i].first << "\n"; << " * v" << objective[i].first << " ";
} }
verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";); verbose_stream() << " + " << m_objective_consts[v] << "\n";);
unsigned num_nodes = get_num_vars(); unsigned num_nodes = get_num_vars();
unsigned num_edges = m_edges.size(); unsigned num_edges = m_edges.size();
@ -964,7 +976,15 @@ namespace smt {
core.push_back(tmp); core.push_back(tmp);
} }
} }
for (unsigned i = 0; i < num_nodes; ++i) {
mpq_inf const& val = S.get_value(i);
rational q(val.first), eps(val.second);
numeral a(q);
m_assignment[i] = a;
// TBD: if epsilon is != 0, then adjust a by some small fraction.
}
blocker = mk_gt(v, r); blocker = mk_gt(v, r);
IF_VERBOSE(10, verbose_stream() << blocker << "\n";);
return inf_eps(rational(0), r); return inf_eps(rational(0), r);
} }
default: default: