Method is_value

src/ast/array_decl_plugin.cpp:560–575

}

bool array_decl_plugin::is_value(app * _e) const {
    expr* e = _e;
    array_util u(*m_manager);
    while (true) {
        if (u.is_const(e, e))
            return m_manager->is_value(e);
        if (u.is_store(e)) {            
            for (unsigned i = 1; i < to_app(e)->get_num_args(); ++i)
                if (!m_manager->is_value(to_app(e)->get_arg(i)))
                    return false;
            e = to_app(e)->get_arg(0);
            continue;
        }
        return false;
    }
}

bool array_decl_plugin::is_unique_value(app* _e) const {
    array_util u(*m_manager);