Fix typos.

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

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
 

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 { 

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>

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 
      **/

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

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)))

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

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());

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;

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"),

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
 

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);

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);
 
         /**

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. 
 

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();

src/tactic/tactic_exception.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Tactic expection object.
+    Tactic exception object.
 
 Author:
 

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);