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

remove constructor

Browse source
This commit is contained in:
Jakob Rath 2022-08-22 15:00:35 +02:00
parent 28ddd4ad56
commit 9fcea37625
2 changed files with 3 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -10,7 +10,7 @@ Module Name:
Author: Author:
Nikolaj Bjorner (nbjorner) 2021-03-19 Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6 Jakob Rath 2021-04-06
--*/ --*/
#pragma once #pragma once
@ -29,13 +29,6 @@ namespace polysat {
/** Create invalid fi_record */ /** Create invalid fi_record */
fi_record(): interval(eval_interval::full()) {} 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 { struct less {
bool operator()(fi_record const& a, fi_record const& b) const { bool operator()(fi_record const& a, fi_record const& b) const {
return a.interval.lo_val() < b.interval.lo_val(); return a.interval.lo_val() < b.interval.lo_val();

6
src/math/polysat/viable.h
View file

@ -11,7 +11,7 @@ Module Name:
Author: Author:
Nikolaj Bjorner (nbjorner) 2021-03-19 Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6 Jakob Rath 2021-04-06
--*/ --*/
#pragma once #pragma once
@ -37,9 +37,7 @@ namespace polysat {
solver& s; solver& s;
forbidden_intervals m_forbidden_intervals; forbidden_intervals m_forbidden_intervals;
struct entry : public dll_base<entry>, public fi_record { struct entry : public dll_base<entry>, public fi_record {};
entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {}
};
enum class entry_kind { unit_e, equal_e, diseq_e }; enum class entry_kind { unit_e, equal_e, diseq_e };
ptr_vector<entry> m_alloc; ptr_vector<entry> m_alloc;