mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

working on internalizer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-26 15:03:39 +08:00
parent ebed5fa037
commit 3852b3a753
2 changed files with 30 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_diff_logic.h
View file

@ -310,6 +310,7 @@ namespace smt {
typedef vector <std::pair<theory_var, rational> > objective_term; typedef vector <std::pair<theory_var, rational> > objective_term;
vector<objective_term> m_objectives; vector<objective_term> m_objectives;
vector<rational> m_objective_vars;
void internalize_objective(app * n, objective_term & objective); void internalize_objective(app * n, objective_term & objective);

53
src/smt/theory_diff_logic_def.h
View file

@ -55,6 +55,8 @@ std::ostream& theory_diff_logic<Ext>::atom::display(theory_diff_logic const& th,
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::nc_functor::reset() { void theory_diff_logic<Ext>::nc_functor::reset() {
m_antecedents.reset(); m_antecedents.reset();
m_objectives.reset();
m_objective_vars.reset();
} }
@ -999,11 +1001,11 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
template<typename Ext> template<typename Ext>
bool theory_diff_logic<Ext>::maximize(theory_var v) { bool theory_diff_logic<Ext>::maximize(theory_var v) {
IF_VERBOSE(1, IF_VERBOSE(1,
objective_term objective = m_objectives[v]; objective_term const& objective = m_objectives[v];
for (unsigned i = 0; i < objective.size(); ++i) { for (unsigned i = 0; i < objective.size(); ++i) {
verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n"; verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
} }
verbose_stream() << "\n";); verbose_stream() << m_objective_vars[v] << "\n";);
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return false; return false;
} }
@ -1011,39 +1013,38 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
template<typename Ext> template<typename Ext>
theory_var theory_diff_logic<Ext>::add_objective(app* term) { theory_var theory_diff_logic<Ext>::add_objective(app* term) {
objective_term objective; objective_term objective;
internalize_objective(term, objective); theory_var result = m_objectives.size();
m_objectives.push_back(objective); rational q(1), r(0);
return m_objectives.size()-1; if (!internalize_objective(term, q, r, objective)) {
result = null_theory_var;
}
else {
m_objectives.push_back(objective);
m_objective_vars.push_back(r);
}
return result;
} }
template<typename Ext> template<typename Ext>
inf_eps_rational<inf_rational> theory_diff_logic<Ext>::get_objective_value(theory_var v) { inf_eps_rational<inf_rational> theory_diff_logic<Ext>::get_objective_value(theory_var v) {
inf_rational objective; inf_rational objective;
inf_eps_rational<inf_rational> val(objective); inf_eps_rational<inf_rational> val(objective);
return val; return val;
} }
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::internalize_objective(app * n, objective_term & objective) { bool theory_diff_logic<Ext>::internalize_objective(app * n, rational& q, objective_term & objective) {
// TODO: Need some simplification on n to ensure no bad case
SASSERT(!m_util.is_div(n));
SASSERT(!m_util.is_idiv(n));
SASSERT(!m_util.is_mod(n));
SASSERT(!m_util.is_rem(n));
SASSERT(!m_util.is_to_real(n));
SASSERT(!m_util.is_to_int(n));
SASSERT(!m_util.is_power(n));
SASSERT(!m_util.is_irrational_algebraic_numeral(n));
// Compile term into objective_term format // Compile term into objective_term format
rational r; rational r;
if (m_util.is_numeral(n, r)) { if (m_util.is_numeral(n, r)) {
theory_var v = mk_num(n, r); q += r;
objective.push_back(std::make_pair(v, r));
} }
else if (m_util.is_add(n)) { else if (m_util.is_add(n)) {
for (unsigned i = 0; i < n->get_num_args(); ++i) { for (unsigned i = 0; i < n->get_num_args(); ++i) {
internalize_objective(to_app(n->get_arg(i)), objective); if (!internalize_objective(to_app(n->get_arg(i)), objective)) {
return false;
}
}; };
} }
else if (m_util.is_mul(n)) { else if (m_util.is_mul(n)) {
@ -1054,17 +1055,21 @@ void theory_diff_logic<Ext>::internalize_objective(app * n, objective_term & obj
SASSERT(m_util.is_numeral(lhs, r) || m_util.is_numeral(rhs, r)); SASSERT(m_util.is_numeral(lhs, r) || m_util.is_numeral(rhs, r));
if (!m_util.is_numeral(lhs, r)) if (!m_util.is_numeral(lhs, r))
std::swap(lhs, rhs); std::swap(lhs, rhs);
m_util.is_numeral(lhs, r); m_util.is_numeral(lhs, r);
theory_var v = mk_var(rhs); theory_var v = mk_var(rhs);
objective.push_back(std::make_pair(v, r)); objective.push_back(std::make_pair(v, r));
} }
else if (n->get_family_id() == m_util.get_family_id()) {
return false;
}
else { else {
theory_var v = mk_var(n); theory_var v = mk_var(n);
rational r(1); rational r(1);
objective.push_back(std::make_pair(v, r)); objective.push_back(std::make_pair(v, r));
} }
return true;
} }
#endif /* _THEORY_DIFF_LOGIC_DEF_H_ */ #endif /* _THEORY_DIFF_LOGIC_DEF_H_ */