mirror of
https://github.com/Z3Prover/z3
synced 2026-07-20 22:15:49 +00:00
6ac3075022
This is another PR towards the goal of getting Z3 to compile cleanly when included via FetchContents into clang-tidy, which uses a pretty strict set of warnings. This is a second version of https://github.com/Z3Prover/z3/pull/9957. I address @NikolajBjorner 's comments about not changing the semicolons after macro invocations, because some editors work better with them present. It now, to the best of my ability, only deletes semis: * after the closing brace of namespace decl. * after the closing brace of an extern "C" decl. * after a function definition. This PR is very large, but it consists entirely of deletions of semicolons in these situations. (If there was a way to update the previous PR, which had been closed, and that is preferable, please let me know. I couldn't figure it out.)
110 lines
2.8 KiB
C++
110 lines
2.8 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
smt_for_each_relevant_expr.h
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2009-01-05.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "ast/ast.h"
|
|
#include "util/obj_hashtable.h"
|
|
#include "util/vector.h"
|
|
|
|
namespace smt {
|
|
|
|
class context;
|
|
|
|
|
|
class check_at_labels {
|
|
ast_manager & m_manager;
|
|
bool m_first;
|
|
unsigned count_at_labels_pos(expr* n);
|
|
unsigned count_at_labels_neg(expr* n);
|
|
unsigned count_at_labels_lit(expr* n, bool polarity);
|
|
|
|
public:
|
|
check_at_labels(ast_manager& m) : m_manager(m) {}
|
|
|
|
/**
|
|
\brief Check that 'n' as a formula contains at most one @ label within each and-or path.
|
|
*/
|
|
|
|
bool check(expr* cnstr);
|
|
};
|
|
/**
|
|
\brief Functor used to traverse the relevant expressions in a logical context.
|
|
*/
|
|
class for_each_relevant_expr {
|
|
protected:
|
|
ast_manager & m_manager;
|
|
context & m_context;
|
|
obj_hashtable<expr> m_cache;
|
|
ptr_vector<expr> m_todo;
|
|
bool m_first;
|
|
|
|
void process_app(app * n);
|
|
void process_relevant_child(app * n, lbool val);
|
|
void process_and(app * n);
|
|
void process_or(app * n);
|
|
void process_ite(app * n);
|
|
lbool get_assignment(expr * n);
|
|
bool is_relevant(expr * n);
|
|
|
|
|
|
public:
|
|
for_each_relevant_expr(context & ctx);
|
|
virtual ~for_each_relevant_expr() = default;
|
|
/**
|
|
\brief Visit the relevant sub-expressions of n.
|
|
That is, only subexpressions m of n, such that m_context.is_relevant(m).
|
|
This method also tries to minimize the number of subexpressions visited.
|
|
For each visited expression the method operator() is invoked.
|
|
Only not-already-visited expressions are visited.
|
|
*/
|
|
void process(expr * n);
|
|
|
|
/**
|
|
\see process
|
|
*/
|
|
virtual void operator()(expr * n);
|
|
/**
|
|
\brief Reset the cache of already visited expressions.
|
|
*/
|
|
void reset();
|
|
};
|
|
|
|
class collect_relevant_label_lits : public for_each_relevant_expr {
|
|
buffer<symbol> & m_buffer;
|
|
public:
|
|
collect_relevant_label_lits(context & ctx, buffer<symbol> & b):
|
|
for_each_relevant_expr(ctx),
|
|
m_buffer(b) {
|
|
}
|
|
void operator()(expr * n) override;
|
|
};
|
|
|
|
class collect_relevant_labels : public for_each_relevant_expr {
|
|
buffer<symbol> & m_buffer;
|
|
public:
|
|
collect_relevant_labels(context & ctx, buffer<symbol> & b):
|
|
for_each_relevant_expr(ctx),
|
|
m_buffer(b) {
|
|
}
|
|
void operator()(expr * n) override;
|
|
};
|
|
|
|
}
|
|
|
|
|