mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

move definitions to cpp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 11:09:59 -07:00
parent 5a9161ed7b
commit ff104c4b13
3 changed files with 32 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_ac_plugin.h
View file

@ -138,7 +138,7 @@ namespace euf {
};
theory_id m_fid = 0;
unsigned m_op = null_decl_kind;
decl_kind m_op = null_decl_kind;
func_decl* m_decl = nullptr;
vector<eq> m_eqs;
ptr_vector<node> m_nodes;

29
src/ast/sls/sls_arith_base.cpp
View file

@ -20,6 +20,35 @@ Author:
namespace sls {
template<typename num_t>
bool arith_base<num_t>::ineq::is_true() const {
switch (m_op) {
case ineq_kind::LE:
return m_args_value + m_coeff <= 0;
case ineq_kind::EQ:
return m_args_value + m_coeff == 0;
default:
return m_args_value + m_coeff < 0;
}
}
template<typename num_t>
std::ostream& arith_base<num_t>::ineq::display(std::ostream& out) const {
bool first = true;
for (auto const& [c, v] : m_args)
out << (first ? "" : " + ") << c << " * v" << v, first = false;
if (m_coeff != 0)
out << " + " << m_coeff;
switch (m_op) {
case ineq_kind::LE:
return out << " <= " << 0 << "(" << m_args_value + m_coeff << ")";
case ineq_kind::EQ:
return out << " == " << 0 << "(" << m_args_value + m_coeff << ")";
default:
return out << " < " << 0 << "(" << m_args_value + m_coeff << ")";
}
}
template<typename num_t>
arith_base<num_t>::arith_base(context& ctx) :
plugin(ctx),

27
src/ast/sls/sls_arith_base.h
View file

@ -57,31 +57,8 @@ namespace sls {
num_t m_args_value;
unsigned m_var_to_flip = UINT_MAX;
bool is_true() const {
switch (m_op) {
case ineq_kind::LE:
return m_args_value + m_coeff <= 0;
case ineq_kind::EQ:
return m_args_value + m_coeff == 0;
default:
return m_args_value + m_coeff < 0;
}
}
std::ostream& display(std::ostream& out) const {
bool first = true;
for (auto const& [c, v] : m_args)
out << (first ? "" : " + ") << c << " * v" << v, first = false;
if (m_coeff != 0)
out << " + " << m_coeff;
switch (m_op) {
case ineq_kind::LE:
return out << " <= " << 0 << "(" << m_args_value + m_coeff << ")";
case ineq_kind::EQ:
return out << " == " << 0 << "(" << m_args_value + m_coeff << ")";
default:
return out << " < " << 0 << "(" << m_args_value + m_coeff << ")";
}
}
bool is_true() const;
std::ostream& display(std::ostream& out) const;
};
private: