From 949ad4d2fc454d0665c5c00abc91af877cf8d377 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 12:28:10 +0000 Subject: [PATCH] Trailing whitespace removed. --- src/cmd_context/cmd_context.cpp | 106 ++++++++++++++++---------------- src/shell/smtlib_frontend.cpp | 18 +++--- 2 files changed, 61 insertions(+), 63 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8648775ee..132418a11 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -131,11 +131,11 @@ bool func_decls::clash(func_decl * f) const { func_decl * g = *it; if (g == f) continue; - if (g->get_arity() != f->get_arity()) + if (g->get_arity() != f->get_arity()) continue; unsigned num = g->get_arity(); unsigned i; - for (i = 0; i < num; i++) + for (i = 0; i < num; i++) if (g->get_domain(i) != f->get_domain(i)) break; if (i == num) @@ -273,12 +273,12 @@ public: virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } - virtual bool uses(symbol const & s) const { - return + virtual bool uses(symbol const & s) const { + return m_owner.m_builtin_decls.contains(s) || m_owner.m_func_decls.contains(s); } - virtual format_ns::format * pp_sort(sort * s) { + virtual format_ns::format * pp_sort(sort * s) { return m_owner.pp(s); } virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len) { @@ -309,7 +309,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_main_ctx(main_ctx), m_logic(l), m_interactive_mode(false), - m_global_decls(false), + m_global_decls(false), m_print_success(m_params.m_smtlib2_compliant), m_random_seed(0), m_produce_unsat_cores(false), @@ -318,7 +318,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_numeral_as_real(false), m_ignore_check(false), m_exit_on_error(false), - m_manager(m), + m_manager(m), m_own_manager(m == 0), m_manager_initialized(false), m_pmanager(0), @@ -331,7 +331,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): install_core_tactic_cmds(*this); install_interpolant_cmds(*this); SASSERT(m != 0 || !has_manager()); - if (m_main_ctx) { + if (m_main_ctx) { set_verbose_stream(diagnostic_stream()); } } @@ -343,7 +343,7 @@ cmd_context::~cmd_context() { finalize_cmds(); finalize_tactic_cmds(); finalize_probes(); - reset(true); + reset(true); m_solver = 0; m_check_sat_result = 0; } @@ -351,7 +351,7 @@ cmd_context::~cmd_context() { void cmd_context::set_cancel(bool f) { if (m_solver) { if (f) { - m_solver->cancel(); + m_solver->cancel(); } else { m_solver->reset_cancel(); @@ -412,20 +412,20 @@ void cmd_context::set_produce_interpolants(bool f) { // set_solver_factory(mk_smt_solver_factory()); } -bool cmd_context::produce_models() const { +bool cmd_context::produce_models() const { return m_params.m_model; } -bool cmd_context::produce_proofs() const { +bool cmd_context::produce_proofs() const { return m_params.m_proof; } -bool cmd_context::produce_interpolants() const { +bool cmd_context::produce_interpolants() const { // FIXME currently synonym for produce_proofs return m_params.m_proof; } -bool cmd_context::produce_unsat_cores() const { +bool cmd_context::produce_unsat_cores() const { return m_params.m_unsat_core; } @@ -497,7 +497,7 @@ void cmd_context::load_plugin(symbol const & name, bool install, svector::iterator it = fids.begin(); svector::iterator end = fids.end(); for (; it != end; ++it) { @@ -686,8 +686,8 @@ void cmd_context::init_external_manager() { } bool cmd_context::supported_logic(symbol const & s) const { - return s == "QF_UF" || s == "UF" || - logic_has_arith_core(s) || logic_has_bv_core(s) || + return s == "QF_UF" || s == "UF" || + logic_has_arith_core(s) || logic_has_bv_core(s) || logic_has_array_core(s) || logic_has_seq_core(s) || logic_has_horn(s) || logic_has_fpa_core(s); } @@ -695,11 +695,11 @@ bool cmd_context::supported_logic(symbol const & s) const { bool cmd_context::set_logic(symbol const & s) { if (has_logic()) throw cmd_exception("the logic has already been set"); - if (has_manager() && m_main_ctx) - throw cmd_exception("logic must be set before initialization"); + if (has_manager() && m_main_ctx) + throw cmd_exception("logic must be set before initialization"); if (!supported_logic(s)) { if (m_params.m_smtlib2_compliant) { - return false; + return false; } else { warning_msg("unknown logic, ignoring set-logic command"); @@ -719,10 +719,10 @@ bool cmd_context::set_logic(symbol const & s) { return true; } -std::string cmd_context::reason_unknown() const { +std::string cmd_context::reason_unknown() const { if (m_check_sat_result.get() == 0) throw cmd_exception("state of the most recent check-sat command is not unknown"); - return m_check_sat_result->reason_unknown(); + return m_check_sat_result->reason_unknown(); } bool cmd_context::is_func_decl(symbol const & s) const { @@ -865,7 +865,7 @@ static builtin_decl const & peek_builtin_decl(builtin_decl const & first, family return first; } -func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, +func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, unsigned arity, sort * const * domain, sort * range) const { builtin_decl d; if (m_builtin_decls.find(s, d)) { @@ -891,7 +891,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, throw cmd_exception("invalid function declaration reference, invalid builtin reference ", s); return f; } - + if (m_macros.contains(s)) throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); @@ -907,7 +907,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, throw cmd_exception("invalid function declaration reference, unknown function ", s); return f; } - + psort_decl * cmd_context::find_psort_decl(symbol const & s) const { psort_decl * p = 0; m_psort_decls.find(s, p); @@ -1222,7 +1222,7 @@ void cmd_context::reset(bool finalize) { // reinit cmd_context if this is not a finalization step if (!finalize) init_external_manager(); - else + else m_manager_initialized = false; } } @@ -1272,14 +1272,14 @@ void cmd_context::push() { s.m_macros_stack_lim = m_macros_stack.size(); s.m_aux_pdecls_lim = m_aux_pdecls.size(); s.m_assertions_lim = m_assertions.size(); - if (m_solver) + if (m_solver) m_solver->push(); - if (m_opt) + if (m_opt) m_opt->push(); } void cmd_context::push(unsigned n) { - for (unsigned i = 0; i < n; i++) + for (unsigned i = 0; i < n; i++) push(); } @@ -1371,7 +1371,7 @@ void cmd_context::pop(unsigned n) { if (m_solver) { m_solver->pop(n); } - if (m_opt) + if (m_opt) m_opt->pop(n); unsigned new_lvl = lvl - n; scope & s = m_scopes[new_lvl]; @@ -1523,8 +1523,8 @@ void cmd_context::validate_check_sat_result(lbool r) { } } -void cmd_context::set_diagnostic_stream(char const * name) { - m_diagnostic.set(name); +void cmd_context::set_diagnostic_stream(char const * name) { + m_diagnostic.set(name); if (m_main_ctx) { set_warning_stream(&(*m_diagnostic)); set_verbose_stream(diagnostic_stream()); @@ -1536,15 +1536,15 @@ struct contains_array_op_proc { family_id m_array_fid; contains_array_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")) {} void operator()(var * n) {} - void operator()(app * n) { + void operator()(app * n) { if (n->get_family_id() != m_array_fid) return; decl_kind k = n->get_decl_kind(); - if (k == OP_AS_ARRAY || - k == OP_STORE || - k == OP_ARRAY_MAP || + if (k == OP_AS_ARRAY || + k == OP_STORE || + k == OP_ARRAY_MAP || k == OP_CONST_ARRAY) - throw found(); + throw found(); } void operator()(quantifier * n) {} }; @@ -1553,7 +1553,7 @@ struct contains_array_op_proc { \brief Check if the current model satisfies the quantifier free formulas. */ void cmd_context::validate_model() { - if (!validate_model_enabled()) + if (!validate_model_enabled()) return; if (!is_model_available()) return; @@ -1562,8 +1562,8 @@ void cmd_context::validate_model() { SASSERT(md.get() != 0); params_ref p; p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree. - p.set_uint("sort_store", true); - p.set_bool("completion", true); + p.set_uint("sort_store", true); + p.set_bool("completion", true); model_evaluator evaluator(*(md.get()), p); contains_array_op_proc contains_array(m()); { @@ -1612,8 +1612,6 @@ void cmd_context::mk_solver() { m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); } - - void cmd_context::set_interpolating_solver_factory(solver_factory * f) { SASSERT(!has_manager()); m_interpolating_solver_factory = f; @@ -1718,7 +1716,7 @@ void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const { void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const { format_ns::format_ref f(format_ns::fm(m())); f = pp(s); - if (indent > 0) + if (indent > 0) f = format_ns::mk_indent(m(), indent, f); ::pp(out, f.get(), m()); } @@ -1726,7 +1724,7 @@ void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const { void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const { format_ns::format_ref f(format_ns::fm(m())); pp(n, num_vars, var_prefix, f, var_names); - if (indent > 0) + if (indent > 0) f = format_ns::mk_indent(m(), indent, f); ::pp(out, f.get(), m()); } @@ -1739,7 +1737,7 @@ void cmd_context::display(std::ostream & out, expr * n, unsigned indent) const { void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) const { format_ns::format_ref f(format_ns::fm(m())); pp(d, f); - if (indent > 0) + if (indent > 0) f = format_ns::mk_indent(m(), indent, f); ::pp(out, f.get(), m()); } @@ -1763,7 +1761,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr } // TODO: display uninterpreted sort decls, and datatype decls. - + unsigned num_decls = decls.get_num_decls(); func_decl * const * fs = decls.get_func_decls(); for (unsigned i = 0; i < num_decls; i++) { @@ -1779,7 +1777,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr out << "(check-sat)" << std::endl; } -void cmd_context::slow_progress_sample() { +void cmd_context::slow_progress_sample() { SASSERT(m_solver); statistics st; regular_stream() << "(progress\n"; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index eb3b3587d..834fe4429 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -56,7 +56,7 @@ static void display_statistics() { } static void on_timeout() { - #pragma omp critical (g_display_stats) + #pragma omp critical (g_display_stats) { display_statistics(); exit(0); @@ -65,7 +65,7 @@ static void on_timeout() { static void on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) + #pragma omp critical (g_display_stats) { display_statistics(); } @@ -78,9 +78,9 @@ unsigned read_smtlib_file(char const * benchmark_file) { signal(SIGINT, on_ctrl_c); smtlib::solver solver; g_solver = &solver; - + bool ok = true; - + ok = solver.solve_smt(benchmark_file); if (!ok) { if (benchmark_file) { @@ -90,8 +90,8 @@ unsigned read_smtlib_file(char const * benchmark_file) { std::cerr << "ERROR: solving input stream.\n"; } } - - #pragma omp critical (g_display_stats) + + #pragma omp critical (g_display_stats) { display_statistics(); register_on_timeout_proc(0); @@ -117,7 +117,7 @@ unsigned read_smtlib2_commands(char const * file_name) { g_cmd_context = &ctx; signal(SIGINT, on_ctrl_c); - + bool result = true; if (file_name) { std::ifstream in(file_name); @@ -130,9 +130,9 @@ unsigned read_smtlib2_commands(char const * file_name) { else { result = parse_smt2_commands(ctx, std::cin, true); } - - #pragma omp critical (g_display_stats) + + #pragma omp critical (g_display_stats) { display_statistics(); g_cmd_context = 0;