From 31496b662548844350d1468d5a7e51502131589b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 25 Aug 2017 15:29:29 +0100 Subject: [PATCH] Whitespace --- src/ast/macros/quasi_macros.h | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h index 3a9b6074e..849fe8bce 100644 --- a/src/ast/macros/quasi_macros.h +++ b/src/ast/macros/quasi_macros.h @@ -34,22 +34,22 @@ class quasi_macros { macro_manager & m_macro_manager; simplifier & m_simplifier; occurrences_map m_occurrences; - ptr_vector m_todo; + ptr_vector m_todo; vector m_new_var_names; expr_ref_vector m_new_vars; expr_ref_vector m_new_eqs; sort_ref_vector m_new_qsorts; - std::stringstream m_new_name; + std::stringstream m_new_name; expr_mark m_visited_once; expr_mark m_visited_more; - + bool is_unique(func_decl * f) const; bool is_non_ground_uninterp(expr const * e) const; - bool fully_depends_on(app * a, quantifier * q) const; + bool fully_depends_on(app * a, quantifier * q) const; bool depends_on(expr * e, func_decl * f) const; - bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const; + bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const; void quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro); void find_occurrences(expr * e); @@ -59,11 +59,11 @@ class quasi_macros { public: quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s); ~quasi_macros(); - + /** \brief Find pure function macros and apply them. */ - bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); }; #endif