From 6eaab00e83097a290cc2d6e43c4885c9a4a505c6 Mon Sep 17 00:00:00 2001 From: Fabian Wolff Date: Sat, 9 Jul 2016 11:46:43 +0200 Subject: [PATCH] Fix spelling errors --- src/ast/dl_decl_plugin.cpp | 2 +- src/ast/normal_forms/pull_quant.cpp | 4 ++-- src/ast/pp_params.pyg | 2 +- src/cmd_context/cmd_util.cpp | 2 +- src/cmd_context/cmd_util.h | 2 +- src/cmd_context/tactic_cmds.cpp | 2 +- src/math/subpaving/subpaving_t.h | 2 +- src/muz/base/dl_util.h | 2 +- src/muz/fp/datalog_parser.cpp | 4 ++-- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_context_pp.cpp | 4 ++-- src/tactic/arith/diff_neq_tactic.h | 2 +- src/tactic/probe.h | 2 +- src/tactic/sls/sls_tracker.h | 2 +- src/util/mpff.h | 2 +- 15 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 46f610c18..f7d6d9d1c 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -461,7 +461,7 @@ namespace datalog { return 0; } if (!ps.is_ast() || !is_sort(ps.get_ast()) || !is_fin_sort(to_sort(ps.get_ast()))) { - m_manager->raise_exception("second paramter should be a finite domain sort"); + m_manager->raise_exception("second parameter should be a finite domain sort"); return 0; } sort* s = to_sort(ps.get_ast()); diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index bb9b30dc5..74c7cafde 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -125,8 +125,8 @@ struct pull_quant::imp { // of nested_q->get_expr(). m_shift(nested_q->get_expr(), nested_q->get_num_decls(), // bound for shift1/shift2 - num_decls - nested_q->get_num_decls(), // shift1 (shift by this ammount if var idx >= bound) - shift_amount, // shift2 (shift by this ammount if var idx < bound) + num_decls - nested_q->get_num_decls(), // shift1 (shift by this amount if var idx >= bound) + shift_amount, // shift2 (shift by this amount if var idx < bound) adjusted_child); TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount << " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) << diff --git a/src/ast/pp_params.pyg b/src/ast/pp_params.pyg index d831cada9..46273b140 100644 --- a/src/ast/pp_params.pyg +++ b/src/ast/pp_params.pyg @@ -15,5 +15,5 @@ def_module_params('pp', ('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'), ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'), ('single_line', BOOL, False, 'ignore line breaks when true'), - ('bounded', BOOL, False, 'ignore characters exceeding max widht'), + ('bounded', BOOL, False, 'ignore characters exceeding max width'), ('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing'))) diff --git a/src/cmd_context/cmd_util.cpp b/src/cmd_context/cmd_util.cpp index 083493751..9774c75ff 100644 --- a/src/cmd_context/cmd_util.cpp +++ b/src/cmd_context/cmd_util.cpp @@ -6,7 +6,7 @@ Module Name: cmd_util.cpp Abstract: - Macros for definining new SMT2 front-end cmds. + Macros for defining new SMT2 front-end cmds. Author: diff --git a/src/cmd_context/cmd_util.h b/src/cmd_context/cmd_util.h index f0660af37..e575783f5 100644 --- a/src/cmd_context/cmd_util.h +++ b/src/cmd_context/cmd_util.h @@ -6,7 +6,7 @@ Module Name: cmd_util.h Abstract: - Macros for definining new SMT2 front-end cmds. + Macros for defining new SMT2 front-end cmds. Author: diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index f044c9736..86900e175 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -97,7 +97,7 @@ void help_tactic(cmd_context & ctx) { buf << "- (or-else +) tries the given tactics in sequence until one of them succeeds (i.e., the first that doesn't fail).\n"; buf << "- (par-or +) executes the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).\n"; buf << "- (par-then ) executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.\n"; - buf << "- (try-for ) excutes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds.\n"; + buf << "- (try-for ) executes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds.\n"; buf << "- (if ) if evaluates to true, then execute the first tactic. Otherwise execute the second.\n"; buf << "- (when ) shorthand for (if skip).\n"; buf << "- (fail-if ) fail if evaluates to true.\n"; diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index a6aa3cf32..ccef1a318 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -354,7 +354,7 @@ public: }; /** - \brief Watched element (aka occurence) can be: + \brief Watched element (aka occurrence) can be: - A clause - A definition (i.e., a variable) diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index 78ce453ec..b1719577b 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -591,7 +591,7 @@ namespace datalog { /** - \brief Remove the first occurence of \c el from \c v and return \c true. If + \brief Remove the first occurrence of \c el from \c v and return \c true. If \c el is not present in \c v, return \c false. The order of elements in \c v is not preserved. */ diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 41c0f77af..b51af7d53 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -480,7 +480,7 @@ protected: str2sort m_sort_dict; - // true if an error occured during the current call to the parse_stream + // true if an error occurred during the current call to the parse_stream // function bool m_error; public: @@ -896,7 +896,7 @@ protected: tok = m_lexer->next_token(); if (tok != TK_COLON) { tok = unexpected(tok, - "Expecting colon in declaration (first occurence of a predicate must be a declaration)"); + "Expecting colon in declaration (first occurrence of a predicate must be a declaration)"); return tok; } tok = m_lexer->next_token(); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 153d948f5..35652608c 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -13,7 +13,7 @@ def_module_params(module_name='smt', ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'), ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'), ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'), - ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'), + ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (0 means immediate timeout)'), diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index b0138f70c..ff45c5089 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -253,7 +253,7 @@ namespace smt { void context::display_app_enode_map(std::ostream & out) const { if (!m_e_internalized_stack.empty()) { - out << "expresion -> enode:\n"; + out << "expression -> enode:\n"; unsigned sz = m_e_internalized_stack.size(); for (unsigned i = 0; i < sz; i++) { expr * n = m_e_internalized_stack.get(i); @@ -265,7 +265,7 @@ namespace smt { void context::display_expr_bool_var_map(std::ostream & out) const { if (!m_b_internalized_stack.empty()) { - out << "expresion -> bool_var:\n"; + out << "expression -> bool_var:\n"; unsigned sz = m_b_internalized_stack.size(); for (unsigned i = 0; i < sz; i++) { expr * n = m_b_internalized_stack.get(i); diff --git a/src/tactic/arith/diff_neq_tactic.h b/src/tactic/arith/diff_neq_tactic.h index 5a5c24000..205fb7bb5 100644 --- a/src/tactic/arith/diff_neq_tactic.h +++ b/src/tactic/arith/diff_neq_tactic.h @@ -29,6 +29,6 @@ class tactic; tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p = params_ref()); /* - ADD_TACTIC("diff-neq", "specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numberal, and all constants are bounded.", "mk_diff_neq_tactic(m, p)") + ADD_TACTIC("diff-neq", "specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numeral, and all constants are bounded.", "mk_diff_neq_tactic(m, p)") */ #endif diff --git a/src/tactic/probe.h b/src/tactic/probe.h index a4754f8ed..3f7229d36 100644 --- a/src/tactic/probe.h +++ b/src/tactic/probe.h @@ -62,7 +62,7 @@ probe * mk_depth_probe(); probe * mk_size_probe(); /* - ADD_PROBE("memory", "ammount of used memory in megabytes.", "mk_memory_probe()") + ADD_PROBE("memory", "amount of used memory in megabytes.", "mk_memory_probe()") ADD_PROBE("depth", "depth of the input goal.", "mk_depth_probe()") ADD_PROBE("size", "number of assertions in the given goal.", "mk_size_probe()") */ diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 39d76bee6..dfdbd4685 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -464,7 +464,7 @@ public: if (!m_weights.contains(e)) m_weights.insert(e, m_paws_init); - // positive/negative occurences used for early pruning + // positive/negative occurrences used for early pruning setup_occs(as[i]); } diff --git a/src/util/mpff.h b/src/util/mpff.h index a4cab898c..eadfa0390 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -94,7 +94,7 @@ class mpff_manager { // // - All values of type int, unsigned, int64 and uint64 can be precisely represented as mpff numerals. // - // - Hardware float and double values (corresponding to rationals) can also be precisely represented as mpff numberals. + // - Hardware float and double values (corresponding to rationals) can also be precisely represented as mpff numerals. // That is, NaN, +oo and -oo are not supported by this module. // // - An exception (mpff_manager::exception) is thrown if overflow occurs. This can happen because the exponent is