diff --git a/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake index 36fe82bb3..a8006e2d3 100644 --- a/cmake/msvc_legacy_quirks.cmake +++ b/cmake/msvc_legacy_quirks.cmake @@ -8,13 +8,13 @@ # FIXME: All the commented out defines should be removed once # we are confident it is correct to not set them. set(Z3_MSVC_LEGACY_DEFINES - # Don't set `_DEBUG`. The old build sytem sets this but this + # Don't set `_DEBUG`. The old build system sets this but this # is wrong. MSVC will set this depending on which runtime is being used. # See https://msdn.microsoft.com/en-us/library/b0084kay.aspx # _DEBUG # The old build system only set `UNICODE` and `_UNICODE` for x86_64 release. - # That seems completly wrong so set it for all configurations. + # That seems completely wrong so set it for all configurations. # According to https://blogs.msdn.microsoft.com/oldnewthing/20040212-00/?p=40643/ # `UNICODE` affects Windows headers and `_UNICODE` affects C runtime header files. # There is some discussion of this define at https://msdn.microsoft.com/en-us/library/dybsewaf.aspx @@ -116,7 +116,7 @@ z3_add_cxx_flag("/analyze-" REQUIRED) ################################################################################ # By default CMake enables incremental linking for Debug and RelWithDebInfo -# builds. The old build sytem disables it for all builds so try to do the same +# builds. The old build system disables it for all builds so try to do the same # by changing all configurations if necessary string(TOUPPER "${available_build_types}" _build_types_as_upper) foreach (_build_type ${_build_types_as_upper}) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index d87ffbe61..8ab6e045d 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -7,7 +7,7 @@ function(z3_expand_dependencies output_var) if (ARGC LESS 2) message(FATAL_ERROR "Invalid number of arguments") endif() - # Remaing args should be component names + # Remaining args should be component names set(_expanded_deps ${ARGN}) set(_old_number_of_deps 0) list(LENGTH _expanded_deps _number_of_deps) @@ -33,7 +33,7 @@ function(z3_add_component_dependencies_to_target target_name) if (NOT (TARGET ${target_name})) message(FATAL_ERROR "Target \"${target_name}\" does not exist") endif() - # Remaing args should be component names + # Remaining args should be component names set(_expanded_deps ${ARGN}) foreach (dependency ${_expanded_deps}) # Ensure this component's dependencies are built before this component. @@ -219,7 +219,7 @@ macro(z3_add_component component_name) # Record this component's dependencies foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES}) if (NOT (TARGET ${dependency})) - message(FATAL_ERROR "Component \"${component_name}\" depends on a non existant component \"${dependency}\"") + message(FATAL_ERROR "Component \"${component_name}\" depends on a non existent component \"${dependency}\"") endif() set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_DEPS "${dependency}") endforeach() diff --git a/contrib/ci/README.md b/contrib/ci/README.md index bd1c52792..d0f336f92 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -1,4 +1,4 @@ -# Continous integration scripts +# Continuous integration scripts ## TravisCI @@ -45,7 +45,7 @@ the future. * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) * `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`) * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. -* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option pased to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) +* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) ### Linux diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 9c4b464c2..e58b561c9 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -944,7 +944,7 @@ HTML_STYLESHEET = # user-defined cascading style sheet that is included after the standard # style sheets created by doxygen. Using this option one can overrule # certain style aspects. This is preferred over using HTML_STYLESHEET -# since it does not replace the standard style sheet and is therefor more +# since it does not replace the standard style sheet and is therefore more # robust against future updates. Doxygen will copy the style sheet file to # the output directory. @@ -1711,7 +1711,7 @@ UML_LOOK = NO # the class node. If there are many fields or methods and many nodes the # graph may become too big to be useful. The UML_LIMIT_NUM_FIELDS # threshold limits the number of items for each type to make the size more -# managable. Set this to 0 for no limit. Note that the threshold may be +# manageable. Set this to 0 for no limit. Note that the threshold may be # exceeded by 50% before the limit is enforced. UML_LIMIT_NUM_FIELDS = 10 diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt index 0a41d6a93..52758889d 100644 --- a/examples/c++/CMakeLists.txt +++ b/examples/c++/CMakeLists.txt @@ -7,8 +7,8 @@ find_package(Z3 REQUIRED CONFIG # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. - # This should prevent us from accidently picking up an installed - # copy of Z3. This is here to benefit Z3's build sytem when building + # This should prevent us from accidentally picking up an installed + # copy of Z3. This is here to benefit Z3's build system when building # this project. When making your own project you probably shouldn't # use this option. NO_DEFAULT_PATH diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt index c47a4947a..e45c82d37 100644 --- a/examples/c/CMakeLists.txt +++ b/examples/c/CMakeLists.txt @@ -24,8 +24,8 @@ find_package(Z3 REQUIRED CONFIG # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. - # This should prevent us from accidently picking up an installed - # copy of Z3. This is here to benefit Z3's build sytem when building + # This should prevent us from accidentally picking up an installed + # copy of Z3. This is here to benefit Z3's build system when building # this project. When making your own project you probably shouldn't # use this option. NO_DEFAULT_PATH diff --git a/examples/maxsat/CMakeLists.txt b/examples/maxsat/CMakeLists.txt index 019243ecf..e59486297 100644 --- a/examples/maxsat/CMakeLists.txt +++ b/examples/maxsat/CMakeLists.txt @@ -11,8 +11,8 @@ find_package(Z3 REQUIRED CONFIG # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. - # This should prevent us from accidently picking up an installed - # copy of Z3. This is here to benefit Z3's build sytem when building + # This should prevent us from accidentally picking up an installed + # copy of Z3. This is here to benefit Z3's build system when building # this project. When making your own project you probably shouldn't # use this option. NO_DEFAULT_PATH diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs index 1c82406be..5297d3e67 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs @@ -226,7 +226,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 } /// - /// Adds a MSF variable with the coresponding assertion to the Z3 variables. + /// Adds a MSF variable with the corresponding assertion to the Z3 variables. /// /// The MSF id of the variable internal void AddVariable(int vid) diff --git a/examples/tptp/CMakeLists.txt b/examples/tptp/CMakeLists.txt index 8e8dfb8ea..7870e5408 100644 --- a/examples/tptp/CMakeLists.txt +++ b/examples/tptp/CMakeLists.txt @@ -7,8 +7,8 @@ find_package(Z3 REQUIRED CONFIG # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. - # This should prevent us from accidently picking up an installed - # copy of Z3. This is here to benefit Z3's build sytem when building + # This should prevent us from accidentally picking up an installed + # copy of Z3. This is here to benefit Z3's build system when building # this project. When making your own project you probably shouldn't # use this option. NO_DEFAULT_PATH diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index facbf6c0a..882c2bbe2 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -233,7 +233,7 @@ class env { void check_arity(unsigned num_args, unsigned arity) { if (num_args != arity) { - throw failure_ex("arity missmatch"); + throw failure_ex("arity mismatch"); } } diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 97e2b65f2..0657a2686 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3276,7 +3276,7 @@ class MakeRuleCmd(object): needed commands used in Makefile rules Note that several of the method are meant for use during ``make install`` and ``make uninstall``. These methods correctly use - ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable + ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable to writing commands manually which can be error prone. """ @classmethod diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 420fbda10..df0aac15e 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -276,7 +276,7 @@ struct lackr_model_constructor::imp { SASSERT(a->get_num_args() == 0); func_decl * const fd = a->get_decl(); expr * val = m_abstr_model->get_const_interp(fd); - if (val == nullptr) { // TODO: avoid model completetion? + if (val == nullptr) { // TODO: avoid model completion? sort * s = fd->get_range(); val = m_abstr_model->get_some_value(s); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 4b3b85399..c236ba3e8 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -219,7 +219,7 @@ namespace api { if (m_user_ref_count) { // Corner case bug: n may be in m_last_result, and this is the only reference to n. // When, we execute reset() it is deleted - // To avoid this bug, I bump the reference counter before reseting m_last_result + // To avoid this bug, I bump the reference counter before resetting m_last_result ast_ref node(n, m()); m_last_result.reset(); m_last_result.push_back(std::move(node)); diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index c2f437391..06207cee6 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -210,7 +210,7 @@ extern "C" { if (!out) { return Z3_FALSE; } - // must start loggging here, since function uses Z3_get_sort_kind above + // must start logging here, since function uses Z3_get_sort_kind above LOG_Z3_get_finite_domain_sort_size(c, s, out); RESET_ERROR_CODE(); VERIFY(mk_c(c)->datalog_util().try_get_size(to_sort(s), *out)); diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs index b6beaef0c..1c42fd78a 100644 --- a/src/api/dotnet/ArithExpr.cs +++ b/src/api/dotnet/ArithExpr.cs @@ -45,7 +45,7 @@ namespace Microsoft.Z3 private static ArithExpr MkNum(ArithExpr e, double d) { return (ArithExpr)e.Context.MkNumeral(d.ToString(), e.Context.MkRealSort()); } - /// Operator overloading for arithmetical divsion operator (over reals) + /// Operator overloading for arithmetical division operator (over reals) public static ArithExpr operator /(ArithExpr a, ArithExpr b) { return a.Context.MkDiv(a, b); } /// Operator overloading for arithmetical operator diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index c8decb59b..ef85a8713 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2459,7 +2459,7 @@ namespace Microsoft.Z3 #endregion - #region Sequence, string and regular expresions + #region Sequence, string and regular expressions /// /// Create the empty sequence. @@ -3131,7 +3131,7 @@ namespace Microsoft.Z3 /// /// Create a bit-vector numeral. /// - /// An array of bits representing the bit-vector. Least signficant bit is at position 0. + /// An array of bits representing the bit-vector. Least significant bit is at position 0. public BitVecNum MkBV(bool[] bits) { Contract.Ensures(Contract.Result() != null); diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 99baaa8e4..5d1896221 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -842,7 +842,7 @@ namespace Microsoft.Z3 public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } /// - /// Check whether expression is a concatentation. + /// Check whether expression is a concatenation. /// /// a Boolean public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } } diff --git a/src/api/python/z3/z3util.py b/src/api/python/z3/z3util.py index fe7e76b86..6e5165c9a 100644 --- a/src/api/python/z3/z3util.py +++ b/src/api/python/z3/z3util.py @@ -199,7 +199,7 @@ def prove(claim,assume=None,verbose=0): >>> r,m = prove(True,assume=And(x,Not(x)),verbose=0) Traceback (most recent call last): ... - AssertionError: Assumption is alway False! + AssertionError: Assumption is always False! >>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False) assume: @@ -238,7 +238,7 @@ def prove(claim,assume=None,verbose=0): is_proved,_ = prove(Not(assume)) def _f(): - emsg = "Assumption is alway False!" + emsg = "Assumption is always False!" if verbose >= 2: emsg = "{}\n{}".format(assume,emsg) return emsg diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b02b3eb3b..de446d9a8 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3772,7 +3772,7 @@ extern "C" { ); /** - \brief Create a lambda expression. It taks an expression \c body that contains bound variables + \brief Create a lambda expression. It takes an expression \c body that contains bound variables of the same sorts as the sorts listed in the array \c sorts. The bound variables are de-Bruijn indices created using #Z3_mk_bound. The array \c decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the \c decl_names and \c sorts array @@ -4609,7 +4609,7 @@ extern "C" { Z3_bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a); /** - \brief Determine if ast is a lambda expresion. + \brief Determine if ast is a lambda expression. \pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST @@ -5996,7 +5996,7 @@ extern "C" { Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target); /** - \brief Ad-hoc method for importing model convertion from solver. + \brief Ad-hoc method for importing model conversion from solver. def_API('Z3_solver_import_model_converter', VOID, (_in(CONTEXT), _in(SOLVER), _in(SOLVER))) */ @@ -6215,7 +6215,7 @@ extern "C" { The third argument is a vector of variables that may be used for cubing. The contents of the vector is only used in the first call. The initial list of variables is used in subsequent calls until it returns the unsatisfiable cube. - The vector is modified to contain a set of Autarky variables that occor in clauses that + The vector is modified to contain a set of Autarky variables that occur in clauses that are affected by the (last literal in the) cube. These variables could be used by a different cuber (on a different solver object) for further recursive cubing. diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index 23c2205bb..a45c65d82 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -123,7 +123,7 @@ inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args. /** Return a if arg = (not a) - Retur (not arg) otherwise + Return (not arg) otherwise */ expr * mk_not(ast_manager & m, expr * arg); diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index b2614e27d..7195f7179 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -31,7 +31,7 @@ fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, m_bindings(m) { updt_params(p); - // We need to make sure that the mananger has the BV plugin loaded. + // We need to make sure that the manager has the BV plugin loaded. symbol s_bv("bv"); if (!m_manager.has_plugin(s_bv)) m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); diff --git a/src/ast/func_decl_dependencies.h b/src/ast/func_decl_dependencies.h index b813dc31f..9bc0be22d 100644 --- a/src/ast/func_decl_dependencies.h +++ b/src/ast/func_decl_dependencies.h @@ -58,7 +58,7 @@ public: void reset(); /** - \brief Create a dependecy set. + \brief Create a dependency set. This set should be populated using #collect_func_decls. After populating the set, it must be used as an argument for the #insert method. diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index ee1b77545..c91f19df8 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -263,7 +263,7 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) { m_occurrences.reset(); - // Find out how many non-ground appearences for each uninterpreted function there are + // Find out how many non-ground appearances for each uninterpreted function there are for (unsigned i = 0 ; i < n ; i++) find_occurrences(exprs[i]); @@ -301,7 +301,7 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { m_occurrences.reset(); - // Find out how many non-ground appearences for each uninterpreted function there are + // Find out how many non-ground appearances for each uninterpreted function there are for ( unsigned i = 0 ; i < n ; i++ ) find_occurrences(exprs[i].get_fml()); diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index f6c8788d0..cf3c8bc31 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -687,7 +687,7 @@ bool pattern_inference_cfg::reduce_quantifier( mk_patterns(result2->get_num_decls(), result2->get_expr(), 0, nullptr, new_patterns); if (!new_patterns.empty()) { if (m_params.m_pi_warnings) { - warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str()); + warning_msg("pulled nested quantifier to be able to find an usable pattern (quantifier id: %s)", q->get_qid().str().c_str()); } new_q = m.update_quantifier(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr()); if (m.proofs_enabled()) { diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index c81c7385a..81226b010 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2679,7 +2679,7 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu } const unsigned sz = m_util.get_bv_size(rhs); - if (sz == 1) { // detect (lhs = N) ? C : D, where N, C, D are 1 bit numberals + if (sz == 1) { // detect (lhs = N) ? C : D, where N, C, D are 1 bit numerals numeral rhs_n, e_n, t_n; unsigned rhs_sz, e_sz, t_sz; if (is_numeral(rhs, rhs_n, rhs_sz) diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp index 194668b9c..4d688e682 100644 --- a/src/ast/rewriter/datatype_rewriter.cpp +++ b/src/ast/rewriter/datatype_rewriter.cpp @@ -124,7 +124,7 @@ br_status datatype_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & resul // (= (+ c5 a5) b5) <<< NOT SIMPLIFIED WITH RESPECT TO ARITHMETIC // (= (cons a6 nil) (cons b6 nil))) <<< NOT SIMPLIFIED WITH RESPECT TO DATATYPE theory // - // Note that asserted_formulas::reduce() applied the simplier many times. + // Note that asserted_formulas::reduce() applied the simplifier many times. // After the first simplification step we had: // (= a1 b1) // (= (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil)))))) diff --git a/src/ast/rewriter/der.h b/src/ast/rewriter/der.h index 47e57c4fb..4dcf1e537 100644 --- a/src/ast/rewriter/der.h +++ b/src/ast/rewriter/der.h @@ -108,7 +108,7 @@ Revision History: apply var_subst using m_map to this child, and store the result in a new children array Create a new OR (new body of the quantifier) using the new children Then, we create a new quantifier using this new body, and use the function elim_unused_vars to - eliminate the ununsed variables. + eliminate the unused variables. Remark: let us implement the new version inside the class der. Use #if 0 ... #endif to comment the old version. diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h index 8f737ea4d..a04cb6fbc 100644 --- a/src/ast/rewriter/push_app_ite.h +++ b/src/ast/rewriter/push_app_ite.h @@ -41,7 +41,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg { \brief Variation of push_app_ite that applies the transformation on nonground terms only. \remark This functor uses the app::is_ground method. This method is not - completly precise, for instance, any term containing a quantifier is marked as non ground. + completely precise, for instance, any term containing a quantifier is marked as non ground. */ class ng_push_app_ite_cfg : public push_app_ite_cfg { protected: diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index cf0fd5111..a89e76edb 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -85,7 +85,7 @@ ATOMIC_CMD(get_user_tactics_cmd, "get-user-tactics", "display tactics defined us void help_tactic(cmd_context & ctx) { std::ostringstream buf; buf << "combinators:\n"; - buf << "- (and-then +) executes the given tactics sequencially.\n"; + buf << "- (and-then +) executes the given tactics sequentially.\n"; 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"; diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp index 70b424375..4b65ab6ea 100644 --- a/src/math/euclid/euclidean_solver.cpp +++ b/src/math/euclid/euclidean_solver.cpp @@ -690,7 +690,7 @@ struct euclidean_solver::imp { m().del(eq.m_as[j]); eq.m_as.shrink(new_sz); eq.m_xs.shrink(new_sz); - // ajust c + // adjust c mpz new_c; decompose(m_next_pos_a, m_next_a, eq.m_c, new_c, eq.m_c); // create auxiliary equation diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 528c10537..17360f35b 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -948,7 +948,7 @@ namespace algebraic_numbers { // zero is a root of p, and r_i is an isolating interval containing zero, // then c is zero reset(c); - TRACE("algebraic", tout << "reseting\nresult: "; display_root(tout, c); tout << "\n";); + TRACE("algebraic", tout << "resetting\nresult: "; display_root(tout, c); tout << "\n";); return; } int zV = upm().sign_variations_at_zero(seq); @@ -1728,7 +1728,7 @@ namespace algebraic_numbers { COMPARE_INTERVAL(); // if cell_a and cell_b, contain the same polynomial, - // and the intervals are overlaping, then they are + // and the intervals are overlapping, then they are // the same root. if (compare_p(cell_a, cell_b)) { m_compare_poly_eq++; @@ -1825,7 +1825,7 @@ namespace algebraic_numbers { // Here is an unexplored option for comparing numbers. // - // The isolating intervals of a and b are still overlaping + // The isolating intervals of a and b are still overlapping // Then we compute // r(x) = Resultant(x - y1 + y2, p1(y1), p2(y2)) // where p1(y1) and p2(y2) are the polynomials defining a and b. diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 00a4d0593..aec901f61 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -4052,7 +4052,7 @@ namespace polynomial { // select a new random value in GF(p) that is not in vals, and store it in r void peek_fresh(scoped_numeral_vector const & vals, unsigned p, scoped_numeral & r) { - SASSERT(vals.size() < p); // otherwise we cant keep the fresh value + SASSERT(vals.size() < p); // otherwise we can't keep the fresh value unsigned sz = vals.size(); while (true) { m().set(r, rand() % p); @@ -4149,7 +4149,7 @@ namespace polynomial { TRACE("mgcd_detail", tout << "counter: " << counter << "\nidx: " << idx << "\nq: " << q << "\ndeg_q: " << deg_q << "\nmin_deg_q: " << min_deg_q << "\nnext_x: x" << vars[idx+1] << "\nmax_var(q): " << q_var << "\n";); if (deg_q < min_deg_q) { - TRACE("mgcd_detail", tout << "reseting...\n";); + TRACE("mgcd_detail", tout << "resetting...\n";); counter = 0; min_deg_q = deg_q; // start from scratch diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 374a51084..169ee8273 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -131,12 +131,12 @@ namespace polynomial { ~factors(); /** - \brief Numer of distinct factors (not counting multiplicities). + \brief Number of distinct factors (not counting multiplicities). */ unsigned distinct_factors() const { return m_factors.size(); } /** - \brief Numer of distinct factors (counting multiplicities). + \brief Number of distinct factors (counting multiplicities). */ unsigned total_factors() const { return m_total_factors; } diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index cc2442981..39bdb6812 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -362,7 +362,7 @@ namespace upolynomial { set_size(sz-1, buffer); } - // Divide coeffients of p by their GCD + // Divide coefficients of p by their GCD void core_manager::normalize(unsigned sz, numeral * p) { if (sz == 0) return; @@ -395,7 +395,7 @@ namespace upolynomial { } } - // Divide coeffients of p by their GCD + // Divide coefficients of p by their GCD void core_manager::normalize(numeral_vector & p) { normalize(p.size(), p.c_ptr()); } @@ -568,7 +568,7 @@ namespace upolynomial { SASSERT(!is_alias(p1, buffer)); SASSERT(!is_alias(p2, buffer)); unsigned d; rem(sz1, p1, sz2, p2, d, buffer); - // We don't ned to flip the sign if d is odd and leading coefficient of p2 is negative + // We don't need to flip the sign if d is odd and leading coefficient of p2 is negative if (d % 2 == 0 || (sz2 > 0 && m().is_pos(p2[sz2-1]))) neg(buffer.size(), buffer.c_ptr()); } @@ -2005,7 +2005,7 @@ namespace upolynomial { continue; bool pos_a_n_k = m().is_pos(a_n_k); if (pos_a_n_k == pos_a_n) - continue; // must have oposite signs + continue; // must have opposite signs unsigned log2_a_n_k = pos_a_n_k ? m().log2(a_n_k) : m().mlog2(a_n_k); if (log2_a_n > log2_a_n_k) continue; @@ -2103,7 +2103,7 @@ namespace upolynomial { frame_stack.pop_back(); } - // Auxiliar method for isolating the roots of p in the interval (0, 1). + // Auxiliary method for isolating the roots of p in the interval (0, 1). // The basic idea is to split the interval in: (0, 1/2) and (1/2, 1). // This is accomplished by analyzing the roots in the interval (0, 1) of the following polynomials. // p1(x) := 2^n * p(x/2) where n = sz-1 @@ -2574,10 +2574,10 @@ namespace upolynomial { We say an interval (a, b) of a polynomial p is ISOLATING if p has only one root in the interval (a, b). - We say an isolating interval (a, b) of a square free polynomial p is REFINEABLE if + We say an isolating interval (a, b) of a square free polynomial p is REFINABLE if sign(p(a)) = -sign(p(b)) - Not every isolating interval (a, b) of a square free polynomial p is refineable, because + Not every isolating interval (a, b) of a square free polynomial p is refinable, because sign(p(a)) or sign(p(b)) may be zero. Refinable intervals of square free polynomials are useful, because we can increase precision diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index 439b4be9f..ad6942ffb 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -256,12 +256,12 @@ namespace upolynomial { void derivative(numeral_vector const & p, numeral_vector & d_p) { derivative(p.size(), p.c_ptr(), d_p); } /** - \brief Divide coeffients of p by their GCD + \brief Divide coefficients of p by their GCD */ void normalize(unsigned sz, numeral * p); /** - \brief Divide coeffients of p by their GCD + \brief Divide coefficients of p by their GCD */ void normalize(numeral_vector & p); diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h index e422c15a6..10bfb4d8b 100644 --- a/src/math/polynomial/upolynomial_factorization_int.h +++ b/src/math/polynomial/upolynomial_factorization_int.h @@ -195,7 +195,7 @@ namespace upolynomial { // the index we are currently trying to fix int current_i = m_current_size - 1; - // the value we found as plausable (-1 we didn't find anything) + // the value we found as plausible (-1 we didn't find anything) int current_value = -1; if (remove_current) { diff --git a/src/math/realclosure/mpz_matrix.h b/src/math/realclosure/mpz_matrix.h index 92716ec0d..99ff8bce4 100644 --- a/src/math/realclosure/mpz_matrix.h +++ b/src/math/realclosure/mpz_matrix.h @@ -107,7 +107,7 @@ public: this method will give preference to the row that occurs first. \remark The vector r must have at least A.n() capacity - The numer of linear independent rows is returned. + The number of linear independent rows is returned. Store the new matrix in B. */ diff --git a/src/math/realclosure/rcf_params.pyg b/src/math/realclosure/rcf_params.pyg index 36c13035b..fc15dbe93 100644 --- a/src/math/realclosure/rcf_params.pyg +++ b/src/math/realclosure/rcf_params.pyg @@ -6,5 +6,5 @@ def_module_params('rcf', ('initial_precision', UINT, 24, "a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division"), ('inf_precision', UINT, 24, "a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values"), ('max_precision', UINT, 128, "during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision"), - ('lazy_algebraic_normalization', BOOL, True, "during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the definining polynomial is monic") + ('lazy_algebraic_normalization', BOOL, True, "during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the defining polynomial is monic") )) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index d41937c29..77623a2df 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -4790,7 +4790,7 @@ namespace realclosure { /** \brief Determine the sign of the new rational function value. - The idea is to keep refinining the interval until interval of v does not contain 0. + The idea is to keep refining the interval until interval of v does not contain 0. After a couple of steps we switch to expensive sign determination procedure. Return false if v is actually zero. @@ -5474,7 +5474,7 @@ namespace realclosure { } else { // Let sdt be alpha->sdt(); - // In pricipal, the signs of the polynomials sdt->qs can be used + // In principal, the signs of the polynomials sdt->qs can be used // to discriminate the roots of new_p. The signs of this polynomials // depend only on alpha, and not on the polynomial used to define alpha // So, in principle, we can reuse m_qs and m_sign_conditions. diff --git a/src/math/simplex/network_flow.h b/src/math/simplex/network_flow.h index d4c7df77f..f4147b16f 100644 --- a/src/math/simplex/network_flow.h +++ b/src/math/simplex/network_flow.h @@ -148,7 +148,7 @@ namespace smt { vector m_potentials; // nodes + 1 |-> initial: +/- 1 // Duals of flows which are convenient to compute dual solutions // become solutions to Dual simplex. - vector m_flows; // edges + nodes |-> assignemnt Basic feasible flows + vector m_flows; // edges + nodes |-> assignment Basic feasible flows svector m_states; unsigned m_step; edge_id m_enter_id; diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 02c538828..ec514df8f 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -202,7 +202,7 @@ public: public: node(context_t & s, unsigned id); node(node * parent, unsigned id); - // return unique indentifier. + // return unique identifier. unsigned id() const { return m_id; } bound_array_manager & bm() const { return m_bm; } bound_array & lowers() { return m_lowers; } diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index cf93fbfad..b13f41c54 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -248,7 +248,7 @@ public: /** - \brief Auxiliary static method used to diplay a bound specified by (x, k, lower, open). + \brief Auxiliary static method used to display a bound specified by (x, k, lower, open). */ template void context_t::display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc, var x, numeral & k, bool lower, bool open) { diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 23926c3d1..a14ef163f 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -615,7 +615,7 @@ namespace datalog { void ensure_engine(); - // auxilary functions for SMT2 pretty-printer. + // auxiliary functions for SMT2 pretty-printer. void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out); //undefined and private copy constructor and operator= diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 7e85199cf..45b75c254 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -110,7 +110,7 @@ namespace datalog { /** \brief Manager for the \c rule class - \remark \c rule_manager objects are interchangable as long as they + \remark \c rule_manager objects are interchangeable as long as they contain the same \c ast_manager object. */ class rule_manager diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index c6e214f79..7e38b9e9f 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -97,7 +97,7 @@ namespace datalog { \brief Auxiliary function used to create a tail based on \c pred for a new rule. The variables in \c pred are re-assigned using \c next_idx and \c varidx2var. A variable is considered non-local to the rule if it is in the set \c non_local_vars. - Non-local variables are coppied to new_rule_args, and their sorts to \c new_rule_domain. + Non-local variables are copied to new_rule_args, and their sorts to \c new_rule_domain. The new predicate is stored in \c new_pred. */ void mk_new_rule_tail(ast_manager & m, app * pred, diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 18eb85662..325ecaaa6 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -143,8 +143,8 @@ def_module_params('fp', ('spacer.native_mbp', BOOL, True, "Use native mbp of Z3"), ('spacer.eq_prop', BOOL, True, "Enable equality and bound propagation in arithmetic"), ('spacer.weak_abs', BOOL, True, "Weak abstraction"), - ('spacer.restarts', BOOL, False, "Enable reseting obligation queue"), - ('spacer.restart_initial_threshold', UINT, 10, "Intial threshold for restarts"), + ('spacer.restarts', BOOL, False, "Enable resetting obligation queue"), + ('spacer.restart_initial_threshold', UINT, 10, "Initial threshold for restarts"), ('spacer.random_seed', UINT, 0, "Random seed to be used by SMT solver"), ('spacer.mbqi', BOOL, True, 'Enable mbqi'), diff --git a/src/muz/base/hnf.h b/src/muz/base/hnf.h index 330dfab70..70f803975 100644 --- a/src/muz/base/hnf.h +++ b/src/muz/base/hnf.h @@ -11,7 +11,7 @@ Copyright (c) 2015 Microsoft Corporation Abstract: - Horn normal form convertion. + Horn normal form conversion. Author: diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index a4fe5f0fa..d3460738c 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -332,7 +332,7 @@ namespace datalog { void internalize() { - // populate maps (should be bit-sets) of decendants. + // populate maps (should be bit-sets) of descendants. if (m_internalized) { return; } diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index a23d654b0..1cc85e6cd 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -120,7 +120,7 @@ public: This operation invalidates the line previously retrieved. - This operatio can be called only if we are not at the end of file. + This operation can be called only if we are not at the end of file. User is free to modify the content of the returned array until the terminating NULL character. */ @@ -876,7 +876,7 @@ protected: /** \brief Parse predicate arguments. If \c f==0, they are arguments of a predicate declaration. - If parsing a declaration, argumens names are pushed to the \c arg_names vector. + If parsing a declaration, argument names are pushed to the \c arg_names vector. */ dtoken parse_args(dtoken tok, func_decl* f, expr_ref_vector& args, svector & arg_names) { if (tok != TK_LP) { diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 4d202f2a2..decf499a2 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -295,7 +295,7 @@ namespace datalog { Precondition: &orig.get_plugin()==this */ virtual base_object * mk_empty(const signature & s, family_id kind) { - SASSERT(kind==get_kind()); //if plugin uses multiple kinds, this function needs to be overriden + SASSERT(kind==get_kind()); //if plugin uses multiple kinds, this function needs to be overridden return mk_empty(s); } diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index fb80a2105..0b1fbc840 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -1319,7 +1319,7 @@ namespace datalog { if(!m_table_cond_columns.empty()) { //We will keep the table variables that appear in the condition together - //with the index column and then iterate throught the tuples, evaluating + //with the index column and then iterate through the tuples, evaluating //the rest of the condition on the inner relations. unsigned_vector removed_cols; unsigned table_data_col_cnt = r.m_table_sig.size()-1; diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index f7d1665d2..2b76d99f7 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -640,7 +640,7 @@ namespace datalog { reg_idx m_src; reg_idx m_tgt; reg_idx m_delta; - bool m_widen; //if true, widening is performed intead of an union + bool m_widen; //if true, widening is performed instead of an union public: instr_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widen) : m_src(src), m_tgt(tgt), m_delta(delta), m_widen(widen) {} diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index bd7b9ae8c..5fb468ef5 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -253,7 +253,7 @@ namespace datalog { \brief Return functor that transforms a table into one that lacks columns listed in \c removed_cols array. - The \c removed_cols cotains columns of table \c t in strictly ascending order. + The \c removed_cols contains columns of table \c t in strictly ascending order. */ relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, const unsigned * removed_cols); @@ -420,7 +420,7 @@ namespace datalog { \brief Return functor that transforms a table into one that lacks columns listed in \c removed_cols array. - The \c removed_cols cotains columns of table \c t in strictly ascending order. + The \c removed_cols contains columns of table \c t in strictly ascending order. If a project operation removes a non-functional column, all functional columns become non-functional (so that none of the values in functional columns are lost) diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index bb48211c7..a51fbf3b1 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -568,7 +568,7 @@ namespace datalog { } /** - In this function we modify the content of table functional columns without reseting indexes. + In this function we modify the content of table functional columns without resetting indexes. This is ok as long as we do not allow indexing on functional columns. */ void sparse_table::ensure_fact(const table_fact & f) { diff --git a/src/muz/rel/rel_context.h b/src/muz/rel/rel_context.h index 0a31c4e9f..dbcc42248 100644 --- a/src/muz/rel/rel_context.h +++ b/src/muz/rel/rel_context.h @@ -85,7 +85,7 @@ namespace datalog { /** \brief Restrict the set of used predicates to \c res. - The function deallocates unsused relations, it does not deal with rules. + The function deallocates unused relations, it does not deal with rules. */ void restrict_predicates(func_decl_set const& predicates) override; diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp index 291226b55..b8d8324fb 100644 --- a/src/muz/spacer/spacer_farkas_learner.cpp +++ b/src/muz/spacer/spacer_farkas_learner.cpp @@ -7,8 +7,8 @@ Module Name: Abstract: - Proviced abstract interface and some inplementations of algorithms - for strenghtning lemmas + Provides abstract interface and some implementations of algorithms + for strenghtening lemmas Author: @@ -161,7 +161,7 @@ bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e, ast_manag in a clausal version. NB: the routine is not interpolating, though an interpolating variant would - be preferrable because then we can also use it for model propagation. + be preferable because then we can also use it for model propagation. We collect the unit derivable nodes from bs. These are the weakenings of bs, besides the diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index f3307a596..63b204736 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -186,7 +186,7 @@ void lemma_quantifier_generalizer::find_candidates(expr *e, std::sort(candidates.c_ptr(), candidates.c_ptr() + candidates.size(), index_lt_proc(m)); - // keep actual select indecies in the order found at the back of + // keep actual select indices in the order found at the back of // candidate list. There is no particular reason for this order candidates.append(extra); } @@ -199,24 +199,24 @@ bool lemma_quantifier_generalizer::match_sk_idx(expr *e, app_ref_vector const &z contains_app has_zk(m, zks.get(0)); if (!contains_selects(e, m)) return false; - app_ref_vector indicies(m); - get_select_indices(e, indicies); - if (indicies.size() > 2) return false; + app_ref_vector indices(m); + get_select_indices(e, indices); + if (indices.size() > 2) return false; unsigned i=0; - if (indicies.size() == 1) { - if (!has_zk(indicies.get(0))) return false; + if (indices.size() == 1) { + if (!has_zk(indices.get(0))) return false; } else { - if (has_zk(indicies.get(0)) && !has_zk(indicies.get(1))) + if (has_zk(indices.get(0)) && !has_zk(indices.get(1))) i = 0; - else if (!has_zk(indicies.get(0)) && has_zk(indicies.get(1))) + else if (!has_zk(indices.get(0)) && has_zk(indices.get(1))) i = 1; - else if (!has_zk(indicies.get(0)) && !has_zk(indicies.get(1))) + else if (!has_zk(indices.get(0)) && !has_zk(indices.get(1))) return false; } - idx = indicies.get(i); + idx = indices.get(i); sk = zks.get(0); return true; } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index aeb509c2e..77e88fb32 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -124,7 +124,7 @@ namespace spacer { * We can rewrite (E2) to rewrite (E1) to * (BP*Fark(BP)) => (neg(A*Fark(A) + BNP*Fark(BNP) + (neg D)*Fark(D))) (E3) * and since we can derive (A*Fark(A) + BNP*Fark(BNP) + (neg D)*Fark(D)) from - * A, BNP and D, we also know that it is inconsisent. Therefore + * A, BNP and D, we also know that it is inconsistent. Therefore * neg(A*Fark(A) + BNP*Fark(BNP) + (neg D)*Fark(D)) is a solution. * * Finally we also need the following workaround: diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index b5be996dc..3b8fd2ee0 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1097,7 +1097,7 @@ namespace tb { m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2); constraint = m.mk_and(tmp, tmp2); - // perform trival quantifier-elimination: + // perform trivial quantifier-elimination: uint_set index_set; expr_free_vars fv; fv(head); diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 058d9dca8..0a183b923 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -280,7 +280,7 @@ namespace datalog { } } - // model convertion: identity function. + // model conversion: identity function. if (instantiated) { result->inherit_predicates(source); diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index da41b4ba4..c970aedeb 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -45,7 +45,7 @@ namespace datalog { unsigned pt_len = r->get_positive_tail_size(); if(pt_len != r->get_uninterpreted_tail_size()) { - // we dont' expect rules with negative tails to be total + // we don't expect rules with negative tails to be total return false; } @@ -97,7 +97,7 @@ namespace datalog { void mk_subsumption_checker::scan_for_total_rules(const rule_set & rules) { bool new_discovered; //we cycle through the rules until we keep discovering new total relations - //(discovering a total relation migh reveal other total relations) + //(discovering a total relation might reveal other total relations) do { new_discovered = false; rule_set::iterator rend = rules.end(); diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index a93c4fb3e..e04b95a40 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -377,7 +377,7 @@ namespace nlsat { } /** - \brief Return the sign of the polynomial in the current interpration. + \brief Return the sign of the polynomial in the current interpretation. \pre All variables of p are assigned in the current interpretation. */ @@ -469,7 +469,7 @@ namespace nlsat { } } - // Evalute the sign of p1^e1*...*pn^en (of atom a) in cell c of table t. + // Evaluate the sign of p1^e1*...*pn^en (of atom a) in cell c of table t. int sign_at(ineq_atom * a, sign_table const & t, unsigned c) const { int sign = 1; unsigned num_ps = a->size(); @@ -556,7 +556,7 @@ namespace nlsat { result = m_ism.mk(true, true, dummy, true, true, dummy, jst); } else { - // save -oo as begining of infeasible interval + // save -oo as beginning of infeasible interval prev_open = true; prev_inf = true; prev_root_id = UINT_MAX; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 58b16717d..0662cacb5 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1987,7 +1987,7 @@ namespace smt2 { if (expr_stack().size() == fr->m_expr_spos) { if (!ignore_bad_patterns()) throw parser_exception("invalid empty pattern"); - // ingoring empty pattern + // ignoring empty pattern expr_stack().shrink(fr->m_expr_spos); } else { @@ -2698,7 +2698,7 @@ namespace smt2 { next(); } unsigned spos = sort_stack().size(); - parse_sorts("Invalid function name. Expecting sort list startig with '(' to disambiguate function name"); + parse_sorts("Invalid function name. Expecting sort list starting with '(' to disambiguate function name"); unsigned domain_size = sort_stack().size() - spos; parse_sort("Invalid function name"); func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back()); diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index f8c519285..a09c4046e 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -316,7 +316,7 @@ namespace qe { void mk_bound_aux(rational const& a, expr* t, rational const& b, expr* s, expr_ref& result) { SASSERT(a.is_neg() == b.is_neg()); expr_ref tt(t, m), ss(s, m), e(m); - // hack to fix wierd gcc compilation error + // hack to fix weird gcc compilation error rational abs_a(a); rational abs_b(b); if (abs_a.is_neg()) abs_a.neg(); diff --git a/src/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp index 81a402ba4..25332d164 100644 --- a/src/qe/qe_datatype_plugin.cpp +++ b/src/qe/qe_datatype_plugin.cpp @@ -46,7 +46,7 @@ Copyright (c) 2015 Microsoft Corporation // -> \/_i R_C(t_i) & phi[t_i/x] \/ phi[false, true] // // Justification: -// - We will asume that each of t_i, s_j are constructor terms. +// - We will assume that each of t_i, s_j are constructor terms. // - We can assume that x \notin t_i, x \notin s_j, or otherwise use simplification. // - We can assume that x occurs only in equalities or disequalities, or the recognizer, since // otherwise, we could simplify equalities, or QE does not apply. diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index d900bff5d..3226f7554 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -1816,7 +1816,7 @@ namespace fm { } // An integer variable x may be eliminated, if - // 1- All variables in the contraints it occur are integer. + // 1- All variables in the constraints it occur are integer. // 2- The coefficient of x in all lower bounds (or all upper bounds) is unit. bool can_eliminate(var x) const { if (!is_int(x)) diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index fdc4c3c6a..1cc2be0cb 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -47,7 +47,7 @@ namespace qe { /** * \brief Utility that works modulo a background state. * - vars - * variables to preferrably project onto (other variables would require quantification to fit interpolation signature) + * variables to preferably project onto (other variables would require quantification to fit interpolation signature) * - lits * set of literals to check satisfiability with respect to. * - mdl diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 97b044f5b..b5de20368 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -669,7 +669,7 @@ namespace qe { // Here we could also walk equivalence classes that // contain interpreted values by sort and extract - // disequalities bewteen non-unique value + // disequalities between non-unique value // representatives. these disequalities are implied // and can be mined using other means, such as theory // aware core minimization diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 4f06c2e98..01d627115 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2519,7 +2519,7 @@ namespace sat { * ~lit does not occur in clauses * ~lit is only in one constraint use list * lit == C - * -> ignore assignemnts to ~lit for C + * -> ignore assignments to ~lit for C * * ~lit does not occur in clauses * lit is only in one constraint use list diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 5fd69a740..baf072419 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -118,7 +118,7 @@ namespace sat { local_search_config m_config; // objective function: maximize - svector ob_constraint; // the objective function *constraint*, sorted in decending order + svector ob_constraint; // the objective function *constraint*, sorted in descending order // information about the variable int_vector coefficient_in_ob_constraint; // var! initialized to be 0 @@ -169,8 +169,8 @@ namespace sat { // unsat constraint stack bool m_is_unsat; - unsigned_vector m_unsat_stack; // store all the unsat constraits - unsigned_vector m_index_in_unsat_stack; // which position is a contraint in the unsat_stack + unsigned_vector m_unsat_stack; // store all the unsat constraints + unsigned_vector m_index_in_unsat_stack; // which position is a constraint in the unsat_stack // configuration changed decreasing variables (score>0 and conf_change==true) bool_var_vector m_goodvar_stack; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 72792b182..389cdb19b 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1220,7 +1220,7 @@ namespace sat { double operator()(literal l) override { return lh.literal_occs(l); } }; - // Ternary clause managagement: + // Ternary clause management: void lookahead::add_ternary(literal u, literal v, literal w) { SASSERT(u != w && u != v && v != w && ~u != w && ~u != v && ~w != v); @@ -1377,7 +1377,7 @@ namespace sat { } - // new n-ary clause managment + // new n-ary clause management void lookahead::add_clause(clause const& c) { SASSERT(c.size() > 3); @@ -1636,7 +1636,7 @@ namespace sat { } // Sum_{ clause C that contains ~l } 1 - // FIXME: counts occurences of ~l; misleading + // FIXME: counts occurrences of ~l; misleading double lookahead::literal_occs(literal l) { double result = m_binary[l.index()].size(); result += literal_big_occs(l); @@ -1644,7 +1644,7 @@ namespace sat { } // Sum_{ clause C that contains ~l such that |C| > 2} 1 - // FIXME: counts occurences of ~l; misleading + // FIXME: counts occurrences of ~l; misleading double lookahead::literal_big_occs(literal l) { double result = m_nary_count[(~l).index()]; result += m_ternary_count[(~l).index()]; @@ -1718,7 +1718,7 @@ namespace sat { } // VERIFY(!missed_propagation()); if (unsat) { - TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); + TRACE("sat", tout << "backtracking and setting " << ~lit << "\n";); lookahead_backtrack(); assign(~lit); propagate(); diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index c2282e779..046750832 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -471,7 +471,7 @@ namespace sat { watch_list& get_wlist(literal l) { return m_watches[l.index()]; } watch_list const& get_wlist(literal l) const { return m_watches[l.index()]; } - // new clause managment: + // new clause management: void add_ternary(literal u, literal v, literal w); void propagate_ternary(literal l); lbool propagate_ternary(literal l1, literal l2); diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index c6e29f64c..33cb02a87 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -232,7 +232,7 @@ namespace sat { } if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) { // time to update local search with new clauses. - // there could be multiple local search engines runing at the same time. + // there could be multiple local search engines running at the same time. IF_VERBOSE(1, verbose_stream() << "(sat-parallel refresh :from " << m_num_clauses << " :to " << s.m_clauses.size() << ")\n";); m_solver_copy = alloc(solver, s.m_params, s.rlimit()); m_solver_copy->copy(s); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index d19cd14d4..21d264af5 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -984,7 +984,7 @@ namespace sat { queue m_queue; literal_vector m_covered_clause; // covered clause - svector m_covered_antecedent; // explainations for literals in covered clause + svector m_covered_antecedent; // explanations for literals in covered clause literal_vector m_intersection; // current resolution intersection literal_vector m_tautology; // literals that are used in blocking tautology literal_vector m_new_intersection; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 3787b5894..990b87b10 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -74,7 +74,7 @@ namespace sat { // config bool m_abce; // block clauses using asymmetric added literals bool m_cce; // covered clause elimination - bool m_acce; // cce with asymetric literal addition + bool m_acce; // cce with asymmetric literal addition bool m_bca; // blocked (binary) clause addition. unsigned m_bce_delay; bool m_bce; // blocked clause elimination diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 883255b8a..4b1c6e4a6 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -492,7 +492,7 @@ bool arith_eq_solver::solve_integer_equations_omega( return false; } else if (r[index].is_zero()) { - // Row is trival + // Row is trivial rows_solved.pop_back(); continue; } diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 0f6c03f5b..d1434103b 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -64,14 +64,14 @@ struct qi_params { Enodes in the input problem have generation 0. Some combinations of m_qi_cost and m_qi_new_gen will prevent Z3 from breaking matching loops. - For example, the "Weight 0" peformace bug was triggered by the following combination: + For example, the "Weight 0" performance bug was triggered by the following combination: - m_qi_cost: (+ weight generation) - m_qi_new_gen: cost If a quantifier has weight 0, then the cost of instantiating it with a term in the input problem has cost 0. The new enodes created during the instantiation will be tagged with generation = const = 0. So, every enode will have generation 0, and consequently every quantifier instantiation will have cost 0. - Although dangerous, this feature was requested by the Boogie team. In their case, the patterns are carefully constructred, + Although dangerous, this feature was requested by the Boogie team. In their case, the patterns are carefully constructed, and there are no matching loops. Moreover, the tag some quantifiers with weight 0 to instruct Z3 to never block their instances. An example is the select-store axiom. They need this feature to be able to analyze code that contains very long execution paths. diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 76e9f03b1..b8b561e37 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -12,7 +12,7 @@ def_module_params(module_name='smt', ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'), ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'), ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'), - ('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'), + ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current 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, 6 - activity-based case split with theory-aware branching activity'), ('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, ignored if delay_units is false'), diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 94868ef6e..d621a9f50 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -175,7 +175,7 @@ namespace smt { } } m_new_entries.reset(); - TRACE("new_entries_bug", tout << "[qi:instatiate]\n";); + TRACE("new_entries_bug", tout << "[qi:instantiate]\n";); } void qi_queue::display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation) { diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index f7bc60051..93c172bf1 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -51,7 +51,7 @@ namespace smt { } /** - \brief Mark all enodes in a 'proof' tree brach starting at n + \brief Mark all enodes in a 'proof' tree branch starting at n n -> ... -> root */ template diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f275b0ebf..17a7ce3a3 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -518,7 +518,7 @@ namespace smt { // 2. r1 is interpreted but r2 is not. // // The second condition is used to enforce the invariant that if a class contain - // an interepreted enode then the root is also interpreted. + // an interpreted enode then the root is also interpreted. if ((r1->get_class_size() > r2->get_class_size() && !r2->is_interpreted()) || r1->is_interpreted()) { SASSERT(!r2->is_interpreted()); std::swap(n1, n2); @@ -529,7 +529,7 @@ namespace smt { " n1: #" << n1->get_owner_id() << "\n";); // It is necessary to propagate relevancy to other elements of - // the equivalence class. This is nessary to enforce the invariant + // the equivalence class. This is necessary to enforce the invariant // in the field m_parent of the enode class. if (is_relevant(r1)) { // && !m_manager.is_eq(r1->get_owner())) !is_eq HACK // NOTE for !is_eq HACK... the !is_eq HACK does not propagate relevancy when two @@ -4067,7 +4067,7 @@ namespace smt { A literal may have been marked relevant within the scope that gets popped during conflict resolution. In this case, the literal is no longer marked as relevant after the pop. This can cause quantifier instantiation to miss relevant triggers and thereby - cause incmpleteness. + cause incompleteness. */ void context::record_relevancy(unsigned n, literal const* lits) { m_relevant_conflict_literals.reset(); @@ -4281,7 +4281,7 @@ namespace smt { return true; } - // the variabe is shared if the equivalence class of n + // the variable is shared if the equivalence class of n // contains a parent application. theory_var_list * l = n->get_th_var_list(); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 61fed786b..74fcbfb45 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -73,7 +73,7 @@ namespace smt { class tmp_enode; /** - \brief Aditional data-structure for implementing congruence closure, + \brief Additional data-structure for implementing congruence closure, equality propagation, and the theory central bus of equalities. */ class enode { diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h index 1f69eb324..a26113a16 100644 --- a/src/smt/smt_model_generator.h +++ b/src/smt/smt_model_generator.h @@ -96,7 +96,7 @@ namespace smt { class model_value_dependency { bool m_fresh; //!< True if the dependency is a new fresh value; union { - enode * m_enode; //!< When m_fresh == false, contains an enode depedency. + enode * m_enode; //!< When m_fresh == false, contains an enode dependency. extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value }; public: diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 9e38fef69..6dcc9448c 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -203,7 +203,7 @@ namespace smt { static void check_no_arithmetic(static_features const & st, char const * logic) { if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) - throw default_exception("Benchmark constains arithmetic, but specified loging does not support it."); + throw default_exception("Benchmark constains arithmetic, but specified logic does not support it."); } void setup::setup_QF_UF() { @@ -519,7 +519,7 @@ namespace smt { m_params.m_arith_eq2ineq = true; m_params.m_eliminate_term_ite = true; // if (st.m_num_exprs < 5000 && st.m_num_ite_terms < 50) { // safeguard to avoid high memory consumption - // TODO: implement analsysis function to decide where lift ite is too expensive. + // TODO: implement analysis function to decide where lift ite is too expensive. // m_params.m_lift_ite = LI_FULL; // } } diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index b791d890e..f65ffe922 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -68,7 +68,7 @@ namespace smt { public: /** - \brief Return ture if the given enode is attached to a + \brief Return true if the given enode is attached to a variable of the theory. \remark The result is not equivalent to @@ -389,7 +389,7 @@ namespace smt { \brief When an eq atom n is created during the search, the default behavior is to make sure that the n->get_arg(0)->get_id() < n->get_arg(1)->get_id(). This may create some redundant atoms, since some theories/families use different - convetions in their simplifiers. For example, arithmetic always force a numeral + conventions in their simplifiers. For example, arithmetic always force a numeral to be in the right hand side. So, this method should be redefined if the default behavior conflicts with a convention used by the theory/family. */ diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 89737fb42..9561aa089 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1073,7 +1073,7 @@ namespace smt { /** \brief: Create an atom that enforces the inequality v > val The arithmetical expression encoding the inequality suffices - for the theory of aritmetic. + for the theory of arithmetic. */ template expr_ref theory_arith::mk_gt(theory_var v) { @@ -1146,7 +1146,7 @@ namespace smt { template void theory_arith::enable_record_conflict(expr* bound) { m_params.m_arith_bound_prop = BP_NONE; - SASSERT(propagation_mode() == BP_NONE); // bound propagtion rules are not (yet) handled. + SASSERT(propagation_mode() == BP_NONE); // bound propagation rules are not (yet) handled. if (bound) { context& ctx = get_context(); m_bound_watch = ctx.get_bool_var(bound); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index bce029753..3da78e8ee 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3128,7 +3128,7 @@ namespace smt { // // 1) Handling inequalities: (n1, k1) <= (n2, k2) // - // The only intersting case is n1 < n2 and k1 > k2. + // The only interesting case is n1 < n2 and k1 > k2. // Using the definition of infinitesimal numbers // we have: // n1 + k1 * epsilon <= n2 + k2 - epsilon @@ -3533,7 +3533,7 @@ namespace smt { } /** - \brief reset and retrieve built-in explanation hints for arithmetic lemmmas. + \brief reset and retrieve built-in explanation hints for arithmetic lemmas. */ template diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index c27d3b44a..24e1020fd 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1337,7 +1337,7 @@ namespace smt { } /** - \brief Diplay a nested form expression + \brief Display a nested form expression */ template void theory_arith::display_nested_form(std::ostream & out, expr * p) { @@ -1682,7 +1682,7 @@ namespace smt { if (!get_manager().int_real_coercions() && is_mixed_real_integer(r)) return true; // giving up... see comment above - TRACE("cross_nested", tout << "cheking problematic row...\n";); + TRACE("cross_nested", tout << "checking problematic row...\n";); rational c = rational::one(); if (is_integer(r)) @@ -1764,7 +1764,7 @@ namespace smt { updated with the fixed variables in m. A variable is only added to dep if it is not already in already_found. - Return null if the monomial was simplied to 0. + Return null if the monomial was simplified to 0. */ template grobner::monomial * theory_arith::mk_gb_monomial(rational const & _coeff, expr * m, grobner & gb, v_dependency * & dep, var_set & already_found) { diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 3dfba6b1b..369209e49 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -756,7 +756,7 @@ namespace smt { (n_x, k_x) <= (n_y + n_c, k_y + k_c) - The only intersting case is n_x < n_y + n_c and k_x > k_y + k_c. + The only interesting case is n_x < n_y + n_c and k_x > k_y + k_c. Using the definition of infinitesimal numbers we have: diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 24309ba88..4a04fdaaf 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3225,7 +3225,7 @@ public: theory_var w; if (m_solver->is_term(ti.var())) { //w = m_term_index2theory_var.get(m_solver->adjust_term_index(ti.var()), null_theory_var); - //if (w == null_theory_var) // if extracing expressions directly from nested term + //if (w == null_theory_var) // if extracting expressions directly from nested term lp::lar_term const& term1 = m_solver->get_term(ti.var()); rational coeff2 = coeff * ti.coeff(); term2coeffs(term1, coeffs, coeff2, offset); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 3a0ee723f..c20683d73 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -107,7 +107,7 @@ namespace smt { struct ineq { unsynch_mpz_manager& m_mpz; // mpz manager. - literal m_lit; // literal repesenting predicate + literal m_lit; // literal representing predicate bool m_is_eq; // is this an = or >=. arg_t m_args[2]; // encode args[0]*coeffs[0]+...+args[n-1]*coeffs[n-1] >= k(); // Watch the first few positions until the sum satisfies: @@ -192,7 +192,7 @@ namespace smt { // If none are available, then perform unit propagation. // class card { - literal m_lit; // literal repesenting predicate + literal m_lit; // literal representing predicate literal_vector m_args; unsigned m_bound; unsigned m_num_propagations; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 093a47146..2fb95e676 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1412,7 +1412,7 @@ bool theory_seq::is_complex(eq const& e) { \brief Decompose ls = rs into Xa = bYc, such that 1. - X != Y - - |b| <= |X| <= |bY| in currrent model + - |b| <= |X| <= |bY| in current model - b is non-empty. 2. X != Y - b is empty diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ec192cd89..856ba728e 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5074,7 +5074,7 @@ namespace smt { } } else { // ------------------------------------------------------------------------------------------------ - // subStr doesn't have an eqc contant value + // subStr doesn't have an eqc constant value // however, subStr equals to some concat(arg_1, arg_2, ..., arg_n) // if arg_j is a constant and is not a part of the strConst, it's sure that the contains is false // ** This check is needed here because the "strConst" and "strAst" may not be in a same eqc yet diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 61094c29c..e8fb34815 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -39,7 +39,7 @@ Notes: The object switches to incremental when: - push is used - - assertions are peformed after a check_sat + - assertions are performed after a check_sat - parameter ignore_solver1==false */ class combined_solver : public solver { diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index 2d58cbb81..cb37138ee 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -9,7 +9,7 @@ def_module_params('parallel', ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), ('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'), - ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multipled by simplify.exp ^ depth'), + ('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multiplied by simplify.exp ^ depth'), ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'), ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), )) diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index fc41f54a4..bd99e4303 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1231,7 +1231,7 @@ class fm_tactic : public tactic { } // An integer variable x may be eliminated, if - // 1- All variables in the contraints it occur are integer. + // 1- All variables in the constraints it occur are integer. // 2- The coefficient of x in all lower bounds (or all upper bounds) is unit. bool can_eliminate(var x) const { if (!is_int(x)) diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 3ca296eb7..97947c03a 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -40,7 +40,7 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con m_fmc(nullptr), extra_assertions(m) { updt_params(p); - // We need to make sure that the mananger has the BV and array plugins loaded. + // We need to make sure that the manager has the BV and array plugins loaded. symbol s_bv("bv"); if (!m_manager.has_plugin(s_bv)) m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 1b435791c..6afcdee41 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -197,7 +197,7 @@ struct cofactor_elim_term_ite::imp { switch (arg->get_kind()) { case AST_VAR: case AST_QUANTIFIER: - // ingore quantifiers + // ignore quantifiers break; case AST_APP: if (to_app(arg)->get_num_args() > 0) { @@ -264,7 +264,7 @@ struct cofactor_elim_term_ite::imp { switch (arg->get_kind()) { case AST_VAR: case AST_QUANTIFIER: - // ingore quantifiers + // ignore quantifiers break; case AST_APP: if (to_app(arg)->get_num_args() > 0) { diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 7f17c8dae..50d606197 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -273,8 +273,8 @@ private: } /** - \brief decompose large sums into smaller sums by intoducing - auxilary variables. + \brief decompose large sums into smaller sums by introducing + auxiliary variables. */ void decompose(goal_ref const& g) { expr_ref fml1(m), fml2(m); diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 9c5b72830..73432219f 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -31,7 +31,7 @@ Notes: This property holds for both eval, that decides on a fixed value for constants that have no interpretation in m and for 'peval' - (partial eval) that retuns just the constants that are unfixed. + (partial eval) that returns just the constants that are unfixed. (in the model evaluator one can control this behavior using a configuration flag) @@ -48,7 +48,7 @@ Notes: mc(G) & F_s is SAT iff G & F is SAT For a model converter that is a sequence of definitions and removals - of functions we can obtain mc(G) by adding back or expanding definitinos + of functions we can obtain mc(G) by adding back or expanding definitions that are required to interpret G fully in the context of F_s. --*/ diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 745b0352d..a02c2d327 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -8,7 +8,7 @@ Module Name: Abstract: Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories. - It is designed to allow cooprating between the nlsat solver and other theories + It is designed to allow cooperation between the nlsat solver and other theories in a decoupled way. Let goal be formula F. @@ -446,7 +446,7 @@ private: expr* pred = fresh_preds[i]; if (mdl->eval(pred, tmp)) { polarity_t pol = m_polarities.find(pred); - // if assumptinon literals are used to satisfy NL state, + // if assumption literals are used to satisfy NL state, // we have to assume them when satisfying SMT state if (pol != pol_neg && m.is_false(tmp)) { m_asms.push_back(m.mk_not(pred)); @@ -767,7 +767,7 @@ public: // then annotate subformulas by polarities, // finally extract polynomial inequalities by // creating a place-holder predicate inside the - // original goal and extracing pure nlsat clauses. + // original goal and extracting pure nlsat clauses. r.set_interface_var_mode(); rewrite_goal(r, g); if (!g->unsat_core_enabled()) { diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index f5b5ec1b2..1285e46cf 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -182,7 +182,7 @@ bool sls_engine::what_if( // Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection. // r += 0.0001 * m_tracker.get_random_uint(8); - // Andreas: For some reason it is important to use > here instead of >=. Probably related to prefering the LSB. + // Andreas: For some reason it is important to use > here instead of >=. Probably related to preferring the LSB. if (r > best_score) { best_score = r; best_const = fd_inx; diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index a8ad95319..7c410e721 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -36,7 +36,7 @@ Notes: static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { params_ref solve_eq_p; - // conservative guassian elimination. + // conservative gaussian elimination. solve_eq_p.set_uint("solve_eqs_max_occs", 2); params_ref simp2_p = p; diff --git a/src/test/ast.cpp b/src/test/ast.cpp index 59bdfc8e4..0826306f2 100644 --- a/src/test/ast.cpp +++ b/src/test/ast.cpp @@ -44,7 +44,7 @@ static void tst1() { // ast_ref v3 (m.mk_var(1), m); // ENSURE(v1 != v2); // ENSURE(v1 == v3); -// TRACE("ast", tout << "reseting v1\n";); +// TRACE("ast", tout << "resetting v1\n";); // v1.reset(); // TRACE("ast", tout << "overwriting v3\n";); // v3 = v2; diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index 003e5bdb8..b1bb624a2 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -15,7 +15,7 @@ Copyright (c) 2015 Microsoft Corporation #include /* -TBD: count number of nodes, number of operations accross all insertions +TBD: count number of nodes, number of operations across all insertions */ void read_nums(std::istream& is, unsigned & x, unsigned& y) { diff --git a/src/test/fuzzing/expr_delta.h b/src/test/fuzzing/expr_delta.h index d69ed33f1..f59e4c4d5 100644 --- a/src/test/fuzzing/expr_delta.h +++ b/src/test/fuzzing/expr_delta.h @@ -33,7 +33,7 @@ public: // // Create the n'th delta in dfs mode. - // resturn 'true' if a delta was obtained. + // return 'true' if a delta was obtained. // bool delta_dfs(unsigned n, expr_ref_vector& result); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index ffdbb5af8..192bd46b0 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -117,7 +117,7 @@ void test_matrix(square_sparse_matrix & a) { } void tst1() { - std::cout << "testing the minimial matrix with 1 row and 1 column" << std::endl; + std::cout << "testing the minimal matrix with 1 row and 1 column" << std::endl; square_sparse_matrix m0(1, 1); m0.set(0, 0, 1); // print_matrix(m0); @@ -192,7 +192,7 @@ void tst1() { // print_matrix(m10by9); } -vector allocate_basis_heading(unsigned count) { // the rest of initilization will be handled by lu_QR +vector allocate_basis_heading(unsigned count) { // the rest of initialization will be handled by lu_QR vector basis_heading(count, -1); return basis_heading; } @@ -850,7 +850,7 @@ void fill_uniformly(dense_matrix & m, unsigned dim) { } } -void square_sparse_matrix_with_permutaions_test() { +void square_sparse_matrix_with_permutations_test() { unsigned dim = 4; square_sparse_matrix m(dim, dim); fill_uniformly(m, dim); @@ -1023,7 +1023,7 @@ void test_dense_matrix() { -vector> vector_of_permutaions() { +vector> vector_of_permutations() { vector> ret; { permutation_matrix p0(5); @@ -1058,7 +1058,7 @@ void test_apply_reverse_from_right_to_perm(permutation_matrix & } void test_apply_reverse_from_right() { - auto vec = vector_of_permutaions(); + auto vec = vector_of_permutations(); for (unsigned i = 0; i < vec.size(); i++) { test_apply_reverse_from_right_to_perm(vec[i]); } @@ -1901,17 +1901,17 @@ void setup_args_parser(argument_parser & parser) { parser.add_option_with_after_string_with_help("--density", "the percentage of non-zeroes in the matrix below which it is not dense"); parser.add_option_with_after_string_with_help("--harris_toler", "harris tolerance"); parser.add_option_with_help_string("--test_swaps", "test row swaps with a permutation"); - parser.add_option_with_help_string("--test_perm", "test permutaions"); + parser.add_option_with_help_string("--test_perm", "test permutations"); parser.add_option_with_after_string_with_help("--checklu", "the file name for lu checking"); parser.add_option_with_after_string_with_help("--partial_pivot", "the partial pivot constant, a number somewhere between 10 and 100"); parser.add_option_with_after_string_with_help("--percent_for_enter", "which percent of columns check for entering column"); - parser.add_option_with_help_string("--totalinf", "minimizes the total infeasibility instead of diminishin infeasibility of the rows"); + parser.add_option_with_help_string("--totalinf", "minimizes the total infeasibility instead of diminishing infeasibility of the rows"); parser.add_option_with_after_string_with_help("--rep_frq", "the report frequency, in how many iterations print the cost and other info "); parser.add_option_with_help_string("--smt", "smt file format"); parser.add_option_with_after_string_with_help("--filelist", "the file containing the list of files"); parser.add_option_with_after_string_with_help("--file", "the input file name"); parser.add_option_with_after_string_with_help("--random_seed", "random seed"); - parser.add_option_with_help_string("--bp", "bound propogation"); + parser.add_option_with_help_string("--bp", "bound propagation"); parser.add_option_with_help_string("--min", "will look for the minimum for the given file if --file is used; the default is looking for the max"); parser.add_option_with_help_string("--max", "will look for the maximum for the given file if --file is used; it is the default behavior"); parser.add_option_with_after_string_with_help("--max_iters", "maximum total iterations in a core solver stage"); @@ -1932,7 +1932,7 @@ void setup_args_parser(argument_parser & parser) { parser.add_option_with_help_string("--lar", "test lar_solver"); parser.add_option_with_after_string_with_help("--maxng", "max iterations without progress"); parser.add_option_with_help_string("-tbq", "test binary queue"); - parser.add_option_with_help_string("--randomize_lar", "test randomize funclionality"); + parser.add_option_with_help_string("--randomize_lar", "test randomize functionality"); parser.add_option_with_help_string("--smap", "test stacked_map"); parser.add_option_with_help_string("--term", "simple term test"); parser.add_option_with_help_string("--eti"," run a small evidence test for total infeasibility scenario"); @@ -3722,7 +3722,7 @@ void test_lp_local(int argn, char**argv) { test_init_U(); test_replace_column(); #ifdef Z3DEBUG - square_sparse_matrix_with_permutaions_test(); + square_sparse_matrix_with_permutations_test(); test_dense_matrix(); test_swap_operations(); test_permutations(); diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index 1116c5420..ad982d024 100644 --- a/src/test/sat_local_search.cpp +++ b/src/test/sat_local_search.cpp @@ -7,7 +7,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search) { char line[16383]; - // for temperally storage + // for temporary storage std::ifstream infile(filename); //if (infile == NULL) //linux @@ -28,7 +28,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea sat::literal_vector lits; // process objective function: - // read coefficents + // read coefficients infile >> cur_term; while (cur_term != 0) { coefficients.push_back(cur_term); @@ -43,7 +43,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea } if (lits.size() != coefficients.size()) { - std::cout << "Objective function format error. They have different lenghts.\n"; + std::cout << "Objective function format error. They have different lengths.\n"; return false; } diff --git a/src/util/bit_util.cpp b/src/util/bit_util.cpp index a38f42fdd..fdca2dc83 100644 --- a/src/util/bit_util.cpp +++ b/src/util/bit_util.cpp @@ -126,7 +126,7 @@ unsigned ntz(unsigned sz, unsigned const * data) { /** \brief dst <- src - Trucate if src_sz > dst_sz. + Truncate if src_sz > dst_sz. Fill range [src_sz, dst_sz) of dst with zeros if dst_sz > src_sz. */ void copy(unsigned src_sz, unsigned const * src, diff --git a/src/util/bit_util.h b/src/util/bit_util.h index 5729e8eed..7a0923400 100644 --- a/src/util/bit_util.h +++ b/src/util/bit_util.h @@ -48,7 +48,7 @@ unsigned ntz(unsigned sz, unsigned const * data); /** \brief dst <- src - Trucate if src_sz > dst_sz. + Truncate if src_sz > dst_sz. Fill range [src_sz, dst_sz) of dst with zeros if dst_sz > src_sz. */ void copy(unsigned src_sz, unsigned const * src, unsigned dst_sz, unsigned * dst); @@ -87,7 +87,7 @@ void shr(unsigned sz, unsigned const * src, unsigned k, unsigned * dst); \brief dst <- src >> k Store in dst the result of shifting src k bits to the right. - Trucate if src_sz > dst_sz. + Truncate if src_sz > dst_sz. Fill range [src_sz, dst_sz) of dst with zeros if dst_sz > src_sz. \pre src_sz != 0 diff --git a/src/util/list.h b/src/util/list.h index 075d5a0e1..82ca73308 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -68,7 +68,7 @@ unsigned length(list * l) { } /** - \brief Non destructive apppend operation. The new nodes are allocated + \brief Non destructive append operation. The new nodes are allocated using the given region allocator. */ template diff --git a/src/util/lp/binary_heap_priority_queue_def.h b/src/util/lp/binary_heap_priority_queue_def.h index 232959c83..d0a08c27d 100644 --- a/src/util/lp/binary_heap_priority_queue_def.h +++ b/src/util/lp/binary_heap_priority_queue_def.h @@ -76,7 +76,7 @@ template void binary_heap_priority_queue::remove(unsigned o) { put_at(o_in_heap, m_heap[m_heap_size--]); if (m_priorities[m_heap[o_in_heap]] > priority_of_o) { fix_heap_under(o_in_heap); - } else { // we need to propogate the m_heap[o_in_heap] up + } else { // we need to propagate the m_heap[o_in_heap] up unsigned i = o_in_heap; while (i > 1) { unsigned ip = i >> 1; diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h index 549c8e5ce..a20b4850a 100644 --- a/src/util/lp/bound_analyzer_on_row.h +++ b/src/util/lp/bound_analyzer_on_row.h @@ -270,7 +270,7 @@ public : } } - // // it is the coefficent before the bounded column + // // it is the coefficient before the bounded column // void provide_evidence(bool coeff_is_pos) { // /* // auto & be = m_ibounds.back(); diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/util/lp/lp_core_solver_base_def.h index c3a0a0a00..6844ab839 100644 --- a/src/util/lp/lp_core_solver_base_def.h +++ b/src/util/lp/lp_core_solver_base_def.h @@ -74,7 +74,7 @@ lp_core_solver_base(static_matrix & A, } template void lp_core_solver_base:: -allocate_basis_heading() { // the rest of initilization will be handled by the factorization class +allocate_basis_heading() { // the rest of initialization will be handled by the factorization class init_basis_heading_and_non_basic_columns_vector(); lp_assert(basis_heading_is_correct()); } diff --git a/src/util/lp/lp_dual_core_solver_def.h b/src/util/lp/lp_dual_core_solver_def.h index 86e6231fc..e7ab73928 100644 --- a/src/util/lp/lp_dual_core_solver_def.h +++ b/src/util/lp/lp_dual_core_solver_def.h @@ -276,7 +276,7 @@ template bool lp_dual_core_solver::can_be_breakpo bool grawing = m_sign_of_alpha_r * this->m_pivot_row[j] > 0; return lower_bound == grawing; } - case column_type::fixed: // is always dual feasible so we ingore it + case column_type::fixed: // is always dual feasible so we ignore it return false; case column_type::free_column: return true; diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h index 872922f60..d86ebf548 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/util/lp/lp_primal_core_solver_def.h @@ -284,7 +284,7 @@ template int lp_primal_core_solver::advance_on_so break; } else { if ((numeric_traits::precise() == false) || ( numeric_traits::is_zero(slope_at_entering) && this->m_settings.random_next() % 2 == 0)) { - // it is not cost benefitial to advance the delta more, so just break to increas the randomness + // it is not cost beneficial to advance the delta more, so just break to increase the randomness break; } } @@ -612,7 +612,7 @@ template int lp_primal_core_solver::refresh_re return 2; // abort entering } else { if (refreshed_cost > -m_epsilon_of_reduced_cost) - return 2; // abort entiring + return 2; // abort entering } return 1; // go on with this entering } else { @@ -621,7 +621,7 @@ template int lp_primal_core_solver::refresh_re return 2; // abort entering } else { if (refreshed_cost > -m_epsilon_of_reduced_cost) - return 2; // abort entiring + return 2; // abort entering } } return 0; diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 1bbefd154..d0bdc284d 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -68,7 +68,7 @@ enum class lp_status { CANCELLED }; -// when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only +// when the ratio of the vector length to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only template unsigned ratio_of_index_size_to_all_size() { if (numeric_traits::precise()) @@ -145,7 +145,7 @@ public: double pivot_epsilon; // see Chatal, page 115 double positive_price_epsilon; - // a quatation "if some choice of the entering vairable leads to an eta matrix + // a quotation "if some choice of the entering variable leads to an eta matrix // whose diagonal element in the eta column is less than e2 (entering_diag_epsilon) in magnitude, the this choice is rejected ... double entering_diag_epsilon; int c_partial_pivoting; // this is the constant c from page 410 diff --git a/src/util/lp/scaler_def.h b/src/util/lp/scaler_def.h index 2710f89bf..4c9784a43 100644 --- a/src/util/lp/scaler_def.h +++ b/src/util/lp/scaler_def.h @@ -126,7 +126,7 @@ template void scaler::scale_once_for_ratio() { T max_ratio_on_rows = get_max_ratio_on_rows(); T max_ratio_on_columns = get_max_ratio_on_columns(); bool scale_rows_first = max_ratio_on_rows > max_ratio_on_columns; - // if max_ratio_on_columns is the largerst then the rows are in worser shape then columns + // if max_ratio_on_columns is the largest then the rows are in worse shape than columns if (scale_rows_first) { scale_rows_with_geometric_mean(); scale_columns_with_geometric_mean(); diff --git a/src/util/lp/square_sparse_matrix_def.h b/src/util/lp/square_sparse_matrix_def.h index 791bdb6ae..cc6625453 100644 --- a/src/util/lp/square_sparse_matrix_def.h +++ b/src/util/lp/square_sparse_matrix_def.h @@ -186,7 +186,7 @@ void square_sparse_matrix::init_row_headers() { } template -void square_sparse_matrix::init_column_headers() { // we alway have only square square_sparse_matrix +void square_sparse_matrix::init_column_headers() { // we always have only square square_sparse_matrix for (unsigned l = 0; l < m_row_permutation.size(); l++) { m_columns.push_back(col_header()); } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 7549a7bb3..49335467d 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -952,7 +952,7 @@ void my_mpz_sqrt(unsynch_mpz_manager & m, unsigned sbits, bool odd_exp, mpz & in scoped_mpz lower(m), upper(m); scoped_mpz mid(m), product(m), diff(m); // we have lower <= a.significand <= upper and we need 1.[52+3 bits] in the bounds. - // since we comapre upper*upper to a.significand further down, we need a.significand + // since we compare upper*upper to a.significand further down, we need a.significand // to be of twice the size. m.set(lower, 1); m.mul2k(lower, sbits+2-1); @@ -978,7 +978,7 @@ void my_mpz_sqrt(unsynch_mpz_manager & m, unsigned sbits, bool odd_exp, mpz & in } else { STRACE("mpf_dbg", tout << "choosing upper" << std::endl;); - m.set(o, upper); // chosing upper is like a sticky bit here. + m.set(o, upper); // choosing upper is like a sticky bit here. } break; } diff --git a/src/util/obj_ref_hashtable.h b/src/util/obj_ref_hashtable.h index 23a2a1867..80d198607 100644 --- a/src/util/obj_ref_hashtable.h +++ b/src/util/obj_ref_hashtable.h @@ -7,7 +7,7 @@ Module Name: Abstract: - corresponding obj_map with reference count managment. + corresponding obj_map with reference count management. Author: