mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

Nikolaj's changes is mk_eq

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-18 11:53:26 -08:00 • committed by Lev Nachmanson
parent ad98594447
commit 3192db64a1
1 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_lra.cpp
View file

@ -1722,19 +1722,24 @@ public:
return FC_GIVEUP; return FC_GIVEUP;
} }
// create an eq atom representing "term = offset" // create an eq atom representing "term = offset"
app_ref mk_eq(lp::lar_term const& term, rational const& offset) { app_ref mk_eq(lp::lar_term const& term, rational const& offset) {
u_map<rational> coeffs; u_map<rational> coeffs;
term2coeffs(term, coeffs); term2coeffs(term, coeffs);
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 t = coeffs2app(coeffs, rational::zero(), isint); app_ref t = coeffs2app(coeffs, rational::zero(), isint);
app_ref atom(m.mk_eq(t, a.mk_numeral(offset, isint)), m); app_ref s(a.mk_numeral(offset, isint), m);
ctx().internalize(atom, true); if (s == t) {
ctx().mark_as_relevant(atom.get()); return app_ref(m.mk_true(), m);
return atom; }
else {
app_ref atom(m.mk_eq(t, s), m);
ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get());
return atom;
}
} }
// 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) {
rational offset = k; rational offset = k;