mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
make a few functions static
This commit is contained in:
parent
7ebc660b6d
commit
42b26c63e5
|
@ -32,7 +32,7 @@ namespace smt {
|
|||
return static_cast<unsigned>(acc / m_lemmas.size());
|
||||
}
|
||||
|
||||
void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
|
||||
static void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
|
||||
unsigned num_lits = cls->get_num_literals();
|
||||
for (unsigned i = 0; i < num_lits; i++) {
|
||||
literal l = cls->get_literal(i);
|
||||
|
@ -40,7 +40,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
|
||||
static void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
|
||||
clause_vector::const_iterator it = v.begin();
|
||||
clause_vector::const_iterator end = v.end();
|
||||
for (; it != end; ++it)
|
||||
|
@ -79,7 +79,7 @@ namespace smt {
|
|||
out << (m_assigned_literals.size() - n) << "]";
|
||||
}
|
||||
|
||||
void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
|
||||
static void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
|
||||
unsigned num_lits = cls->get_num_literals();
|
||||
for (unsigned i = 0; i < num_lits; i++) {
|
||||
literal l = cls->get_literal(i);
|
||||
|
@ -87,7 +87,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
|
||||
static void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
|
||||
clause_vector::const_iterator it = v.begin();
|
||||
clause_vector::const_iterator end = v.end();
|
||||
for (; it != end; ++it)
|
||||
|
@ -114,7 +114,7 @@ namespace smt {
|
|||
out << "\n";
|
||||
}
|
||||
|
||||
void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
|
||||
static void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
|
||||
unsigned num_lits = cls->get_num_literals();
|
||||
bool_var min_var = cls->get_literal(0).var();
|
||||
for (unsigned i = 1; i < num_lits; i++) {
|
||||
|
@ -125,7 +125,7 @@ namespace smt {
|
|||
var2num_min_occs[min_var]++;
|
||||
}
|
||||
|
||||
void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
|
||||
static void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
|
||||
clause_vector::const_iterator it = v.begin();
|
||||
clause_vector::const_iterator end = v.end();
|
||||
for (; it != end; ++it)
|
||||
|
|
|
@ -335,7 +335,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
bool find_arg(app * n, expr * t, expr * & other) {
|
||||
static bool find_arg(app * n, expr * t, expr * & other) {
|
||||
SASSERT(n->get_num_args() == 2);
|
||||
if (n->get_arg(0) == t) {
|
||||
other = n->get_arg(1);
|
||||
|
@ -348,7 +348,7 @@ namespace smt {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool check_args(app * n, expr * t1, expr * t2) {
|
||||
static bool check_args(app * n, expr * t1, expr * t2) {
|
||||
SASSERT(n->get_num_args() == 2);
|
||||
return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
|
||||
}
|
||||
|
|
|
@ -363,9 +363,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
struct scoped_set_relevancy {
|
||||
};
|
||||
|
||||
bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
|
||||
SASSERT(md != 0);
|
||||
m_root2value = &root2value;
|
||||
|
|
|
@ -188,7 +188,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void check_no_arithmetic(static_features const & st, char const * logic) {
|
||||
static void check_no_arithmetic(static_features const & st, char const * logic) {
|
||||
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
|
||||
throw default_exception("Benchmark constains arithmetic, but specified loging does not support it.");
|
||||
}
|
||||
|
@ -231,21 +231,21 @@ namespace smt {
|
|||
(st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9;
|
||||
}
|
||||
|
||||
bool is_in_diff_logic(static_features const & st) {
|
||||
static bool is_in_diff_logic(static_features const & st) {
|
||||
return
|
||||
st.m_num_arith_eqs == st.m_num_diff_eqs &&
|
||||
st.m_num_arith_terms == st.m_num_diff_terms &&
|
||||
st.m_num_arith_ineqs == st.m_num_diff_ineqs;
|
||||
}
|
||||
|
||||
bool is_diff_logic(static_features const & st) {
|
||||
static bool is_diff_logic(static_features const & st) {
|
||||
return
|
||||
is_in_diff_logic(st) &&
|
||||
(st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0)
|
||||
;
|
||||
}
|
||||
|
||||
void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
|
||||
static void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
|
||||
if (st.m_num_uninterpreted_functions != 0)
|
||||
throw default_exception("Benchmark contains uninterpreted function symbols, but specified logic does not support them.");
|
||||
}
|
||||
|
|
|
@ -53,26 +53,26 @@ struct aig {
|
|||
aig() {}
|
||||
};
|
||||
|
||||
inline bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
|
||||
inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
|
||||
inline bool is_var(aig * n) { return n->m_children[0].is_null(); }
|
||||
inline bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
|
||||
inline unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
|
||||
inline unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
|
||||
inline aig_lit left(aig * n) { return n->m_children[0]; }
|
||||
inline aig_lit right(aig * n) { return n->m_children[1]; }
|
||||
inline aig_lit left(aig_lit const & n) { return left(n.ptr()); }
|
||||
inline aig_lit right(aig_lit const & n) { return right(n.ptr()); }
|
||||
static bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
|
||||
static bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
|
||||
static bool is_var(aig * n) { return n->m_children[0].is_null(); }
|
||||
static bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
|
||||
static unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
|
||||
static unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
|
||||
static aig_lit left(aig * n) { return n->m_children[0]; }
|
||||
static aig_lit right(aig * n) { return n->m_children[1]; }
|
||||
static aig_lit left(aig_lit const & n) { return left(n.ptr()); }
|
||||
static aig_lit right(aig_lit const & n) { return right(n.ptr()); }
|
||||
|
||||
inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; }
|
||||
|
||||
void unmark(unsigned sz, aig_lit const * ns) {
|
||||
static void unmark(unsigned sz, aig_lit const * ns) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
ns[i].ptr()->m_mark = false;
|
||||
}
|
||||
}
|
||||
|
||||
void unmark(unsigned sz, aig * const * ns) {
|
||||
static void unmark(unsigned sz, aig * const * ns) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
ns[i]->m_mark = false;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue