From 8b6d7c0251722ba70b406759f935b7a8ea56fa37 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Sep 2017 17:34:51 +0100 Subject: [PATCH] Style, formatting --- src/ackermannization/ackr_model_converter.cpp | 61 ++++++++++--------- src/ackermannization/ackr_model_converter.h | 8 +-- 2 files changed, 35 insertions(+), 34 deletions(-) diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 0697686eb..b48ab9af4 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation Module Name: -ackr_model_converter.cpp + ackr_model_converter.cpp Abstract: Author: -Mikolas Janota + Mikolas Janota Revision History: --*/ @@ -22,8 +22,8 @@ Revision History: class ackr_model_converter : public model_converter { public: ackr_model_converter(ast_manager & m, - const ackr_info_ref& info, - model_ref& abstr_model) + const ackr_info_ref& info, + model_ref& abstr_model) : m(m) , info(info) , abstr_model(abstr_model) @@ -31,7 +31,7 @@ public: { } ackr_model_converter(ast_manager & m, - const ackr_info_ref& info) + const ackr_info_ref& info) : m(m) , info(info) , fixed_model(false) @@ -51,8 +51,6 @@ public: virtual void operator()(model_ref & md) { operator()(md, 0); } - //void display(std::ostream & out); - virtual model_converter * translate(ast_translation & translator) { ackr_info_ref retv_info = info->translate(translator); if (fixed_model) { @@ -63,22 +61,23 @@ public: return alloc(ackr_model_converter, translator.to(), retv_info); } } + protected: - ast_manager& m; + ast_manager & m; const ackr_info_ref info; model_ref abstr_model; bool fixed_model; void convert(model * source, model * destination); void add_entry(model_evaluator & evaluator, - app* term, expr* value, - obj_map& interpretations); + app* term, expr* value, + obj_map& interpretations); void convert_constants(model * source, model * destination); }; void ackr_model_converter::convert(model * source, model * destination) { destination->copy_func_interps(*source); destination->copy_usort_interps(*source); - convert_constants(source,destination); + convert_constants(source, destination); } void ackr_model_converter::convert_constants(model * source, model * destination) { @@ -89,16 +88,17 @@ void ackr_model_converter::convert_constants(model * source, model * destination func_decl * const c = source->get_constant(i); app * const term = info->find_term(c); expr * value = source->get_const_interp(c); - if(!term) { + if (!term) { destination->register_decl(c, value); - } else { + } + else { add_entry(evaluator, term, value, interpretations); } } obj_map::iterator e = interpretations.end(); for (obj_map::iterator i = interpretations.begin(); - i!=e; ++i) { + i != e; ++i) { func_decl* const fd = i->m_key; func_interp* const fi = i->get_value(); fi->set_else(m.get_some_value(fd->get_range())); @@ -107,34 +107,35 @@ void ackr_model_converter::convert_constants(model * source, model * destination } void ackr_model_converter::add_entry(model_evaluator & evaluator, - app* term, expr* value, - obj_map& interpretations) { + app* term, expr* value, + obj_map& interpretations) { TRACE("ackr_model", tout << "add_entry" - << mk_ismt2_pp(term, m, 2) - << "->" - << mk_ismt2_pp(value, m, 2) << "\n"; + << mk_ismt2_pp(term, m, 2) + << "->" + << mk_ismt2_pp(value, m, 2) << "\n"; ); - func_interp* fi = 0; + func_interp * fi = 0; func_decl * const declaration = term->get_decl(); const unsigned sz = declaration->get_arity(); SASSERT(sz == term->get_num_args()); - if (!interpretations.find(declaration, fi)) { - fi = alloc(func_interp,m,sz); - interpretations.insert(declaration, fi); + if (!interpretations.find(declaration, fi)) { + fi = alloc(func_interp, m, sz); + interpretations.insert(declaration, fi); } expr_ref_vector args(m); for (unsigned gi = 0; gi < sz; ++gi) { - expr * const arg = term->get_arg(gi); - expr_ref aarg(m); - info->abstract(arg, aarg); - expr_ref arg_value(m); - evaluator(aarg,arg_value); - args.push_back(arg_value); + expr * const arg = term->get_arg(gi); + expr_ref aarg(m); + info->abstract(arg, aarg); + expr_ref arg_value(m); + evaluator(aarg, arg_value); + args.push_back(arg_value); } if (fi->get_entry(args.c_ptr()) == 0) { fi->insert_new_entry(args.c_ptr(), value); - } else { + } + else { TRACE("ackr_model", tout << "entry already present\n";); } } diff --git a/src/ackermannization/ackr_model_converter.h b/src/ackermannization/ackr_model_converter.h index cee7472aa..659b45926 100644 --- a/src/ackermannization/ackr_model_converter.h +++ b/src/ackermannization/ackr_model_converter.h @@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation Module Name: -ackr_model_converter.h + ackr_model_converter.h Abstract: Author: -Mikolas Janota + Mikolas Janota Revision History: --*/ @@ -19,7 +19,7 @@ Revision History: #include "tactic/model_converter.h" #include "ackermannization/ackr_info.h" -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info); +model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model); +model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info); #endif /* LACKR_MODEL_CONVERTER_H_ */