From 3113901c8fecf70ce0284bce0797ab2f7013ee67 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 Sep 2018 23:15:57 -0700
Subject: [PATCH] rename is_atom
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/solver/solver.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 66fedb36f..1f0dac0ce 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -257,7 +257,7 @@ expr_ref_vector solver::get_units(ast_manager& m) {
return result;
}
-static bool is_atom(ast_manager& m, expr* f) {
+static bool is_m_atom(ast_manager& m, expr* f) {
if (!is_app(f)) return true;
app* _f = to_app(f);
family_id bfid = m.get_basic_family_id();
@@ -284,13 +284,13 @@ expr_ref_vector solver::get_non_units(ast_manager& m) {
if (_f->get_family_id() == bfid) {
// basic objects are true/false/and/or/not/=/distinct
// and proof objects (that are not Boolean).
- if (i < sz0 && m.is_not(f) && is_atom(m, _f->get_arg(0))) {
+ if (i < sz0 && m.is_not(f) && is_m_atom(m, _f->get_arg(0))) {
marked.mark(_f->get_arg(0));
}
else if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) {
fmls.append(_f->get_num_args(), _f->get_args());
}
- else if (i >= sz0 && is_atom(m, f)) {
+ else if (i >= sz0 && is_m_atom(m, f)) {
result.push_back(f);
}
}