mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix build (add conversion operator)

Browse source
This commit is contained in:
Jakob Rath 2023-01-10 17:17:14 +01:00
parent 0c799524e8
commit 1d0ad1ccc0
3 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/clause_builder.h
View file

@ -49,14 +49,12 @@ namespace polysat {
/// Insert constraints into the clause.
void insert(sat::literal lit);
void insert(signed_constraint c);
void insert(inequality const& i) { insert(i.as_signed_constraint()); }
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to \b false.
/// \pre Constraint must be \b false in the current assignment.
void insert_eval(sat::literal lit);
void insert_eval(signed_constraint c);
void insert_eval(inequality const& i) { insert_eval(i.as_signed_constraint()); }
/// Insert constraints into the clause.
/// If possible, evaluate them as in insert_eval.

1
src/math/polysat/constraint.h
View file

@ -225,6 +225,7 @@ namespace polysat {
pdd const& rhs() const { return m_rhs; }
bool is_strict() const { return m_src.is_negative(); }
signed_constraint as_signed_constraint() const { return m_src; }
operator signed_constraint() const { return m_src; }
};
class constraint_pp {

4
src/math/polysat/saturation.cpp
View file

@ -1720,7 +1720,7 @@ namespace polysat {
VERIFY(x_min <= x_max);
// TODO: d +/- 1 would suffice here
// TODO: d +/- M would suffice here
rational d1 = dd1;
rational d2 = dd2;
VERIFY(adjust_bound(x_min, x_max, y0, M, a1, b1, c1, d1, nullptr));
@ -1801,7 +1801,7 @@ namespace polysat {
vector<signed_constraint> bounds;
rational x_min, x_max;
if (!s.m_viable.has_max_forbidden(x, a_l_b.as_signed_constraint(), x_max, x_min, bounds))
if (!s.m_viable.has_max_forbidden(x, a_l_b, x_max, x_min, bounds))
return false;
// retrieved maximal forbidden interval [x_max, x_min[.