diff --git a/CMakeLists.txt b/CMakeLists.txt
index 69a0ca123..7bc60e135 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -434,7 +434,7 @@ else()
endif()
################################################################################
-# Postion independent code
+# Position independent code
################################################################################
# This is required because code built in the components will end up in a shared
# library. If not building a shared library ``-fPIC`` isn't needed and would add
diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py
index d0502c19d..39d4e9439 100755
--- a/scripts/mk_consts_files.py
+++ b/scripts/mk_consts_files.py
@@ -72,7 +72,7 @@ def main(args):
if count == 0:
logging.info('No files generated. You need to specific an output directory'
- ' for the relevant langauge bindings')
+ ' for the relevant language bindings')
# TODO: Add support for other bindings
return 0
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 49f6cfbf3..42467cb22 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -989,7 +989,7 @@ namespace z3 {
/**
\brief sequence and regular expression operations.
- + is overloaeded as sequence concatenation and regular expression union.
+ + is overloaded as sequence concatenation and regular expression union.
concat is overloaded to handle sequences and regular expressions
*/
expr extract(expr const& offset, expr const& length) const {
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index cbd6a1bac..b3b24a6d1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2515,7 +2515,7 @@ namespace Microsoft.Z3
/// <summary>
- /// Concatentate sequences.
+ /// Concatenate sequences.
/// </summary>
public SeqExpr MkConcat(params SeqExpr[] t)
{
@@ -3597,7 +3597,7 @@ namespace Microsoft.Z3
}
/// <summary>
- /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
+ /// Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
/// or trivially unsatisfiable (i.e., contains `false').
/// </summary>
public Tactic FailIfNotDecided()
@@ -4656,7 +4656,7 @@ namespace Microsoft.Z3
/// Conversion of a floating-point term into a bit-vector.
/// </summary>
/// <remarks>
- /// Produces a term that represents the conversion of the floating-poiunt term t into a
+ /// Produces a term that represents the conversion of the floating-point term t into a
/// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
/// the result will be rounded according to rounding mode rm.
/// </remarks>
@@ -4677,7 +4677,7 @@ namespace Microsoft.Z3
/// Conversion of a floating-point term into a real-numbered term.
/// </summary>
/// <remarks>
- /// Produces a term that represents the conversion of the floating-poiunt term t into a
+ /// Produces a term that represents the conversion of the floating-point term t into a
/// real number. Note that this type of conversion will often result in non-linear
/// constraints over real terms.
/// </remarks>
@@ -4696,7 +4696,7 @@ namespace Microsoft.Z3
/// <remarks>
/// The size of the resulting bit-vector is automatically determined. Note that
/// IEEE 754-2008 allows multiple different representations of NaN. This conversion
- /// knows only one NaN and it will always produce the same bit-vector represenatation of
+ /// knows only one NaN and it will always produce the same bit-vector representation of
/// that NaN.
/// </remarks>
/// <param name="t">FloatingPoint term.</param>
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index ba96209b3..3c5caadee 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable {
}
/**
- * Concatentate sequences.
+ * Concatenate sequences.
*/
public SeqExpr mkConcat(SeqExpr... t)
{
@@ -2781,7 +2781,7 @@ public class Context implements AutoCloseable {
}
/**
- * Create a tactic that fails if the goal is not triviall satisfiable (i.e.,
+ * Create a tactic that fails if the goal is not trivially satisfiable (i.e.,
* empty) or trivially unsatisfiable (i.e., contains `false').
**/
public Tactic failIfNotDecided()
@@ -3769,7 +3769,7 @@ public class Context implements AutoCloseable {
* @param sz Size of the resulting bit-vector.
* @param signed Indicates whether the result is a signed or unsigned bit-vector.
* Remarks:
- * Produces a term that represents the conversion of the floating-poiunt term t into a
+ * Produces a term that represents the conversion of the floating-point term t into a
* bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
* the result will be rounded according to rounding mode rm.
* @throws Z3Exception
@@ -3786,7 +3786,7 @@ public class Context implements AutoCloseable {
* Conversion of a floating-point term into a real-numbered term.
* @param t FloatingPoint term
* Remarks:
- * Produces a term that represents the conversion of the floating-poiunt term t into a
+ * Produces a term that represents the conversion of the floating-point term t into a
* real number. Note that this type of conversion will often result in non-linear
* constraints over real terms.
* @throws Z3Exception
@@ -3802,7 +3802,7 @@ public class Context implements AutoCloseable {
* Remarks:
* The size of the resulting bit-vector is automatically determined. Note that
* IEEE 754-2008 allows multiple different representations of NaN. This conversion
- * knows only one NaN and it will always produce the same bit-vector represenatation of
+ * knows only one NaN and it will always produce the same bit-vector representation of
* that NaN.
* @throws Z3Exception
**/
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 1cfb10179..e68d7280d 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2428,7 +2428,7 @@ def is_rational_value(a):
return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
def is_algebraic_value(a):
- """Return `True` if `a` is an algerbraic value of sort Real.
+ """Return `True` if `a` is an algebraic value of sort Real.
>>> is_algebraic_value(RealVal("3/5"))
False
@@ -4437,7 +4437,7 @@ class Datatype:
"""Declare constructor named `name` with the given accessors `args`.
Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
- In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
+ In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
declares the constructor named `cons` that builds a new List using an integer and a List.
It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
@@ -4457,7 +4457,7 @@ class Datatype:
return "Datatype(%s, %s)" % (self.name, self.constructors)
def create(self):
- """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
+ """Create a Z3 datatype based on the constructors declared using the method `declare()`.
The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
@@ -8874,7 +8874,7 @@ class FPNumRef(FPRef):
def isSubnormal(self):
return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
- """Indicates whether the numeral is postitive."""
+ """Indicates whether the numeral is positive."""
def isPositive(self):
return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
@@ -9670,7 +9670,7 @@ def fpToIEEEBV(x, ctx=None):
The size of the resulting bit-vector is automatically determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
- knows only one NaN and it will always produce the same bit-vector represenatation of
+ knows only one NaN and it will always produce the same bit-vector representation of
that NaN.
>>> x = FP('x', FPSort(8, 24))
@@ -9845,7 +9845,7 @@ def Empty(s):
raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
def Full(s):
- """Create the regular expression that accepts the universal langauge
+ """Create the regular expression that accepts the universal language
>>> e = Full(ReSort(SeqSort(IntSort())))
>>> print(e)
re.all
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 358a3c619..7d237c6e7 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -756,7 +756,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into an unsigned bit-vector.
- Produces a term that represents the conversion of the floating-poiunt term t into a
+ Produces a term that represents the conversion of the floating-point term t into a
bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
@@ -772,7 +772,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into a signed bit-vector.
- Produces a term that represents the conversion of the floating-poiunt term t into a
+ Produces a term that represents the conversion of the floating-point term t into a
bit-vector term of size sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
@@ -788,7 +788,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into a real-numbered term.
- Produces a term that represents the conversion of the floating-poiunt term t into a
+ Produces a term that represents the conversion of the floating-point term t into a
real number. Note that this type of conversion will often result in non-linear
constraints over real terms.
@@ -1011,7 +1011,7 @@ extern "C" {
determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
- knows only one NaN and it will always produce the same bit-vector represenatation of
+ knows only one NaN and it will always produce the same bit-vector representation of
that NaN.
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h
index bcee0e22d..2441d4339 100644
--- a/src/api/z3_interp.h
+++ b/src/api/z3_interp.h
@@ -98,7 +98,7 @@ extern "C" {
Interpolant may not necessarily be computable from all
proofs. To be sure an interpolant can be computed, the proof
- must be generated by an SMT solver for which interpoaltion is
+ must be generated by an SMT solver for which interpolation is
supported, and the premises must be expressed using only
theories and operators for which interpolation is supported.
@@ -199,7 +199,7 @@ extern "C" {
(implies (and c1 ... cn f) v)
where c1 .. cn are the children of v (which must precede v in the file)
- and f is the formula assiciated to node v. The last formula in the
+ and f is the formula associated to node v. The last formula in the
file is the root vertex, and is represented by the predicate "false".
A solution to a tree interpolation problem can be thought of as a
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 658fb2e05..878f4ef4c 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -358,7 +358,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
if (ProofGen) {
NOT_IMPLEMENTED_YET();
// We do not support the use of bindings in proof generation mode.
- // Thus we have to apply the subsitution here, and
+ // Thus we have to apply the substitution here, and
// beta_reducer subst(m());
// subst.set_bindings(new_num_args, new_args);
// expr_ref r2(m());
diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp
index cfea511ad..511342819 100644
--- a/src/interp/iz3checker.cpp
+++ b/src/interp/iz3checker.cpp
@@ -43,7 +43,7 @@ struct iz3checker : iz3base {
/* HACK: for tree interpolants, we assume that uninterpreted functions
are global. This is because in the current state of the tree interpolation
code, symbols that appear in sibling sub-trees have to be global, and
- we have no way to eliminate such function symbols. When tree interpoaltion is
+ we have no way to eliminate such function symbols. When tree interpolation is
fixed, we can tree function symbols the same as constant symbols. */
bool is_tree;
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 0c2f03460..753a45e06 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -33,7 +33,7 @@ def_module_params('fixedpoint',
"updated relation was modified or not"),
('datalog.compile_with_widening', BOOL, False,
"widening will be used to compile recursive rules"),
- ('datalog.default_table_checked', BOOL, False, "if true, the detault " +
+ ('datalog.default_table_checked', BOOL, False, "if true, the default " +
'table will be default_table inside a wrapper that checks that its results ' +
'are the same as of default_table_checker table'),
('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
@@ -59,7 +59,7 @@ def_module_params('fixedpoint',
('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
('duality.feasible_edges', BOOL, True,
- 'Don\'t expand definitley infeasible edges'),
+ 'Don\'t expand definitely infeasible edges'),
('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
('duality.recursion_bound', UINT, UINT_MAX,
@@ -130,7 +130,7 @@ def_module_params('fixedpoint',
('xform.magic', BOOL, False,
"perform symbolic magic set transformation"),
('xform.scale', BOOL, False,
- "add scaling variable to linear real arithemtic clauses"),
+ "add scaling variable to linear real arithmetic clauses"),
('xform.inline_linear', BOOL, True, "try linear inlining method"),
('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
('xform.inline_linear_branch', BOOL, False,
@@ -176,7 +176,7 @@ def_module_params('fixedpoint',
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
- ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministicly"),
+ ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"),
('spacer.split_farkas_literals', BOOL, False, "Split Farkas literals"),
diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h
index cd5715a4f..b2e80ab84 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.h
+++ b/src/muz/transforms/dl_mk_array_instantiation.h
@@ -26,7 +26,7 @@ Implementation:
1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array.
- 2) Inforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
+ 2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option
corresponds to fixedpoint.xform.instantiate_arrays.enforce
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.h b/src/muz/transforms/dl_mk_interp_tail_simplifier.h
index 713827588..0d4c65d11 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.h
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.h
@@ -53,7 +53,7 @@ namespace datalog {
*/
void reset(rule * r);
- /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+ /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
bool unify(expr * e1, expr * e2);
void get_result(rule_ref & res);
diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h
index 27b6dd418..9146343fa 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.h
+++ b/src/muz/transforms/dl_mk_rule_inliner.h
@@ -45,7 +45,7 @@ namespace datalog {
: m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx),
m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
- /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+ /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
/**
diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h
index c171a1d06..94090ec93 100644
--- a/src/muz/transforms/dl_mk_scale.h
+++ b/src/muz/transforms/dl_mk_scale.h
@@ -7,7 +7,7 @@ Module Name:
Abstract:
- Add scale factor to linear (Real) arithemetic Horn clauses.
+ Add scale factor to linear (Real) arithmetic Horn clauses.
The transformation replaces occurrences of isolated constants by
a scale multiplied to each constant.
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index 40c68f72a..6afac32b8 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -267,7 +267,7 @@ struct aig_manager::imp {
}
if (b == r) {
if (sign1) {
- // subsitution
+ // substitution
// not (a and b) and r --> (not a) and r IF b == r
l = a;
l.invert();
diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h
index 177524726..bdf2636a9 100644
--- a/src/tactic/tactic_exception.h
+++ b/src/tactic/tactic_exception.h
@@ -7,7 +7,7 @@ Module Name:
Abstract:
- Tactic expection object.
+ Tactic exception object.
Author:
diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h
index 169566f39..9ec2f901f 100644
--- a/src/tactic/tactical.h
+++ b/src/tactic/tactical.h
@@ -47,7 +47,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
tactic * repeat(tactic * t, unsigned max = UINT_MAX);
/**
- \brief Fails if \c t produeces more than \c threshold subgoals.
+ \brief Fails if \c t produces more than \c threshold subgoals.
Otherwise, it behaves like \c t.
*/
tactic * fail_if_branching(tactic * t, unsigned threshold = 1);