mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

move fi_record

Browse source
This commit is contained in:
Jakob Rath 2022-08-22 14:14:30 +02:00
parent 26fcfc6ecd
commit 3a759c1a28
2 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -293,29 +293,6 @@ namespace polysat {
return c.display(out);
}
struct fi_record {
eval_interval interval;
vector<signed_constraint> side_cond;
signed_constraint src;
rational coeff;
/** Create invalid fi_record */
fi_record(): interval(eval_interval::full()) {}
fi_record(eval_interval interval, vector<signed_constraint> side_cond, signed_constraint src, rational coeff):
interval(interval),
side_cond(side_cond),
src(src),
coeff(coeff)
{}
struct less {
bool operator()(fi_record const& a, fi_record const& b) const {
return a.interval.lo_val() < b.interval.lo_val();
}
};
};
class constraint_pp {
constraint const* c;
lbool status;

23
src/math/polysat/forbidden_intervals.h
View file

@ -20,6 +20,29 @@ namespace polysat {
class solver;
struct fi_record {
eval_interval interval;
vector<signed_constraint> side_cond;
signed_constraint src;
rational coeff;
/** Create invalid fi_record */
fi_record(): interval(eval_interval::full()) {}
fi_record(eval_interval interval, vector<signed_constraint> side_cond, signed_constraint src, rational coeff):
interval(interval),
side_cond(side_cond),
src(src),
coeff(coeff)
{}
struct less {
bool operator()(fi_record const& a, fi_record const& b) const {
return a.interval.lo_val() < b.interval.lo_val();
}
};
};
class forbidden_intervals {
solver& s;