mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

take coefficient into account (#87)

Browse source 
* take coefficient into account

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* take coefficient into account

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-25 17:57:11 -07:00 • committed by Lev Nachmanson
parent 4ba7b6b047
commit 545bfff827
1 changed files with 23 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/smt/theory_lra.cpp
View file

@ -226,10 +226,10 @@ class theory_lra::imp {
lp::var_index m_rzero_var; lp::var_index m_rzero_var;
enum constraint_source { enum constraint_source {
inequality_source, inequality_source,
equality_source, equality_source,
definition_source, definition_source,
null_source null_source
}; };
svector<constraint_source> m_constraint_sources; svector<constraint_source> m_constraint_sources;
svector<literal> m_inequalities; // asserted rows corresponding to inequality literals. svector<literal> m_inequalities; // asserted rows corresponding to inequality literals.
@ -928,7 +928,7 @@ public:
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_solver(nullptr), m_solver(nullptr),
m_resource_limit(*this), m_resource_limit(*this),
m_switcher(*this) { m_switcher(*this) {
} }
~imp() { ~imp() {
@ -1680,17 +1680,14 @@ public:
return FC_GIVEUP; return FC_GIVEUP;
} }
// create a eq atom representing "term = 0" // create an eq atom representing "term = offset"
app_ref mk_eq(lp::lar_term const& term) { app_ref mk_eq(lp::lar_term const& term, rational const& offset) {
rational offset(0);
u_map<rational> coeffs; u_map<rational> coeffs;
term2coeffs(term, coeffs, rational::one(), offset); term2coeffs(term, coeffs);
offset.neg();
bool isint = offset.is_int(); bool isint = offset.is_int();
for (auto const& kv : coeffs) isint &= is_int(kv.m_key) && kv.m_value.is_int(); for (auto const& kv : coeffs) isint &= is_int(kv.m_key) && kv.m_value.is_int();
app_ref atom(m);
app_ref t = coeffs2app(coeffs, rational::zero(), isint); app_ref t = coeffs2app(coeffs, rational::zero(), isint);
atom = m.mk_eq(t, a.mk_numeral(offset, isint)); app_ref atom(m.mk_eq(t, a.mk_numeral(offset, isint)), m);
ctx().internalize(atom, true); ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get()); ctx().mark_as_relevant(atom.get());
return atom; return atom;
@ -1698,11 +1695,10 @@ public:
// create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) { app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
bool is_int = k.is_int(); rational offset = k;
rational offset = -k; bool is_int = offset.is_int();
u_map<rational> coeffs; u_map<rational> coeffs;
term2coeffs(term, coeffs, rational::one(), offset); term2coeffs(term, coeffs);
offset.neg();
TRACE("arith", TRACE("arith",
m_solver->print_term(term, tout << "term: ") << "\n"; m_solver->print_term(term, tout << "term: ") << "\n";
for (auto const& kv : coeffs) { for (auto const& kv : coeffs) {
@ -2096,11 +2092,11 @@ public:
TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";); TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
app_ref atom(m); app_ref atom(m);
if (is_eq) { if (is_eq) {
atom = mk_eq(ineq.m_term); atom = mk_eq(ineq.m_term, ineq.m_rs);
} }
else { else {
// create term >= 0 (or term <= 0) // create term >= 0 (or term <= 0)
atom = mk_bound(ineq.m_term, rational::zero(), is_lower); atom = mk_bound(ineq.m_term, ineq.m_rs, is_lower);
} }
literal lit(ctx().get_bool_var(atom), pos); literal lit(ctx().get_bool_var(atom), pos);
core.push_back(~lit); core.push_back(~lit);
@ -2118,7 +2114,7 @@ public:
} }
return r; return r;
} }
lbool check_nra() { lbool check_nra() {
m_use_nra_model = false; m_use_nra_model = false;
if (m.canceled()) { if (m.canceled()) {
@ -3525,7 +3521,11 @@ public:
return internalize_def(term); return internalize_def(term);
} }
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff, rational& offset) { void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs) {
term2coeffs(term, coeffs, rational::one());
}
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
for (const auto & ti : term) { for (const auto & ti : term) {
theory_var w; theory_var w;
if (m_solver->is_term(ti.var())) { if (m_solver->is_term(ti.var())) {
@ -3533,7 +3533,7 @@ public:
//if (w == null_theory_var) // if extracting expressions directly from nested term //if (w == null_theory_var) // if extracting expressions directly from nested term
lp::lar_term const& term1 = m_solver->get_term(ti.var()); lp::lar_term const& term1 = m_solver->get_term(ti.var());
rational coeff2 = coeff * ti.coeff(); rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2, offset); term2coeffs(term1, coeffs, coeff2);
continue; continue;
} }
else { else {
@ -3575,9 +3575,8 @@ public:
app_ref mk_term(lp::lar_term const& term, bool is_int) { app_ref mk_term(lp::lar_term const& term, bool is_int) {
u_map<rational> coeffs; u_map<rational> coeffs;
rational offset; term2coeffs(term, coeffs);
term2coeffs(term, coeffs, rational::one(), offset); return coeffs2app(coeffs, rational::zero(), is_int);
return coeffs2app(coeffs, offset, is_int);
} }
rational gcd_reduce(u_map<rational>& coeffs) { rational gcd_reduce(u_map<rational>& coeffs) {