mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-07 17:04:32 +02:00
parent a6643955e6
commit 146d107961
2 changed files with 5 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/math/polysat/eq_constraint.cpp
View file

@ -87,39 +87,6 @@ namespace polysat {
return r.is_never_zero(); return r.is_never_zero();
} }
/**
* Equality constraints
*/
// constraint_ref eq_constraint::eq_resolve(solver& s, pvar v) {
// LOG("Resolve " << *this << " upon v" << v);
// if (s.m_conflict.size() != 1)
// return nullptr;
// if (!s.m_conflict.clauses().empty())
// return nullptr;
// constraint* c = s.m_conflict.units()[0];
// SASSERT(c->is_currently_false(s));
// // 'c == this' can happen if propagation was from decide() with only one value left
// // (e.g., if there's an unsatisfiable clause and we try all values).
// // Resolution would give us '0 == 0' in this case, which is useless.
// if (c == this)
// return nullptr;
// SASSERT(is_currently_true(s)); // TODO: might not always hold (due to similar case as in comment above?)
// if (c->is_eq() && c->is_positive()) {
// pdd a = c->to_eq().p();
// pdd b = p();
// pdd r = a;
// if (!a.resolve(v, b, r))
// return nullptr;
// p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm);
// unsigned lvl = std::max(c->level(), level());
// return s.m_constraints.eq(lvl, pos_t, r, d);
// }
// return nullptr;
// }
inequality eq_constraint::as_inequality(bool is_positive) const { inequality eq_constraint::as_inequality(bool is_positive) const {
pdd zero = p() - p(); pdd zero = p() - p();
if (is_positive) if (is_positive)

13
src/math/polysat/forbidden_intervals.cpp
View file

@ -174,15 +174,12 @@ namespace polysat {
} }
// TODO:
// review translation from is_positive to ineq.strict
/** Precondition: all variables other than v are assigned. /** Precondition: all variables other than v are assigned.
* *
* \param[out] out_interval The forbidden interval for this constraint * \param[out] out_interval The forbidden interval for this constraint
* \param[out] out_neg_cond Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant. * \param[out] out_neg_cond Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant.
* \returns True iff a forbidden interval exists and the output parameters were set. * \returns True iff a forbidden interval exists and the output parameters were set.
*/ */
bool forbidden_intervals::get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) bool forbidden_intervals::get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
{ {