diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 96093ed79..afe3130bf 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -10,7 +10,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ #pragma once @@ -29,13 +29,6 @@ namespace polysat { /** Create invalid fi_record */ fi_record(): interval(eval_interval::full()) {} - fi_record(eval_interval interval, vector 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(); diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index b0d76d9cf..b58eade59 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -11,7 +11,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ #pragma once @@ -37,9 +37,7 @@ namespace polysat { solver& s; forbidden_intervals m_forbidden_intervals; - struct entry : public dll_base, public fi_record { - entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {} - }; + struct entry : public dll_base, public fi_record {}; enum class entry_kind { unit_e, equal_e, diseq_e }; ptr_vector m_alloc;