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

remove unused ckind_t::smul_fl_t

Browse source
This commit is contained in:
Jakob Rath 2024-04-23 14:38:33 +02:00
parent 69ea52407f
commit f8c593edf9
2 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/polysat/constraints.h
View file

@ -29,7 +29,7 @@ namespace polysat {
using pdd = dd::pdd;
using pvar = unsigned;
enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t };
enum ckind_t { ule_t, umul_ovfl_t, op_t };
class constraint {
unsigned_vector m_vars;
@ -86,7 +86,6 @@ namespace polysat {
ckind_t op() const { return m_op; }
bool is_ule() const { return m_op == ule_t; }
bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
bool is_smul_fl() const { return m_op == smul_fl_t; }
bool is_op() const { return m_op == op_t; }
ule_constraint const& to_ule() const { SASSERT(is_ule()); return *reinterpret_cast<ule_constraint*>(m_constraint); }
umul_ovfl_constraint const& to_umul_ovfl() const { SASSERT(is_umul_ovfl()); return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }

3
src/sat/smt/polysat_solver.cpp
View file

@ -477,9 +477,6 @@ namespace polysat {
case ckind_t::op_t:
UNREACHABLE();
break;
case ckind_t::smul_fl_t:
NOT_IMPLEMENTED_YET();
break;
}
return result;
}