mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43: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 15:09:25 +02:00
parent 4c7ec75868
commit f48e0498d0
1 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -155,11 +155,14 @@ namespace polysat {
unsigned const next_i = seq[(seq_i+1) % seq.size()]; unsigned const next_i = seq[(seq_i+1) % seq.size()];
// Build constraint: upper bound of each interval is not contained in the next interval, // Build constraint: upper bound of each interval is not contained in the next interval,
// using the equivalence: t \in [l;h[ <=> t-l < h-l // using the equivalence: t \in [l;h[ <=> t-l < h-l
auto const& hi = records[i].interval.hi(); auto hi = records[i].interval.hi();
auto const& next_lo = records[next_i].interval.lo(); auto next_lo = records[next_i].interval.lo();
auto const& next_hi = records[next_i].interval.hi(); auto next_hi = records[next_i].interval.hi();
auto const& lhs = hi - next_lo; auto lhs = hi - next_lo;
auto const& rhs = next_hi - next_lo; auto rhs = next_hi - next_lo;
// NB: do we really have to pass in the level to this new literal?
// seems separating the level from the constraint is what we want
// the level of a literal is when it was assigned. Lemmas could have unassigned literals.
signed_constraint c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs); signed_constraint c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs);
LOG("constraint: " << c); LOG("constraint: " << c);
clause.push_new_constraint(std::move(c)); clause.push_new_constraint(std::move(c));