From 6ba9ada1e2d4aefd6cbe0602b743124b40e11628 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 22 Aug 2022 02:40:07 +0700 Subject: [PATCH] Fix typos. (#6291) --- src/api/js/src/high-level/high-level.test.ts | 4 ++-- src/api/js/src/high-level/types.ts | 20 ++++++++++---------- src/api/ml/README.md | 4 ++-- src/math/interval/dep_intervals.cpp | 2 +- src/math/interval/dep_intervals.h | 2 +- src/math/lp/lar_solver.h | 2 +- src/muz/fp/dl_cmds.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 8 ++++---- src/smt/theory_arith_eq.h | 2 +- src/smt/theory_arith_int.h | 2 +- 10 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index aeb0939a05b..7fb20e62732 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -8,7 +8,7 @@ import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types'; * * **NOTE**: The set of solutions might be infinite. * Always ensure to limit amount generated, either by knowing that the - * solution space is constrainted, or by taking only a specified + * solution space is constrained, or by taking only a specified * amount of solutions * ```typescript * import { sliceAsync } from 'iter-tools'; @@ -46,7 +46,7 @@ async function* allSolutions(...assertions: Bool[]): .filter(decl => decl.arity() === 0) .map(decl => { const term = decl.call(); - // TODO(ritave): Assert not an array / uinterpeted sort + // TODO(ritave): Assert not an array / uninterpreted sort const value = model.eval(term, true); return term.neq(value); }), diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index c27395d21b8..57e5c37f8f0 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -617,7 +617,7 @@ export interface Arith extends Expr | number | bigint | string): Arith; /** - * Substract second number from the first one + * Subtract second number from the first one */ sub(other: Arith | number | bigint | string): Arith; /** @@ -709,7 +709,7 @@ export interface RatNum extends Arith { } /** - * A Sort represting Bit Vector numbers of specified {@link BitVecSort.size size} + * A Sort representing Bit Vector numbers of specified {@link BitVecSort.size size} * * @typeParam Bits - A number representing amount of bits for this sort * @category Bit Vectors @@ -878,42 +878,42 @@ export interface BitVecget_family_id() != null_family_id) { - throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted"); + throw cmd_exception("Invalid query argument, expected uninterpreted function name, but argument is interpreted"); } datalog::context& dlctx = m_dl_ctx->dlctx(); if (!dlctx.get_predicates().contains(t)) { diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index eda00b64d71..834bb41ef6e 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -25,7 +25,7 @@ Revision History: Let x_i, y_i, z_i be indices into the vectors x, y, z. Suppose that positions in P and R are annotated with what is - slicable. + sliceable. Sufficient conditions for sliceability: @@ -43,9 +43,9 @@ Revision History: and the positions where z_i is used in P and R are sliceable - A more refined approach may be using Gaussean elimination based + A more refined approach may be using Gaussian elimination based on x,z and eliminating variables from x,y (expressing them in terms - of a disjoint subeset of x,z). + of a disjoint subset of x,z). --*/ @@ -441,7 +441,7 @@ namespace datalog { void mk_slice::filter_unique_vars(rule& r) { // - // Variables that occur in multiple uinterpreted predicates are not sliceable. + // Variables that occur in multiple uninterpreted predicates are not sliceable. // uint_set used_vars; for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index fab67a80136..cffac245988 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -37,7 +37,7 @@ namespace smt { return; SASSERT(is_fixed(v)); - // WARNINING: it is not safe to use get_value(v) here, since + // WARNING: it is not safe to use get_value(v) here, since // get_value(v) may not satisfy v bounds at this point. if (!lower_bound(v).is_rational()) return; diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 56fbd4ecf4f..699ebd5d235 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -711,7 +711,7 @@ namespace smt { for (; it != end; ++it) { if (!it->is_dead()) { if (is_fixed(it->m_var)) { - // WARNINING: it is not safe to use get_value(it->m_var) here, since + // WARNING: it is not safe to use get_value(it->m_var) here, since // get_value(it->m_var) may not satisfy it->m_var bounds at this point. numeral aux = lcm_den * it->m_coeff; consts += aux * lower_bound(it->m_var).get_rational();